awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
rw₁ : s ⊆ a • s ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
rw₂ : s ⊆ a • s ↔ (↑s : Set α) ⊆ (↑(a • s) : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
have rw₃ : s ⊆ a • s ↔ s ⊆ a • s
Tactic: rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_subset_smul_finset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
have rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
Tactic: classical
  rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_subset_smul_finset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
have rw₁ : s ⊆ a • s ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
Tactic: classical
  rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_subset_smul_finset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
rw₁ : s ⊆ a • s ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
have rw₂ : s ⊆ a • s ↔ (↑s : Set α) ⊆ (↑(a • s) : Set α)
Tactic: classical
  rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_subset_smul_finset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
rw₁ : s ⊆ a • s ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
rw₂ : s ⊆ a • s ↔ (↑s : Set α) ⊆ (↑(a • s) : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
have rw₃ : s ⊆ a • s ↔ s ⊆ a • s
Tactic: classical
  rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_subset_smul_finset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
hs : s.Finite
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • s ⊆ s
have lift : ∀ (s : Finset α), Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
have rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
Tactic: rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_smul_finset_subset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
have rw₁ : a • s ⊆ s ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
Tactic: rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_smul_finset_subset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
rw₁ : a • s ⊆ s ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
have rw₂ : a • s ⊆ s ↔ (↑(a • s) : Set α) ⊆ (↑s : Set α)
Tactic: rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_smul_finset_subset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
rw₁ : a • s ⊆ s ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
rw₂ : a • s ⊆ s ↔ (↑(a • s) : Set α) ⊆ (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
have rw₃ : a • s ⊆ s ↔ a • s ⊆ s
Tactic: rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_smul_finset_subset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
have rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
Tactic: classical
  rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_smul_finset_subset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
have rw₁ : a • s ⊆ s ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
Tactic: classical
  rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_smul_finset_subset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
rw₁ : a • s ⊆ s ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
have rw₂ : a • s ⊆ s ↔ (↑(a • s) : Set α) ⊆ (↑s : Set α)
Tactic: classical
  rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_smul_finset_subset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
rw₁ : a • s ⊆ s ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
rw₂ : a • s ⊆ s ↔ (↑(a • s) : Set α) ⊆ (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
have rw₃ : a • s ⊆ s ↔ a • s ⊆ s
Tactic: classical
  rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_smul_finset_subset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
hs : s.Finite
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
have lift : ∀ (s : Finset α),
  Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ ∀ ⦃b : α⦄, b ∈ (↑s : Set α) → a • b ∈ (↑s : Set α)
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
⊢ s * (↑(stabilizer G s) : Set G) = s
have rw : (↑(stabilizer G s) : Set G) * s = s
Tactic: rw [mul_comm, stabilizer_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
rw : (↑(stabilizer G s) : Set G) * s = s
⊢ s * (↑(stabilizer G s) : Set G) = s
have rw₁ : s = s
Tactic: rw [mul_comm, stabilizer_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
⊢ Eq (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)))
    (stabilizer (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (α :=
      Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' s))
    ⊥
have h : ∀ (a : HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)),
  Membership.mem (γ := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)))
      (stabilizer (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (α :=
        Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' s))
      a ↔
    Membership.mem (γ := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) ⊥ a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)
⊢ Membership.mem (γ := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)))
      (stabilizer (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (α :=
        Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' s))
      a ↔
    Membership.mem (γ := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) ⊥ a
have h : ∀ (a : G),
  Membership.mem (γ := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)))
      (stabilizer (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (α :=
        Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' s))
      (↑a : G ⧸ stabilizer G s) ↔
    Membership.mem (γ := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) ⊥
      (↑a : G ⧸ stabilizer G s)
Tactic: induction a using QuotientGroup.induction_on with | _ a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : G
⊢ Membership.mem (γ := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)))
      (stabilizer (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (α :=
        Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' s))
      (↑a : G ⧸ stabilizer G s) ↔
    Membership.mem (γ := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) ⊥
      (↑a : G ⧸ stabilizer G s)
have h : HSMul.hSMul (α := HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (β :=
      Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (↑a : G ⧸ stabilizer G s)
      (QuotientGroup.mk '' s) =
    QuotientGroup.mk '' s ↔
  a • s = s
Tactic: simp only [mem_stabilizer_iff, Subgroup.mem_bot, QuotientGroup.eq_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : G
⊢ HSMul.hSMul (α := HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (β :=
        Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (↑a : G ⧸ stabilizer G s)
        (QuotientGroup.mk '' s) =
      QuotientGroup.mk '' s ↔
    a • s = s
have this : HSMul.hSMul (α := HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (β :=
    Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (↑a : G ⧸ stabilizer G s) (QuotientGroup.mk '' s) =
  QuotientGroup.mk '' (a • s)
Tactic: have : q a • q '' s = q '' (a • s) :=
    (image_smul_distrib (QuotientGroup.mk' <| stabilizer G s) _ _).symm
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : G
this :
  HSMul.hSMul (α := HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (β :=
      Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (↑a : G ⧸ stabilizer G s)
      (QuotientGroup.mk '' s) =
    QuotientGroup.mk '' (a • s)
⊢ HSMul.hSMul (α := HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (β :=
        Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (↑a : G ⧸ stabilizer G s)
        (QuotientGroup.mk '' s) =
      QuotientGroup.mk '' s ↔
    a • s = s
have h : Eq (α := Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' (a • s))
    (QuotientGroup.mk '' s) ↔
  a • s = s
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : G
this :
  HSMul.hSMul (α := HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (β :=
      Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (↑a : G ⧸ stabilizer G s)
      (QuotientGroup.mk '' s) =
    QuotientGroup.mk '' (a • s)
h : a • s = s
⊢ Eq (α := Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' (a • s))
    (QuotientGroup.mk '' s)
have rw : Eq (α := Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' s)
  (QuotientGroup.mk '' s)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : G
this :
  HSMul.hSMul (α := HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (β :=
      Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (↑a : G ⧸ stabilizer G s)
      (QuotientGroup.mk '' s) =
    QuotientGroup.mk '' (a • s)
⊢ Eq (α := Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' (a • s))
      (QuotientGroup.mk '' s) ↔
    a • s = s
have h : ∀
  (h :
    Eq (α := Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' (a • s))
      (QuotientGroup.mk '' s)),
  a • s = s
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : G
this :
  HSMul.hSMul (α := HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (β :=
      Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (↑a : G ⧸ stabilizer G s)
      (QuotientGroup.mk '' s) =
    QuotientGroup.mk '' (a • s)
h :
  Eq (α := Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' (a • s))
    (QuotientGroup.mk '' s)
⊢ a • s = s
have h₁ : ∀ (h : (↑(stabilizer G s) : Set G) * a • s = (↑(stabilizer G s) : Set G) * s), a • s = s
Tactic: rwa [QuotientGroup.image_coe_inj, mul_smul_comm, stabilizer_mul_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : G
this :
  HSMul.hSMul (α := HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (β :=
      Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (↑a : G ⧸ stabilizer G s)
      (QuotientGroup.mk '' s) =
    QuotientGroup.mk '' (a • s)
h :
  Eq (α := Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' (a • s))
    (QuotientGroup.mk '' s)
h₁ : ∀ (h : (↑(stabilizer G s) : Set G) * a • s = (↑(stabilizer G s) : Set G) * s), a • s = s
⊢ a • s = s
have h₂ : ∀ (h : a • ((↑(stabilizer G s) : Set G) * s) = (↑(stabilizer G s) : Set G) * s), a • s = s
Tactic: rwa [QuotientGroup.image_coe_inj, mul_smul_comm, stabilizer_mul_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : G
this :
  HSMul.hSMul (α := HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)) (β :=
      Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (↑a : G ⧸ stabilizer G s)
      (QuotientGroup.mk '' s) =
    QuotientGroup.mk '' (a • s)
h :
  Eq (α := Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' (a • s))
    (QuotientGroup.mk '' s)
h₁ : ∀ (h : (↑(stabilizer G s) : Set G) * a • s = (↑(stabilizer G s) : Set G) * s), a • s = s
h₂ : ∀ (h : a • ((↑(stabilizer G s) : Set G) * s) = (↑(stabilizer G s) : Set G) * s), a • s = s
⊢ a • s = s
have h₃ : ∀ (h : a • s = s), a • s = s
Tactic: rwa [QuotientGroup.image_coe_inj, mul_smul_comm, stabilizer_mul_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p_1 q r_1 : R[X]
r : R
p : A[X]
⊢ (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) r) : A[X]) p).toFinsupp =
    (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) r) : A[X])).toFinsupp
have simp_rw : HMul.hMul (α := AddMonoidAlgebra A ℕ)
    (AddMonoidAlgebra.single 0 ((algebraMap R A : (a : R) → A) r) : AddMonoidAlgebra A ℕ) p.toFinsupp =
  HMul.hMul (β := AddMonoidAlgebra A ℕ) p.toFinsupp
    (AddMonoidAlgebra.single 0 ((algebraMap R A : (a : R) → A) r) : AddMonoidAlgebra A ℕ)
Tactic: simp_rw [toFinsupp_mul, toFinsupp_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p_1 q r_1 : R[X]
r : R
p : A[X]
⊢ (r • p).toFinsupp =
    (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) r) : A[X]) p).toFinsupp
have rw : r • p.toFinsupp =
  HMul.hMul (α := AddMonoidAlgebra A ℕ)
    (AddMonoidAlgebra.single 0 ((algebraMap R A : (a : R) → A) r) : AddMonoidAlgebra A ℕ) p.toFinsupp
Tactic: rw [toFinsupp_smul, toFinsupp_mul, toFinsupp_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p q r : R[X]
inst_5 : Nontrivial A
⊢ Ne.{z + 1} (α := Subalgebra R A[X]) ⊥ ⊤
have rw : ∃ (x : A[X]), ¬(Membership.mem (γ := Subalgebra R A[X]) ⊥ x ↔ Membership.mem (γ := Subalgebra R A[X]) ⊤ x)
Tactic: rw [Ne, SetLike.ext_iff, not_forall]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p q r : R[X]
inst_5 : Nontrivial A
⊢ ∃ (x : A[X]), ¬(Membership.mem (γ := Subalgebra R A[X]) ⊥ x ↔ Membership.mem (γ := Subalgebra R A[X]) ⊤ x)
have refine : ¬(Membership.mem (γ := Subalgebra R A[X]) ⊥ X ↔ Membership.mem (γ := Subalgebra R A[X]) ⊤ X)
Tactic: refine ⟨X, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p q r : R[X]
inst_5 : Nontrivial A
⊢ ¬(Membership.mem (γ := Subalgebra R A[X]) ⊥ X ↔ Membership.mem (γ := Subalgebra R A[X]) ⊤ X)
have simp : ∀ (x : R), ¬Eq.{z + 1} (α := A[X]) ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) x) : A[X]) (X : A[X])
Tactic: simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top,
        algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p q r : R[X]
inst_5 : Nontrivial A
x : R
⊢ ¬Eq.{z + 1} (α := A[X]) ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) x) : A[X]) (X : A[X])
have rw : ∃ (x_1 : ℕ), ¬Eq.{z + 1} (α := A) (coeff ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) x)) x_1) (coeff X x_1)
Tactic: rw [ext_iff, not_forall]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p q r : R[X]
inst_5 : Nontrivial A
x : R
⊢ ∃ (x_1 : ℕ), ¬Eq.{z + 1} (α := A) (coeff ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) x)) x_1) (coeff X x_1)
have refine : ¬Eq.{z + 1} (α := A) (coeff ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) x)) 1) (coeff X 1)
Tactic: refine ⟨1, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ (f : (a : A) → B) (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) ((f : (a : A) → B) a) p
have simp : Eq.{u_5 + 1} (α := B)
  ((f : (a : A) → B) (∑ n ∈ p.support, HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (p.coeff n) : A) (a ^ n)) : B)
  (∑ n ∈ p.support,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) (p.coeff n) : B)
        (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) :
    B)
Tactic: simp only [eval₂_eq_sum, sum_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
| ((f : (a : R[X]) → A) p : A)
have rw : ((f : (a : R[X]) → A)
    (p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
  A)
Tactic: rw [← Polynomial.sum_C_mul_X_pow_eq p]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ eval₂ (algebraMap R A) ((f : (a : R[X]) → A) X) p = (f : (a : R[X]) → A) p
have conv_rhs : eval₂ (algebraMap R A) ((f : (a : R[X]) → A) X) p =
  (f : (a : R[X]) → A)
    (p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: conv_rhs => rw [← Polynomial.sum_C_mul_X_pow_eq p]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ eval₂ (algebraMap R A) ((f : (a : R[X]) → A) X) p =
    (f : (a : R[X]) → A)
      (p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
have simp : Eq.{u_4 + 1} (α := A)
  (∑ n ∈ p.support,
      HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (p.coeff n) : A)
        (HPow.hPow (α := A) ((f : (a : R[X]) → A) X : A) n) :
    A)
  ((f : (a : R[X]) → A)
      (∑ n ∈ p.support, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)) :
    A)
Tactic: simp only [eval₂_eq_sum, sum_def]