awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
h :
  ∀ (m : M),
    m ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ) ↔
      Membership.mem (γ := Finset M)
        (Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯)
        m
⊢ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ) =
    Finite.toFinset (s :=
      Function.support (M := MvPolynomial σ R) fun (m : M) ↦
        (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
      ⋯

Tactic:
ext m
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
h :
  (decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0 ↔
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ m ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ) ↔
    Membership.mem (γ := Finset M)
      (Finite.toFinset (s :=
        Function.support (M := MvPolynomial σ R) fun (m : M) ↦
          (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
        ⋯)
      m

Tactic:
simp only [DFinsupp.mem_support_toFun, ne_eq, Set.Finite.mem_toFinset, Function.mem_support,
      not_iff_not]

Premises used: not_iff_not, DFinsupp.mem_support_toFun, Set.Finite.mem_toFinset, ne_eq, Function.mem_support
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
rw :
  (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (↑0 : MvPolynomial σ R)
| (decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0

Tactic:
rw [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
h :
  (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
      (↑0 : MvPolynomial σ R) ↔
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ (decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0 ↔
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      (0 : MvPolynomial σ R)

Tactic:
conv_lhs => rw [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
h :
  Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      ((↑0 : MvPolynomial σ R) : MvPolynomial σ R) ↔
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
h₁ h₂ :
  Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      (0 : MvPolynomial σ R) ↔
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
      (↑0 : MvPolynomial σ R) ↔
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      (0 : MvPolynomial σ R)

Tactic:
rw [decompose'_apply, Submodule.coe_zero]

Premises used: MvPolynomial.decompose'_apply, Submodule.coe_zero
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
x : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)
h :
  ∀ (i : M),
    (decompose' R w
            ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
                (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
              x) :
          (a : M) → ↥(weightedHomogeneousSubmodule R w a))
        i =
      (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i
⊢ decompose' R w
      ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    x

Tactic:
apply DFinsupp.ext

Premises used: DFinsupp.ext
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
x : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)
m : M
h :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
⊢ (decompose' R w
          ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
              (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
            x) :
        (a : M) → ↥(weightedHomogeneousSubmodule R w a))
      m =
    (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m

Tactic:
rw [← Subtype.coe_inj, decompose'_apply]

Premises used: Subtype.coe_inj, MvPolynomial.decompose'_apply
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
x : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)

Tactic:
weightedHomogeneousComponent_directSum R w x m

Premises used: Set.Mem, MvPolynomial.weightedHomogeneousComponent_directSum, Trunc.lift
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
x : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)

Tactic:
exact weightedHomogeneousComponent_directSum R w x m

Premises used: MvPolynomial.weightedHomogeneousComponent_directSum
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
x : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)
h h₁ :
  ∀ (m : M),
    (decompose' R w
            ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
                (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
              x) :
          (a : M) → ↥(weightedHomogeneousSubmodule R w a))
        m =
      (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m
h₂ :
  ∀ (m : M),
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
            (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
          x) =
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
⊢ decompose' R w
      ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    x

Tactic:
classical
    apply DFinsupp.ext
    intro m
    rw [← Subtype.coe_inj, decompose'_apply]
    exact weightedHomogeneousComponent_directSum R w x m

Premises used: DFinsupp.ext, Subtype.coe_inj, MvPolynomial.decompose'_apply
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
⊢ Eq (α := MvPolynomial σ R → DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
    (@DirectSum.Decomposition.decompose' _ _ _ inst_2 _ _ _ _ _) fun (φ : MvPolynomial σ R) ↦
    ((DirectSum.mk (fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
            (Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) :
          ((i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
              ↥(weightedHomogeneousSubmodule R w (↑i : M))) →+
            DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) :
        (a :
            (i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
              ↥(weightedHomogeneousSubmodule R w (↑i : M))) →
          DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
      fun (m : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) ↦
      Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (↑m : M)) x)
        ((weightedHomogeneousComponent w (↑m : M) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) ⋯

Tactic:
rfl

Premises used: Set.Mem, setOf, MvPolynomial.decompose', rfl
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ (↑((@DirectSum.Decomposition.decompose' _ _ _ inst_2 _ _ _ _ _ φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a))
          m) :
      MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ

Tactic:
MvPolynomial.decompose'_apply R w φ m

Premises used: MvPolynomial.decompose'_apply
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
⊢ Function.Injective (α := K) (β := MvPolynomial σ K ⧸ I)
    (⇑(RingHom.comp (Ideal.Quotient.mk I) C) : (a : K) → MvPolynomial σ K ⧸ I)

Tactic:
(injective_iff_map_eq_zero _).2 fun x hx => ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
refine :
  ∀ (x : K)
    (hx :
      Eq (α := MvPolynomial σ K ⧸ I)
        ((RingHom.comp (Ideal.Quotient.mk I) C : (a : K) → MvPolynomial σ K ⧸ I) x : MvPolynomial σ K ⧸ I)
        (0 : MvPolynomial σ K ⧸ I)),
    x = 0
⊢ Function.Injective (α := K) (β := MvPolynomial σ K ⧸ I)
    (⇑(RingHom.comp (Ideal.Quotient.mk I) C) : (a : K) → MvPolynomial σ K ⧸ I)

Tactic:
refine (injective_iff_map_eq_zero _).2 fun x hx => ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx :
  Eq (α := MvPolynomial σ K ⧸ I)
    ((RingHom.comp (Ideal.Quotient.mk I) C : (a : K) → MvPolynomial σ K ⧸ I) x : MvPolynomial σ K ⧸ I)
    (0 : MvPolynomial σ K ⧸ I)
⊢ Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K)

Tactic:
rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem] at hx

Premises used: Ideal.Quotient.eq_zero_iff_mem, RingHom.comp_apply
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K)
⊢ x = 0

Tactic:
_root_.by_contradiction fun hx0 => absurd (I.eq_top_iff_one.2 ?_) hI

Premises used: Iff.mpr, Ideal.eq_top_iff_one, absurd, by_contradiction
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K)
refine : ∀ (hx0 : ¬x = 0), 1 ∈ I
⊢ x = 0

Tactic:
refine _root_.by_contradiction fun hx0 => absurd (I.eq_top_iff_one.2 ?_) hI

Premises used: Iff.mpr, Ideal.eq_top_iff_one, absurd, by_contradiction
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K)
hx0 : ¬x = 0
⊢ HMul.hMul (α := MvPolynomial σ K) (β := MvPolynomial σ K) ((C : (a : K) → MvPolynomial σ K) x⁻¹ : MvPolynomial σ K)
      ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K) ∈
    I

Tactic:
have := I.mul_mem_left (MvPolynomial.C x⁻¹) hx
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K)
hx0 : ¬x = 0
this :
  HMul.hMul (α := MvPolynomial σ K) (β := MvPolynomial σ K) ((C : (a : K) → MvPolynomial σ K) x⁻¹ : MvPolynomial σ K)
      ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K) ∈
    I
rwa :
  ∀ (this : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) (x⁻¹ * x) : MvPolynomial σ K)),
    1 ∈ I
rwa₁ : ∀ (this : (C : (a : K) → MvPolynomial σ K) 1 ∈ I), 1 ∈ I
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : 1 ∈ I), 1 ∈ I
⊢ 1 ∈ I

Tactic:
rwa [← MvPolynomial.C.map_mul, inv_mul_cancel₀ hx0, MvPolynomial.C_1] at this

Premises used: MvPolynomial.C_1, RingHom.map_mul, MvPolynomial.C, inv_mul_cancel₀
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : CommRing K
inst_1 : Nontrivial K
rw : lift.{u, max u v} (Module.rank K (MvPolynomial σ K)) = lift.{u, max u v} (lift.{v, u} #(σ →₀ ℕ))
rw₁ : lift.{max u v, u} #(σ →₀ ℕ) = lift.{u, max u v} (lift.{v, u} #(σ →₀ ℕ))
rw₂ : lift.{max u v, u} #(σ →₀ ℕ) = lift.{max v u, u} #(σ →₀ ℕ)
rw₃ rw₄ : lift.{v, u} #(σ →₀ ℕ) = lift.{v, u} #(σ →₀ ℕ)
⊢ Module.rank K (MvPolynomial σ K) = lift.{v, u} #(σ →₀ ℕ)

Tactic:
rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank, lift_lift, lift_umax.{u, v}]

Premises used: Module.Basis.mk_eq_rank, Cardinal.lift_lift, MvPolynomial.basisMonomials, Cardinal.lift_inj
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
K : Type v
inst : CommRing K
inst_1 : Nontrivial K
σ : Type v
rw : lift.{v, v} (Module.rank K (MvPolynomial σ K)) = lift.{v, v} #(σ →₀ ℕ)
rw₁ rw₂ : lift.{v, v} #(σ →₀ ℕ) = lift.{v, v} #(σ →₀ ℕ)
⊢ Module.rank K (MvPolynomial σ K) = #(σ →₀ ℕ)

Tactic:
rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank]

Premises used: Module.Basis.mk_eq_rank, MvPolynomial.basisMonomials, Cardinal.lift_inj
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : CommRing K
inst_1 : Nontrivial K
inst_2 : Nonempty σ
⊢ Module.finrank K (MvPolynomial σ K) = 0

Tactic:
(basisMonomials σ K).linearIndependent.finrank_eq_zero_of_infinite

Premises used: LinearIndependent.finrank_eq_zero_of_infinite, MvPolynomial.basisMonomials, Module.Basis.linearIndependent
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : CommRing K
inst_1 : IsEmpty σ
inl : Subsingleton K → Module.rank K (MvPolynomial σ K) = 1
inr : Nontrivial K → Module.rank K (MvPolynomial σ K) = 1
⊢ Module.rank K (MvPolynomial σ K) = 1

Tactic:
cases subsingleton_or_nontrivial K

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : CommRing K
inst_1 : IsEmpty σ
h : Subsingleton K
⊢ Module.rank K (MvPolynomial σ K) = 1

Tactic:
simp [rank_eq_lift]

Premises used: MvPolynomial.rank_eq_lift
-- Module: Mathlib.RingTheory.MvPolynomial
Goal:
σ : Type u
K : Type v
inst : CommRing K
inst_1 : IsEmpty σ
h : Nontrivial K
⊢ Module.rank K (MvPolynomial σ K) = 1

Tactic:
simp [rank_eq_lift]

Premises used: MvPolynomial.rank_eq_lift
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Nontrivial R
⊢ Nontrivial (MvPowerSeries σ R)

Tactic:
inferInstanceAs <| Nontrivial ((σ →₀ ℕ) → R)

Premises used: _private.0.MvPowerSeries.instNontrivial._proof_1
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : SMul R S
inst_6 : IsScalarTower R S A
⊢ IsScalarTower R S (MvPowerSeries σ A)

Tactic:
inferInstanceAs <| IsScalarTower R S ((σ →₀ ℕ) → A)

Premises used: _private.0.MvPowerSeries.instIsScalarTower._proof_1
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (coeff d : (a : MvPowerSeries σ R) → R) f = f d

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ ψ : MvPowerSeries σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)
⊢ φ = ψ

Tactic:
funext h

Premises used: MvPowerSeries, funext
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
n : σ →₀ ℕ
⊢ Eq (α := R →ₗ[R] MvPowerSeries σ R) (LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R)
    (LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
n : σ →₀ ℕ
⊢ Eq (α := R →ₗ[R] MvPowerSeries σ R) (LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R)
    (LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R)

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
m n : σ →₀ ℕ
a : R
dsimp :
  (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
      ((monomial n : (a : R) → (σ →₀ ℕ) → R) a : (σ →₀ ℕ) → R) =
    if m = n then a else 0
⊢ (coeff m : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) =
    if m = n then a else 0

Tactic:
dsimp only [coeff, MvPowerSeries]

Premises used: MvPowerSeries, MvPowerSeries.coeff
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
m n : σ →₀ ℕ
a : R
rw :
  (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
      (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → (σ →₀ ℕ) → R) a :
        (σ →₀ ℕ) → R) =
    if m = n then a else 0
rw₁ :
  ((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → (σ →₀ ℕ) → R) a m =
    if m = n then a else 0
rw₂ : Pi.single (M := fun (x : σ →₀ ℕ) ↦ R) n a m = if m = n then a else 0
rw₃ rw₄ : (if m = n then a else 0) = if m = n then a else 0
⊢ (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
      ((monomial n : (a : R) → (σ →₀ ℕ) → R) a : (σ →₀ ℕ) → R) =
    if m = n then a else 0

Tactic:
rw [monomial_def, LinearMap.proj_apply (i := m), LinearMap.single_apply, Pi.single_apply]

Premises used: Pi.single_apply, MvPowerSeries.monomial_def, LinearMap.proj_apply, LinearMap.single_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
a : R
rw :
  (coeff n : (a : MvPowerSeries σ R) → R)
      (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
        MvPowerSeries σ R) =
    a
⊢ (coeff n : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) = a

Tactic:
rw [monomial_def]

Premises used: MvPowerSeries.monomial_def
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff n : (a : MvPowerSeries σ R) → R)
      (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
        MvPowerSeries σ R) =
    a

Tactic:
Pi.single_eq_same _ _

Premises used: Function.update, Pi.single, dite, Pi.single_eq_same
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff n : (a : MvPowerSeries σ R) → R)
      (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
        MvPowerSeries σ R) =
    a

Tactic:
exact Pi.single_eq_same _ _

Premises used: Pi.single_eq_same
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
a : R
rw rw₁ rw₂ :
  (coeff n : (a : MvPowerSeries σ R) → R)
      (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
        MvPowerSeries σ R) =
    a
⊢ (coeff n : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) = a

Tactic:
classical
  rw [monomial_def]
  exact Pi.single_eq_same _ _

Premises used: MvPowerSeries.monomial_def, Pi.single_eq_same
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
rw :
  Eq.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
          MvPowerSeries σ R) :
      R)
    (0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) : R)
    (0 : R)

Tactic:
rw [monomial_def]

Premises used: MvPowerSeries.monomial_def
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
          MvPowerSeries σ R) :
      R)
    (0 : R)

Tactic:
Pi.single_eq_of_ne h _

Premises used: Function.update, Pi.single_eq_of_ne, Pi.single, dite
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
          MvPowerSeries σ R) :
      R)
    (0 : R)

Tactic:
exact Pi.single_eq_of_ne h _

Premises used: Pi.single_eq_of_ne