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

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]
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⁻))

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
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⁻))

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
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⁻))

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
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⁻))

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
State after:
no goals