Theorem: IMOSL.IMO2012A7.MetaClosure.neg_mem (IMOSLLean4/IMO2012/A7/A7Group.lean)

State before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-(a✝ ⊓ b✝))
Tactic:
rw [neg_inf]
State after:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-a✝ ⊔ -b✝)

State before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-a✝ ⊔ -b✝)
Tactic:
exact ofSup
State after:
no goals

State before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-(a✝ ⊔ b✝))
Tactic:
rw [neg_sup]
State after:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-a✝ ⊓ -b✝)

State before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-a✝ ⊓ -b✝)
Tactic:
exact ofInf
State after:
no goals