awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
h : Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = g
h₁ : g = Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯
h₂ : g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = 1
h₃ : Membership.mem (γ := Subgroup α) ⊥ (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)
h₄ :
  Membership.mem (γ := Subgroup α) (stabilizer α (g⁻¹ • x)) (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)
h₅ : (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯) • g⁻¹ • x = g⁻¹ • x
⊢ (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g = 1
have h₆ : g⁻¹ • Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) sorry • g⁻¹ • x = g⁻¹ • x
Tactic: rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot,
        ← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x), mem_stabilizer_iff, mul_smul,
        (exists_smul_eq α (g⁻¹ • x) x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
h : Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = g
h₁ : g = Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯
h₂ : g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = 1
h₃ : Membership.mem (γ := Subgroup α) ⊥ (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)
h₄ :
  Membership.mem (γ := Subgroup α) (stabilizer α (g⁻¹ • x)) (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)
h₅ : (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯) • g⁻¹ • x = g⁻¹ • x
h₆ : g⁻¹ • Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ • g⁻¹ • x = g⁻¹ • x
⊢ (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g = 1
have h₇ : g⁻¹ • x = g⁻¹ • x
Tactic: rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot,
        ← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x), mem_stabilizer_iff, mul_smul,
        (exists_smul_eq α (g⁻¹ • x) x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card G / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
have rw : Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
  Fintype.card.{u_1} (ConjAct G) / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
Tactic: rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (ConjAct G) / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
have rw : Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
  Fintype.card.{u_1} (↑(MulAction.orbit (ConjAct G) g) : Type u_1)
Tactic: rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
rw :
  Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (↑(MulAction.orbit (ConjAct G) g) : Type u_1)
⊢ Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (ConjAct G) / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
have H : 0 < Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
Tactic: rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card G / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
have rw : Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
  Fintype.card.{u_1} (ConjAct G) / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
Tactic: classical
  rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
  rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
  · simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
  · exact Fintype.card_pos_iff.mpr inferInstance
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
rw rw₁ rw₂ :
  Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (ConjAct G) / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card G / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
have rw₃ : Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
  Fintype.card.{u_1} (↑(MulAction.orbit (ConjAct G) g) : Type u_1)
Tactic: classical
  rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
  rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
  · simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
  · exact Fintype.card_pos_iff.mpr inferInstance
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
rw rw₁ rw₂ :
  Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (ConjAct G) / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
rw₃ :
  Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (↑(MulAction.orbit (ConjAct G) g) : Type u_1)
⊢ Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card G / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
have H : 0 < Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
Tactic: classical
  rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
  rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
  · simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
  · exact Fintype.card_pos_iff.mpr inferInstance
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.normalCore = MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))
have a : H.normalCore ≤ MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : H.normalCore ≤ MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))
⊢ H.normalCore = MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))
have a₁ : MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H)) ≤ H.normalCore
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
⊢ Membership.mem (γ := Subgroup G) (MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))) g
have a : ∀ (x : G ⧸ H),
  Eq (α := G ⧸ H)
    ((((MulAction.toPermHom G (G ⧸ H) : (a : G) → Equiv.Perm (G ⧸ H)) g : Equiv.Perm (G ⧸ H)) : (a : G ⧸ H) → G ⧸ H) x :
      G ⧸ H)
    ((1 : (a : G ⧸ H) → G ⧸ H) x : G ⧸ H)
Tactic: apply Equiv.Perm.ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
⊢ ∀ (x : G ⧸ H),
    Eq (α := G ⧸ H)
      ((((MulAction.toPermHom G (G ⧸ H) : (a : G) → Equiv.Perm (G ⧸ H)) g : Equiv.Perm (G ⧸ H)) : (a : G ⧸ H) → G ⧸ H)
          x :
        G ⧸ H)
      ((1 : (a : G ⧸ H) → G ⧸ H) x : G ⧸ H)
have a : ∀ (q : G ⧸ H) (z : G),
  Eq (α := G ⧸ H)
    ((((MulAction.toPermHom G (G ⧸ H) : (a : G) → Equiv.Perm (G ⧸ H)) g : Equiv.Perm (G ⧸ H)) : (a : G ⧸ H) → G ⧸ H)
        (↑z : G ⧸ H) :
      G ⧸ H)
    ((1 : (a : G ⧸ H) → G ⧸ H) (↑z : G ⧸ H) : G ⧸ H)
Tactic: refine fun q ↦ QuotientGroup.induction_on q ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
⊢ ∀ (z : G),
    Eq (α := G ⧸ H)
      ((((MulAction.toPermHom G (G ⧸ H) : (a : G) → Equiv.Perm (G ⧸ H)) g : Equiv.Perm (G ⧸ H)) : (a : G ⧸ H) → G ⧸ H)
          (↑z : G ⧸ H) :
        G ⧸ H)
      ((1 : (a : G ⧸ H) → G ⧸ H) (↑z : G ⧸ H) : G ⧸ H)
have a : ∀ (g' : G), (g • g')⁻¹ * g' ∈ H
Tactic: refine fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ (g • g')⁻¹ * g' ∈ H
have a : g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H
Tactic: rw [smul_eq_mul, mul_inv_rev, ← inv_inv g', inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H)) ≤ H.normalCore
have a : ∀ (g : G)
  (hg : Membership.mem (γ := Subgroup G) (MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))) g),
  g ∈ H
Tactic: refine (Subgroup.normal_le_normalCore.mpr fun g hg => ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))) g
⊢ g ∈ H
have a : Eq (α := G ⧸ H) (↑(g * 1) : G ⧸ H) (↑1 : G ⧸ H)
Tactic: rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Ring (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : (n • x) • y = n • x • y
⊢ ((n + 1) • x) • y = (n + 1) • x • y
have succ : (n • x + x) • y = n • x • y + x • y
Tactic: simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Ring (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : (n • x) • y = n • x • y
succ : (n • x + x) • y = n • x • y + x • y
⊢ ((n + 1) • x) • y = (n + 1) • x • y
have succ₁ : (n • x + x) • y = (n • x) • y + x • y
Tactic: simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Ring (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : (n • x) • y = n • x • y
succ : (n • x + x) • y = n • x • y + x • y
succ₁ : (n • x + x) • y = (n • x) • y + x • y
⊢ ((n + 1) • x) • y = (n + 1) • x • y
have succ₂ : (n • x + x) * y = n • x * y + x * y
Tactic: simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Ring (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
n : ℕ
x y : R
⊢ (n • x) • y = n • x • y
have zero : HSMul.hSMul (α := ℕ) 0 x • y = HSMul.hSMul (α := ℕ) 0 (x • y)
Tactic: induction n with
    | zero => simp
    | succ n ih => simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Ring (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
n : ℕ
x y : R
zero : HSMul.hSMul (α := ℕ) 0 x • y = HSMul.hSMul (α := ℕ) 0 (x • y)
⊢ (n • x) • y = n • x • y
have succ : ∀ (n : ℕ) (ih : (n • x) • y = n • x • y), ((n + 1) • x) • y = (n + 1) • x • y
Tactic: induction n with
    | zero => simp
    | succ n ih => simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Ring (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
n_1 : ℤ
x y : R
n : ℕ
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) x • y = HSMul.hSMul (α := ℤ) (↑n : ℤ) (x • y)
have simp_rw : (n • x) • y = n • x • y
Tactic: simp_rw [natCast_zsmul, smul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Ring (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
n_1 : ℤ
x y : R
n : ℕ
⊢ (-[n+1] • x) • y = -[n+1] • x • y
have simp_rw : -((n + 1) • x) • y = -((n + 1) • x • y)
Tactic: simp_rw [negSucc_zsmul, smul_eq_mul, neg_mul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Ring (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
n_1 : ℤ
x y : R
n : ℕ
simp_rw : -((n + 1) • x) • y = -((n + 1) • x • y)
⊢ (-[n+1] • x) • y = -[n+1] • x • y
have simp_rw₁ : -((n + 1) • x) * y = -((n + 1) • (x * y))
Tactic: simp_rw [negSucc_zsmul, smul_eq_mul, neg_mul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Ring (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
n_1 : ℤ
x y : R
n : ℕ
simp_rw : -((n + 1) • x) • y = -((n + 1) • x • y)
simp_rw₁ : -((n + 1) • x) * y = -((n + 1) • (x * y))
⊢ (-[n+1] • x) • y = -[n+1] • x • y
have simp_rw₂ : -((n + 1) • x * y) = -((n + 1) • (x * y))
Tactic: simp_rw [negSucc_zsmul, smul_eq_mul, neg_mul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
n : ℕ
s : (↑(powersetCard α n) : Type u_2)
⊢ Eq (α := Subgroup G) (stabilizer G s) (stabilizer G (↑s : Set α))
have h : ∀ (g : G),
  Membership.mem (γ := Subgroup G) (stabilizer G s) g ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1 ↔
    Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
have refine_1 : ∀ (h : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1),
  Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
refine_1 :
  ∀ (h : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1),
    Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1 ↔
    Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
have refine_2 : ∀ (h : Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1),
  Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
⊢ Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
have refine_1 : ∀ (h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1),
  ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
Tactic: contrapose h with h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
have this : ∃ (a : α), g +ᵥ a ≠ a
Tactic: have : ∃ a, (g +ᵥ a : α) ≠ a := by simpa [Equiv.ext_iff] using h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
this : ∃ (a : α), g +ᵥ a ≠ a
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
have refine_1 : ∀ (a : α) (ha : g +ᵥ a ≠ a), ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
Tactic: obtain ⟨a, ha⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
have refine_1 : ∀ (s : (↑(powersetCard α n) : Type u_2)) (has : a ∈ s) (has' : g +ᵥ a ∉ s),
  ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
Tactic: obtain ⟨s, has, has'⟩ := exists_mem_notMem hn hα (Ne.symm ha)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g +ᵥ a ∉ s
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
have refine_1 : ∃ (x : (↑(powersetCard α n) : Type u_2)),
  ¬Eq (α := (↑(powersetCard α n) : Type u_2))
      ((AddAction.toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
        (↑(powersetCard α n) : Type u_2))
      ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
        (↑(powersetCard α n) : Type u_2))
Tactic: rw [Equiv.ext_iff, not_forall]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g +ᵥ a ∉ s
⊢ ∃ (x : (↑(powersetCard α n) : Type u_2)),
    ¬Eq (α := (↑(powersetCard α n) : Type u_2))
        ((AddAction.toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
          (↑(powersetCard α n) : Type u_2))
        ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
          (↑(powersetCard α n) : Type u_2))
have h₁ : ¬Eq (α := (↑(powersetCard α n) : Type u_2))
    ((AddAction.toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
      (↑(powersetCard α n) : Type u_2))
    ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
      (↑(powersetCard α n) : Type u_2))
Tactic: use s
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g +ᵥ a ∉ s
⊢ ¬Eq (α := (↑(powersetCard α n) : Type u_2))
      ((AddAction.toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
        (↑(powersetCard α n) : Type u_2))
      ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
        (↑(powersetCard α n) : Type u_2))
have h₁ : ∀
  (has' :
    Eq (α := (↑(powersetCard α n) : Type u_2))
      ((AddAction.toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
        (↑(powersetCard α n) : Type u_2))
      ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
        (↑(powersetCard α n) : Type u_2))),
  g +ᵥ a ∈ s
Tactic: contrapose has'
Cleared hypotheses: has'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' :
  Eq (α := (↑(powersetCard α n) : Type u_2))
    ((AddAction.toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
      (↑(powersetCard α n) : Type u_2))
    ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
      (↑(powersetCard α n) : Type u_2))
⊢ g +ᵥ a ∈ s
have has'₁ : g +ᵥ s = s
Tactic: simp only [AddAction.toPerm_apply, coe_one, id_eq] at has'
Cleared hypotheses: has'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g +ᵥ s = s
⊢ g +ᵥ a ∈ s
have h₁ : g +ᵥ a ∈ g +ᵥ s
Tactic: rw [← has']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
have refine_2 : ∀ (h : ∀ (x : α), g +ᵥ x = (1 : (a : α) → α) x) (x : (↑(powersetCard α n) : Type u_2)),
  g +ᵥ x = (1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x
Tactic: simp only [Equiv.ext_iff, AddAction.toPerm_apply] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulVAdd G α
⊢ FaithfulVAdd.{u_3, u_2} G (↑(powersetCard α n) : Type u_2)
have rw : ∀ (g : G), (∀ (a : (↑(powersetCard α n) : Type u_2)), g +ᵥ a = a) → g = 0
Tactic: rw [faithfulVAdd_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulVAdd G α
g : G
hg : ∀ (a : (↑(powersetCard α n) : Type u_2)), g +ᵥ a = a
⊢ g = 0
have a : Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) (AddAction.toPerm.{u_3, u_2} (α := G) 0)
Tactic: apply AddAction.toPerm_injective (α := G) (β := α)