internlm/Lean-Github huggingface dataset:
Theorem: Usa2018P1.am_gm
Proof state before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 2 * (a * b) ^ (1 / 2) ≤ a + b
Tactic:
have hw : (0 : ℝ) ≤ 1/2 := by norm_num
Proof state after:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
⊢ 2 * (a * b) ^ (1 / 2) ≤ a + b
Theorem: Usa2018P1.am_gm
Proof state before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
⊢ 2 * (a * b) ^ (1 / 2) ≤ a + b
Tactic:
rw [Real.mul_rpow ha hb]
Proof state after:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
⊢ 2 * (a ^ (1 / 2) * b ^ (1 / 2)) ≤ a + b
Theorem: Usa2018P1.am_gm
Proof state before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
⊢ 2 * (a ^ (1 / 2) * b ^ (1 / 2)) ≤ a + b
Tactic:
have := Real.geom_mean_le_arith_mean2_weighted hw hw ha hb (by norm_num)
Proof state after:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
this : a ^ (1 / 2) * b ^ (1 / 2) ≤ 1 / 2 * a + 1 / 2 * b
⊢ 2 * (a ^ (1 / 2) * b ^ (1 / 2)) ≤ a + b
Theorem: Usa2018P1.am_gm
Proof state before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
this : a ^ (1 / 2) * b ^ (1 / 2) ≤ 1 / 2 * a + 1 / 2 * b
⊢ 2 * (a ^ (1 / 2) * b ^ (1 / 2)) ≤ a + b
Tactic:
linarith
Proof state after:
no goals
Theorem: Usa2018P1.am_gm
Proof state before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Usa2018P1.am_gm
Proof state before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
⊢ 1 / 2 + 1 / 2 = 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo1986P5.IsGood.map_eq_zero
Proof state before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
⊢ f x = 0 ↔ 2 ≤ x
Tactic:
refine ⟨fun hx₀ ↦ not_lt.1 fun hlt ↦ hf.map_ne_zero x hlt hx₀, fun hle ↦ ?_⟩
Proof state after:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hle : 2 ≤ x
⊢ f x = 0
Theorem: Imo1986P5.IsGood.map_eq_zero
Proof state before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hle : 2 ≤ x
⊢ f x = 0
Tactic:
rcases exists_add_of_le hle with ⟨x, rfl⟩
Proof state after:
case intro
f : ℝ≥0 → ℝ≥0
hf : IsGood f
y x : ℝ≥0
hle : 2 ≤ 2 + x
⊢ f (2 + x) = 0
Theorem: Imo1986P5.IsGood.map_eq_zero
Proof state before:
case intro
f : ℝ≥0 → ℝ≥0
hf : IsGood f
y x : ℝ≥0
hle : 2 ≤ 2 + x
⊢ f (2 + x) = 0
Tactic:
rw [add_comm, hf.map_add, hf.map_two, mul_zero]
Proof state after:
no goals
Theorem: Imo1986P5.IsGood.map_ne_zero_iff
Proof state before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
⊢ f x ≠ 0 ↔ x < 2
Tactic:
simp [hf.map_eq_zero]
Proof state after:
no goals
Theorem: Imo1986P5.IsGood.map_of_lt_two
Proof state before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
⊢ f x = 2 / (2 - x)
Tactic:
have hx' : 2 - x ≠ 0 := (tsub_pos_of_lt hx).ne'
Proof state after:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
⊢ f x = 2 / (2 - x)
Theorem: Imo1986P5.IsGood.map_of_lt_two
Proof state before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
⊢ f x = 2 / (2 - x)
Tactic:
have hfx : f x ≠ 0 := hf.map_ne_zero_iff.2 hx
Proof state after:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f x = 2 / (2 - x)
Theorem: Imo1986P5.IsGood.map_of_lt_two
Proof state before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f x = 2 / (2 - x)
Tactic:
apply le_antisymm
Proof state after:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f x ≤ 2 / (2 - x)

case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ 2 / (2 - x) ≤ f x
Theorem: Imo1986P5.IsGood.map_of_lt_two
Proof state before:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f x ≤ 2 / (2 - x)
Tactic:
rw [NNReal.le_div_iff hx', ← NNReal.le_div_iff' hfx, tsub_le_iff_right, ← hf.map_eq_zero,
 hf.map_add, div_mul_cancel₀ _ hfx, hf.map_two, zero_mul]
Proof state after:
no goals
Theorem: Imo1986P5.IsGood.map_of_lt_two
Proof state before:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ 2 / (2 - x) ≤ f x
Tactic:
rw [NNReal.div_le_iff' hx', ← hf.map_eq_zero]
Proof state after:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f ((2 - x) * f x) = 0
Theorem: Imo1986P5.IsGood.map_of_lt_two
Proof state before:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f ((2 - x) * f x) = 0
Tactic:
refine (mul_eq_zero.1 ?_).resolve_right hfx
Proof state after:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f ((2 - x) * f x) * f x = 0
Theorem: Imo1986P5.IsGood.map_of_lt_two
Proof state before:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f ((2 - x) * f x) * f x = 0
Tactic:
rw [hf.map_add_rev, hf.map_eq_zero, tsub_add_cancel_of_le hx.le]
Proof state after:
no goals
Theorem: Imo1986P5.IsGood.map_eq
Proof state before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x✝ y x : ℝ≥0
hx : 2 ≤ x
⊢ f x = 2 / (2 - x)
Tactic:
rwa [tsub_eq_zero_of_le hx, div_zero, hf.map_eq_zero]
Proof state after:
no goals
Theorem: Usa1987P1.lemma2
Proof state before:
a b c : ℤ
h : a * b ^ 2 = c ^ 2
⊢ IsSquare a ∨ b = 0
Tactic:
obtain rfl | hb := eq_or_ne b 0
Proof state after:
case inl
a c : ℤ
h : a * 0 ^ 2 = c ^ 2
⊢ IsSquare a ∨ 0 = 0

case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
⊢ IsSquare a ∨ b = 0
Theorem: Usa1987P1.lemma2
Proof state before:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
⊢ IsSquare a ∨ b = 0
Tactic:
simp only [hb, or_false]
Proof state after:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
⊢ IsSquare a
Theorem: Usa1987P1.lemma2
Proof state before:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
⊢ IsSquare a
Tactic:
have h1 : b^2 ∣ c^2 := Dvd.intro_left a h
Proof state after:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
h1 : b ^ 2 ∣ c ^ 2
⊢ IsSquare a
Theorem: Usa1987P1.lemma2
Proof state before:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
h1 : b ^ 2 ∣ c ^ 2
⊢ IsSquare a
Tactic:
rw [Int.pow_dvd_pow_iff two_ne_zero] at h1
Proof state after:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
h1 : b ∣ c
⊢ IsSquare a
Theorem: Usa1987P1.lemma2
Proof state before:
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
h1 : b ∣ c
⊢ IsSquare a
Tactic:
obtain ⟨k, rfl⟩ := h1
Proof state after:
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a * b ^ 2 = (b * k) ^ 2
⊢ IsSquare a
Theorem: Usa1987P1.lemma2
Proof state before:
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a * b ^ 2 = (b * k) ^ 2
⊢ IsSquare a
Tactic:
rw [mul_pow, mul_comm, mul_right_inj' (pow_ne_zero _ hb)] at h
Proof state after:
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a = k ^ 2
⊢ IsSquare a
Theorem: Usa1987P1.lemma2
Proof state before:
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a = k ^ 2
⊢ IsSquare a
Tactic:
rw [h]
Proof state after:
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a = k ^ 2
⊢ IsSquare (k ^ 2)
Theorem: Usa1987P1.lemma2
Proof state before:
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a = k ^ 2
⊢ IsSquare (k ^ 2)
Tactic:
exact ⟨k, sq k⟩
Proof state after:
no goals
Theorem: Usa1987P1.lemma2
Proof state before:
case inl
a c : ℤ
h : a * 0 ^ 2 = c ^ 2
⊢ IsSquare a ∨ 0 = 0
Tactic:
right
Proof state after:
case inl.h
a c : ℤ
h : a * 0 ^ 2 = c ^ 2
⊢ 0 = 0
Theorem: Usa1987P1.lemma2
Proof state before:
case inl.h
a c : ℤ
h : a * 0 ^ 2 = c ^ 2
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Imo1977P6.imo1977_p6_nat
Proof state before:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
⊢ ∀ (n : ℕ), f n = n
Tactic:
have hf : ∀ n, n ≤ f n := fun n => h' n n rfl.le
Proof state after:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
⊢ ∀ (n : ℕ), f n = n
Theorem: Imo1977P6.imo1977_p6_nat
Proof state before:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
⊢ ∀ (n : ℕ), f n = n
Tactic:
have hf_mono : StrictMono f := strictMono_nat_of_lt_succ fun _ => lt_of_le_of_lt (hf _) (h _)
Proof state after:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
hf_mono : StrictMono f
⊢ ∀ (n : ℕ), f n = n
Theorem: Imo1977P6.imo1977_p6_nat
Proof state before:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
hf_mono : StrictMono f
⊢ ∀ (n : ℕ), f n = n
Tactic:
intro
Proof state after:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
hf_mono : StrictMono f
n✝ : ℕ
⊢ f n✝ = n✝
Theorem: Imo1977P6.imo1977_p6_nat
Proof state before:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
hf_mono : StrictMono f
n✝ : ℕ
⊢ f n✝ = n✝
Tactic:
exact Nat.eq_of_le_of_lt_succ (hf _) (hf_mono.lt_iff_lt.mp (h _))
Proof state after:
no goals
Theorem: Imo1977P6.imo1977_p6_nat
Proof state before:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
⊢ ∀ (k n : ℕ), k ≤ n → k ≤ f n
Tactic:
intro k
Proof state after:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
⊢ ∀ (n : ℕ), k ≤ n → k ≤ f n
Theorem: Imo1977P6.imo1977_p6_nat
Proof state before:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
⊢ ∀ (n : ℕ), k ≤ n → k ≤ f n
Tactic:
induction' k with k h_ind
Proof state after:
case zero
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
⊢ ∀ (n : ℕ), 0 ≤ n → 0 ≤ f n

case succ
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
⊢ ∀ (n : ℕ), k + 1 ≤ n → k + 1 ≤ f n
Theorem: Imo1977P6.imo1977_p6_nat
Proof state before:
case zero
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
⊢ ∀ (n : ℕ), 0 ≤ n → 0 ≤ f n
Tactic:
intros
Proof state after:
case zero
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
n✝ : ℕ
a✝ : 0 ≤ n✝
⊢ 0 ≤ f n✝
Theorem: Imo1977P6.imo1977_p6_nat
Proof state before:
case zero
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
n✝ : ℕ
a✝ : 0 ≤ n✝
⊢ 0 ≤ f n✝
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: Imo1977P6.imo1977_p6_nat
Proof state before:
case succ
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
⊢ ∀ (n : ℕ), k + 1 ≤ n → k + 1 ≤ f n
Tactic:
intro n hk
Proof state after:
case succ
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
hk : k + 1 ≤ n
⊢ k + 1 ≤ f n
Theorem: Imo1977P6.imo1977_p6_nat
Proof state before:
case succ
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
hk : k + 1 ≤ n
⊢ k + 1 ≤ f n
Tactic:
apply Nat.succ_le_of_lt
Proof state after:
case succ.h
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
hk : k + 1 ≤ n
⊢ k < f n
Theorem: Imo1977P6.imo1977_p6_nat
Proof state before:
case succ.h
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
hk : k + 1 ≤ n
⊢ k < f n
Tactic:
calc
  k ≤ f (f (n - 1)) := h_ind _ (h_ind (n - 1) (le_tsub_of_add_le_right hk))
  _ < f n := tsub_add_cancel_of_le (le_trans (Nat.succ_le_succ (Nat.zero_le _)) hk) ▸ h _
Proof state after:
no goals
Theorem: Usa2015P1.iff_comm
Proof state before:
a b c : Prop
⊢ (a → c) → (b → c) → (c → (a ↔ b)) → (a ↔ b)
Tactic:
tauto
Proof state after:
no goals
Theorem: Usa2015P1.abc
Proof state before:
a b c : ℤ
hb : b ≠ 0
⊢ a ^ 2 = b ^ 2 * c → ∃ d, c = d ^ 2
Tactic:
intro h
Proof state after:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
⊢ ∃ d, c = d ^ 2
Theorem: Usa2015P1.abc
Proof state before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
⊢ ∃ d, c = d ^ 2
Tactic:
have h1 : b ^ 2 ∣ a ^ 2 := by simp_all only [ne_eq, dvd_mul_right]
Proof state after:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
⊢ ∃ d, c = d ^ 2
Theorem: Usa2015P1.abc
Proof state before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
⊢ ∃ d, c = d ^ 2
Tactic:
have h2 : b ∣ a := by apply (Int.pow_dvd_pow_iff (by positivity)).mp h1
Proof state after:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
h2 : b ∣ a
⊢ ∃ d, c = d ^ 2
Theorem: Usa2015P1.abc
Proof state before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
h2 : b ∣ a
⊢ ∃ d, c = d ^ 2
Tactic:
obtain ⟨d, rfl⟩ := h2
Proof state after:
case intro
b c : ℤ
hb : b ≠ 0
d : ℤ
h : (b * d) ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ ∃ d, c = d ^ 2
Theorem: Usa2015P1.abc
Proof state before:
case intro
b c : ℤ
hb : b ≠ 0
d : ℤ
h : (b * d) ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ ∃ d, c = d ^ 2
Tactic:
rw [mul_pow, mul_right_inj' (by positivity)] at h
Proof state after:
case intro
b c : ℤ
hb : b ≠ 0
d : ℤ
h : d ^ 2 = c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ ∃ d, c = d ^ 2
Theorem: Usa2015P1.abc
Proof state before:
case intro
b c : ℤ
hb : b ≠ 0
d : ℤ
h : d ^ 2 = c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ ∃ d, c = d ^ 2
Tactic:
use d
Proof state after:
case h
b c : ℤ
hb : b ≠ 0
d : ℤ
h : d ^ 2 = c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ c = d ^ 2
Theorem: Usa2015P1.abc
Proof state before:
case h
b c : ℤ
hb : b ≠ 0
d : ℤ
h : d ^ 2 = c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ c = d ^ 2
Tactic:
exact h.symm
Proof state after:
no goals
Theorem: Usa2015P1.abc
Proof state before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
⊢ b ^ 2 ∣ a ^ 2
Tactic:
simp_all only [ne_eq, dvd_mul_right]
Proof state after:
no goals
Theorem: Usa2015P1.abc
Proof state before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
⊢ b ∣ a
Tactic:
apply (Int.pow_dvd_pow_iff (by positivity)).mp h1
Proof state after:
no goals
Theorem: Usa2015P1.abc
Proof state before:
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
⊢ 2 ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: Usa2015P1.abc
Proof state before:
b c : ℤ
hb : b ≠ 0
d : ℤ
h : b ^ 2 * d ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ b ^ 2 ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2012P4.sub_sq''
Proof state before:
x y : ℤ
⊢ x ^ 2 + y ^ 2 = 2 * x * y ↔ x = y
Tactic:
rw [← sub_eq_zero, ← sub_sq', sq_eq_zero_iff, sub_eq_zero]
Proof state after:
no goals
Theorem: Imo2012P4.Int.lt_of_ns_lt_ns
Proof state before:
x x' : ℕ
h : Int.negSucc x < Int.negSucc x'
⊢ x' < x
Tactic:
have := Int.neg_lt_neg h
Proof state after:
x x' : ℕ
h : Int.negSucc x < Int.negSucc x'
this : -Int.negSucc x' < -Int.negSucc x
⊢ x' < x
Theorem: Imo2012P4.Int.lt_of_ns_lt_ns
Proof state before:
x x' : ℕ
h : Int.negSucc x < Int.negSucc x'
this : -Int.negSucc x' < -Int.negSucc x
⊢ x' < x
Tactic:
rw [Int.neg_negSucc, Int.neg_negSucc, Int.ofNat_lt] at this
Proof state after:
x x' : ℕ
h : Int.negSucc x < Int.negSucc x'
this : x'.succ < x.succ
⊢ x' < x
Theorem: Imo2012P4.Int.lt_of_ns_lt_ns
Proof state before:
x x' : ℕ
h : Int.negSucc x < Int.negSucc x'
this : x'.succ < x.succ
⊢ x' < x
Tactic:
apply Nat.lt_of_succ_lt_succ this
Proof state after:
no goals
Theorem: Imo2001P1.lemma1
Proof state before:
t : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))
⊢ ∡ (Affine.Simplex.circumcenter t) (t.points 2) (t.points 1) = ↑Real.pi - ∡ (t.points 1) (t.points 0) (t.points 2)
Tactic:
sorry
Proof state after:
no goals
Theorem: Usa2023P5.injective_of_permuted_rows
Proof state before:
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
⊢ Function.Injective2 fun r c => f r (p r c)
Tactic:
intro a1 a2 b1 b2 hab
Proof state after:
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
⊢ a1 = a2 ∧ b1 = b2
Theorem: Usa2023P5.injective_of_permuted_rows
Proof state before:
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
⊢ a1 = a2 ∧ b1 = b2
Tactic:
obtain ⟨ha1, hp1⟩ := hf hab
Proof state after:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a1 = a2
hp1 : p a1 b1 = p a2 b2
⊢ a1 = a2 ∧ b1 = b2
Theorem: Usa2023P5.injective_of_permuted_rows
Proof state before:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a1 = a2
hp1 : p a1 b1 = p a2 b2
⊢ a1 = a2 ∧ b1 = b2
Tactic:
rw [ha1] at *
Proof state after:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a2 = a2
hp1 : p a2 b1 = p a2 b2
⊢ a2 = a2 ∧ b1 = b2
Theorem: Usa2023P5.injective_of_permuted_rows
Proof state before:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a2 = a2
hp1 : p a2 b1 = p a2 b2
⊢ a2 = a2 ∧ b1 = b2
Tactic:
rw [hp a2 hp1]
Proof state after:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a2 = a2
hp1 : p a2 b1 = p a2 b2
⊢ a2 = a2 ∧ b2 = b2
Theorem: Usa2023P5.injective_of_permuted_rows
Proof state before:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a2 = a2
hp1 : p a2 b1 = p a2 b2
⊢ a2 = a2 ∧ b2 = b2
Tactic:
simp only [and_self]
Proof state after:
no goals
Theorem: Imo2005P3.key_insight
Proof state before:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
⊢ (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) ≥ (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2)
Tactic:
have key :
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) -
      (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) /
      ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) := by
  field_simp
  ring
Proof state after:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
key :
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)))
⊢ (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) ≥ (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2)
Theorem: Imo2005P3.key_insight
Proof state before:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
key :
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)))
⊢ (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) ≥ (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2)
Tactic:
have h₅ :
  (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) /
      ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) ≥ 0 := by positivity
Proof state after:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
key :
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)))
h₅ : (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) ≥ 0
⊢ (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) ≥ (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2)
Theorem: Imo2005P3.key_insight
Proof state before:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
key :
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)))
h₅ : (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) ≥ 0
⊢ (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) ≥ (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2)
Tactic:
calc
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2)
    ≥ (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) := by linarith only [key, h₅]
  _ ≥ (x ^ 5 - x ^ 2 * (x * y * z)) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) := by gcongr
  _ = (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2) := by field_simp; ring
Proof state after:
no goals
Theorem: Imo2005P3.key_insight
Proof state before:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
⊢ (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)))
Tactic:
field_simp
Proof state after:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
⊢ (x ^ 5 - x ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) - (x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 5 - x ^ 2) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2)
Theorem: Imo2005P3.key_insight
Proof state before:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
⊢ (x ^ 5 - x ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) - (x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 5 - x ^ 2) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2)
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2005P3.key_insight
Proof state before:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
key :
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)))
⊢ (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) ≥ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2005P3.key_insight
Proof state before:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
key :
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)))
h₅ : (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) ≥ 0
⊢ (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) ≥ (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))
Tactic:
linarith only [key, h₅]
Proof state after:
no goals
Theorem: Imo2005P3.key_insight
Proof state before:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
key :
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)))
h₅ : (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) ≥ 0
⊢ (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) ≥
    (x ^ 5 - x ^ 2 * (x * y * z)) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))
Tactic:
gcongr
Proof state after:
no goals
Theorem: Imo2005P3.key_insight
Proof state before:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
key :
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)))
h₅ : (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) ≥ 0
⊢ (x ^ 5 - x ^ 2 * (x * y * z)) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) = (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2)
Tactic:
field_simp
Proof state after:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
key :
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)))
h₅ : (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) ≥ 0
⊢ (x ^ 5 - x ^ 2 * (x * y * z)) * (x ^ 2 + y ^ 2 + z ^ 2) = (x ^ 2 - y * z) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))