Theorem: IMOSL.IMO2012A7.MetaClosure.add_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 b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
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) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) (a✝¹ + a✝ ⊓ b✝)
Tactic:
rw [add_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 b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
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) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) ((a✝¹ + a✝) ⊓ (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 b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
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) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) ((a✝¹ + a✝) ⊓ (a✝¹ + b✝))
Tactic:
exact ofInf
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 b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
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) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) (a✝¹ + a✝ ⊔ b✝)
Tactic:
rw [add_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 b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
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) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) ((a✝¹ + a✝) ⊔ (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 b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
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) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) ((a✝¹ + a✝) ⊔ (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 b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) (a✝ ⊓ b✝ + b)
Tactic:
rw [inf_add]
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 b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) ((a✝ + b) ⊓ (b✝ + 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 b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) ((a✝ + b) ⊓ (b✝ + b))
Tactic:
exact ofInf
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 b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) (a✝ ⊔ b✝ + b)
Tactic:
rw [sup_add]
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 b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) ((a✝ + b) ⊔ (b✝ + 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 b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) ((a✝ + b) ⊔ (b✝ + b))
Tactic:
exact ofSup
State after:
no goals