Theorem: IMOSL.IMO2012A7.MetaClosure.Pi_closure_pos_part_mul_closure_pos_part_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
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]
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✝¹⁺)

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

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]
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✝¹⁺)

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

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]
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✝⁺)

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

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]
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✝⁺)

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