chore: remove a few superfluous semicolons (#5880)

Alongside any necessary spacing/flow changes to accommodate their removal.

Mathlib/Data/Bool/Basic.lean

@@ -381,7 +381,7 @@ def ofNat (n : Nat) : Bool :=
 #align bool.of_nat Bool.ofNat
 
 theorem ofNat_le_ofNat {n m : Nat} (h : n ≤ m) : ofNat n ≤ ofNat m := by
-  simp only [ofNat, ne_eq, _root_.decide_not];
+  simp only [ofNat, ne_eq, _root_.decide_not]
   cases Nat.decEq n 0 with
   | isTrue hn => rw [decide_eq_true hn]; exact false_le
   | isFalse hn =>
@@ -393,7 +393,7 @@ theorem ofNat_le_ofNat {n m : Nat} (h : n ≤ m) : ofNat n ≤ ofNat m := by
 theorem toNat_le_toNat {b₀ b₁ : Bool} (h : b₀ ≤ b₁) : toNat b₀ ≤ toNat b₁ := by
   cases h with
   | inl h => subst h; exact Nat.zero_le _
-  | inr h => subst h; cases b₀ <;> simp;
+  | inr h => subst h; cases b₀ <;> simp
 #align bool.to_nat_le_to_nat Bool.toNat_le_toNat
 
 theorem ofNat_toNat (b : Bool) : ofNat (toNat b) = b := by

Mathlib/Data/Int/Order/Lemmas.lean

@@ -59,7 +59,7 @@ theorem dvd_div_of_mul_dvd {a b c : ℤ} (h : a * b ∣ c) : b ∣ c / a := by
 
 
 theorem eq_zero_of_abs_lt_dvd {m x : ℤ} (h1 : m ∣ x) (h2 : |x| < m) : x = 0 := by
-  by_cases hm : m = 0;
+  by_cases hm : m = 0
   · subst m
     exact zero_dvd_iff.mp h1
   rcases h1 with ⟨d, rfl⟩

Mathlib/Data/List/Basic.lean

@@ -1169,10 +1169,9 @@ theorem indexOf_of_not_mem {l : List α} {a : α} : a ∉ l → indexOf a l = le
 theorem indexOf_le_length {a : α} {l : List α} : indexOf a l ≤ length l := by
   induction' l with b l ih; · rfl
   simp only [length, indexOf_cons]
-  by_cases h : a = b;
-  · rw [if_pos h]
-    exact Nat.zero_le _
-  rw [if_neg h]; exact succ_le_succ ih
+  by_cases h : a = b
+  · rw [if_pos h]; exact Nat.zero_le _
+  · rw [if_neg h]; exact succ_le_succ ih
 #align list.index_of_le_length List.indexOf_le_length
 
 theorem indexOf_lt_length {a} {l : List α} : indexOf a l < length l ↔ a ∈ l :=
@@ -2969,7 +2968,7 @@ theorem intercalate_splitOn (x : α) [DecidableEq α] : [x].intercalate (xs.spli
   cases' h' : splitOnP (· == x) tl with hd' tl'; · exact (splitOnP_ne_nil _ tl h').elim
   rw [h'] at ih
   rw [splitOnP_cons]
-  split_ifs with h;
+  split_ifs with h
   · rw [beq_iff_eq] at h
     subst h
     simp [ih, join, h']
@@ -3113,9 +3112,9 @@ theorem attach_map_val (l : List α) : l.attach.map Subtype.val = l :=
 @[simp]
 theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach
   | ⟨a, h⟩ => by
-    have := mem_map.1 (by rw [attach_map_val] <;> exact h);
-      · rcases this with ⟨⟨_, _⟩, m, rfl⟩
-        exact m
+    have := mem_map.1 (by rw [attach_map_val] <;> exact h)
+    rcases this with ⟨⟨_, _⟩, m, rfl⟩
+    exact m
 #align list.mem_attach List.mem_attach
 
 @[simp]

Mathlib/Data/Nat/Choose/Basic.lean

@@ -109,8 +109,8 @@ theorem choose_pos : ∀ {n k}, k ≤ n → 0 < choose n k
   | 0, _, hk => by rw [Nat.eq_zero_of_le_zero hk]; decide
   | n + 1, 0, _ => by simp
   | n + 1, k + 1, hk => by
-    rw [choose_succ_succ];
-      exact add_pos_of_pos_of_nonneg (choose_pos (le_of_succ_le_succ hk)) (Nat.zero_le _)
+    rw [choose_succ_succ]
+    exact add_pos_of_pos_of_nonneg (choose_pos (le_of_succ_le_succ hk)) (Nat.zero_le _)
 #align nat.choose_pos Nat.choose_pos
 
 theorem choose_eq_zero_iff {n k : ℕ} : n.choose k = 0 ↔ n < k :=
@@ -132,13 +132,13 @@ theorem choose_mul_factorial_mul_factorial : ∀ {n k}, k ≤ n → choose n k *
   | n + 1, succ k, hk => by
     cases' lt_or_eq_of_le hk with hk₁ hk₁
     · have h : choose n k * k.succ ! * (n - k)! = (k + 1) * n ! := by
-        rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)];
-          simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
+        rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
+        simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
       have h₁ : (n - k)! = (n - k) * (n - k.succ)! := by
         rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
       have h₂ : choose n (succ k) * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n ! := by
-        rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)];
-          simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
+        rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
+        simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
       have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
       rw [choose_succ_succ, add_mul, add_mul, succ_sub_succ, h, h₁, h₂, add_mul, tsub_mul,
         factorial_succ, ← add_tsub_assoc_of_le h₃, add_assoc, ← add_mul, add_tsub_cancel_left,

Mathlib/Data/Nat/Choose/Central.lean

@@ -113,8 +113,8 @@ theorem four_pow_le_two_mul_self_mul_centralBinom :
   | n + 4, _ =>
     calc
       4 ^ (n+4) ≤ (n+4) * centralBinom (n+4) := (four_pow_lt_mul_centralBinom _ le_add_self).le
-      _ ≤ 2 * (n+4) * centralBinom (n+4) := by rw [mul_assoc];
-                                               refine' le_mul_of_pos_left zero_lt_two
+      _ ≤ 2 * (n+4) * centralBinom (n+4) := by
+        rw [mul_assoc]; refine' le_mul_of_pos_left zero_lt_two
 #align nat.four_pow_le_two_mul_self_mul_central_binom Nat.four_pow_le_two_mul_self_mul_centralBinom
 
 theorem two_dvd_centralBinom_succ (n : ℕ) : 2 ∣ centralBinom (n + 1) := by

Mathlib/Data/Nat/Pairing.lean

@@ -96,7 +96,7 @@ theorem pair_eq_pair {a b c d : ℕ} : pair a b = pair c d ↔ a = c ∧ b = d :
 
 theorem unpair_lt {n : ℕ} (n1 : 1 ≤ n) : (unpair n).1 < n := by
   let s := sqrt n
-  simp [unpair];
+  simp [unpair]
   by_cases h : n - s * s < s <;> simp [h]
   · exact lt_of_lt_of_le h (sqrt_le_self _)
   · simp at h

Mathlib/Data/Num/Lemmas.lean

@@ -967,7 +967,7 @@ theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = Nat.shiftl m n := by
 
 @[simp, norm_cast]
 theorem shiftr_to_nat (m n) : (shiftr m n : ℕ) = Nat.shiftr m n := by
-  cases' m with m <;> dsimp only [shiftr];
+  cases' m with m <;> dsimp only [shiftr]
   · symm
     apply Nat.zero_shiftr
   induction' n with n IH generalizing m

Mathlib/Data/PFun.lean

@@ -330,10 +330,10 @@ theorem fix_fwd {f : α →. Sum β α} {b : β} {a a' : α} (hb : b ∈ f.fix a
 @[elab_as_elim]
 def fixInduction {C : α → Sort _} {f : α →. Sum β α} {b : β} {a : α} (h : b ∈ f.fix a)
     (H : ∀ a', b ∈ f.fix a' → (∀ a'', Sum.inr a'' ∈ f a' → C a'') → C a') : C a := by
-  have h₂ := (Part.mem_assert_iff.1 h).snd;
+  have h₂ := (Part.mem_assert_iff.1 h).snd
   -- Porting note: revert/intro trick required to address `generalize_proofs` bug
   revert h₂
-  generalize_proofs h₁;
+  generalize_proofs h₁
   intro h₂; clear h
   induction' h₁ with a ha IH
   have h : b ∈ f.fix a := Part.mem_assert_iff.2 ⟨⟨a, ha⟩, h₂⟩

Mathlib/Data/Part.lean

@@ -542,10 +542,9 @@ theorem bind_toOption (f : α → Part β) (o : Part α) [Decidable o.Dom] [∀
 theorem bind_assoc {γ} (f : Part α) (g : α → Part β) (k : β → Part γ) :
     (f.bind g).bind k = f.bind fun x => (g x).bind k :=
   ext fun a => by
-    simp;
-      exact
-        ⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩, fun ⟨_, h₁, _, h₂, h₃⟩ =>
-          ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩
+    simp
+    exact ⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩,
+           fun ⟨_, h₁, _, h₂, h₃⟩ => ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩
 #align part.bind_assoc Part.bind_assoc
 
 @[simp]

Mathlib/Data/Seq/Parallel.lean

@@ -292,7 +292,7 @@ theorem map_parallel (f : α → β) (S) : map f (parallel S) = parallel (S.map
           c1 = map f (corec parallel.aux1 (l, S)) ∧
             c2 = corec parallel.aux1 (l.map (map f), S.map (map f)))
       _ ⟨[], S, rfl, rfl⟩
-  intro c1 c2 h;
+  intro c1 c2 h
   exact
     match c1, c2, h with
     | _, _, ⟨l, S, rfl, rfl⟩ => by

Mathlib/Data/Seq/Seq.lean

@@ -724,7 +724,7 @@ theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s)
   apply
     eq_of_bisim (fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) _
       ⟨s, t, rfl, rfl⟩
-  intro s1 s2 h;
+  intro s1 s2 h
   exact
     match s1, s2, h with
     | _, _, ⟨s, t, rfl, rfl⟩ => by

Mathlib/Data/Seq/WSeq.lean

@@ -893,8 +893,8 @@ def toSeq (s : WSeq α) [Productive s] : Seq α :=
 
 theorem get?_terminates_le {s : WSeq α} {m n} (h : m ≤ n) :
     Terminates (get? s n) → Terminates (get? s m) := by
-  induction' h with m' _ IH <;> [exact id;
-    exact fun T => IH (@head_terminates_of_head_tail_terminates _ _ T)]
+  induction' h with m' _ IH
+  exacts [id, fun T => IH (@head_terminates_of_head_tail_terminates _ _ T)]
 #align stream.wseq.nth_terminates_le Stream'.WSeq.get?_terminates_le
 
 theorem head_terminates_of_get?_terminates {s : WSeq α} {n} :
@@ -1442,8 +1442,8 @@ theorem exists_of_mem_join {a : α} : ∀ {S : WSeq (WSeq α)}, a ∈ join S →
   intro ss h; apply mem_rec_on h <;> [intro b ss o; intro ss IH] <;> intro s S
   · induction' s using WSeq.recOn with b' s s <;>
       [induction' S using WSeq.recOn with s S S; skip; skip] <;>
-      intro ej m <;> simp at ej <;> have := congr_arg Seq.destruct ej <;> simp at this;
-      try cases this; try contradiction
+      intro ej m <;> simp at ej <;> have := congr_arg Seq.destruct ej <;>
+      simp at this; try cases this; try contradiction
     substs b' ss
     simp at m ⊢
     cases' o with e IH

Mathlib/Data/Set/Image.lean

@@ -1089,7 +1089,7 @@ theorem Sum.elim_range (f : α → γ) (g : β → γ) : range (Sum.elim f g) =
 
 theorem range_ite_subset' {p : Prop} [Decidable p] {f g : α → β} :
     range (if p then f else g) ⊆ range f ∪ range g := by
-  by_cases h : p;
+  by_cases h : p
   · rw [if_pos h]
     exact subset_union_left _ _
   · rw [if_neg h]

Mathlib/Data/Stream/Init.lean

@@ -328,7 +328,7 @@ theorem bisim_simple (s₁ s₂ : Stream' α) :
     head s₁ = head s₂ → s₁ = tail s₁ → s₂ = tail s₂ → s₁ = s₂ := fun hh ht₁ ht₂ =>
   eq_of_bisim (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂)
     (fun s₁ s₂ ⟨h₁, h₂, h₃⟩ => by
-      constructor; exact h₁; rw [← h₂, ← h₃];
+      constructor; exact h₁; rw [← h₂, ← h₃]
       (repeat' constructor) <;> assumption)
     (And.intro hh (And.intro ht₁ ht₂))
 #align stream.bisim_simple Stream'.bisim_simple
@@ -467,13 +467,13 @@ theorem head_even (s : Stream' α) : head (even s) = head s :=
 #align stream.head_even Stream'.head_even
 
 theorem tail_even (s : Stream' α) : tail (even s) = even (tail (tail s)) := by
-  unfold even;
-  rw [corec_eq];
+  unfold even
+  rw [corec_eq]
   rfl
 #align stream.tail_even Stream'.tail_even
 
 theorem even_cons_cons (a₁ a₂ : α) (s : Stream' α) : even (a₁::a₂::s) = a₁::even s := by
-  unfold even;
+  unfold even
   rw [corec_eq]; rfl
 #align stream.even_cons_cons Stream'.even_cons_cons
 
@@ -685,13 +685,13 @@ theorem tails_eq_iterate (s : Stream' α) : tails s = iterate tail (tail s) :=
 
 theorem inits_core_eq (l : List α) (s : Stream' α) :
     initsCore l s = l::initsCore (l ++ [head s]) (tail s) := by
-    unfold initsCore corecOn;
+    unfold initsCore corecOn
     rw [corec_eq]
 #align stream.inits_core_eq Stream'.inits_core_eq
 
 theorem tail_inits (s : Stream' α) :
     tail (inits s) = initsCore [head s, head (tail s)] (tail (tail s)) := by
-    unfold inits;
+    unfold inits
     rw [inits_core_eq]; rfl
 #align stream.tail_inits Stream'.tail_inits
 

Mathlib/Data/Sym/Sym2.lean

@@ -240,7 +240,7 @@ theorem coe_lift₂_symm_apply (F : Sym2 α → Sym2 β → γ) (a₁ a₂ : α)
 def map (f : α → β) : Sym2 α → Sym2 β :=
   Quotient.map (Prod.map f f)
     (by
-      intro _ _ h;
+      intro _ _ h
       cases h
       · constructor
       apply Rel.swap)
@@ -590,12 +590,12 @@ def sym2EquivSym' : Equiv (Sym2 α) (Sym' α 2)
         rintro ⟨x, hx⟩ ⟨y, hy⟩ h
         cases' x with _ x; · simp at hx
         cases' x with _ x; · simp at hx
-        cases' x with _ x; swap;
+        cases' x with _ x; swap
         · exfalso
           simp at hx
         cases' y with _ y; · simp at hy
         cases' y with _ y; · simp at hy
-        cases' y with _ y; swap;
+        cases' y with _ y; swap
         · exfalso
           simp at hy
         rcases perm_card_two_iff.mp h with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Mathlib/Data/TypeVec.lean

@@ -61,7 +61,7 @@ open MvFunctor
 @[ext]
 theorem Arrow.ext {α β : TypeVec n} (f g : α ⟹ β) :
     (∀ i, f i = g i) → f = g := by
-  intro h; funext i; apply h;
+  intro h; funext i; apply h
 
 instance Arrow.inhabited (α β : TypeVec n) [∀ i, Inhabited (β i)] : Inhabited (α ⟹ β) :=
   ⟨fun _ _ => default⟩
@@ -335,12 +335,11 @@ protected theorem casesCons_append1  (n : ℕ) {β : TypeVec (n + 1) → Sort _}
 def typevecCasesNil₃  {β : ∀ v v' : TypeVec 0, v ⟹ v' → Sort _}
                       (f : β Fin2.elim0 Fin2.elim0 nilFun) :
     ∀ v v' fs, β v v' fs := fun v v' fs => by
-  refine' cast _ f;
+  refine' cast _ f
   have eq₁ : v = Fin2.elim0 := by funext i; contradiction
   have eq₂ : v' = Fin2.elim0 := by funext i; contradiction
-  have eq₃ : fs = nilFun := by funext i; contradiction;
-  cases eq₁; cases eq₂; cases eq₃;
-  rfl
+  have eq₃ : fs = nilFun := by funext i; contradiction
+  cases eq₁; cases eq₂; cases eq₃; rfl
 #align typevec.typevec_cases_nil₃ TypeVec.typevecCasesNil₃
 
 /-- cases distinction for an arrow in the category of (n+1)-length type vectors -/
@@ -567,26 +566,26 @@ protected def prod.map : ∀ {n} {α α' β β' : TypeVec.{u} n}, α ⟹ β →
 
 theorem fst_prod_mk {α α' β β' : TypeVec n} (f : α ⟹ β) (g : α' ⟹ β') :
     TypeVec.prod.fst ⊚ (f ⊗' g) = f ⊚ TypeVec.prod.fst := by
-  funext i; induction i;
+  funext i; induction i
   case fz => rfl
   case fs _ _ i_ih => apply i_ih
 #align typevec.fst_prod_mk TypeVec.fst_prod_mk
 
 theorem snd_prod_mk {α α' β β' : TypeVec n} (f : α ⟹ β) (g : α' ⟹ β') :
     TypeVec.prod.snd ⊚ (f ⊗' g) = g ⊚ TypeVec.prod.snd := by
-  funext i; induction i;
+  funext i; induction i
   case fz => rfl
   case fs _ _ i_ih => apply i_ih
 #align typevec.snd_prod_mk TypeVec.snd_prod_mk
 
 theorem fst_diag {α : TypeVec n} : TypeVec.prod.fst ⊚ (prod.diag : α ⟹ _) = id := by
-  funext i; induction i;
+  funext i; induction i
   case fz => rfl
   case fs _ _ i_ih => apply i_ih
 #align typevec.fst_diag TypeVec.fst_diag
 
 theorem snd_diag {α : TypeVec n} : TypeVec.prod.snd ⊚ (prod.diag : α ⟹ _) = id := by
-  funext i; induction i;
+  funext i; induction i
   case fz => rfl
   case fs _ _ i_ih => apply i_ih
 #align typevec.snd_diag TypeVec.snd_diag

Mathlib/Data/Vector/MapLemmas.lean

@@ -93,7 +93,7 @@ theorem mapAccumr_mapAccumr₂ (f₁ : γ → σ₁ → σ₁ × ζ) (f₂ : α
           let r₂ := f₂ x y s.snd
           let r₁ := f₁ r₂.snd s.fst
           ((r₁.fst, r₂.fst), r₁.snd)
-        ) xs ys (s₁, s₂);
+        ) xs ys (s₁, s₂)
       (m.fst.fst, m.snd) := by
   induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all
 
@@ -110,7 +110,7 @@ theorem mapAccumr₂_mapAccumr₂_left_left (f₁ : γ → α → σ₁ → σ
                 let r₁ := f₁ r₂.snd x s₁
                 ((r₁.fst, r₂.fst), r₁.snd)
               )
-            xs ys (s₁, s₂);
+            xs ys (s₁, s₂)
     (m.fst.fst, m.snd) := by
   induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all
 
@@ -123,7 +123,7 @@ theorem mapAccumr₂_mapAccumr₂_left_right
                 let r₁ := f₁ r₂.snd y s₁
                 ((r₁.fst, r₂.fst), r₁.snd)
               )
-            xs ys (s₁, s₂);
+            xs ys (s₁, s₂)
     (m.fst.fst, m.snd) := by
   induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all
 
@@ -136,7 +136,7 @@ theorem mapAccumr₂_mapAccumr₂_right_left  (f₁ : α → γ → σ₁ → σ
                 let r₁ := f₁ x r₂.snd s₁
                 ((r₁.fst, r₂.fst), r₁.snd)
               )
-            xs ys (s₁, s₂);
+            xs ys (s₁, s₂)
     (m.fst.fst, m.snd) := by
   induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all
 
@@ -149,7 +149,7 @@ theorem mapAccumr₂_mapAccumr₂_right_right (f₁ : β → γ → σ₁ → σ
                 let r₁ := f₁ y r₂.snd s₁
                 ((r₁.fst, r₂.fst), r₁.snd)
               )
-            xs ys (s₁, s₂);
+            xs ys (s₁, s₂)
     (m.fst.fst, m.snd) := by
   induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all
 

Mathlib/Init/Algebra/Functions.lean

@@ -57,7 +57,7 @@ lemma min_assoc (a b c : α) : min (min a b) c = min a (min b c) := by
   apply eq_min
   · apply le_trans; apply min_le_left; apply min_le_left
   · apply le_min; apply le_trans; apply min_le_left; apply min_le_right; apply min_le_right
-  · intros d h₁ h₂; apply le_min; apply le_min h₁; apply le_trans h₂; apply min_le_left;
+  · intros d h₁ h₂; apply le_min; apply le_min h₁; apply le_trans h₂; apply min_le_left
     apply le_trans h₂; apply min_le_right
 
 lemma min_left_comm : @LeftCommutative α α min :=
@@ -84,7 +84,7 @@ lemma max_assoc (a b c : α) : max (max a b) c = max a (max b c) := by
   apply eq_max
   · apply le_trans; apply le_max_left a b; apply le_max_left
   · apply max_le; apply le_trans; apply le_max_right a b; apply le_max_left; apply le_max_right
-  · intros d h₁ h₂; apply max_le; apply max_le h₁; apply le_trans (le_max_left _ _) h₂;
+  · intros d h₁ h₂; apply max_le; apply max_le h₁; apply le_trans (le_max_left _ _) h₂
     apply le_trans (le_max_right _ _) h₂
 
 lemma max_left_comm : ∀ (a b c : α), max a (max b c) = max b (max a c) :=

Mathlib/Init/Data/List/Instances.lean

@@ -68,10 +68,10 @@ instance decidableBex : ∀ (l : List α), Decidable (∃ x ∈ l, p x)
     then isTrue ⟨x, mem_cons_self _ _, h₁⟩
     else match decidableBex xs with
       | isTrue h₂  => isTrue <| by
-        cases' h₂ with y h; cases' h with hm hp;
+        cases' h₂ with y h; cases' h with hm hp
         exact ⟨y, mem_cons_of_mem _ hm, hp⟩
       | isFalse h₂ => isFalse <| by
-        intro h; cases' h with y h; cases' h with hm hp;
+        intro h; cases' h with y h; cases' h with hm hp
         cases' mem_cons.1 hm with h h
         · rw [h] at hp; contradiction
         · exact absurd ⟨y, h, hp⟩ h₂