awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
t' : G
ht' : t' ∈ (↑T : Set G)
h : t'⁻¹ * f⁻¹ • g ∈ H
⊢ t' = (↑t : G)

Tactic:
exact Subtype.ext_iff.mp (ht2 ⟨t', ht'⟩ h)

Premises used: Subtype.ext_iff, Subtype.mk, Iff.mp
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
S : H.LeftTransversal
g : G
⊢ f • (↑(⋯.toLeftFun (S := (↑S : Set G)) g) : G) = (↑(⋯.toLeftFun (S := (↑(f • S) : Set G)) (f • g)) : G)

Tactic:
Subtype.ext_iff.mp <| @ExistsUnique.unique (↥(f • (S : Set G))) (fun s => (↑s)⁻¹ * f • g ∈ H)
    (isComplement_iff_existsUnique_inv_mul_mem.mp (f • S).2 (f • g))
    ⟨f • (S.2.toLeftFun g : G), Set.smul_mem_smul_set (Subtype.coe_prop _)⟩
      ((f • S).2.toLeftFun (f • g))
    (QuotientAction.inv_mul_mem f (S.2.inv_toLeftFun_mul_mem g))
      ((f • S).2.inv_toLeftFun_mul_mem (f • g))

Premises used: MulAction.QuotientAction.inv_mul_mem, Subtype.ext_iff, Subgroup.IsComplement.inv_toLeftFun_mul_mem, Subgroup.isComplement_iff_existsUnique_inv_mul_mem, Iff.mp, ExistsUnique.unique, HSMul.hSMul, Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
S : H.LeftTransversal
q : G ⧸ H
⊢ HSMul.hSMul (β := G) f
      (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G) =
    (↑((⋯.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) (f • q)) : G)

Tactic:
Quotient.inductionOn' q fun g => smul_toLeftFun f S g

Premises used: Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
S : H.LeftTransversal
q : G ⧸ H
rw :
  Eq.{u_1 + 1} (α := G)
    (↑((⋯.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) q) : G)
    (↑((⋯.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) (f • f⁻¹ • q)) :
      G)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := G)
    (↑((⋯.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) q) : G)
    (↑((⋯.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) q) : G)
⊢ (↑((⋯.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) q) : G) =
    HSMul.hSMul (β := G) f
      (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) (f⁻¹ • q)) : G)

Tactic:
rw [smul_leftQuotientEquiv, smul_inv_smul]

Premises used: Subgroup.smul_leftQuotientEquiv, smul_inv_smul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
⊢ IsCompl H K

Tactic:
⟨disjoint_iff_inf_le.mpr fun g ⟨p, q⟩ =>
        let x : H × K := ⟨⟨g, p⟩, 1⟩
        let y : H × K := ⟨1, g, q⟩
        Subtype.ext_iff.mp
          (Prod.ext_iff.mp (show x = y from h.1 ((mul_one g).trans (one_mul g).symm))).1,
      codisjoint_iff_le_sup.mpr fun g _ => ?_⟩

Premises used: Iff.mpr, Membership.mem, Prod.ext_iff, Prod.mk, codisjoint_iff_le_sup, Bot.bot, Subtype.ext_iff, Subtype.mk, And.left, _private.0.Subgroup.IsComplement'.isCompl.match_1, Iff.mp, IsCompl.mk, mul_one, disjoint_iff_inf_le, OfNat.ofNat, Eq.symm, one_mul, Eq.trans
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
fun : ∀ (g : G), Membership.mem (γ := Subgroup G) ⊤ g → g ∈ H ⊔ K
⊢ IsCompl H K

Tactic:
refine
    ⟨disjoint_iff_inf_le.mpr fun g ⟨p, q⟩ =>
        let x : H × K := ⟨⟨g, p⟩, 1⟩
        let y : H × K := ⟨1, g, q⟩
        Subtype.ext_iff.mp
          (Prod.ext_iff.mp (show x = y from h.1 ((mul_one g).trans (one_mul g).symm))).1,
      codisjoint_iff_le_sup.mpr fun g _ => ?_⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
g : G
h_1 : Membership.mem (γ := Subgroup G) ⊤ g
obtain :
  ∀ (h : (↑(↑H : Set G) : Type u_1)) (k : (↑(↑K : Set G) : Type u_1)),
    Membership.mem (γ := Subgroup G) ⊤
        ((fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) (h, k)) →
      (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) (h, k) ∈ H ⊔ K
⊢ g ∈ H ⊔ K

Tactic:
obtain ⟨⟨h, k⟩, rfl⟩ := h.2 g

Premises used: And.right, rfl
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h_1 : H.IsComplement' K
h : (↑(↑H : Set G) : Type u_1)
k : (↑(↑K : Set G) : Type u_1)
h_2 :
  Membership.mem (γ := Subgroup G) ⊤
    ((fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) (h, k))
⊢ (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) (h, k) ∈ H ⊔ K

Tactic:
Subgroup.mul_mem_sup h.2 k.2

Premises used: Set.Mem, Subgroup.mul_mem_sup, Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h_1 : H.IsComplement' K
h : (↑(↑H : Set G) : Type u_1)
k : (↑(↑K : Set G) : Type u_1)
h_2 :
  Membership.mem (γ := Subgroup G) ⊤
    ((fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) (h, k))
⊢ (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) (h, k) ∈ H ⊔ K

Tactic:
exact Subgroup.mul_mem_sup h.2 k.2

Premises used: Subgroup.mul_mem_sup, Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
⊢ H ⊔ K = ⊤

Tactic:
h.isCompl.sup_eq_top

Premises used: IsCompl.sup_eq_top, Subgroup.IsComplement'.isCompl
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
⊢ Disjoint H K

Tactic:
h.isCompl.disjoint

Premises used: Subgroup.IsComplement'.isCompl, IsCompl.disjoint
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
⊢ K.index = Nat.card.{u_1} ↥H

Tactic:
h.card_left.symm

Premises used: Subgroup.IsComplement.card_left, Eq.symm
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
h : IsComplement S T
⊢ Nat.card.{u_1} (↑S : Type u_1) * Nat.card.{u_1} (↑T : Type u_1) = Nat.card G

Tactic:
(Nat.card_prod _ _).symm.trans (Nat.card_eq_of_bijective _ h)

Premises used: Nat.card_prod, Eq.symm, Nat.card_eq_of_bijective, Eq.trans
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
⊢ Nat.card.{u_1} ↥H * Nat.card.{u_1} ↥K = Nat.card G

Tactic:
IsComplement.card_mul h

Premises used: Subgroup.IsComplement.card_mul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : (↑H : Set G) * (↑K : Set G) = univ
⊢ H.IsComplement' K

Tactic:
⟨mul_injective_of_disjoint h1, fun g => ?_⟩

Premises used: Subgroup.mul_injective_of_disjoint, And.intro, Function.Bijective, Subgroup.IsComplement
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : (↑H : Set G) * (↑K : Set G) = univ
refine :
  ∀ (g : G),
    ∃ (a : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)),
      (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a = g
⊢ H.IsComplement' K

Tactic:
refine ⟨mul_injective_of_disjoint h1, fun g => ?_⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : (↑H : Set G) * (↑K : Set G) = univ
g : G
obtain :
  ∀ (h : G) (hh : h ∈ (↑H : Set G)) (k : G) (hk : k ∈ (↑K : Set G)) (hg : (fun (x1 x2 : G) ↦ x1 * x2) h k = g),
    ∃ (a : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)),
      (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a = g
⊢ ∃ (a : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)),
    (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a = g

Tactic:
obtain ⟨h, hh, k, hk, hg⟩ := Set.eq_univ_iff_forall.mp h2 g

Premises used: Set.eq_univ_iff_forall, Iff.mp
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : (↑H : Set G) * (↑K : Set G) = univ
g h : G
hh : h ∈ (↑H : Set G)
k : G
hk : k ∈ (↑K : Set G)
hg : (fun (x1 x2 : G) ↦ x1 * x2) h k = g
⊢ ∃ (a : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)),
    (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a = g

Tactic:
⟨(⟨h, hh⟩, ⟨k, hk⟩), hg⟩

Premises used: Prod.mk, Subtype.mk, Exists.intro
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : (↑H : Set G) * (↑K : Set G) = univ
g h : G
hh : h ∈ (↑H : Set G)
k : G
hk : k ∈ (↑K : Set G)
hg : (fun (x1 x2 : G) ↦ x1 * x2) h k = g
⊢ ∃ (a : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)),
    (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a = g

Tactic:
exact ⟨(⟨h, hh⟩, ⟨k, hk⟩), hg⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : Finite G
h1 : Nat.card.{u_1} ↥H * Nat.card.{u_1} ↥K = Nat.card G
h2 : Disjoint H K
⊢ H.IsComplement' K

Tactic:
(Nat.bijective_iff_injective_and_card _).mpr
    ⟨mul_injective_of_disjoint h2, (Nat.card_prod H K).trans h1⟩

Premises used: Iff.mpr, Membership.mem, Subtype, Nat.bijective_iff_injective_and_card, Subgroup.mul_injective_of_disjoint, And.intro, Nat.card_prod, Subgroup.IsComplement, Eq.trans
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : Finite G
⊢ H.IsComplement' K ↔ Nat.card.{u_1} ↥H * Nat.card.{u_1} ↥K = Nat.card G ∧ Disjoint H K

Tactic:
⟨fun h => ⟨h.card_mul, h.disjoint⟩, fun h => isComplement'_of_card_mul_and_disjoint h.1 h.2⟩

Premises used: Subgroup.IsComplement'.card_mul, And.right, And.left, Subgroup.isComplement'_of_card_mul_and_disjoint, And.intro, Iff.intro, Subgroup.IsComplement'.disjoint
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : Finite G
h1 : Nat.card.{u_1} ↥H * Nat.card.{u_1} ↥K = Nat.card G
h2 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥K)
⊢ H.IsComplement' K

Tactic:
isComplement'_of_card_mul_and_disjoint h1 (disjoint_iff.mpr (inf_eq_bot_of_coprime h2))

Premises used: Iff.mpr, disjoint_iff, Subgroup.isComplement'_of_card_mul_and_disjoint, Subgroup.inf_eq_bot_of_coprime
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
⊢ H.IsComplement' (MulAction.stabilizer G a)

Tactic:
isComplement_iff_existsUnique.mpr fun g => ?_

Premises used: Iff.mpr, Subgroup.isComplement_iff_existsUnique
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
refine :
  ∀ (g : G),
    ∃! x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
⊢ H.IsComplement' (MulAction.stabilizer G a)

Tactic:
refine isComplement_iff_existsUnique.mpr fun g => ?_

Premises used: Iff.mpr, Subgroup.isComplement_iff_existsUnique
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
g : G
obtain :
  ∀ (h : ↥H) (hh : h • g • a = a),
    ∃! x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
⊢ ∃! x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g

Tactic:
obtain ⟨h, hh⟩ := h2 g
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
g : G
h : ↥H
hh : h • g • a = a
rwa rwa₁ rwa₂ rwa₃ : (↑h : G) • g • a = a
⊢ ((↑h : G) * g) • a = a

Tactic:
rwa [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
g : G
h : ↥H
hh : h • g • a = a
⊢ ((↑h : G) * g) • a = a

Tactic:
have hh' : (↑h * g) • a = a := by rwa [mul_smul]
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
g : G
h : ↥H
hh : h • g • a = a
hh' : ((↑h : G) * g) • a = a
⊢ ∃! x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g

Tactic:
⟨⟨h⁻¹, h * g, hh'⟩, inv_mul_cancel_left ↑h g, ?_⟩

Premises used: HMul.hMul, Prod.mk, Subtype.mk, Inv.inv, ExistsUnique, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
g : G
h : ↥H
hh : h • g • a = a
hh' : ((↑h : G) * g) • a = a
refine :
  ∀ (y : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1)),
    (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1)) ↦
          (↑x.1 : G) * (↑x.2 : G) = g)
        y →
      y = (h⁻¹, Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) ((↑h : G) * g) hh')
⊢ ∃! x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g

Tactic:
refine ⟨⟨h⁻¹, h * g, hh'⟩, inv_mul_cancel_left ↑h g, ?_⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
rwa : h • h' • a = a
rwa₁ : h • (↑h' : G) • a = a
rwa₂ : h • (↑h' : G) • g • a = g • a
rwa₃ : h • ((↑h' : G) * g) • a = g • a
rwa₄ rwa₅ rwa₆ rwa₇ : h • ((↑h' : G) * g) • a = a
⊢ (h * h') • a = a

Tactic:
rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg]

Premises used: Subgroup.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
⊢ h * h' = 1

Tactic:
specialize h1 (h * h') (by rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg])

Premises used: HMul.hMul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
h1 : h * h' = 1
⊢ Eq (α := (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1))
    (h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg)
    (h⁻¹,
      Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
        ((↑h : G) *
          ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
            (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
        hh')

Tactic:
Prod.ext (eq_inv_of_mul_eq_one_right h1) (Subtype.ext ?_)

Premises used: Prod.ext, eq_inv_of_mul_eq_one_right, Subtype.ext
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
h1 : h * h' = 1
refine :
  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
    (↑(h⁻¹,
            Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
              ((↑h : G) *
                ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
              hh').2 :
      G)
⊢ Eq (α := (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1))
    (h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg)
    (h⁻¹,
      Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
        ((↑h : G) *
          ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
            (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
        hh')

Tactic:
refine Prod.ext (eq_inv_of_mul_eq_one_right h1) (Subtype.ext ?_)

Premises used: Prod.ext, Subtype.ext
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c_1 c d : Con M
h : c = d
⊢ ∀ (a₁ a₂ : M),
    (c.toSetoid : M → M → Prop) a₁ a₂ ↔
      (d.toSetoid : M → M → Prop) ((Equiv.refl M : (a : M) → M) a₁ : M) ((Equiv.refl M : (a : M) → M) a₂ : M)

Tactic:
apply Con.ext_iff.mp h

Premises used: Iff.mp, Con.ext_iff
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c_1 c d : Con M
h : c = d
x y : c.Quotient
mk :
  ∀ (a : M),
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a * y) =
      (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
        (Quotient.congr (Equiv.refl M) ⋯).toFun y
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (x * y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun x * (Quotient.congr (Equiv.refl M) ⋯).toFun y

Tactic:
rcases x with ⟨⟩
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c_1 c d : Con M
h : c = d
x y : c.Quotient
a : M
mk :
  ∀ (a_1 : M),
    (Quotient.congr (Equiv.refl M) ⋯).toFun
        (HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) a)
          (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)) =
      (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
        (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a * y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
      (Quotient.congr (Equiv.refl M) ⋯).toFun y

Tactic:
rcases y with ⟨⟩
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c_1 c d : Con M
h : c = d
x y : c.Quotient
a a_1 : M
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun
      (HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) a)
        (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
      (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
inst : Mul M
c d : Con M
h : c = d
a : M
⊢ Eq (α := d.Quotient) ((Con.congr h : (a : c.Quotient) → d.Quotient) (↑a : c.Quotient) : d.Quotient)
    ((↑a : d.Quotient) : d.Quotient)

Tactic:
rfl

Premises used: Quot.map, Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
rel : N → N → Prop
x y : M
h : (conGen fun (x y : M) ↦ rel (f x) (f y) : (a : M) → M → Prop) x y
⊢ (conGen rel : (a : N) → N → Prop) (f x) (f y)

Tactic:
.rec (fun x y h ↦ .of (f x) (f y) h) (fun x ↦ .refl (f x))
    (fun _ h ↦ .symm h) (fun _ _ h1 h2 ↦ h1.trans h2) (fun {w x y z} _ _ h1 h2 ↦
    (congrArg (fun a ↦ conGen rel a (f (x * z))) (H w y)).mpr
    (((congrArg (fun a ↦ conGen rel (f w * f y) a) (H x z))).mpr
    (.mul h1 h2))) h

Premises used: ConGen.Rel.rec
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
rel : N → N → Prop
x y : M
h : (conGen fun (x y : M) ↦ rel (f x) (f y) : (a : M) → M → Prop) x y
⊢ (conGen rel : (a : N) → N → Prop) (f x) (f y)

Tactic:
exact .rec (fun x y h ↦ .of (f x) (f y) h) (fun x ↦ .refl (f x))
    (fun _ h ↦ .symm h) (fun _ _ h1 h2 ↦ h1.trans h2) (fun {w x y z} _ _ h1 h2 ↦
    (congrArg (fun a ↦ conGen rel a (f (x * z))) (H w y)).mpr
    (((congrArg (fun a ↦ conGen rel (f w * f y) a) (H x z))).mpr
    (.mul h1 h2))) h
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
rel : N → N → Prop
apply :
  LE.le (α := Con M) (comap (⇑f : (a : M) → N) ⋯ (conGen rel))
    (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y))
⊢ Eq (α := Con M) (comap (⇑f : (a : M) → N) ⋯ (conGen rel))
    (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y))

Tactic:
apply le_antisymm _ (le_comap_conGen f (map_mul f) rel)

Premises used: map_mul, le_antisymm, Con.le_comap_conGen, DFunLike.coe