awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a z : α
zh_1 : z ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
zh : (orbitRel G α : α → α → Prop) z a
g : G
yh : (fun (m : G) ↦ m • a) g ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
⊢ ∃ (g_1 : G),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
          ((fun (m : G) ↦ m • a) g) yh =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) z zh_1
have h : ∀ (h : G) (zh : (fun (m : G) ↦ m • a) h ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)),
  ∃ (g_1 : G),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
          ((fun (m : G) ↦ m • a) g) yh =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
        ((fun (m : G) ↦ m • a) h) zh
Tactic: rcases zh with ⟨h, rfl⟩
Cleared hypotheses: z, zh_1, zh
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
g : G
yh : (fun (m : G) ↦ m • a) g ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
h : G
zh : (fun (m : G) ↦ m • a) h ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
⊢ ∃ (g_1 : G),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
          ((fun (m : G) ↦ m • a) g) yh =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
        ((fun (m : G) ↦ m • a) h) zh
have h₁ : (h * g⁻¹) •
    Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
      ((fun (m : G) ↦ m • a) g) yh =
  Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
    ((fun (m : G) ↦ m • a) h) zh
Tactic: refine ⟨h * g⁻¹, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
g : G
yh : (fun (m : G) ↦ m • a) g ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
h : G
zh : (fun (m : G) ↦ m • a) h ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
⊢ (h * g⁻¹) •
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
        ((fun (m : G) ↦ m • a) g) yh =
    Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
      ((fun (m : G) ↦ m • a) h) zh
have h₁ : (↑((h * g⁻¹) •
        Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
          ((fun (m : G) ↦ m • a) g) yh) :
    α) =
  (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
        ((fun (m : G) ↦ m • a) h) zh) :
    α)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Finite G
inst_3 : Finite.{u_2 + 1} Ω
⊢ Finite α
have rw : Finite.{u_2 + 1} ((ω : Ω) × (↑ω.orbit : Type u_2))
Tactic: rw [(selfEquivSigmaOrbits' G _).finite_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Finite G
inst_3 : Finite.{u_2 + 1} Ω
g : Ω
⊢ Finite.{u_2 + 1} (↑g.orbit : Type u_2)
have h : ∀ (a : α), Finite.{u_2 + 1} (↑(orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) : Type u_2)
Tactic: induction g using Quotient.inductionOn'
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Finite G
inst_3 : Finite.{u_2 + 1} Ω
⊢ Finite.{u_2 + 1} ((ω : Ω) × (↑ω.orbit : Type u_2))
have this : ∀ (g : Ω), Finite.{u_2 + 1} (↑g.orbit : Type u_2)
Tactic: have : ∀ g : Ω, Finite g.orbit := by
    intro g
    induction g using Quotient.inductionOn'
    simpa [Set.finite_coe_iff] using Finite.finite_mulAction_orbit _
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
⊢ Eq (α := Subgroup G) (stabilizer G (g • a))
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a))
have h : ∀ (h : G),
  Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
Tactic: ext h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
have h₁ : h • g • a = g • a ↔
  Membership.mem (γ := Subgroup G)
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
Tactic: rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : G
h₁ :
  h • g • a = g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
have h₂ : g⁻¹ • h • g • a = g⁻¹ • g • a ↔
  Membership.mem (γ := Subgroup G)
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
Tactic: rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : G
h₁ :
  h • g • a = g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₂ :
  g⁻¹ • h • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
have h₃ : (g⁻¹ * h) • g • a = g⁻¹ • g • a ↔
  Membership.mem (γ := Subgroup G)
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
Tactic: rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : G
h₁ :
  h • g • a = g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₂ :
  g⁻¹ • h • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₃ :
  (g⁻¹ * h) • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
have h₄ : (g⁻¹ * h * g) • a = g⁻¹ • g • a ↔
  Membership.mem (γ := Subgroup G)
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
Tactic: rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : G
h₁ :
  h • g • a = g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₂ :
  g⁻¹ • h • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₃ :
  (g⁻¹ * h) • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₄ :
  (g⁻¹ * h * g) • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
have h₅ : (g⁻¹ * h * g) • a = (g⁻¹ * g) • a ↔
  Membership.mem (γ := Subgroup G)
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
Tactic: rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : G
h₁ :
  h • g • a = g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₂ :
  g⁻¹ • h • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₃ :
  (g⁻¹ * h) • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₄ :
  (g⁻¹ * h * g) • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₅ :
  (g⁻¹ * h * g) • a = (g⁻¹ * g) • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
have h₆ : (g⁻¹ * h * g) • a = HSMul.hSMul.{u_1, u_2, u_2} (α := G) 1 a ↔
  Membership.mem (γ := Subgroup G)
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
Tactic: rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : G
h₁ :
  h • g • a = g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₂ :
  g⁻¹ • h • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₃ :
  (g⁻¹ * h) • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₄ :
  (g⁻¹ * h * g) • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₅ :
  (g⁻¹ * h * g) • a = (g⁻¹ * g) • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₆ :
  (g⁻¹ * h * g) • a = HSMul.hSMul.{u_1, u_2, u_2} (α := G) 1 a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
have h₇ : (g⁻¹ * h * g) • a = a ↔
  Membership.mem (γ := Subgroup G)
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
Tactic: rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : G
h₁ :
  h • g • a = g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₂ :
  g⁻¹ • h • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₃ :
  (g⁻¹ * h) • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₄ :
  (g⁻¹ * h * g) • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₅ :
  (g⁻¹ * h * g) • a = (g⁻¹ * g) • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₆ :
  (g⁻¹ * h * g) • a = HSMul.hSMul.{u_1, u_2, u_2} (α := G) 1 a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₇ :
  (g⁻¹ * h * g) • a = a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
have h₈ : Membership.mem (γ := Subgroup G) (stabilizer G a) (g⁻¹ * h * g) ↔
  Membership.mem (γ := Subgroup G)
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
Tactic: rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : G
h₁ :
  h • g • a = g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₂ :
  g⁻¹ • h • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₃ :
  (g⁻¹ * h) • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₄ :
  (g⁻¹ * h * g) • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₅ :
  (g⁻¹ * h * g) • a = (g⁻¹ * g) • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₆ :
  (g⁻¹ * h * g) • a = HSMul.hSMul.{u_1, u_2, u_2} (α := G) 1 a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₇ :
  (g⁻¹ * h * g) • a = a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₈ :
  Membership.mem (γ := Subgroup G) (stabilizer G a) (g⁻¹ * h * g) ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
have h₉ : Membership.mem (γ := Subgroup G) (stabilizer G a) (g⁻¹ * h * g) ↔
  Membership.mem (α := G) (γ := Subgroup G) (stabilizer G a)
    ((MulEquiv.symm ((MulAut.conj : (a : G) → MulAut G) g) : (a : G) → G) h : G)
Tactic: rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : G
h₁ :
  h • g • a = g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₂ :
  g⁻¹ • h • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₃ :
  (g⁻¹ * h) • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₄ :
  (g⁻¹ * h * g) • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₅ :
  (g⁻¹ * h * g) • a = (g⁻¹ * g) • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₆ :
  (g⁻¹ * h * g) • a = HSMul.hSMul.{u_1, u_2, u_2} (α := G) 1 a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₇ :
  (g⁻¹ * h * g) • a = a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₈ :
  Membership.mem (γ := Subgroup G) (stabilizer G a) (g⁻¹ * h * g) ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₉ :
  Membership.mem (γ := Subgroup G) (stabilizer G a) (g⁻¹ * h * g) ↔
    Membership.mem (α := G) (γ := Subgroup G) (stabilizer G a)
      ((MulEquiv.symm ((MulAut.conj : (a : G) → MulAut G) g) : (a : G) → G) h : G)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
have h₁₀ : Membership.mem (γ := Subgroup G) (stabilizer G a) (g⁻¹ * h * g) ↔
  Membership.mem (γ := Subgroup G) (stabilizer G a) (g⁻¹ * h * g)
Tactic: rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
g h k : G
a b c : α
hg : b = g • a
⊢ Eq (α := Subgroup G) (Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) (stabilizer G a))
    (stabilizer G b)
have rw : Eq (α := Subgroup G) (Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) (stabilizer G a))
  (stabilizer G (g • a))
Tactic: rw [hg, stabilizer_smul_eq_stabilizer_map_conj g a, ← MulEquiv.toMonoidHom_eq_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
g h k : G
a b c : α
hg : b = g • a
rw :
  Eq (α := Subgroup G) (Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) (stabilizer G a))
    (stabilizer G (g • a))
⊢ Eq (α := Subgroup G) (Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) (stabilizer G a))
    (stabilizer G b)
have rw₁ : Eq (α := Subgroup G) (Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) (stabilizer G a))
  (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a))
Tactic: rw [hg, stabilizer_smul_eq_stabilizer_map_conj g a, ← MulEquiv.toMonoidHom_eq_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
g h k : G
a b c : α
hg : b = g • a
rw :
  Eq (α := Subgroup G) (Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) (stabilizer G a))
    (stabilizer G (g • a))
rw₁ :
  Eq (α := Subgroup G) (Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) (stabilizer G a))
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a))
⊢ Eq (α := Subgroup G) (Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) (stabilizer G a))
    (stabilizer G b)
have rw₂ : Eq (α := Subgroup G) (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a))
  (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a))
Tactic: rw [hg, stabilizer_smul_eq_stabilizer_map_conj g a, ← MulEquiv.toMonoidHom_eq_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
⊢ (stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = stabilizerEquivStabilizer hk
have h₁ : ∀ (x : ↥(stabilizer G a)),
  Eq.{u_1 + 1} (α := G)
    (↑(((stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) :
            (a : ↥(stabilizer G a)) → ↥(stabilizer G c))
          x) :
      G)
    (↑((stabilizerEquivStabilizer hk : (a : ↥(stabilizer G a)) → ↥(stabilizer G c)) x) : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
⊢ Eq (α := ↥(stabilizer G a) ≃* ↥(stabilizer G a)) (stabilizerEquivStabilizer ⋯) (MulEquiv.refl ↥(stabilizer G a))
have h : ∀ (x : ↥(stabilizer G a)),
  Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer sorry : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)
    (↑((MulEquiv.refl ↥(stabilizer G a) : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)
Tactic: ext