internlm/Lean-Github huggingface dataset:
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
hxδ : x < x + δ
⊢ ∃ z, x < ↑z ∧ dist (↑z) x < δ
Tactic:
obtain ⟨z, hz1, hz2⟩ := exists_rat_btwn hxδ
Proof state after:
case intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
hxδ : x < x + δ
z : ℚ
hz1 : x < ↑z
hz2 : ↑z < x + δ
⊢ ∃ z, x < ↑z ∧ dist (↑z) x < δ
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
hxδ : x < x + δ
z : ℚ
hz1 : x < ↑z
hz2 : ↑z < x + δ
⊢ ∃ z, x < ↑z ∧ dist (↑z) x < δ
Tactic:
refine ⟨z, hz1, ?_⟩
Proof state after:
case intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
hxδ : x < x + δ
z : ℚ
hz1 : x < ↑z
hz2 : ↑z < x + δ
⊢ dist (↑z) x < δ
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
hxδ : x < x + δ
z : ℚ
hz1 : x < ↑z
hz2 : ↑z < x + δ
⊢ dist (↑z) x < δ
Tactic:
. rw [Real.dist_eq, abs_of_pos (sub_pos.mpr hz1)]
  exact sub_left_lt_of_lt_add hz2
Proof state after:
no goals
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
hxδ : x < x + δ
z : ℚ
hz1 : x < ↑z
hz2 : ↑z < x + δ
⊢ dist (↑z) x < δ
Tactic:
rw [Real.dist_eq, abs_of_pos (sub_pos.mpr hz1)]
Proof state after:
case intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
hxδ : x < x + δ
z : ℚ
hz1 : x < ↑z
hz2 : ↑z < x + δ
⊢ ↑z - x < δ
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
hxδ : x < x + δ
z : ℚ
hz1 : x < ↑z
hz2 : ↑z < x + δ
⊢ ↑z - x < δ
Tactic:
exact sub_left_lt_of_lt_add hz2
Proof state after:
no goals
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : dist (u ↑z) (f x) < ε
⊢ u ↑z < u x
Tactic:
have hufp : 0 < u x - f x := by linarith
Proof state after:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : dist (u ↑z) (f x) < ε
hufp : 0 < u x - f x
⊢ u ↑z < u x
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : dist (u ↑z) (f x) < ε
hufp : 0 < u x - f x
⊢ u ↑z < u x
Tactic:
have hua : ε = u x - f x := abs_of_pos hufp
Proof state after:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : dist (u ↑z) (f x) < ε
hufp : 0 < u x - f x
hua : ε = u x - f x
⊢ u ↑z < u x
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : dist (u ↑z) (f x) < ε
hufp : 0 < u x - f x
hua : ε = u x - f x
⊢ u ↑z < u x
Tactic:
rw [hua, Real.dist_eq] at hbzb
Proof state after:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : |u ↑z - f x| < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
⊢ u ↑z < u x
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : |u ↑z - f x| < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
⊢ u ↑z < u x
Tactic:
cases em (f x < u z)
Proof state after:
case inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : |u ↑z - f x| < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
h✝ : f x < u ↑z
⊢ u ↑z < u x

case inr
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : |u ↑z - f x| < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
h✝ : ¬f x < u ↑z
⊢ u ↑z < u x
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : dist (u ↑z) (f x) < ε
⊢ 0 < u x - f x
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : |u ↑z - f x| < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
h✝ : f x < u ↑z
⊢ u ↑z < u x
Tactic:
have : 0 ≤ u z - f x := by linarith
Proof state after:
case inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : |u ↑z - f x| < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
h✝ : f x < u ↑z
this : 0 ≤ u ↑z - f x
⊢ u ↑z < u x
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : |u ↑z - f x| < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
h✝ : f x < u ↑z
this : 0 ≤ u ↑z - f x
⊢ u ↑z < u x
Tactic:
rw[abs_eq_self.mpr this] at hbzb
Proof state after:
case inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : u ↑z - f x < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
h✝ : f x < u ↑z
this : 0 ≤ u ↑z - f x
⊢ u ↑z < u x
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : u ↑z - f x < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
h✝ : f x < u ↑z
this : 0 ≤ u ↑z - f x
⊢ u ↑z < u x
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : |u ↑z - f x| < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
h✝ : f x < u ↑z
⊢ 0 ≤ u ↑z - f x
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case inr
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : |u ↑z - f x| < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
h✝ : ¬f x < u ↑z
⊢ u ↑z < u x
Tactic:
linarith
Proof state after:
no goals
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
⊢ ∀ (a b c : ℝ), a > 0 → b > 0 → c > 0 → a ≥ b → b ≥ c → a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
Tactic:
intros a b c ha hb hc hab hbc
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
Tactic:
have habc : a * b * c > 0 := Real.mul_pos (Real.mul_pos ha hb) hc
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
Tactic:
have h : (a ^ a * b ^ b * c ^ c) * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) =
          (a * b * c) ^ (a + b + c) := by
  simp (discharger := positivity) only [Real.rpow_add, Real.mul_rpow]
  ring
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
Tactic:
apply le_of_pow_le_pow_left (by decide : 3 ≠ 0) (by positivity)
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ ((a * b * c) ^ ((a + b + c) / 3)) ^ 3 ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ ((a * b * c) ^ ((a + b + c) / 3)) ^ 3 ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Tactic:
rw [←Real.rpow_natCast]
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ ((a * b * c) ^ ((a + b + c) / 3)) ^ ↑3 ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ ((a * b * c) ^ ((a + b + c) / 3)) ^ ↑3 ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Tactic:
rw [←(Real.rpow_mul (le_of_lt habc))]
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ (a * b * c) ^ ((a + b + c) / 3 * ↑3) ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ (a * b * c) ^ ((a + b + c) / 3 * ↑3) ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Tactic:
norm_num
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ (a * b * c) ^ (a + b + c) ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ (a * b * c) ^ (a + b + c) ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Tactic:
rw [←h]
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Tactic:
rw [pow_three']
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)
Tactic:
have hab' := Real.log_le_log hb hab
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)
Tactic:
have hbc' := Real.log_le_log hc hbc
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)
Tactic:
gcongr ?_ * ?_ * ?_
Proof state after:
case h₁.h₁
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ a * b ^ b * c ^ c ≤ a ^ a * b ^ b * c ^ c

case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ b * b ^ c * c ^ a ≤ a ^ a * b ^ b * c ^ c

case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ c * b ^ a * c ^ b ≤ a ^ a * b ^ b * c ^ c
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
Tactic:
simp (discharger := positivity) only [Real.rpow_add, Real.mul_rpow]
Proof state after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) =
    a ^ a * b ^ a * c ^ a * (a ^ b * b ^ b * c ^ b) * (a ^ c * b ^ c * c ^ c)
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) =
    a ^ a * b ^ a * c ^ a * (a ^ b * b ^ b * c ^ b) * (a ^ c * b ^ c * c ^ c)
Tactic:
ring
Proof state after:
no goals
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ 3 ≠ 0
Tactic:
decide
Proof state after:
no goals
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ 0 ≤ a ^ a * b ^ b * c ^ c
Tactic:
positivity
Proof state after:
no goals
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
case h₁.h₁
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ a * b ^ b * c ^ c ≤ a ^ a * b ^ b * c ^ c
Tactic:
rfl
Proof state after:
no goals
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ b * b ^ c * c ^ a ≤ a ^ a * b ^ b * c ^ c
Tactic:
rw [←(Real.log_le_log_iff (by positivity) (by positivity))]
Proof state after:
case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ (a ^ b * b ^ c * c ^ a).log ≤ (a ^ a * b ^ b * c ^ c).log
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ (a ^ b * b ^ c * c ^ a).log ≤ (a ^ a * b ^ b * c ^ c).log
Tactic:
simp (discharger := positivity) only [Real.log_mul, Real.log_rpow]
Proof state after:
case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ b * a.log + c * b.log + a * c.log ≤ a * a.log + b * b.log + c * c.log
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ b * a.log + c * b.log + a * c.log ≤ a * a.log + b * b.log + c * c.log
Tactic:
nlinarith only [hab', hbc', hab, hbc]
Proof state after:
no goals
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ 0 < a ^ b * b ^ c * c ^ a
Tactic:
positivity
Proof state after:
no goals