chore(Archive/IMO/1962Q1): better hypothesis names (#16845)

Do not use `h1` for a hypothesis that doesn't involve the number `1`.
Also, lemmas for this IMO solution are now `lemma` and the word `digits` is plural.

Archive/Imo/Imo1962Q1.lean

@@ -32,110 +32,104 @@ def ProblemPredicate (n : ℕ) : Prop :=
 First, it's inconvenient to work with digits, so let's simplify them out of the problem.
 -/
 
-
 abbrev ProblemPredicate' (c n : ℕ) : Prop :=
   n = 10 * c + 6 ∧ 6 * 10 ^ (digits 10 c).length + c = 4 * n
 
-theorem without_digits {n : ℕ} (h1 : ProblemPredicate n) : ∃ c : ℕ, ProblemPredicate' c n := by
+lemma without_digits {n : ℕ} (hn : ProblemPredicate n) : ∃ c : ℕ, ProblemPredicate' c n := by
   use n / 10
   cases' n with n
-  · have h2 : ¬ProblemPredicate 0 := by norm_num [ProblemPredicate]
+  · have hpp : ¬ProblemPredicate 0 := by norm_num [ProblemPredicate]
     contradiction
   · rw [ProblemPredicate, digits_def' (by decide : 2 ≤ 10) n.succ_pos, List.headI, List.tail_cons,
-      List.concat_eq_append] at h1
+      List.concat_eq_append] at hn
     constructor
-    · rw [← h1.left, div_add_mod (n + 1) 10]
-    · rw [← h1.right, ofDigits_append, ofDigits_digits, ofDigits_singleton, add_comm, mul_comm]
+    · rw [← hn.left, div_add_mod (n + 1) 10]
+    · rw [← hn.right, ofDigits_append, ofDigits_digits, ofDigits_singleton, add_comm, mul_comm]
 
 /-!
 Now we can eliminate possibilities for `(digits 10 c).length` until we get to the one that works.
 -/
 
-
-theorem case_0_digit {c n : ℕ} (h1 : (digits 10 c).length = 0) : ¬ProblemPredicate' c n := by
-  intro h2
-  have h3 : 6 * 10 ^ 0 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
-  have h4 : 6 * 10 ^ 0 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
+lemma case_0_digits {c n : ℕ} (hc : (digits 10 c).length = 0) : ¬ProblemPredicate' c n := by
+  intro hpp
+  have hpow : 6 * 10 ^ 0 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [hc]
+  have hmul : 6 * 10 ^ 0 + c = 4 * (10 * c + 6) := by rw [hpow, hpp.right, hpp.left]
   linarith
 
-theorem case_1_digit {c n : ℕ} (h1 : (digits 10 c).length = 1) : ¬ProblemPredicate' c n := by
-  intro h2
-  have h3 : 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
-  have h4 : 6 * 10 ^ 1 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
-  have h6 : c > 0 := by linarith
+lemma case_1_digits {c n : ℕ} (hc : (digits 10 c).length = 1) : ¬ProblemPredicate' c n := by
+  intro hpp
+  have hpow : 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [hc]
+  have hmul : 6 * 10 ^ 1 + c = 4 * (10 * c + 6) := by rw [hpow, hpp.right, hpp.left]
+  have hpos : c > 0 := by linarith
   linarith
 
-theorem case_2_digit {c n : ℕ} (h1 : (digits 10 c).length = 2) : ¬ProblemPredicate' c n := by
-  intro h2
-  have h3 : 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
-  have h4 : 6 * 10 ^ 2 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
-  have h5 : c > 14 := by linarith
+lemma case_2_digits {c n : ℕ} (hc : (digits 10 c).length = 2) : ¬ProblemPredicate' c n := by
+  intro hpp
+  have hpow : 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [hc]
+  have hmul : 6 * 10 ^ 2 + c = 4 * (10 * c + 6) := by rw [hpow, hpp.right, hpp.left]
+  have hgt : c > 14 := by linarith
   linarith
 
-theorem case_3_digit {c n : ℕ} (h1 : (digits 10 c).length = 3) : ¬ProblemPredicate' c n := by
-  intro h2
-  have h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
-  have h4 : 6 * 10 ^ 3 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
-  have h5 : c > 153 := by linarith
+lemma case_3_digits {c n : ℕ} (hc : (digits 10 c).length = 3) : ¬ProblemPredicate' c n := by
+  intro hpp
+  have hpow : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [hc]
+  have hmul : 6 * 10 ^ 3 + c = 4 * (10 * c + 6) := by rw [hpow, hpp.right, hpp.left]
+  have hgt : c > 153 := by linarith
   linarith
 
-theorem case_4_digit {c n : ℕ} (h1 : (digits 10 c).length = 4) : ¬ProblemPredicate' c n := by
-  intro h2
-  have h3 : 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
-  have h4 : 6 * 10 ^ 4 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
-  have h5 : c > 1537 := by linarith
+lemma case_4_digits {c n : ℕ} (hc : (digits 10 c).length = 4) : ¬ProblemPredicate' c n := by
+  intro hpp
+  have hpow : 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [hc]
+  have hmul : 6 * 10 ^ 4 + c = 4 * (10 * c + 6) := by rw [hpow, hpp.right, hpp.left]
+  have hgt : c > 1537 := by linarith
   linarith
 
 /-- Putting this inline causes a deep recursion error, so we separate it out. -/
-theorem helper_5_digit {c : ℤ} (h : 6 * 10 ^ 5 + c = 4 * (10 * c + 6)) : c = 15384 := by linarith
+private lemma helper_5_digits {c : ℤ} (hc : 6 * 10 ^ 5 + c = 4 * (10 * c + 6)) : c = 15384 := by
+  linarith
 
-theorem case_5_digit {c n : ℕ} (h1 : (digits 10 c).length = 5) (h2 : ProblemPredicate' c n) :
+lemma case_5_digits {c n : ℕ} (hc : (digits 10 c).length = 5) (hpp : ProblemPredicate' c n) :
     c = 15384 := by
-  have h3 : 6 * 10 ^ 5 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
-  have h4 : 6 * 10 ^ 5 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
+  have hpow : 6 * 10 ^ 5 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [hc]
+  have hmul : 6 * 10 ^ 5 + c = 4 * (10 * c + 6) := by rw [hpow, hpp.right, hpp.left]
   zify at *
-  exact helper_5_digit h4
+  exact helper_5_digits hmul
 
 /-- `linarith` fails on numbers this large, so this lemma spells out some of the arithmetic
 that normally would be automated.
 -/
-theorem case_more_digits {c n : ℕ} (h1 : (digits 10 c).length ≥ 6) (h2 : ProblemPredicate' c n) :
+lemma case_more_digits {c n : ℕ} (hc : (digits 10 c).length ≥ 6) (hpp : ProblemPredicate' c n) :
     n ≥ 153846 := by
-  have h3 : c ≠ 0 := by
-    intro h4
-    have h5 : (digits 10 c).length = 0 := by simp [h4]
-    exact case_0_digit h5 h2
+  have hnz : c ≠ 0 := by
+    intro hc0
+    have hcl : (digits 10 c).length = 0 := by simp [hc0]
+    exact case_0_digits hcl hpp
   calc
-    n ≥ 10 * c := le.intro h2.left.symm
-    _ ≥ 10 ^ (digits 10 c).length := base_pow_length_digits_le 10 c (by decide) h3
-    _ ≥ 10 ^ 6 := pow_le_pow_right (by decide) h1
+    n ≥ 10 * c := le.intro hpp.left.symm
+    _ ≥ 10 ^ (digits 10 c).length := base_pow_length_digits_le 10 c (by decide) hnz
+    _ ≥ 10 ^ 6 := pow_le_pow_right (by decide) hc
     _ ≥ 153846 := by norm_num
 
 /-!
 Now we combine these cases to show that 153846 is the smallest solution.
 -/
 
-
-theorem satisfied_by_153846 : ProblemPredicate 153846 := by
+lemma satisfied_by_153846 : ProblemPredicate 153846 := by
   norm_num [ProblemPredicate]
   decide
 
-theorem no_smaller_solutions (n : ℕ) (h1 : ProblemPredicate n) : n ≥ 153846 := by
-  have ⟨c, h2⟩ := without_digits h1
-  have h3 : (digits 10 c).length < 6 ∨ (digits 10 c).length ≥ 6 := by apply lt_or_ge
-  cases h3 with
-  | inr h3 => exact case_more_digits h3 h2
-  | inl h3 =>
-    interval_cases h : (digits 10 c).length
-    · exfalso; exact case_0_digit h h2
-    · exfalso; exact case_1_digit h h2
-    · exfalso; exact case_2_digit h h2
-    · exfalso; exact case_3_digit h h2
-    · exfalso; exact case_4_digit h h2
-    · have h4 : c = 15384 := case_5_digit h h2
-      have h5 : n = 10 * 15384 + 6 := h4 ▸ h2.left
-      norm_num at h5
-      exact h5.ge
+lemma no_smaller_solutions (n : ℕ) (hn : ProblemPredicate n) : n ≥ 153846 := by
+  have ⟨c, hcn⟩ := without_digits hn
+  cases lt_or_ge (digits 10 c).length 6 with
+  | inl =>
+    interval_cases hc : (digits 10 c).length
+    · exfalso; exact case_0_digits hc hcn
+    · exfalso; exact case_1_digits hc hcn
+    · exfalso; exact case_2_digits hc hcn
+    · exfalso; exact case_3_digits hc hcn
+    · exfalso; exact case_4_digits hc hcn
+    · exact (case_5_digits hc hcn ▸ hcn.left).ge
+  | inr hge => exact case_more_digits hge hcn
 
 end Imo1962Q1