From 172a7d42132854022381b3c2832ac0f9afb69b19 Mon Sep 17 00:00:00 2001
From: Pim Otte <pim@otte.dev>
Date: Wed, 13 May 2026 18:06:52 +0200
Subject: [PATCH 1/3] Added conclude by contradiction construction

---
 Verbose/English/We.lean | 8 ++++++++
 Verbose/French/We.lean  | 8 ++++++++
 2 files changed, 16 insertions(+)

diff --git a/Verbose/English/We.lean b/Verbose/English/We.lean
index 051d155..ad74c6d 100644
--- a/Verbose/English/We.lean
+++ b/Verbose/English/We.lean
@@ -1,3 +1,4 @@
+import Verbose.Tactics.Since
 import Verbose.Tactics.We
 import Verbose.English.Common
 
@@ -78,6 +79,10 @@ pure "Specifying the rewriting result is possible only when rewriting in a singl
 implement_endpoint (lang := en) cannotContrapose : CoreM String :=
 pure "Cannot contrapose: the main goal is not an implication."
 
+elab "We" "conclude by contradicting" facts:facts : tactic => do
+  let factsT := factsToArray facts
+  sinceConcludeTac (← `(term| False)) factsT
+
 example (P Q : Prop) (h : P ∨ Q) : True := by
   We proceed using h
   . intro _hP
@@ -376,3 +381,6 @@ is not definitionally equal to target
     We reformulate h as 2 = 3
   We reformulate h as 2 = 2
   trivial
+
+example (p : Prop) (_ : p) (_ : ¬ p) : False := by
+  We conclude by contradicting p and ¬ p
diff --git a/Verbose/French/We.lean b/Verbose/French/We.lean
index 5e44301..a71988e 100644
--- a/Verbose/French/We.lean
+++ b/Verbose/French/We.lean
@@ -1,3 +1,4 @@
+import Verbose.Tactics.Since
 import Verbose.Tactics.We
 import Verbose.French.Common
 
@@ -87,6 +88,10 @@ pure "On ne peut spécifier le résultat de la réécriture que lorsqu’on ne r
 implement_endpoint (lang := fr) cannotContrapose : CoreM String :=
 pure "Il est impossible de contraposer car le but n’est pas une implication."
 
+elab "On" "conclut par contradiction avec " facts:factsFR : tactic => do
+  let factsT := factsFRToArray facts
+  sinceConcludeTac (← `(term| False)) factsT
+
 setLang fr
 
 example (P Q : Prop) (h : P ∨ Q) : True := by
@@ -387,3 +392,6 @@ is not definitionally equal to target
     On reformule l'hypothèse h en 2 = 3
   On reformule l'hypothèse h en 2 = 2
   trivial
+
+example (p : Prop) (_ : p) (_ : ¬ p) : False := by
+  On conclut par contradiction avec p et ¬ p

From ccdb792ef8173322f26508da542acbc28c782944 Mon Sep 17 00:00:00 2001
From: Pim Otte <pim@otte.dev>
Date: Tue, 2 Jun 2026 16:26:54 +0200
Subject: [PATCH 2/3] Add scope to contradiction language, document scopes

---
 Verbose/English/We.lean | 7 ++++++-
 Verbose/French/We.lean  | 7 ++++++-
 basic-configuration.md  | 6 ++++++
 3 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/Verbose/English/We.lean b/Verbose/English/We.lean
index ad74c6d..65894bc 100644
--- a/Verbose/English/We.lean
+++ b/Verbose/English/We.lean
@@ -79,10 +79,14 @@ pure "Specifying the rewriting result is possible only when rewriting in a singl
 implement_endpoint (lang := en) cannotContrapose : CoreM String :=
 pure "Cannot contrapose: the main goal is not an implication."
 
-elab "We" "conclude by contradicting" facts:facts : tactic => do
+namespace Verbose.Contradicting
+
+scoped elab "We" "conclude by contradicting" facts:facts : tactic => do
   let factsT := factsToArray facts
   sinceConcludeTac (← `(term| False)) factsT
 
+end Verbose.Contradicting
+
 example (P Q : Prop) (h : P ∨ Q) : True := by
   We proceed using h
   . intro _hP
@@ -382,5 +386,6 @@ is not definitionally equal to target
   We reformulate h as 2 = 2
   trivial
 
+open Verbose.Contradicting in
 example (p : Prop) (_ : p) (_ : ¬ p) : False := by
   We conclude by contradicting p and ¬ p
diff --git a/Verbose/French/We.lean b/Verbose/French/We.lean
index a71988e..4100f57 100644
--- a/Verbose/French/We.lean
+++ b/Verbose/French/We.lean
@@ -88,10 +88,14 @@ pure "On ne peut spécifier le résultat de la réécriture que lorsqu’on ne r
 implement_endpoint (lang := fr) cannotContrapose : CoreM String :=
 pure "Il est impossible de contraposer car le but n’est pas une implication."
 
-elab "On" "conclut par contradiction avec " facts:factsFR : tactic => do
+namespace Verbose.Contradicting
+
+scoped elab "On" "conclut par contradiction avec " facts:factsFR : tactic => do
   let factsT := factsFRToArray facts
   sinceConcludeTac (← `(term| False)) factsT
 
+end Verbose.Contradicting
+
 setLang fr
 
 example (P Q : Prop) (h : P ∨ Q) : True := by
@@ -393,5 +397,6 @@ is not definitionally equal to target
   On reformule l'hypothèse h en 2 = 2
   trivial
 
+open Verbose.Contradicting in
 example (p : Prop) (_ : p) (_ : ¬ p) : False := by
   On conclut par contradiction avec p et ¬ p
diff --git a/basic-configuration.md b/basic-configuration.md
index d285c7f..54b59ac 100644
--- a/basic-configuration.md
+++ b/basic-configuration.md
@@ -153,3 +153,9 @@ configureDataProviders {
   ℕ : [mkSelf, NumbersDefault] }
 ```
 This is hopefully easy to understand and modify.
+
+## Scoped notation
+
+Some phrases are scoped to namespaces. Examples include: `Verbose.NameLess` with
+phrases that do not refer to hypotheses by name, `Verbose.Named` with phrases
+that do refer to hypothesis by name and `Verbose.Contradicting` for extra phrases around contradiction.

From be6189cabc2f40dcabf9bb3371fb2dc46a680c70 Mon Sep 17 00:00:00 2001
From: Pim Otte <pim@otte.dev>
Date: Tue, 2 Jun 2026 16:33:49 +0200
Subject: [PATCH 3/3] Small extra explanation

---
 basic-configuration.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/basic-configuration.md b/basic-configuration.md
index 54b59ac..5a1a281 100644
--- a/basic-configuration.md
+++ b/basic-configuration.md
@@ -159,3 +159,4 @@ This is hopefully easy to understand and modify.
 Some phrases are scoped to namespaces. Examples include: `Verbose.NameLess` with
 phrases that do not refer to hypotheses by name, `Verbose.Named` with phrases
 that do refer to hypothesis by name and `Verbose.Contradicting` for extra phrases around contradiction.
+Using `open Verbose.NameLess` or equivalent makes these accessible for exercises.