internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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]
Proof 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
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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))
Proof 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)
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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]
Proof 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
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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))
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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]
Proof 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
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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
Proof 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)
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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
Proof 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)
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_closure_pos_part_mul_closure_pos_part_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg✝ : MetaClosure (fun x => x ∈ S) g
a✝¹ : (i : I) → R i
hg : a✝¹ ∈ S
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝⁺ * a✝¹⁺) →
    MetaClosure (fun x => x ∈ S) (b✝⁺ * a✝¹⁺) → MetaClosure (fun x => x ∈ S) ((a✝ ⊓ b✝)⁺ * a✝¹⁺)
Tactic:
rw [inf_pos_part, Pi_inf_mul_pos_part]
Proof state after:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg✝ : MetaClosure (fun x => x ∈ S) g
a✝¹ : (i : I) → R i
hg : a✝¹ ∈ S
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝⁺ * a✝¹⁺) →
    MetaClosure (fun x => x ∈ S) (b✝⁺ * a✝¹⁺) → MetaClosure (fun x => x ∈ S) (a✝⁺ * a✝¹⁺ ⊓ b✝⁺ * a✝¹⁺)
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_closure_pos_part_mul_closure_pos_part_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg✝ : MetaClosure (fun x => x ∈ S) g
a✝¹ : (i : I) → R i
hg : a✝¹ ∈ S
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝⁺ * a✝¹⁺) →
    MetaClosure (fun x => x ∈ S) (b✝⁺ * a✝¹⁺) → MetaClosure (fun x => x ∈ S) (a✝⁺ * a✝¹⁺ ⊓ b✝⁺ * a✝¹⁺)
Tactic:
exact ofInf
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_closure_pos_part_mul_closure_pos_part_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg✝ : MetaClosure (fun x => x ∈ S) g
a✝¹ : (i : I) → R i
hg : a✝¹ ∈ S
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝⁺ * a✝¹⁺) →
    MetaClosure (fun x => x ∈ S) (b✝⁺ * a✝¹⁺) → MetaClosure (fun x => x ∈ S) ((a✝ ⊔ b✝)⁺ * a✝¹⁺)
Tactic:
rw [sup_pos_part, Pi_sup_mul_pos_part]
Proof state after:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg✝ : MetaClosure (fun x => x ∈ S) g
a✝¹ : (i : I) → R i
hg : a✝¹ ∈ S
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝⁺ * a✝¹⁺) →
    MetaClosure (fun x => x ∈ S) (b✝⁺ * a✝¹⁺) → MetaClosure (fun x => x ∈ S) (a✝⁺ * a✝¹⁺ ⊔ b✝⁺ * a✝¹⁺)
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_closure_pos_part_mul_closure_pos_part_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg✝ : MetaClosure (fun x => x ∈ S) g
a✝¹ : (i : I) → R i
hg : a✝¹ ∈ S
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝⁺ * a✝¹⁺) →
    MetaClosure (fun x => x ∈ S) (b✝⁺ * a✝¹⁺) → MetaClosure (fun x => x ∈ S) (a✝⁺ * a✝¹⁺ ⊔ b✝⁺ * a✝¹⁺)
Tactic:
exact ofSup
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_closure_pos_part_mul_closure_pos_part_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * a✝⁺) →
    MetaClosure (fun x => x ∈ S) (f⁺ * b✝⁺) → MetaClosure (fun x => x ∈ S) (f⁺ * (a✝ ⊓ b✝)⁺)
Tactic:
rw [inf_pos_part, Pi_pos_part_mul_inf]
Proof state after:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * a✝⁺) →
    MetaClosure (fun x => x ∈ S) (f⁺ * b✝⁺) → MetaClosure (fun x => x ∈ S) (f⁺ * a✝⁺ ⊓ f⁺ * b✝⁺)
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_closure_pos_part_mul_closure_pos_part_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * a✝⁺) →
    MetaClosure (fun x => x ∈ S) (f⁺ * b✝⁺) → MetaClosure (fun x => x ∈ S) (f⁺ * a✝⁺ ⊓ f⁺ * b✝⁺)
Tactic:
exact ofInf
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_closure_pos_part_mul_closure_pos_part_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * a✝⁺) →
    MetaClosure (fun x => x ∈ S) (f⁺ * b✝⁺) → MetaClosure (fun x => x ∈ S) (f⁺ * (a✝ ⊔ b✝)⁺)
Tactic:
rw [sup_pos_part, Pi_pos_part_mul_sup]
Proof state after:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * a✝⁺) →
    MetaClosure (fun x => x ∈ S) (f⁺ * b✝⁺) → MetaClosure (fun x => x ∈ S) (f⁺ * a✝⁺ ⊔ f⁺ * b✝⁺)
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_closure_pos_part_mul_closure_pos_part_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
a✝ b✝ : (i : I) → R i
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * a✝⁺) →
    MetaClosure (fun x => x ∈ S) (f⁺ * b✝⁺) → MetaClosure (fun x => x ∈ S) (f⁺ * a✝⁺ ⊔ f⁺ * b✝⁺)
Tactic:
exact ofSup
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_mul_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
⊢ MetaClosure (fun x => x ∈ S) (f * g)
Tactic:
rw [← posPart_sub_negPart f, sub_mul,
  ← posPart_sub_negPart g, mul_sub, mul_sub]
Proof state after:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * g⁺ - f⁺ * g⁻ - (f⁻ * g⁺ - f⁻ * g⁻))
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_mul_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * g⁺ - f⁺ * g⁻ - (f⁻ * g⁺ - f⁻ * g⁻))
Tactic:
let T := S.toAddSubgroup
Proof state after:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
T : AddSubgroup ((i : I) → R i) := S.toAddSubgroup
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * g⁺ - f⁺ * g⁻ - (f⁻ * g⁺ - f⁻ * g⁻))
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_mul_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
T : AddSubgroup ((i : I) → R i) := S.toAddSubgroup
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * g⁺ - f⁺ * g⁻ - (f⁻ * g⁺ - f⁻ * g⁻))
Tactic:
have hf₀ : MetaClosure (λ x ↦ x ∈ S) (-f) := neg_mem T hf
Proof state after:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
T : AddSubgroup ((i : I) → R i) := S.toAddSubgroup
hf₀ : MetaClosure (fun x => x ∈ S) (-f)
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * g⁺ - f⁺ * g⁻ - (f⁻ * g⁺ - f⁻ * g⁻))
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_mul_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
T : AddSubgroup ((i : I) → R i) := S.toAddSubgroup
hf₀ : MetaClosure (fun x => x ∈ S) (-f)
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * g⁺ - f⁺ * g⁻ - (f⁻ * g⁺ - f⁻ * g⁻))
Tactic:
have hg₀ : MetaClosure (λ x ↦ x ∈ S) (-g) := neg_mem T hg
Proof state after:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
T : AddSubgroup ((i : I) → R i) := S.toAddSubgroup
hf₀ : MetaClosure (fun x => x ∈ S) (-f)
hg₀ : MetaClosure (fun x => x ∈ S) (-g)
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * g⁺ - f⁺ * g⁻ - (f⁻ * g⁺ - f⁻ * g⁻))
Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_mul_mem
Proof state before:
I : Type u_2
R : I → Type u_1
inst✝ : (i : I) → LinearOrderedRing (R i)
S : Subring ((i : I) → R i)
f g : (i : I) → R i
hf : MetaClosure (fun x => x ∈ S) f
hg : MetaClosure (fun x => x ∈ S) g
T : AddSubgroup ((i : I) → R i) := S.toAddSubgroup
hf₀ : MetaClosure (fun x => x ∈ S) (-f)
hg₀ : MetaClosure (fun x => x ∈ S) (-g)
⊢ MetaClosure (fun x => x ∈ S) (f⁺ * g⁺ - f⁺ * g⁻ - (f⁻ * g⁺ - f⁻ * g⁻))
Tactic:
apply sub_mem T <;> apply sub_mem T <;>
  apply Pi_closure_pos_part_mul_closure_pos_part_mem <;> assumption
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_add_cancel_left
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y : M
⊢ x + (x + y) = y
Tactic:
rw [← add_assoc, add_self_eq_zero, zero_add]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_add_cancel_right
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y : M
⊢ x + y + y = x
Tactic:
rw [add_assoc, add_self_eq_zero, add_zero]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_add_add_cancel_middle
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y z : M
⊢ x + y + (y + z) = x + z
Tactic:
rw [← add_assoc, add_add_cancel_right]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_comm
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y : M
⊢ x + y = y + x
Tactic:
rw [← add_add_cancel_right (x + y) (y + x),
  add_add_add_cancel_middle, add_self_eq_zero, zero_add]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_add_cancel_middle₁
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y : M
⊢ x + (y + x) = y
Tactic:
rw [add_comm, add_add_cancel_right]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_add_cancel_middle₂
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y : M
⊢ x + y + x = y
Tactic:
rw [add_comm, add_add_cancel_left]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_right_inj
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y z : M
h : x + y = x + z
⊢ y = z
Tactic:
rw [← add_add_cancel_left x y, h, add_add_cancel_left]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_left_inj
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y z : M
⊢ x + z = y + z ↔ x = y
Tactic:
rw [add_comm, add_comm y, add_right_inj]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_eq_iff_eq_add
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y z : M
⊢ x + y = z ↔ x = z + y
Tactic:
rw [← add_left_inj (z := y), add_add_cancel_right]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_eq_iff_eq_add'
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y z : M
⊢ x + y = z ↔ x = y + z
Tactic:
rw [add_eq_iff_eq_add, add_comm]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_eq_iff_eq_add''
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y z : M
⊢ x + y = z ↔ y = x + z
Tactic:
rw [add_comm, add_eq_iff_eq_add']
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_eq_iff_eq_add'''
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y z : M
⊢ x + y = z ↔ y = z + x
Tactic:
rw [add_eq_iff_eq_add'', add_comm]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_eq_zero_iff_eq
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y : M
⊢ x + y = 0 ↔ x = y
Tactic:
rw [add_eq_iff_eq_add, zero_add]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_add_add_cancel_left
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y z : M
⊢ x + y + (x + z) = y + z
Tactic:
rw [← add_assoc, add_add_cancel_middle₂]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_add_add_cancel_right
Proof state before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y z : M
⊢ x + z + (y + z) = x + y
Tactic:
rw [add_assoc, add_add_cancel_middle₁]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.sub_eq_add
Proof state before:
G : Type u_1
inst✝¹ : AddGroup G
inst✝ : CharTwo G
x y : G
⊢ x - y = x + y
Tactic:
rw [sub_eq_add_neg, neg_eq_self]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.good_comp_hom
Proof state before:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
R₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring R₀
φ : R₀ →+* R
x y : R₀
⊢ (f ∘ ⇑φ) (x * y + 1) = (f ∘ ⇑φ) x * (f ∘ ⇑φ) y + (f ∘ ⇑φ) (x + y)
Tactic:
simp only [Function.comp_apply]
Proof state after:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
R₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring R₀
φ : R₀ →+* R
x y : R₀
⊢ f (φ (x * y + 1)) = f (φ x) * f (φ y) + f (φ (x + y))
Theorem: IMOSL.IMO2012A5.good_comp_hom
Proof state before:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
R₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring R₀
φ : R₀ →+* R
x y : R₀
⊢ f (φ (x * y + 1)) = f (φ x) * f (φ y) + f (φ (x + y))
Tactic:
rw [φ.map_add, φ.map_mul, φ.map_one, h, φ.map_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.good_hom_comp
Proof state before:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
S₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
x y : R
⊢ (⇑φ ∘ f) (x * y + 1) = (⇑φ ∘ f) x * (⇑φ ∘ f) y + (⇑φ ∘ f) (x + y)
Tactic:
simp only [Function.comp_apply]
Proof state after:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
S₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
x y : R
⊢ φ (f (x * y + 1)) = φ (f x) * φ (f y) + φ (f (x + y))
Theorem: IMOSL.IMO2012A5.good_hom_comp
Proof state before:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
S₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
x y : R
⊢ φ (f (x * y + 1)) = φ (f x) * φ (f y) + φ (f (x + y))
Tactic:
rw [h, φ.map_add, φ.map_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.NontrivialGood.hom_comp
Proof state before:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
S₀ : Type u_1
hf : NontrivialGood f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
⊢ (⇑φ ∘ f) 0 + 1 = 0
Tactic:
rw [← φ.map_one, ← φ.map_zero, ← hf.map_zero_add_one, φ.map_add]
Proof state after:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
S₀ : Type u_1
hf : NontrivialGood f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
⊢ (⇑φ ∘ f) 0 + φ 1 = φ (f 0) + φ 1
Theorem: IMOSL.IMO2012A5.NontrivialGood.hom_comp
Proof state before:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
S₀ : Type u_1
hf : NontrivialGood f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
⊢ (⇑φ ∘ f) 0 + φ 1 = φ (f 0) + φ 1
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.mul_comm
Proof state before:
a b a' b' : ℤ
⊢ { re := a, im := b } * { re := a', im := b' } = { re := a', im := b' } * { re := a, im := b }
Tactic:
rw [mul_def, mul_def, mul_comm a, mul_comm b, add_comm (a * b')]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.mul_assoc
Proof state before:
a b a' b' a'' b'' : ℤ
⊢ { re := a, im := b } * { re := a', im := b' } * { re := a'', im := b'' } =
    { re := a, im := b } * ({ re := a', im := b' } * { re := a'', im := b'' })
Tactic:
rw [mul_def, mul_def, mul_def, mul_def, ℤφ.mk.injEq]
Proof state after:
a b a' b' a'' b'' : ℤ
⊢ { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.re * a'' +
        { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im * b'' =
      a * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.re +
        b * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im ∧
    { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.re * b'' +
          a'' * { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im +
        { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im * b'' =
      a * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im +
          { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.re * b +
        b * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im