awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
rw : a • s = s ↔ s ⊆ a • s
rw₁ : a • s = s ↔ s = a • s
rw₂ rw₃ : s = a • s ↔ s = a • s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ s ⊆ a • s

Tactic:
rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).le, eq_comm]

Premises used: Eq.le, eq_comm, Finset.subset_iff_eq_of_card_le, MulAction.mem_stabilizer_iff, Finset.card_smul_finset
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
rw : a • s = s ↔ a • s ⊆ s
rw₁ rw₂ : a • s = s ↔ a • s = s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • s ⊆ s

Tactic:
rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).ge]

Premises used: Eq.ge, Finset.subset_iff_eq_of_card_le, MulAction.mem_stabilizer_iff, Finset.card_smul_finset
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
rw : s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s

Tactic:
rw [← Subgroup.inv_mem_iff, mem_stabilizer_finset_iff_subset_smul_finset]

Premises used: Subgroup.inv_mem_iff, MulAction.mem_stabilizer_finset_iff_subset_smul_finset
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
simp_rw : s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → b ∈ a⁻¹ • s
⊢ s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s

Tactic:
simp_rw [← Finset.mem_inv_smul_finset_iff, Finset.subset_iff]

Premises used: Finset.mem_inv_smul_finset_iff, Finset.subset_iff
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
hs : s.Finite
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
hs : s.Finite
lift :
  ∀ (s : Finset α), Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ s ⊆ a • s

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
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 α)
rw₃ rw₄ : s ⊆ a • s ↔ s ⊆ a • s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)

Tactic:
rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_subset_smul_finset, ← Finset.coe_smul_finset,
    Finset.coe_subset]

Premises used: Finset.coe_smul_finset, MulAction.stabilizer_coe_finset, MulAction.mem_stabilizer_finset_iff_subset_smul_finset, Finset.coe_subset
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
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 α)
rw₃ rw₄ : s ⊆ a • s ↔ s ⊆ a • s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) 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]

Premises used: Finset.coe_smul_finset, MulAction.stabilizer_coe_finset, MulAction.mem_stabilizer_finset_iff_subset_smul_finset, Finset.coe_subset
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
hs : s.Finite
lift :
  ∀ (s : Finset α), Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ a • (↑s : Set α) ⊆ (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • s ⊆ s

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
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 α)
rw₃ rw₄ : a • s ⊆ s ↔ a • s ⊆ s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) 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]

Premises used: Finset.coe_smul_finset, MulAction.mem_stabilizer_finset_iff_smul_finset_subset, MulAction.stabilizer_coe_finset, Finset.coe_subset
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
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 α)
rw₃ rw₄ : a • s ⊆ s ↔ a • s ⊆ s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) 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]

Premises used: Finset.coe_smul_finset, MulAction.mem_stabilizer_finset_iff_smul_finset_subset, MulAction.stabilizer_coe_finset, Finset.coe_subset
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
hs : s.Finite
lift :
  ∀ (s : Finset α),
    Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ ∀ ⦃b : α⦄, b ∈ (↑s : Set α) → a • b ∈ (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
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 ↔ ∀ ⦃b : α⦄, b ∈ (↑s : Set α) → a • b ∈ (↑s : Set α)

Tactic:
simp [-mem_stabilizer_iff, mem_stabilizer_finset']

Premises used: MulAction.mem_stabilizer_iff, MulAction.mem_stabilizer_finset'
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
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 ↔ ∀ ⦃b : α⦄, b ∈ (↑s : Set α) → a • b ∈ (↑s : Set α)

Tactic:
classical simp [-mem_stabilizer_iff, mem_stabilizer_finset']

Premises used: MulAction.mem_stabilizer_iff, MulAction.mem_stabilizer_finset'
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
rw : (↑(stabilizer G s) : Set G) * s = s
rw₁ rw₂ : s = s
⊢ s * (↑(stabilizer G s) : Set G) = s

Tactic:
rw [mul_comm, stabilizer_mul_self]

Premises used: MulAction.stabilizer_mul_self, mul_comm
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
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
⊢ 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))
    ⊥

Tactic:
ext a
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s)
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)
⊢ 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:
induction a using QuotientGroup.induction_on with | _ a
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : G
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
⊢ 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:
simp only [mem_stabilizer_iff, Subgroup.mem_bot, QuotientGroup.eq_one_iff]

Premises used: MulAction.mem_stabilizer_iff, QuotientGroup.eq_one_iff, Subgroup.mem_bot
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
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 '' (a • s)

Tactic:
have : q a • q '' s = q '' (a • s) :=
    (image_smul_distrib (QuotientGroup.mk' <| stabilizer G s) _ _).symm
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
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
⊢ 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:
rw [this]
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
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
rw rw₁ :
  Eq (α := Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' s)
    (QuotientGroup.mk '' s)
⊢ Eq (α := Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' (a • s))
    (QuotientGroup.mk '' s)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
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 :
  ∀
    (h :
      Eq (α := Set (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G s))) (QuotientGroup.mk '' (a • s))
        (QuotientGroup.mk '' s)),
    a • s = s
⊢ 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]⟩
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
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
h₃ h₄ h₅ h₆ : ∀ (h : a • s = s), a • s = s
⊢ a • s = s

Tactic:
rwa [QuotientGroup.image_coe_inj, mul_smul_comm, stabilizer_mul_self] at h

Premises used: QuotientGroup.image_coe_inj, MulAction.stabilizer_mul_self, mul_smul_comm
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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]
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 ℕ)
⊢ (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

Tactic:
simp_rw [toFinsupp_mul, toFinsupp_C]

Premises used: Polynomial.toFinsupp_mul, Polynomial.toFinsupp_C
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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 (α := AddMonoidAlgebra A ℕ)
      ((algebraMap R (AddMonoidAlgebra A ℕ) : (a : R) → AddMonoidAlgebra A ℕ) r : AddMonoidAlgebra A ℕ) p.toFinsupp =
    HMul.hMul (β := AddMonoidAlgebra A ℕ) p.toFinsupp
      ((algebraMap R (AddMonoidAlgebra A ℕ) : (a : R) → AddMonoidAlgebra A ℕ) r : AddMonoidAlgebra A ℕ)

Tactic:
Algebra.commutes' r p.toFinsupp

Premises used: Polynomial.toFinsupp, Algebra.commutes'
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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 (α := 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:
convert! Algebra.commutes' r p.toFinsupp

Premises used: Polynomial.toFinsupp, Algebra.commutes'
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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]
rw :
  r • p.toFinsupp =
    HMul.hMul (α := AddMonoidAlgebra A ℕ)
      (AddMonoidAlgebra.single 0 ((algebraMap R A : (a : R) → A) r) : AddMonoidAlgebra A ℕ) p.toFinsupp
⊢ (r • p).toFinsupp =
    (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) r) : A[X]) p).toFinsupp

Tactic:
rw [toFinsupp_smul, toFinsupp_mul, toFinsupp_C]

Premises used: Polynomial.toFinsupp_mul, Polynomial.toFinsupp_smul, Polynomial.toFinsupp_C
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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 (α := AddMonoidAlgebra A ℕ)
      (AddMonoidAlgebra.single 0 ((algebraMap R A : (a : R) → A) r) : AddMonoidAlgebra A ℕ) p.toFinsupp

Tactic:
Algebra.smul_def' _ _

Premises used: Algebra.smul_def', Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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 (α := AddMonoidAlgebra A ℕ)
      (AddMonoidAlgebra.single 0 ((algebraMap R A : (a : R) → A) r) : AddMonoidAlgebra A ℕ) p.toFinsupp

Tactic:
exact Algebra.smul_def' _ _

Premises used: Algebra.smul_def'
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Eq.{z + 1} (α := A[X]) ((algebraMap R A[X] : (a : R) → A[X]) r : A[X])
    ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) r) : A[X])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Eq.{z + 1} (α := AddMonoidAlgebra A ℕ)
    (AddMonoidAlgebra.single 0 ((algebraMap R A : (a : R) → A) r) : AddMonoidAlgebra A ℕ)
    ((algebraMap R (AddMonoidAlgebra A ℕ) : (a : R) → AddMonoidAlgebra A ℕ) r : AddMonoidAlgebra A ℕ)

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Eq.{z + 1} (α := A[X]) { toFinsupp := (algebraMap R (AddMonoidAlgebra A ℕ) : (a : R) → AddMonoidAlgebra A ℕ) r }
    ((algebraMap R A[X] : (a : R) → A[X]) r)

Tactic:
toFinsupp_injective (toFinsupp_algebraMap _).symm

Premises used: Polynomial.toFinsupp_injective, Polynomial.toFinsupp_algebraMap, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
r : R
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((algebraMap R R[X] : (a : R) → R[X]) r : R[X])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R →+* R[X]) (algebraMap R R[X]) C

Tactic:
rfl

Premises used: Polynomial.C, rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
B : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f g : AlgHom.{u, z, u_2} R A[X] B
hC : f.comp CAlgHom = g.comp CAlgHom
hX : Eq.{u_2 + 1} (α := B) ((f : (a : A[X]) → B) X : B) ((g : (a : A[X]) → B) X : B)
⊢ f = g

Tactic:
AlgHom.coe_ringHom_injective (ringHom_ext' (congr_arg AlgHom.toRingHom hC) hX)

Premises used: AlgHom.coe_ringHom_injective, Polynomial.ringHom_ext', congr_arg, AlgHom.toRingHom
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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_1 : R[X]
r : R
⊢ Eq (α := R[ℕ]) (Equiv.toFun (RingEquiv.toEquiv (toFinsuppIso R)) ((algebraMap R R[X] : (a : R) → R[X]) r))
    ((algebraMap R R[ℕ] : (a : R) → R[ℕ]) r)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
rw : ∃ (x : A[X]), ¬(Membership.mem (γ := Subalgebra R A[X]) ⊥ x ↔ Membership.mem (γ := Subalgebra R A[X]) ⊤ x)
⊢ Ne.{z + 1} (α := Subalgebra R A[X]) ⊥ ⊤

Tactic:
rw [Ne, SetLike.ext_iff, not_forall]

Premises used: Ne, SetLike.ext_iff, Classical.not_forall
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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)

Tactic:
⟨X, ?_⟩

Premises used: Exists.intro, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
refine : ¬(Membership.mem (γ := Subalgebra R A[X]) ⊥ X ↔ Membership.mem (γ := Subalgebra R A[X]) ⊤ X)
⊢ ∃ (x : A[X]), ¬(Membership.mem (γ := Subalgebra R A[X]) ⊥ x ↔ Membership.mem (γ := Subalgebra R A[X]) ⊤ x)

Tactic:
refine ⟨X, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
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])
⊢ ¬(Membership.mem (γ := Subalgebra R A[X]) ⊥ X ↔ Membership.mem (γ := Subalgebra R A[X]) ⊤ X)

Tactic:
simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top,
        algebraMap_apply]

Premises used: Algebra.mem_top, Set.mem_range, Polynomial.algebraMap_apply, Algebra.mem_bot, iff_true, not_exists
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
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)
⊢ ¬Eq.{z + 1} (α := A[X]) ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) x) : A[X]) (X : A[X])

Tactic:
rw [ext_iff, not_forall]

Premises used: Polynomial.ext_iff, Classical.not_forall
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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)

Tactic:
⟨1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
refine : ¬Eq.{z + 1} (α := A) (coeff ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) x)) 1) (coeff X 1)
⊢ ∃ (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:
refine ⟨1, ?_⟩