Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula (IMOSLLean4/IMO2012/A7/A7PiRing.lean)

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺
Tactic:
rcases le_total a 0 with h | h
State after:
case inl
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : a ≤ 0
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺

case inr
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺

State before:
case inr
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺
Tactic:
rcases le_total b 0 with h0 | h0
State after:
case inr.inl
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : b ≤ 0
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺

case inr.inr
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺

State before:
case inr.inr
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺
Tactic:
rw [posPart_eq_self.mpr h, posPart_eq_self.mpr h0, eq_comm]
State after:
case inr.inr
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
⊢ (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺ = a * b

State before:
case inr.inr
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
⊢ (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺ = a * b
Tactic:
refine (congr_arg _ (min_eq_left <| le_min ?_ ?_)).trans
  (posPart_eq_self.mpr (mul_nonneg h h0))
State after:
case inr.inr.refine_1
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
⊢ a * b ≤ max a (a * b ^ 2)

case inr.inr.refine_2
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
⊢ a * b ≤ max b (a ^ 2 * b)

State before:
case inl
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : a ≤ 0
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺
Tactic:
rw [posPart_eq_zero.mpr h, zero_mul, eq_comm, posPart_eq_zero, min_le_iff, min_le_iff]
State after:
case inl
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : a ≤ 0
⊢ a * b ≤ 0 ∨ max a (a * b ^ 2) ≤ 0 ∨ max b (a ^ 2 * b) ≤ 0

State before:
case inl
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : a ≤ 0
⊢ a * b ≤ 0 ∨ max a (a * b ^ 2) ≤ 0 ∨ max b (a ^ 2 * b) ≤ 0
Tactic:
right
State after:
case inl.h
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : a ≤ 0
⊢ max a (a * b ^ 2) ≤ 0 ∨ max b (a ^ 2 * b) ≤ 0

State before:
case inl.h
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : a ≤ 0
⊢ max a (a * b ^ 2) ≤ 0 ∨ max b (a ^ 2 * b) ≤ 0
Tactic:
left
State after:
case inl.h.h
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : a ≤ 0
⊢ max a (a * b ^ 2) ≤ 0

State before:
case inl.h.h
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : a ≤ 0
⊢ max a (a * b ^ 2) ≤ 0
Tactic:
exact max_le h (mul_nonpos_of_nonpos_of_nonneg h (sq_nonneg b))
State after:
no goals

State before:
case inr.inl
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : b ≤ 0
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺
Tactic:
rw [posPart_eq_zero.mpr h0, mul_zero, eq_comm, posPart_eq_zero, min_le_iff, min_le_iff]
State after:
case inr.inl
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : b ≤ 0
⊢ a * b ≤ 0 ∨ max a (a * b ^ 2) ≤ 0 ∨ max b (a ^ 2 * b) ≤ 0

State before:
case inr.inl
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : b ≤ 0
⊢ a * b ≤ 0 ∨ max a (a * b ^ 2) ≤ 0 ∨ max b (a ^ 2 * b) ≤ 0
Tactic:
right
State after:
case inr.inl.h
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : b ≤ 0
⊢ max a (a * b ^ 2) ≤ 0 ∨ max b (a ^ 2 * b) ≤ 0

State before:
case inr.inl.h
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : b ≤ 0
⊢ max a (a * b ^ 2) ≤ 0 ∨ max b (a ^ 2 * b) ≤ 0
Tactic:
right
State after:
case inr.inl.h.h
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : b ≤ 0
⊢ max b (a ^ 2 * b) ≤ 0

State before:
case inr.inl.h.h
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : b ≤ 0
⊢ max b (a ^ 2 * b) ≤ 0
Tactic:
exact max_le h0 (mul_nonpos_of_nonneg_of_nonpos (sq_nonneg a) h0)
State after:
no goals

State before:
case inr.inr.refine_1
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
⊢ a * b ≤ max a (a * b ^ 2)
Tactic:
have h1 := mul_le_mul_of_nonneg_left (le_max_one_sq b) h
State after:
case inr.inr.refine_1
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
h1 : a * b ≤ a * max 1 (b ^ 2)
⊢ a * b ≤ max a (a * b ^ 2)

State before:
case inr.inr.refine_1
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
h1 : a * b ≤ a * max 1 (b ^ 2)
⊢ a * b ≤ max a (a * b ^ 2)
Tactic:
rwa [mul_max_of_nonneg _ _ h, mul_one] at h1
State after:
no goals

State before:
case inr.inr.refine_2
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
⊢ a * b ≤ max b (a ^ 2 * b)
Tactic:
have h1 := mul_le_mul_of_nonneg_right (le_max_one_sq a) h0
State after:
case inr.inr.refine_2
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
h1 : a * b ≤ max 1 (a ^ 2) * b
⊢ a * b ≤ max b (a ^ 2 * b)

State before:
case inr.inr.refine_2
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
h1 : a * b ≤ max 1 (a ^ 2) * b
⊢ a * b ≤ max b (a ^ 2 * b)
Tactic:
rwa [max_mul_of_nonneg _ _ h0, one_mul] at h1
State after:
no goals