Theorem: n1_2_5' (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
X : Set G
⊢ ↑(Subgroup.closure X) = {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Tactic:
simp only [Subgroup.closure, Subgroup.coe_sInf]
State after:
G : Type u_1
inst✝ : Group G
X : Set G
⊢ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s = {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}

State before:
G : Type u_1
inst✝ : Group G
X : Set G
⊢ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s = {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Tactic:
apply subset_antisymm
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
⊢ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s ⊆ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}

case a
G : Type u_1
inst✝ : Group G
X : Set G
⊢ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x} ⊆ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
⊢ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s ⊆ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Tactic:
intro x hx
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
⊢ x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
⊢ x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Tactic:
simp only [Set.mem_iInter] at hx
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Tactic:
simp only [Set.mem_setOf]
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ ∃ x_1 ∈ n125Set X, List.prod x_1 = x

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ ∃ x_1 ∈ n125Set X, List.prod x_1 = x
Tactic:
specialize hx (n125 X) _
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ n125 X ∈ {K | X ⊆ ↑K}

case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ ↑(n125 X)
⊢ ∃ x_1 ∈ n125Set X, List.prod x_1 = x

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ ↑(n125 X)
⊢ ∃ x_1 ∈ n125Set X, List.prod x_1 = x
Tactic:
simpa [n125] using hx
State after:
no goals

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ n125 X ∈ {K | X ⊆ ↑K}
Tactic:
intro y hy
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ y ∈ ↑(n125 X)

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ y ∈ ↑(n125 X)
Tactic:
simp only [n125, Set.mem_setOf, Subgroup.coe_set_mk]
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ ∃ x ∈ n125Set X, List.prod x = y

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ ∃ x ∈ n125Set X, List.prod x = y
Tactic:
refine' ⟨[y], _, List.prod_singleton⟩
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ [y] ∈ n125Set X

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ [y] ∈ n125Set X
Tactic:
simp only [hy, n125Set, forall_eq, true_or_iff, Set.mem_setOf, List.mem_singleton,
  Set.mem_union]
State after:
no goals

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
⊢ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x} ⊆ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
Tactic:
intro x hx
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
⊢ x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
⊢ x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
Tactic:
simp only [Set.mem_setOf, n125Set] at hx
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
⊢ x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
⊢ x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
Tactic:
simp only [Set.mem_iInter, SetLike.mem_coe]
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
⊢ ∀ i ∈ {K | X ⊆ ↑K}, x ∈ i

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
⊢ ∀ i ∈ {K | X ⊆ ↑K}, x ∈ i
Tactic:
intro i hi
State after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
⊢ x ∈ i

State before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
⊢ x ∈ i
Tactic:
obtain ⟨y, h1, rfl⟩ := hx
State after:
case a.intro.intro
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y : List G
h1 : ∀ x ∈ y, x ∈ X ∪ X⁻¹
⊢ List.prod y ∈ i

State before:
case a.intro.intro.nil
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
h1 : ∀ x ∈ [], x ∈ X ∪ X⁻¹
⊢ List.prod [] ∈ i
Tactic:
simp only [List.prod_nil, one_mem]
State after:
no goals

State before:
case a.intro.intro.cons
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ List.prod (y_hd :: tail) ∈ i
Tactic:
simp only [List.prod_cons]
State after:
case a.intro.intro.cons
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ y_hd * List.prod tail ∈ i

State before:
case a.intro.intro.cons
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ y_hd * List.prod tail ∈ i
Tactic:
apply mul_mem
State after:
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ y_hd ∈ i

case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ List.prod tail ∈ i

State before:
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ y_hd ∈ i
Tactic:
specialize h1 y_hd (List.mem_cons_self _ _)
State after:
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : y_hd ∈ X ∪ X⁻¹
⊢ y_hd ∈ i

State before:
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : y_hd ∈ X ∪ X⁻¹
⊢ y_hd ∈ i
Tactic:
obtain h1 | h1 := (Set.mem_union _ _ _).mp h1
State after:
case a.intro.intro.cons.a.inl
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X
⊢ y_hd ∈ i

case a.intro.intro.cons.a.inr
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X⁻¹
⊢ y_hd ∈ i

State before:
case a.intro.intro.cons.a.inl
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X
⊢ y_hd ∈ i
Tactic:
exact hi h1
State after:
no goals

State before:
case a.intro.intro.cons.a.inr
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X⁻¹
⊢ y_hd ∈ i
Tactic:
rw [← inv_inv y_hd]
State after:
case a.intro.intro.cons.a.inr
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X⁻¹
⊢ y_hd⁻¹⁻¹ ∈ i

State before:
case a.intro.intro.cons.a.inr
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1✝ : y_hd ∈ X ∪ X⁻¹
h1 : y_hd ∈ X⁻¹
⊢ y_hd⁻¹⁻¹ ∈ i
Tactic:
exact Subgroup.inv_mem _ (hi h1)
State after:
no goals

State before:
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ List.prod tail ∈ i
Tactic:
exact y_ih fun y hy => h1 _ (List.mem_cons_of_mem _ hy)
State after:
no goals