ImProver Length optimization

Compfiles/Imo2022P2.lean

@@ -36,34 +36,23 @@ lemma lemma0 {α : Type} {p : α → α → Prop}
     ∀ x, Classical.choose (h1 (Classical.choose (h1 x).exists)).exists = x := by
   intro x
   obtain ⟨y, h1e, h1u⟩ := h1 x
-  have h2' : Classical.choose (h1 x).exists = y :=
-    h1u _ (Classical.choose_spec (h1 x).exists)
-  rw [h2']
-
+  rw [h1u _ (Classical.choose_spec _)]
   obtain ⟨w, h1e', h1u'⟩ := h1 y
-  have h4 := Classical.choose_spec (h1 y).exists
-  have hxw : x = w := by
-    apply h1u'
-    rw [h2]
-    exact h1e
-  rw [hxw]
-  exact h1u' _ h4
+  rw [h1u' _ ((h2 _ _).mpr h1e)]
+  exact h1u' _ (Classical.choose_spec _)
 
 lemma amgm (a b : ℝ+) : ⟨2, two_pos⟩ ≤ a / b + b / a := by
-  change 2 ≤ a.val/b.val + b.val/a.val
+  change 2 ≤ a.val / b.val + b.val / a.val
   obtain ⟨a, ha⟩ := a
   obtain ⟨b, hb⟩ := b
   dsimp only
   field_simp
-  have h1 : 0 < b * a := mul_pos hb ha
-  suffices H : 2 * (b * a) ≤ a * a + b * b by exact (le_div_iff₀ h1).mpr H
-  suffices H : 0 ≤ (a - b)^2 by linarith
-  exact sq_nonneg (a - b)
+  suffices H : 2 * (b * a) ≤ a * a + b * b by exact (le_div_iff₀ (mul_pos hb ha)).mpr H
+  linarith [sq_nonneg (a - b)]
 
 lemma lemma1 (a : ℝ+) : a + a = ⟨2, two_pos⟩ * a := by
   obtain ⟨a, ha⟩ := a
   apply Subtype.val_injective
-  dsimp
   exact (two_mul a).symm
 
 snip end

Compfiles/Usa2018P1.lean

@@ -26,11 +26,10 @@ namespace Usa2018P1
 snip begin
 
 lemma am_gm (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) :
-    2 * (a * b) ^ ((1 : ℝ) / 2) ≤ a + b := by
+    2 * (a * b) ^ ((1 : ℝ) / 2) ≤ a + b   := by
   have hw : (0 : ℝ) ≤ 1/2 := by norm_num
   rw [Real.mul_rpow ha hb]
-  have := Real.geom_mean_le_arith_mean2_weighted hw hw ha hb (by norm_num)
-  linarith
+  linarith [Real.geom_mean_le_arith_mean2_weighted hw hw ha hb (by norm_num)]
 
 snip end
 

Compfiles/Usa2023P2.lean

@@ -38,11 +38,8 @@ lemma lemma_1 (a b c : ℝ+) : (a + b)/c = a/c + b/c := by
   rw [division_def, add_mul, ←division_def, ←division_def]
 
 lemma lemma_3 {a b c : ℝ+} (h : a = b + c) : c < a := by
-  rw [h]
-  obtain ⟨b, hb⟩ := b
-  obtain ⟨c, hc⟩ := c
-  rw [←Subtype.coe_lt_coe, Positive.coe_add]
-  exact lt_add_of_pos_left c hb
+  rw [h, ←Subtype.coe_lt_coe, Positive.coe_add]
+  exact lt_add_of_pos_left _ b.2
 
 snip end