G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ s ⊔ t
⊢ ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x
rw [← closure_eq s, ← closure_eq t, ← closure_union] at h
case refine_1
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x : C), x ∈ ↑s ∪ ↑t → ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x

case refine_2
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = 1

case refine_3
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x y : C),
    (∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x) →
      (∃ y_1, y_1 ∈ s ∧ ∃ z, z ∈ t ∧ y_1 * z = y) → ∃ y_1, y_1 ∈ s ∧ ∃ z, z ∈ t ∧ y_1 * z = x * y

case refine_4
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x : C), (∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x) → ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x⁻¹
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x
refine Subgroup.closure_induction h ?_ ?_ ?_ ?_
case refine_1.inl
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑s
⊢ ∃ y_1, y_1 ∈ s ∧ ∃ z, z ∈ t ∧ y_1 * z = y

case refine_1.inr
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ ∃ y_1, y_1 ∈ s ∧ ∃ z, z ∈ t ∧ y_1 * z = y
case refine_1
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x : C), x ∈ ↑s ∪ ↑t → ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x
rintro y (h | h)
no goals
case refine_1.inl
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑s
⊢ ∃ y_1, y_1 ∈ s ∧ ∃ z, z ∈ t ∧ y_1 * z = y
exact ⟨y, h, 1, t.one_mem, by simp⟩
no goals
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑s
⊢ y * 1 = y
simp
no goals
case refine_1.inr
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ ∃ y_1, y_1 ∈ s ∧ ∃ z, z ∈ t ∧ y_1 * z = y
exact ⟨1, s.one_mem, y, h, by simp⟩
no goals
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ 1 * y = y
simp
no goals
case refine_2
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = 1
exact ⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩
case refine_3.intro.intro.intro.intro.intro.intro.intro.intro
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y₁ : C
hy₁ : y₁ ∈ s
z₁ : C
hz₁ : z₁ ∈ t
y₂ : C
hy₂ : y₂ ∈ s
z₂ : C
hz₂ : z₂ ∈ t
⊢ ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = y₁ * z₁ * (y₂ * z₂)
case refine_3
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x y : C),
    (∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x) →
      (∃ y_1, y_1 ∈ s ∧ ∃ z, z ∈ t ∧ y_1 * z = y) → ∃ y_1, y_1 ∈ s ∧ ∃ z, z ∈ t ∧ y_1 * z = x * y
rintro _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
no goals
case refine_3.intro.intro.intro.intro.intro.intro.intro.intro
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y₁ : C
hy₁ : y₁ ∈ s
z₁ : C
hz₁ : z₁ ∈ t
y₂ : C
hy₂ : y₂ ∈ s
z₂ : C
hz₂ : z₂ ∈ t
⊢ ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = y₁ * z₁ * (y₂ * z₂)
exact ⟨_, mul_mem hy₁ hy₂, _, mul_mem hz₁ hz₂, by simp [mul_assoc, mul_left_comm]⟩
no goals
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y₁ : C
hy₁ : y₁ ∈ s
z₁ : C
hz₁ : z₁ ∈ t
y₂ : C
hy₂ : y₂ ∈ s
z₂ : C
hz₂ : z₂ ∈ t
⊢ y₁ * y₂ * (z₁ * z₂) = y₁ * z₁ * (y₂ * z₂)
simp [mul_assoc, mul_left_comm]
case refine_4.intro.intro.intro.intro
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y : C
hy : y ∈ s
z : C
hz : z ∈ t
⊢ ∃ y_1, y_1 ∈ s ∧ ∃ z_1, z_1 ∈ t ∧ y_1 * z_1 = (y * z)⁻¹
case refine_4
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x : C), (∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x) → ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x⁻¹
rintro _ ⟨y, hy, z, hz, rfl⟩
no goals
case refine_4.intro.intro.intro.intro
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y : C
hy : y ∈ s
z : C
hz : z ∈ t
⊢ ∃ y_1, y_1 ∈ s ∧ ∃ z_1, z_1 ∈ t ∧ y_1 * z_1 = (y * z)⁻¹
exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩
case intro.intro.intro.intro
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
y : C
hy : y ∈ s
z : C
hz : z ∈ t
⊢ y * z ∈ s ⊔ t
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
⊢ (∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x) → x ∈ s ⊔ t
rintro ⟨y, hy, z, hz, rfl⟩
no goals
case intro.intro.intro.intro
G : Type ?u.693133
G' : Type ?u.693136
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.693145
inst✝² : AddGroup A
N : Type ?u.693151
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
y : C
hy : y ∈ s
z : C
hz : z ∈ t
⊢ y * z ∈ s ⊔ t
exact mul_mem_sup hy hz