awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
calc :
  card.{u_3} (Quotient (MulAction.orbitRel (ConjAct G) G)) * card.{u_3} (ConjAct G) =
    card.{u_3} (ConjClasses G) * card G
⊢ card.{u_3} { p : G × G // Commute p.1 p.2 } = card.{u_3} (ConjClasses G) * card G

Tactic:
calc card { p : G × G // Commute p.1 p.2 }
      _ = card ((a : G) × { b // Commute a b }) :=
            card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute)
      _ = ∑ i, card { b // Commute i b } := card_sigma
      _ = ∑ x, card (MulAction.fixedBy G x) :=
            sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
              (fun g ↦ card (MulAction.fixedBy G g))
              fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.eq
      _ = card (Quotient (MulAction.orbitRel (ConjAct G) G)) * card (ConjAct G) :=
             MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group _ _
      _ = card (ConjClasses G) * card G := by
             congr 1; apply card_congr'; congr; ext
             exact (Setoid.comm' _).trans isConj_iff.symm

Premises used: Fintype.card_congr, MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group, Equiv.subtypeProdEquivSigmaSubtype, MulAction.fixedBy, Commute, ConjClasses, ConjAct.toConjAct, Fintype.card_sigma, Set.Elem, Fintype.card, Subtype, MulEquiv.toEquiv, MulAction.orbitRel, Prod.fst, congr_arg, funext, Quotient, Fintype.sum_equiv, Prod.snd, ConjAct, mul_inv_eq_iff_eq_mul, Iff.eq, Fintype.card_congr', Iff.symm, Sigma
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
inl : ∀ (val : Fintype G), Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
inr : Infinite G → Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
inl₁ :
  ∀ (val : Fintype G), Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
inr₁ inr₂ : Infinite G → Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
inl₂ inl₃ :
  ∀ (val : Fintype G), Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
inl₄ : ∀ (val : Fintype G), card.{u_3} { p : G × G // Commute p.1 p.2 } = card.{u_3} (ConjClasses G) * card G
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G

Tactic:
classical
  rcases fintypeOrInfinite G; swap
  · rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
  simp only [Nat.card_eq_fintype_card]
  calc card { p : G × G // Commute p.1 p.2 }
      _ = card ((a : G) × { b // Commute a b }) :=
            card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute)
      _ = ∑ i, card { b // Commute i b } := card_sigma
      _ = ∑ x, card (MulAction.fixedBy G x) :=
            sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
              (fun g ↦ card (MulAction.fixedBy G g))
              fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.eq
      _ = card (Quotient (MulAction.orbitRel (ConjAct G) G)) * card (ConjAct G) :=
             MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group _ _
      _ = card (ConjClasses G) * card G := by
             congr 1; apply card_congr'; congr; ext
             exact (Setoid.comm' _).trans isConj_iff.symm

Premises used: Nat.card_eq_zero_of_infinite, MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group, MulZeroClass.zero_mul, Fintype.card_sigma, mul_comm, fintypeOrInfinite, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Fintype G
⊢ Fintype.card.{u_3} (ConjAct G) = Fintype.card G

Tactic:
rfl

Premises used: ConjAct, rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
p : ConjAct G → Prop
⊢ (∀ (x : ConjAct G), p x) ↔ ∀ (x : G), p ((toConjAct : (a : G) → ConjAct G) x)

Tactic:
id Iff.rfl

Premises used: Iff.rfl, id
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
⊢ Eq.{u_3 + 1} (α := G ≃* ConjAct G) (MulEquiv.symm ofConjAct) toConjAct

Tactic:
rfl

Premises used: ConjAct.toConjAct, rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
⊢ Eq.{u_3 + 1} (α := ConjAct G ≃* G) (MulEquiv.symm toConjAct) ofConjAct

Tactic:
rfl

Premises used: ConjAct.ofConjAct, Equiv.symm, rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
x : ConjAct G
⊢ (toConjAct : (a : G) → ConjAct G) ((ofConjAct : (a : ConjAct G) → G) x : G) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
x : G
⊢ (ofConjAct : (a : ConjAct G) → G) ((toConjAct : (a : G) → ConjAct G) x : ConjAct G) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
⊢ Eq.{u_3 + 1} (α := G) ((ofConjAct : (a : ConjAct G) → G) 1 : G) (1 : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
⊢ Eq.{u_3 + 1} (α := ConjAct G) ((toConjAct : (a : G) → ConjAct G) 1 : ConjAct G) (1 : ConjAct G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
x : ConjAct G
⊢ Eq (α := G) ((ofConjAct : (a : ConjAct G) → G) x⁻¹ : G) (((ofConjAct : (a : ConjAct G) → G) x)⁻¹ : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
x : G
⊢ Eq (α := ConjAct G) ((toConjAct : (a : G) → ConjAct G) x⁻¹ : ConjAct G)
    (((toConjAct : (a : G) → ConjAct G) x)⁻¹ : ConjAct G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
x y : ConjAct G
⊢ (ofConjAct : (a : ConjAct G) → G) (x * y) =
    HMul.hMul (α := G) (β := G) ((ofConjAct : (a : ConjAct G) → G) x : G) ((ofConjAct : (a : ConjAct G) → G) y : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
x y : G
⊢ (toConjAct : (a : G) → ConjAct G) (x * y) =
    HMul.hMul (α := ConjAct G) (β := ConjAct G) ((toConjAct : (a : G) → ConjAct G) x : ConjAct G)
      ((toConjAct : (a : G) → ConjAct G) y : ConjAct G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
g : ConjAct G
h : G
⊢ g • h =
    HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) g : G) h)
      (((ofConjAct : (a : ConjAct G) → G) g)⁻¹ : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : DivInvMonoid G
g h : G
⊢ HSMul.hSMul (α := ConjAct G) ((toConjAct : (a : G) → ConjAct G) g : ConjAct G) h = g * h * g⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
M : Type u_2
inst : Monoid M
g : ConjAct Mˣ
h : M
⊢ g • h = (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) g) : M) * h * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) g)⁻¹ : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
⊢ ∀ (x y : ConjAct Mˣ) (b : M), (x * y) • b = x • y • b

Tactic:
simp [units_smul_def, mul_assoc]

Premises used: mul_assoc, ConjAct.units_smul_def
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
⊢ ∀ (b : M), HSMul.hSMul (α := ConjAct Mˣ) 1 b = b

Tactic:
simp [units_smul_def]

Premises used: ConjAct.units_smul_def
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
⊢ ∀ (r : ConjAct Mˣ), HSMul.hSMul (β := M) r 1 = 1

Tactic:
simp [units_smul_def]

Premises used: ConjAct.units_smul_def
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
⊢ ∀ (r : ConjAct Mˣ) (x y : M), r • (x * y) = r • x * r • y

Tactic:
simp [units_smul_def, mul_assoc]

Premises used: mul_assoc, ConjAct.units_smul_def
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
inst_1 : SMul α M
inst_2 : SMulCommClass α M M
inst_3 : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
rw :
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
    um • a • m
rw₁ :
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
    (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * a • m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)
rw₂ :
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
    a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m) * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)
rw₃ rw₄ :
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
    a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M))
⊢ a • um • m = um • a • m

Tactic:
rw [units_smul_def, units_smul_def, mul_smul_comm, smul_mul_assoc]

Premises used: ConjAct.units_smul_def, smul_mul_assoc, mul_smul_comm
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
inst_1 : SMul α M
inst_2 : SMulCommClass M α M
inst_3 : IsScalarTower α M M
⊢ SMulCommClass (ConjAct Mˣ) α M

Tactic:
haveI : SMulCommClass α M M := SMulCommClass.symm _ _ _
  SMulCommClass.symm _ _ _

Premises used: Units, SMulCommClass.symm, ConjAct
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_4
inst : Group G
H : Subgroup G
g h : ↥H
⊢ (↑(HSMul.hSMul (α := ConjAct ↥H) ((toConjAct : (a : ↥H) → ConjAct ↥H) g : ConjAct ↥H) h) : G) =
    HSMul.hSMul (α := ConjAct G) ((toConjAct : (a : G) → ConjAct G) (↑g : G) : ConjAct G) (↑h : G)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g h : G
rw : g⁻¹ * h * g⁻¹⁻¹ = g⁻¹ * h * g
rw₁ rw₂ : g⁻¹ * h * g = g⁻¹ * h * g
⊢ HSMul.hSMul (α := ConjAct G) ((toConjAct : (a : G) → ConjAct G) g⁻¹ : ConjAct G) h = g⁻¹ * h * g

Tactic:
rw [toConjAct_smul, inv_inv]

Premises used: ConjAct.toConjAct_smul, inv_inv
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
⊢ ∀ (x y : ConjAct G) (b : G), (x * y) • b = x • y • b

Tactic:
simp [smul_def, mul_assoc]

Premises used: ConjAct.smul_def, mul_assoc
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
⊢ ∀ (b : G), HSMul.hSMul (α := ConjAct G) 1 b = b

Tactic:
simp [smul_def]

Premises used: ConjAct.smul_def
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
⊢ ∀ (r : ConjAct G), HSMul.hSMul (β := G) r 1 = 1

Tactic:
simp [smul_def]

Premises used: ConjAct.smul_def
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
⊢ ∀ (r : ConjAct G) (x y : G), r • (x * y) = r • x * r • y

Tactic:
simp [smul_def]

Premises used: ConjAct.smul_def
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
inst_1 : SMul α G
inst_2 : SMulCommClass α G G
inst_3 : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
rw :
  a •
      HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
        (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
    ug • a • g
rw₁ :
  a •
      HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
        (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
    HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) (a • g))
      (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G)
rw₂ :
  a •
      HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
        (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
    HMul.hMul (β := G) (a • HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
      (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G)
rw₃ rw₄ :
  a •
      HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
        (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
    a •
      HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
        (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G)
⊢ a • ug • g = ug • a • g

Tactic:
rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]

Premises used: ConjAct.smul_def, smul_mul_assoc, mul_smul_comm
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
inst_1 : SMul α G
inst_2 : SMulCommClass G α G
inst_3 : IsScalarTower α G G
⊢ SMulCommClass (ConjAct G) α G

Tactic:
haveI := SMulCommClass.symm G α G
  SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm, ConjAct
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g : ConjAct G
h : G
⊢ g • h = (((MulAut.conj : (a : G) → MulAut G) ((ofConjAct : (a : ConjAct G) → G) g) : MulAut G) : (a : G) → G) h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g h : G
⊢ HSMul.hSMul (α := ConjAct G) ((toConjAct : (a : G) → ConjAct G) g : ConjAct G) h =
    (((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
h : ∀ (x : G), x ∈ fixedPoints (ConjAct G) G ↔ x ∈ (↑(center G) : Set G)
⊢ fixedPoints (ConjAct G) G = (↑(center G) : Set G)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
x : G
⊢ x ∈ fixedPoints (ConjAct G) G ↔ x ∈ (↑(center G) : Set G)

Tactic:
simp [mem_center_iff, smul_def, mul_inv_eq_iff_eq_mul]

Premises used: ConjAct.smul_def, Subgroup.mem_center_iff, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g h : G
rw : (∃ (x : ConjAct G), x • h = g) ↔ ∃ (c : G), c * h * c⁻¹ = g
⊢ g ∈ orbit (ConjAct G) h ↔ IsConj g h

Tactic:
rw [isConj_comm, isConj_iff, mem_orbit_iff]

Premises used: isConj_iff, MulAction.mem_orbit_iff, isConj_comm
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g h : G
⊢ (∃ (x : ConjAct G), x • h = g) ↔ ∃ (c : G), c * h * c⁻¹ = g

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g h : G
rw : (g ∈ orbit (ConjAct G) h) = IsConj g h
rw₁ rw₂ : IsConj g h = IsConj g h
⊢ (orbitRel (ConjAct G) G : G → G → Prop) g h = IsConj g h

Tactic:
rw [orbitRel_apply, mem_orbit_conjAct]

Premises used: MulAction.orbitRel_apply, ConjAct.mem_orbit_conjAct
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g : G
h : ∀ (h : G), h ∈ orbit (ConjAct G) g ↔ h ∈ ConjClasses.carrier (ConjClasses.mk g)
⊢ orbit (ConjAct G) g = ConjClasses.carrier (ConjClasses.mk g)

Tactic:
ext h
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g h : G
h₁ : h ∈ orbit (ConjAct G) g ↔ Eq (α := ConjClasses G) (ConjClasses.mk h) (ConjClasses.mk g)
h₂ : h ∈ orbit (ConjAct G) g ↔ IsConj h g
h₃ h₄ : IsConj h g ↔ IsConj h g
⊢ h ∈ orbit (ConjAct G) g ↔ h ∈ ConjClasses.carrier (ConjClasses.mk g)

Tactic:
rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]

Premises used: ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, ConjAct.mem_orbit_conjAct
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g : G
⊢ Eq (α := Subgroup (ConjAct G)) (stabilizer (ConjAct G) g)
    (centralizer (singleton (α := ConjAct G) ((toConjAct : (a : G) → ConjAct G) g : ConjAct G)))

Tactic:
le_antisymm (fun _ hg _ h ↦ h ▸ eq_mul_inv_iff_mul_eq.mp hg.symm) fun _ h =>
    mul_inv_eq_of_eq_mul (h g rfl).symm

Premises used: le_antisymm, mul_inv_eq_of_eq_mul, Eq.symm, rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g : G
h :
  ∀ (k : G),
    Membership.mem (γ := Subgroup G) (centralizer {g}) k ↔
      Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k
⊢ Eq (α := Subgroup G) (centralizer {g}) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g))

Tactic:
ext k
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g k : G
h :
  g * k = k * g ↔ Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k
⊢ Membership.mem (γ := Subgroup G) (centralizer {g}) k ↔
    Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k

Tactic:
simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]

Premises used: Subgroup.mem_centralizer_iff, forall_eq, Set.mem_singleton_iff
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g k : G
h :
  k * g = g * k ↔ Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k
⊢ g * k = k * g ↔ Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g k : G
⊢ k * g = g * k ↔ Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k

Tactic:
Iff.symm mul_inv_eq_iff_eq_mul

Premises used: mul_inv_eq_iff_eq_mul, Iff.symm
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
g k : G
⊢ k * g = g * k ↔ Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k

Tactic:
exact Iff.symm mul_inv_eq_iff_eq_mul

Premises used: mul_inv_eq_iff_eq_mul, Iff.symm
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : ConjAct G
h : ↥H
⊢ (↑(g • h) : G) = g • (↑h : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
h : ↥H
⊢ (↑((((MulAut.conjNormal : (a : G) → MulAut ↥H) g : MulAut ↥H) : (a : ↥H) → ↥H) h) : G) = g * (↑h : G) * g⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
h : ↥H
change :
  HMul.hMul (β := G)
      (HMul.hMul (α := G)
        ((ofConjAct : (a : ConjAct G) → G) (((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g)⁻¹ : ConjAct G) :
          G)
        (↑h : G))
      (((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g)⁻¹⁻¹ : G) =
    g⁻¹ * (↑h : G) * g
⊢ (↑((MulEquiv.symm ((MulAut.conjNormal : (a : G) → MulAut ↥H) g) : (a : ↥H) → ↥H) h) : G) = g⁻¹ * (↑h : G) * g

Tactic:
change _ * _⁻¹⁻¹ = _
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
h : ↥H
rw :
  HMul.hMul (β := G)
      (HMul.hMul (α := G)
        ((ofConjAct : (a : ConjAct G) → G) (((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g)⁻¹ : ConjAct G) :
          G)
        (↑h : G))
      ((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g : ConjAct G) =
    g⁻¹ * (↑h : G) * g
⊢ HMul.hMul (β := G)
      (HMul.hMul (α := G)
        ((ofConjAct : (a : ConjAct G) → G) (((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g)⁻¹ : ConjAct G) :
          G)
        (↑h : G))
      (((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g)⁻¹⁻¹ : G) =
    g⁻¹ * (↑h : G) * g

Tactic:
rw [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
h : ↥H
⊢ HMul.hMul (β := G)
      (HMul.hMul (α := G)
        ((ofConjAct : (a : ConjAct G) → G) (((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g)⁻¹ : ConjAct G) :
          G)
        (↑h : G))
      ((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g : ConjAct G) =
    g⁻¹ * (↑h : G) * g

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
h : ↥H
⊢ (↑(((((MulAut.conjNormal : (a : G) → MulAut ↥H) g)⁻¹ : MulAut ↥H) : (a : ↥H) → ↥H) h) : G) = g⁻¹ * (↑h : G) * g

Tactic:
MulAut.conjNormal_symm_apply g h

Premises used: MulAut.conjNormal_symm_apply
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
inst_1 : H.Normal
h : ↥H
⊢ Eq (α := MulAut ↥H) ((MulAut.conjNormal : (a : G) → MulAut ↥H) (↑h : G) : MulAut ↥H)
    ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H)

Tactic:
MulEquiv.ext fun _ => rfl

Premises used: MulEquiv.ext, rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
H : Subgroup G
hH : H.Normal
K : Subgroup ↥H
h : K.Characteristic
a : G
ha : a ∈ map H.subtype K
b : G
obtain :
  ∀ (a : ↥H) (ha : a ∈ (↑K : Set ↥H)), HMul.hMul (β := G) b ((H.subtype : (a : ↥H) → G) a : G) * b⁻¹ ∈ map H.subtype K
⊢ b * a * b⁻¹ ∈ map H.subtype K

Tactic:
obtain ⟨a, ha, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
H : Subgroup G
hH : H.Normal
K : Subgroup ↥H
h : K.Characteristic
b : G
a : ↥H
ha : a ∈ (↑K : Set ↥H)
⊢ HMul.hMul (β := G) b ((H.subtype : (a : ↥H) → G) a : G) * b⁻¹ ∈ map H.subtype K

Tactic:
K.apply_coe_mem_map H.subtype
      ⟨_, (SetLike.ext_iff.mp (h.fixed (MulAut.conjNormal b)) a).mpr ha⟩

Premises used: Iff.mpr, Subgroup.Characteristic.fixed, MulAut.conjNormal, Subgroup.apply_coe_mem_map, Set.Mem, Subgroup.subtype, SetLike.ext_iff, Subtype.mk, Iff.mp, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
H : Subgroup G
hH : H.Normal
K : Subgroup ↥H
h : K.Characteristic
b : G
a : ↥H
ha : a ∈ (↑K : Set ↥H)
⊢ HMul.hMul (β := G) b ((H.subtype : (a : ↥H) → G) a : G) * b⁻¹ ∈ map H.subtype K

Tactic:
exact K.apply_coe_mem_map H.subtype
      ⟨_, (SetLike.ext_iff.mp (h.fixed (MulAut.conjNormal b)) a).mpr ha⟩

Premises used: Iff.mpr, Subgroup.Characteristic.fixed, MulAut.conjNormal, Subgroup.apply_coe_mem_map, Subgroup.subtype, SetLike.ext_iff, Subtype.mk, Iff.mp, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
⊢ (↑u : ConjAct Mˣ) • x = x

Tactic:
have : (u : ConjAct Mˣ) • x = x := u.2