awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
refine_2 : x * (c * c⁻¹) = x
refine_2₁ : x * 1 = x
⊢ x * c * c⁻¹ = x
have refine_2₂ : x = x
Tactic: rw [mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
⊢ Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}) ⊤
have hs : Surjective (α := ↥N) (β := ↥N)
  (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
    (a : ↥N) → ↥N)
Tactic: have hs : Function.Surjective (((MulAut.conj c).toMonoidHom.restrict N).codRestrict _ h) := by
    rintro ⟨x, hx⟩
    refine ⟨⟨c⁻¹ * x * c, ?_⟩, ?_⟩
    · have h := hn.conj_mem _ hx c⁻¹
      rwa [inv_inv] at h
    simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply,
      MonoidHom.restrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_cancel, one_mul]
    rw [mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
⊢ Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}) ⊤
have rw : map (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) ⊤ ≤
  normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}
Tactic: rw [eq_top_iff, ← MonoidHom.range_eq_top.2 hs, MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
⊢ map (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
      ⊤ ≤
    normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}
have grw : map (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
    (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ≤
  normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}
Tactic: grw [eq_top_iff.1 ht]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
⊢ map (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
      (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ≤
    normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}
have refine : {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg} ⊆
  (↑(comap
        (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
        (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})) :
    Set ↥N)
Tactic: refine map_le_iff_le_comap.2 (normalClosure_le_normal ?_)
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
⊢ {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg} ⊆
    (↑(comap
          (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N
            h)
          (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})) :
      Set ↥N)
have rw : Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg ∈
  comap (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
    (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})
Tactic: rw [Set.singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg ∈
    comap
      (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
      (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})
have simp : Membership.mem (γ := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})
  (Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) sorry)
Tactic: simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply,
    MonoidHom.restrict_apply, mem_comap]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
M : Type u_6
inst : AddGroup M
I : AddSubgroup M
G : Type u_7
inst_1 : Group G
inst_2 : MulAction G M
H : Subgroup G
⊢ Subgroup.map H.subtype (I.inertia ↥H) = I.inertia G ⊓ H
have rw : Subgroup.map H.subtype (Subgroup.subgroupOf (I.inertia G) H) = I.inertia G ⊓ H
Tactic: rw [← AddSubgroup.subgroupOf_inertia, Subgroup.subgroupOf_map_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
M : Type u_6
inst : AddGroup M
I : AddSubgroup M
G : Type u_7
inst_1 : Group G
inst_2 : MulAction G M
H : Subgroup G
rw : Subgroup.map H.subtype (Subgroup.subgroupOf (I.inertia G) H) = I.inertia G ⊓ H
⊢ Subgroup.map H.subtype (I.inertia ↥H) = I.inertia G ⊓ H
have rw₁ : I.inertia G ⊓ H = I.inertia G ⊓ H
Tactic: rw [← AddSubgroup.subgroupOf_inertia, Subgroup.subgroupOf_map_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (hypothesis)
Goal:
S : Type u_3
G : Type u_4
inst : Inv G
inst_1 : SetLike S G
s : S
inst_2 : HasMemOrInvMem s
x : G
h : ¬x ∈ s
⊢ x⁻¹ ∈ s
have this : x ∈ s ∨ x⁻¹ ∈ s
Tactic: have := mem_or_inv_mem s x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (hypothesis)
Goal:
S : Type u_3
G : Type u_4
inst : Inv G
inst_1 : SetLike S G
s : S
inst_2 : HasMemOrInvMem s
x : G
h : ¬x⁻¹ ∈ s
⊢ x ∈ s
have this : x ∈ s ∨ x⁻¹ ∈ s
Tactic: have := mem_or_inv_mem s x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x / y ∈ H
have rw : x * y⁻¹ ∈ H
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ HPow.hPow (β := ℤ) x (↑n : ℤ) ∈ K
have rw : x ^ n ∈ K
Tactic: rw [zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ -[n+1] ∈ K
have rw : (x ^ (n + 1))⁻¹ ∈ K
Tactic: rw [zpow_negSucc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
P : G → Prop
⊢ (∃ (x : G), x ∈ H ∧ P x⁻¹) ↔ ∃ (x : G), x ∈ H ∧ P x
have mp : (∃ (x : G), x ∈ H ∧ P x⁻¹) → ∃ (x : G), x ∈ H ∧ P x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
P : G → Prop
mp : (∃ (x : G), x ∈ H ∧ P x⁻¹) → ∃ (x : G), x ∈ H ∧ P x
⊢ (∃ (x : G), x ∈ H ∧ P x⁻¹) ↔ ∃ (x : G), x ∈ H ∧ P x
have mpr : (∃ (x : G), x ∈ H ∧ P x) → ∃ (x : G), x ∈ H ∧ P x⁻¹
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_4
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : LE S
inst_4 : IsConcreteLE S G
H K L : S
⊢ (↑H : Set G) ⊆ (↑K : Set G) ∪ (↑L : Set G) ↔ H ≤ K ∨ H ≤ L
have refine : ∀ (h : (↑H : Set G) ⊆ (↑K : Set G) ∪ (↑L : Set G)), H ≤ K ∨ H ≤ L
Tactic: refine ⟨fun h ↦ ?_, fun h x xH ↦ h.imp (mem_of_le_of_mem · xH) (mem_of_le_of_mem · xH)⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_4
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : LE S
inst_4 : IsConcreteLE S G
H K L : S
h : (↑H : Set G) ⊆ (↑K : Set G) ∪ (↑L : Set G)
⊢ H ≤ K ∨ H ≤ L
have rw : (∃ (x : G), x ∈ H ∧ ¬x ∈ K) → (↑H : Set G) ⊆ (↑L : Set G)
Tactic: rw [or_iff_not_imp_left, SetLike.not_le_iff_exists, ← SetLike.coe_subset_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : Preorder S
inst_4 : IsConcreteLE S G
x : ↥H
⊢ (inclusion ⋯ : (a : ↥H) → ↥H) x = x
have mk : ∀ (val : G) (property : val ∈ H),
  (inclusion sorry : (a : ↥H) → ↥H) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property) =
    Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H K : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : LE S
inst_4 : IsConcreteLE S G
h : H ≤ K
x : ↥K
hx : (↑x : G) ∈ H
⊢ (inclusion h : (a : ↥H) → ↥K) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (↑x : G) hx) = x
have mk : ∀ (val : G) (property : val ∈ K) (hx : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ K) val property) : G) ∈ H),
  (inclusion h : (a : ↥H) → ↥K)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ K) val property) : G) hx) =
    Subtype.mk (p := fun (x : G) ↦ x ∈ K) val property
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H K : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : Preorder S
inst_4 : IsConcreteLE S G
L : S
hHK : H ≤ K
hKL : K ≤ L
x : ↥H
⊢ Eq (α := ↥L) ((inclusion hKL : (a : ↥K) → ↥L) ((inclusion hHK : (a : ↥H) → ↥K) x) : ↥L)
    ((inclusion ⋯ : (a : ↥H) → ↥L) x : ↥L)
have mk : ∀ (val : G) (property : val ∈ H),
  Eq (α := ↥L)
    ((inclusion hKL : (a : ↥K) → ↥L)
        ((inclusion hHK : (a : ↥H) → ↥K) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property)) :
      ↥L)
    ((inclusion sorry : (a : ↥H) → ↥L) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property) : ↥L)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
p q : Subgroup G
h : Eq.{u_1 + 1} (α := Set G) ((fun (s : Subgroup G) ↦ s.carrier) p) ((fun (s : Subgroup G) ↦ s.carrier) q)
⊢ p = q
have obtain : ∀ (hp : Set G) (mul_mem' : ∀ {a b : G}, a ∈ hp → b ∈ hp → a * b ∈ hp)
  (one_mem' : 1 ∈ { carrier := hp, mul_mem' := @mul_mem' : Subsemigroup G }.carrier)
  (inv_mem' :
    ∀ {x : G},
      x ∈ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid G }.carrier →
        x⁻¹ ∈ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid G }.carrier)
  (h :
    Eq.{u_1 + 1} (α := Set G)
      ((fun (s : Subgroup G) ↦ s.carrier)
        { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' })
      ((fun (s : Subgroup G) ↦ s.carrier) q)),
  { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' : Subgroup G } = q
Tactic: obtain ⟨⟨⟨hp, _⟩, _⟩, _⟩ := p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
q : Subgroup G
hp : Set G
mul_mem' : ∀ {a b : G}, a ∈ hp → b ∈ hp → a * b ∈ hp
one_mem' : 1 ∈ { carrier := hp, mul_mem' := @mul_mem' : Subsemigroup G }.carrier
inv_mem' :
  ∀ {x : G},
    x ∈ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid G }.carrier →
      x⁻¹ ∈ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid G }.carrier
h :
  Eq.{u_1 + 1} (α := Set G)
    ((fun (s : Subgroup G) ↦ s.carrier)
      { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' })
    ((fun (s : Subgroup G) ↦ s.carrier) q)
⊢ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' : Subgroup G } = q
have obtain : ∀ (hq : Set G) (mul_mem'_1 : ∀ {a b : G}, a ∈ hq → b ∈ hq → a * b ∈ hq)
  (one_mem'_1 : 1 ∈ { carrier := hq, mul_mem' := @mul_mem'_1 : Subsemigroup G }.carrier)
  (inv_mem'_1 :
    ∀ {x : G},
      x ∈ { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1 : Submonoid G }.carrier →
        x⁻¹ ∈ { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1 : Submonoid G }.carrier)
  (h :
    Eq.{u_1 + 1} (α := Set G)
      ((fun (s : Subgroup G) ↦ s.carrier)
        { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' })
      ((fun (s : Subgroup G) ↦ s.carrier)
        { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1, inv_mem' := @inv_mem'_1 })),
  { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' : Subgroup G } =
    { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1, inv_mem' := @inv_mem'_1 }
Tactic: obtain ⟨⟨⟨hq, _⟩, _⟩, _⟩ := q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (hypothesis)
Goal:
G : Type u_1
inst : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
⊢ p = q
have this : (↑p.toSubmonoid : Set G) = (↑q.toSubmonoid : Set G)
Tactic: have := SetLike.ext'_iff.1 h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (hypothesis)
Goal:
G : Type u_1
inst : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : (↑p.toSubmonoid : Set G) = (↑q.toSubmonoid : Set G)
⊢ p = q
have this₁ : (↑p : Set G) = (↑q : Set G)
Tactic: rw [coe_toSubmonoid, coe_toSubmonoid] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
⊢ 1 ∈ s
have let : ∀ (x : G) (hx : x ∈ s), 1 ∈ s
Tactic: let ⟨x, hx⟩ := hsn
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
nH : H.Normal
n : G
hn : n ∈ H
g : G
⊢ g⁻¹ * n * g ∈ H
have h : g = g⁻¹⁻¹
Tactic: convert! nH.conj_mem n hn g⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
nH : H.Normal
n : G
hn : n ∈ H
g : G
⊢ g = g⁻¹⁻¹
have h : g = g
Tactic: rw [inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
nH : H.Normal
a b : G
h : a * b ∈ H
⊢ b * a ∈ H
have this : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H
Tactic: have : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H := nH.conj_mem (a * b) h a⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H : Subgroup G
S : Set G
a b : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
hb : ∀ (n : G), n ∈ S ↔ b * n * b⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S
have rw : a * (b * n * b⁻¹) * a⁻¹ ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S
Tactic: rw [hb, ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H : Subgroup G
S : Set G
a : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a⁻¹ * n * a⁻¹⁻¹ ∈ S
have rw : n ∈ S ↔ a * (a⁻¹ * n * a⁻¹⁻¹) * a⁻¹ ∈ S
Tactic: rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
⊢ Membership.mem (γ := Subgroup G) (normalizer S) g ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
have rw : Membership.mem (γ := Subgroup G) (normalizer S) g⁻¹ ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
Tactic: rw [← inv_mem_iff, mem_set_normalizer_iff, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
rw : Membership.mem (γ := Subgroup G) (normalizer S) g⁻¹ ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
⊢ Membership.mem (γ := Subgroup G) (normalizer S) g ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
have rw₁ : (∀ (h : G), h ∈ S ↔ g⁻¹ * h * g⁻¹⁻¹ ∈ S) ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
Tactic: rw [← inv_mem_iff, mem_set_normalizer_iff, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
rw : Membership.mem (γ := Subgroup G) (normalizer S) g⁻¹ ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
rw₁ : (∀ (h : G), h ∈ S ↔ g⁻¹ * h * g⁻¹⁻¹ ∈ S) ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
⊢ Membership.mem (γ := Subgroup G) (normalizer S) g ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
have rw₂ : (∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S) ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
Tactic: rw [← inv_mem_iff, mem_set_normalizer_iff, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : Membership.mem (γ := Subgroup G) (normalizer S) g
n : G
⊢ n * g ∈ S ↔ g * n ∈ S
have rw : g * (n * g) * g⁻¹ ∈ S ↔ g * n ∈ S
Tactic: rw [h, mul_assoc, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : Membership.mem (γ := Subgroup G) (normalizer S) g
n : G
rw : g * (n * g) * g⁻¹ ∈ S ↔ g * n ∈ S
⊢ n * g ∈ S ↔ g * n ∈ S
have rw₁ : g * (n * g * g⁻¹) ∈ S ↔ g * n ∈ S
Tactic: rw [h, mul_assoc, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : Membership.mem (γ := Subgroup G) (normalizer S) g
n : G
rw : g * (n * g) * g⁻¹ ∈ S ↔ g * n ∈ S
rw₁ : g * (n * g * g⁻¹) ∈ S ↔ g * n ∈ S
⊢ n * g ∈ S ↔ g * n ∈ S
have rw₂ : g * n ∈ S ↔ g * n ∈ S
Tactic: rw [h, mul_assoc, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
n : G
⊢ n ∈ S ↔ g * n * g⁻¹ ∈ S
have rw : n ∈ S ↔ g * (n * g⁻¹) ∈ S
Tactic: rw [mul_assoc, ← h, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
n : G
rw : n ∈ S ↔ g * (n * g⁻¹) ∈ S
⊢ n ∈ S ↔ g * n * g⁻¹ ∈ S
have rw₁ : n ∈ S ↔ n * g⁻¹ * g ∈ S
Tactic: rw [mul_assoc, ← h, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
n : G
rw : n ∈ S ↔ g * (n * g⁻¹) ∈ S
rw₁ : n ∈ S ↔ n * g⁻¹ * g ∈ S
⊢ n ∈ S ↔ g * n * g⁻¹ ∈ S
have rw₂ : n ∈ S ↔ n ∈ S
Tactic: rw [mul_assoc, ← h, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ (↑H : Set G) ↔ x * n * x⁻¹ ∈ (↑H : Set G)
have rw : n ∈ H ↔ x * n * x⁻¹ ∈ (↑H : Set G)
Tactic: rw [SetLike.mem_coe, SetLike.mem_coe, H.mul_mem_cancel_right <| H.inv_mem xH,
    H.mul_mem_cancel_left xH]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
rw : n ∈ H ↔ x * n * x⁻¹ ∈ (↑H : Set G)
⊢ n ∈ (↑H : Set G) ↔ x * n * x⁻¹ ∈ (↑H : Set G)
have rw₁ : n ∈ H ↔ x * n * x⁻¹ ∈ H
Tactic: rw [SetLike.mem_coe, SetLike.mem_coe, H.mul_mem_cancel_right <| H.inv_mem xH,
    H.mul_mem_cancel_left xH]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
rw : n ∈ H ↔ x * n * x⁻¹ ∈ (↑H : Set G)
rw₁ : n ∈ H ↔ x * n * x⁻¹ ∈ H
⊢ n ∈ (↑H : Set G) ↔ x * n * x⁻¹ ∈ (↑H : Set G)
have rw₂ : n ∈ H ↔ x * n ∈ H
Tactic: rw [SetLike.mem_coe, SetLike.mem_coe, H.mul_mem_cancel_right <| H.inv_mem xH,
    H.mul_mem_cancel_left xH]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
rw : n ∈ H ↔ x * n * x⁻¹ ∈ (↑H : Set G)
rw₁ : n ∈ H ↔ x * n * x⁻¹ ∈ H
rw₂ : n ∈ H ↔ x * n ∈ H
⊢ n ∈ (↑H : Set G) ↔ x * n * x⁻¹ ∈ (↑H : Set G)
have rw₃ : n ∈ H ↔ n ∈ H
Tactic: rw [SetLike.mem_coe, SetLike.mem_coe, H.mul_mem_cancel_right <| H.inv_mem xH,
    H.mul_mem_cancel_left xH]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : InjOn.{u_4, u_5} (β := H) (⇑f : (a : G) → H) (↑s : Set G)
a : G
ha : a ∈ s
ha' : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H)
⊢ a = 1
have refine : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) 1 : H)
Tactic: refine h ha (one_mem s) ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x : G
hx : x ∈ (↑s : Set G)
y : G
hy : y ∈ (↑s : Set G)
hxy : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
⊢ x = y
have refine_1 : x ∈ s
Tactic: refine mul_inv_eq_one.1 <| h _ (mul_mem ?_ (inv_mem ?_)) ?_