-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem mem_sup : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x :=
  ⟨fun h => by
    rw [sup_eq_closure] at h
    refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h
    · rintro y (h | h)
      · exact ⟨y, h, 1, t.one_mem, by simp⟩
      · exact ⟨1, s.one_mem, y, h, by simp⟩
    · exact ⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩
    · rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨_, mul_mem hy₁ hy₂, _, mul_mem hz₁ hz₂, by simp [mul_assoc, mul_left_comm]⟩
    · rintro _ _ ⟨y, hy, z, hz, rfl⟩
      exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩, by
    rintro ⟨y, hy, z, hz, rfl⟩; exact mul_mem_sup hy hz⟩

Proof state:
case refine_1.inr
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y

Tactic:
exact ⟨1, s.one_mem, y, h, by simp⟩

Result:
no goals

Proof state:
case refine_4.intro.intro.intro.intro
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y : C
hy : y ∈ s
z : C
hz : z ∈ t
hx✝ : y * z ∈ closure (↑s ∪ ↑t)
⊢ ∃ y_1 ∈ s, ∃ z_1 ∈ t, y_1 * z_1 = (y * z)⁻¹

Tactic:
exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
y : C
hy : y ∈ s
z : C
hz : z ∈ t
⊢ y * z ∈ s ⊔ t

Tactic:
exact mul_mem_sup hy hz

Result:
no goals

Proof state:
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ s ⊔ t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
rw [sup_eq_closure] at h

Result:
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Proof state:
case refine_3
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x y : C),
    x ∈ closure (↑s ∪ ↑t) →
      y ∈ closure (↑s ∪ ↑t) →
        (∃ y ∈ s, ∃ z ∈ t, y * z = x) → (∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y) → ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = x * y

Tactic:
rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩

Result:
case refine_3.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y₁ : C
hy₁ : y₁ ∈ s
z₁ : C
hz₁ : z₁ ∈ t
hx✝ : y₁ * z₁ ∈ closure (↑s ∪ ↑t)
y₂ : C
hy₂ : y₂ ∈ s
z₂ : C
hz₂ : z₂ ∈ t
hy✝ : y₂ * z₂ ∈ closure (↑s ∪ ↑t)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = y₁ * z₁ * (y₂ * z₂)

Proof state:
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ 1 * y = y

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h

Result:
case refine_1
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ ↑s ∪ ↑t, ∃ y ∈ s, ∃ z ∈ t, y * z = x

case refine_2
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = 1

case refine_3
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x y : C),
    x ∈ closure (↑s ∪ ↑t) →
      y ∈ closure (↑s ∪ ↑t) →
        (∃ y ∈ s, ∃ z ∈ t, y * z = x) → (∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y) → ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = x * y

case refine_4
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ closure (↑s ∪ ↑t), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹

Proof state:
case refine_3.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y₁ : C
hy₁ : y₁ ∈ s
z₁ : C
hz₁ : z₁ ∈ t
hx✝ : y₁ * z₁ ∈ closure (↑s ∪ ↑t)
y₂ : C
hy₂ : y₂ ∈ s
z₂ : C
hz₂ : z₂ ∈ t
hy✝ : y₂ * z₂ ∈ closure (↑s ∪ ↑t)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = y₁ * z₁ * (y₂ * z₂)

Tactic:
exact ⟨_, mul_mem hy₁ hy₂, _, mul_mem hz₁ hz₂, by simp [mul_assoc, mul_left_comm]⟩

Result:
no goals

Proof state:
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y₁ : C
hy₁ : y₁ ∈ s
z₁ : C
hz₁ : z₁ ∈ t
hx✝ : y₁ * z₁ ∈ closure (↑s ∪ ↑t)
y₂ : C
hy₂ : y₂ ∈ s
z₂ : C
hz₂ : z₂ ∈ t
hy✝ : y₂ * z₂ ∈ closure (↑s ∪ ↑t)
⊢ y₁ * y₂ * (z₁ * z₂) = y₁ * z₁ * (y₂ * z₂)

Tactic:
simp [mul_assoc, mul_left_comm]

Result:
no goals

Proof state:
case refine_4
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ closure (↑s ∪ ↑t), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹

Tactic:
rintro _ _ ⟨y, hy, z, hz, rfl⟩

Result:
case refine_4.intro.intro.intro.intro
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y : C
hy : y ∈ s
z : C
hz : z ∈ t
hx✝ : y * z ∈ closure (↑s ∪ ↑t)
⊢ ∃ y_1 ∈ s, ∃ z_1 ∈ t, y_1 * z_1 = (y * z)⁻¹

Proof state:
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
⊢ (∃ y ∈ s, ∃ z ∈ t, y * z = x) → x ∈ s ⊔ t

Tactic:
rintro ⟨y, hy, z, hz, rfl⟩

Result:
case intro.intro.intro.intro
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
y : C
hy : y ∈ s
z : C
hz : z ∈ t
⊢ y * z ∈ s ⊔ t

Proof state:
case refine_2
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = 1

Tactic:
exact ⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩

Result:
no goals

Proof state:
case refine_1
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ ↑s ∪ ↑t, ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
rintro y (h | h)

Result:
case refine_1.inl
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑s
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y

case refine_1.inr
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y

Proof state:
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑s
⊢ y * 1 = y

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.inl
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑s
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y

Tactic:
exact ⟨y, h, 1, t.one_mem, by simp⟩

Result:
no goals