awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
⊢ Membership.mem (γ := Subgroup G) (⨆ (i : ι), ⨆ (_ : p i), K i) x → ∃ (i : ι), p i ∧ x ∈ K i
have refine_1 : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x → ∃ (i : ι), p i ∧ x ∈ K i
Tactic: suffices x ∈ closure (⋃ i, ⋃ (_ : p i), (K i : Set G)) → ∃ i, p i ∧ x ∈ K i by
      simpa only [closure_iUnion, closure_eq (K _)] using this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
⊢ Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x → ∃ (i : ι), p i ∧ x ∈ K i
have refine_1 : ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x) (x : G)
  (hx : Membership.mem (γ := Set G) (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G)) x), ∃ (i : ι), p i ∧ x ∈ K i
Tactic: refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
refine_1 :
  ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x) (x : G)
    (hx : Membership.mem (γ := Set G) (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G)) x), ∃ (i : ι), p i ∧ x ∈ K i
⊢ Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x → ∃ (i : ι), p i ∧ x ∈ K i
have refine_1₁ : ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x),
  ∃ (i : ι), p i ∧ 1 ∈ K i
Tactic: refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
refine_1 :
  ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x) (x : G)
    (hx : Membership.mem (γ := Set G) (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G)) x), ∃ (i : ι), p i ∧ x ∈ K i
refine_1₁ :
  ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x),
    ∃ (i : ι), p i ∧ 1 ∈ K i
⊢ Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x → ∃ (i : ι), p i ∧ x ∈ K i
have refine_1₂ : ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x) (x y : G)
  (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x)
  (hy : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) y),
  (∃ (i : ι), p i ∧ x ∈ K i) → (∃ (i : ι), p i ∧ y ∈ K i) → ∃ (i : ι), p i ∧ x * y ∈ K i
Tactic: refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
refine_1 :
  ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x) (x : G)
    (hx : Membership.mem (γ := Set G) (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G)) x), ∃ (i : ι), p i ∧ x ∈ K i
refine_1₁ :
  ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x),
    ∃ (i : ι), p i ∧ 1 ∈ K i
refine_1₂ :
  ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x) (x y : G)
    (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x)
    (hy : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) y),
    (∃ (i : ι), p i ∧ x ∈ K i) → (∃ (i : ι), p i ∧ y ∈ K i) → ∃ (i : ι), p i ∧ x * y ∈ K i
⊢ Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x → ∃ (i : ι), p i ∧ x ∈ K i
have refine_1₃ : ∀ (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x) (x : G)
  (hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x),
  (∃ (i : ι), p i ∧ x ∈ K i) → ∃ (i : ι), p i ∧ x⁻¹ ∈ K i
Tactic: refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i_1 : ι
hp : p i_1
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x_1 : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x_1
x y : G
hx_1 : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) x
hy : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), ⋃ (_ : p i), (↑(K i) : Set G))) y
i : ι
hip : p i
hi : x ∈ K i
j : ι
hjp : p j
hj : y ∈ K j
⊢ ∃ (i : ι), p i ∧ x * y ∈ K i
have refine_1 : ∀ (k : ι) (hk : Membership.mem (γ := Set ι) {i : ι | p i} k) (hki : ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) i k)
  (hkj : ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) j k), ∃ (i : ι), p i ∧ x * y ∈ K i
Tactic: rcases hK i hip j hjp with ⟨k, hk, hki, hkj⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i_1 : ι
hp : p i_1
hK : DirectedOn ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on K) {i : ι | p i}
x : G
h : ∃ (i : ι), p i ∧ x ∈ K i
i : ι
hi' : p i
hi : x ∈ K i
⊢ Membership.mem (γ := Subgroup G) (⨆ (i : ι), ⨆ (_ : p i), K i) x
have refine_2 : Membership.mem (γ := Subgroup G) (⨆ (_ : p i), K i) x
Tactic: apply le_iSup (fun i ↦ ⨆ (_ : p i), K i) i
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (hypothesis)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
⊢ x ∈ iSup K ↔ ∃ (i : ι), x ∈ K i
have this : iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down
Tactic: have : iSup K = ⨆ i : PLift ι, ⨆ (_ : True), K i.down := by simp [iSup_plift_down]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down
⊢ x ∈ iSup K ↔ ∃ (i : ι), x ∈ K i
have rw : (∃ (i : PLift ι), True ∧ x ∈ K i.down) ↔ ∃ (i : ι), x ∈ K i
Tactic: rw [this, mem_biSup_of_directedOn trivial]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down
rw : (∃ (i : PLift ι), True ∧ x ∈ K i.down) ↔ ∃ (i : ι), x ∈ K i
⊢ x ∈ iSup K ↔ ∃ (i : ι), x ∈ K i
have hK₁ : DirectedOn.{u_2} (α := PLift ι) ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on fun (i : PLift ι) ↦ K i.down)
  {i : PLift ι | True}
Tactic: rw [this, mem_biSup_of_directedOn trivial]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down
rw : (∃ (i : PLift ι), True ∧ x ∈ K i.down) ↔ ∃ (i : ι), x ∈ K i
hK₁ :
  DirectedOn.{u_2} (α := PLift ι) ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on fun (i : PLift ι) ↦ K i.down)
    {i : PLift ι | True}
⊢ x ∈ iSup K ↔ ∃ (i : ι), x ∈ K i
have rw₁ : PLift ι
Tactic: rw [this, mem_biSup_of_directedOn trivial]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down
⊢ DirectedOn.{u_2} (α := PLift ι) ((fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) on fun (i : PLift ι) ↦ K i.down) univ
have hK₁ : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) fun (i : PLift ι) ↦ K i.down
Tactic: rw [directedOn_onFun_iff, Set.image_univ, directedOn_range]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down
i : PLift ι
⊢ ∀ (y : PLift ι),
    ∃ (z : PLift ι),
      (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) ((fun (i : PLift ι) ↦ K i.down) i) ((fun (i : PLift ι) ↦ K i.down) z) ∧
        (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) ((fun (i : PLift ι) ↦ K i.down) y) ((fun (i : PLift ι) ↦ K i.down) z)
have hK₁ : ∀ (y : PLift ι), ∃ (x : ι), K i.down ≤ K x ∧ K y.down ≤ K x
Tactic: simp only [PLift.exists]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ (i : PLift ι), ⨆ (_ : True), K i.down
i j : PLift ι
⊢ ∃ (x : ι), K i.down ≤ K x ∧ K j.down ≤ K x
have hK₁ : ∀ (a : ι),
  (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) (K i.down) (K a) ∧ (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) (K j.down) (K a) →
    K i.down ≤ K a ∧ K j.down ≤ K a
Tactic: refine (hK i.down j.down).imp ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
p : Prop
K : p → Subgroup G
x : G
⊢ Membership.mem (γ := Subgroup G) (⨆ (h : p), K h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ K h
have pos : ∀ (h : p), Membership.mem (γ := Subgroup G) (⨆ (h : p), K h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ K h
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
p : Prop
K : p → Subgroup G
x : G
pos : ∀ (h : p), Membership.mem (γ := Subgroup G) (⨆ (h : p), K h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ K h
⊢ Membership.mem (γ := Subgroup G) (⨆ (h : p), K h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ K h
have neg : ∀ (h : ¬p), Membership.mem (γ := Subgroup G) (⨆ (h : p), K h) x ↔ x = 1 ∨ ∃ (h : p), x ∈ K h
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (hypothesis)
Goal:
G : Type u_1
inst : Group G
K : Set (Subgroup G)
Kne : K.Nonempty
hK : DirectedOn (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) K
x : G
⊢ x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s
have this : Nonempty.{u_1 + 1} (↑K : Type u_1)
Tactic: haveI : Nonempty K := Kne.to_subtype
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u_1} ↥(⨆ (i : ι), S i)
have refine : ∀ (a : G),
  Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) a →
    ∀ (b : G), Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) b → a * b = b * a
Tactic: refine .of_setLike_mul_comm ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) S
⊢ ∀ (a : G),
    Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) a →
      ∀ (b : G), Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) b → a * b = b * a
have simp_rw : ∀ (a : G) (x : ι) (h : a ∈ S x) (b : G) (x : ι) (h : b ∈ S x), a * b = b * a
Tactic: simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative.{u_1} ↥(S i)
dir : Directed (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) S
a : G
i : ι
ha : a ∈ S i
b : G
j : ι
hb : b ∈ S j
⊢ a * b = b * a
have obtain : ∀ (k : ι) (hik : S i ≤ S k) (hjk : S j ≤ S k), a * b = b * a
Tactic: obtain ⟨k, hik, hjk⟩ := dir i j
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (hypothesis)
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : x ∈ s ⊔ t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have h₁ : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
Tactic: rw [sup_eq_closure] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have refine_1 : ∀ (x : C) (hx : x ∈ (↑s : Set C) ∪ (↑t : Set C)), ∃ y ∈ s, ∃ z ∈ t, y * z = x
Tactic: refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
refine_1 : ∀ (x : C) (hx : x ∈ (↑s : Set C) ∪ (↑t : Set C)), ∃ y ∈ s, ∃ z ∈ t, y * z = x
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have refine_2 : ∃ y ∈ s, ∃ z ∈ t, y * z = 1
Tactic: refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
refine_1 : ∀ (x : C) (hx : x ∈ (↑s : Set C) ∪ (↑t : Set C)), ∃ y ∈ s, ∃ z ∈ t, y * z = x
refine_2 : ∃ y ∈ s, ∃ z ∈ t, y * z = 1
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have refine_3 : ∀ (x y : C) (hx : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x)
  (hy : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) y),
  (∃ 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: refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
C : Type u_2
inst : CommGroup C
s t : Subgroup C
x : C
h : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x
refine_1 : ∀ (x : C) (hx : x ∈ (↑s : Set C) ∪ (↑t : Set C)), ∃ y ∈ s, ∃ z ∈ t, y * z = x
refine_2 : ∃ y ∈ s, ∃ z ∈ t, y * z = 1
refine_3 :
  ∀ (x y : C) (hx : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x)
    (hy : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) y),
    (∃ 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
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have refine_4 : ∀ (x : C) (hx : Membership.mem (γ := Subgroup C) (closure ((↑s : Set C) ∪ (↑t : Set C))) x),
  (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹
Tactic: refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have mp : x ∈ s ⊔ t → ∃ y ∈ s, ∃ z ∈ t, y * z = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
mp : x ∈ s ⊔ t → ∃ y ∈ s, ∃ z ∈ t, y * z = x
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have mpr : (∃ y ∈ s, ∃ z ∈ t, y * z = x) → x ∈ s ⊔ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (hypothesis)
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ s ⊔ t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have hx₁ : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
Tactic: rw [sup_eq_closure] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have mp : ∀ (x : G) (hx : x ∈ (↑s : Set G) ∪ (↑t : Set G)), ∃ y ∈ s, ∃ z ∈ t, y * z = x
Tactic: refine closure_induction ?_ ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
mp : ∀ (x : G) (hx : x ∈ (↑s : Set G) ∪ (↑t : Set G)), ∃ y ∈ s, ∃ z ∈ t, y * z = x
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have mp₁ : ∃ y ∈ s, ∃ z ∈ t, y * z = 1
Tactic: refine closure_induction ?_ ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
mp : ∀ (x : G) (hx : x ∈ (↑s : Set G) ∪ (↑t : Set G)), ∃ y ∈ s, ∃ z ∈ t, y * z = x
mp₁ : ∃ y ∈ s, ∃ z ∈ t, y * z = 1
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have mp₂ : ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x)
  (hy : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) y),
  (∃ 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: refine closure_induction ?_ ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x
mp : ∀ (x : G) (hx : x ∈ (↑s : Set G) ∪ (↑t : Set G)), ∃ y ∈ s, ∃ z ∈ t, y * z = x
mp₁ : ∃ y ∈ s, ∃ z ∈ t, y * z = 1
mp₂ :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x)
    (hy : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) y),
    (∃ 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
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have mp₃ : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure ((↑s : Set G) ∪ (↑t : Set G))) x),
  (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹
Tactic: refine closure_induction ?_ ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (hypothesis)
Goal:
G : Type u_1
inst : Group G
s t : Subgroup G
hs : s.Normal
x : G
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
have h : x ∈ s ⊔ t ↔ ∃ y ∈ t, ∃ z ∈ s, y * z = x
Tactic: have h := (sup_comm t s) ▸ mem_sup_of_normal_right (s := t) (t := s) (x := x)
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
C : Type u_2
inst : CommGroup C
x y z : C
⊢ Membership.mem (γ := Subgroup C) (closure {x, y}) z ↔ ∃ (m : ℤ) (n : ℤ), x ^ m * y ^ n = z
have rw : (∃ (y_1 : C),
    Membership.mem (γ := Subgroup C) (closure {x}) y_1 ∧
      ∃ (z_1 : C), Membership.mem (γ := Subgroup C) (closure {y}) z_1 ∧ y_1 * z_1 = z) ↔
  ∃ (m : ℤ) (n : ℤ), x ^ m * y ^ n = z
Tactic: rw [← Set.singleton_union, Subgroup.closure_union, mem_sup]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
C : Type u_2
inst : CommGroup C
x y z : C
⊢ (∃ (y_1 : C),
      Membership.mem (γ := Subgroup C) (closure {x}) y_1 ∧
        ∃ (z_1 : C), Membership.mem (γ := Subgroup C) (closure {y}) z_1 ∧ y_1 * z_1 = z) ↔
    ∃ (m : ℤ) (n : ℤ), x ^ m * y ^ n = z
have simp_rw : (∃ (y_1 : C), (∃ (n : ℤ), x ^ n = y_1) ∧ ∃ (z_1 : C), (∃ (n : ℤ), y ^ n = z_1) ∧ y_1 * z_1 = z) ↔
  ∃ (m : ℤ) (n : ℤ), x ^ m * y ^ n = z
Tactic: simp_rw [mem_closure_singleton, exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (hypothesis)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy :
  Eq.{u_1 + 1} (α := G) ((fun (g : ↥H₁ × ↥H₂) ↦ (↑g.1 : G) * (↑g.2 : G)) x)
    ((fun (g : ↥H₁ × ↥H₂) ↦ (↑g.1 : G) * (↑g.2 : G)) y)
⊢ x = y
have hxy₁ : (↑y.1 : G)⁻¹ * (↑x.1 : G) * ((↑x.2 : G) * (↑y.2 : G)⁻¹) = 1
Tactic: rw [← inv_mul_eq_iff_eq_mul, ← mul_assoc, ← mul_inv_eq_one, mul_assoc] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (hypothesis)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) * ((↑x.2 : G) * (↑y.2 : G)⁻¹) = 1
⊢ x = y
have hxy₁ : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
Tactic: replace hxy := disjoint_iff_mul_eq_one.mp h (y.1⁻¹ * x.1).prop (x.2 * y.2⁻¹).prop hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
⊢ x = y
have rwa : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1), x = y
Tactic: rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
rwa : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1), x = y
⊢ x = y
have rwa₁ : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
Tactic: rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
rwa : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1), x = y
rwa₁ : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
⊢ x = y
have rwa₂ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
Tactic: rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
rwa : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1), x = y
rwa₁ : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₂ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
⊢ x = y
have rwa₃ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
Tactic: rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
rwa : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1), x = y
rwa₁ : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₂ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₃ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
⊢ x = y
have rwa₄ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
Tactic: rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
Cleared hypotheses: hxy