awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
rw : ¬Eq (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
rw₁ :
  ¬∀ (x : MvPowerSeries σ R),
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x
⊢ Ne (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
have rw₂ : ∃ (x : MvPowerSeries σ R),
  ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
Tactic: classical
      rw [Ne, SetLike.ext_iff, not_forall]
      inhabit σ
      refine ⟨X default, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
      intro x
      rw [MvPowerSeries.ext_iff, not_forall]
      refine ⟨Finsupp.single default 1, ?_⟩
      simp [algebraMap_apply, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
rw : ¬Eq (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
rw₁ :
  ¬∀ (x : MvPowerSeries σ R),
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x
rw₂ rw₃ rw₄ :
  ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
⊢ Ne (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
have rw₅ : ∀ (inhabited_h : Inhabited σ),
  ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
Tactic: classical
      rw [Ne, SetLike.ext_iff, not_forall]
      inhabit σ
      refine ⟨X default, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
      intro x
      rw [MvPowerSeries.ext_iff, not_forall]
      refine ⟨Finsupp.single default 1, ?_⟩
      simp [algebraMap_apply, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
rw : ¬Eq (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
rw₁ :
  ¬∀ (x : MvPowerSeries σ R),
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x
rw₂ rw₃ rw₄ :
  ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
rw₅ :
  ∀ (inhabited_h : Inhabited σ),
    ∃ (x : MvPowerSeries σ R),
      ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
          Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
⊢ Ne (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
have rw₆ : ∀ (inhabited_h : Inhabited σ),
  ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ (X default) ↔
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ (X default))
Tactic: classical
      rw [Ne, SetLike.ext_iff, not_forall]
      inhabit σ
      refine ⟨X default, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
      intro x
      rw [MvPowerSeries.ext_iff, not_forall]
      refine ⟨Finsupp.single default 1, ?_⟩
      simp [algebraMap_apply, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
rw : ¬Eq (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
rw₁ :
  ¬∀ (x : MvPowerSeries σ R),
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x
rw₂ rw₃ rw₄ :
  ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
rw₅ :
  ∀ (inhabited_h : Inhabited σ),
    ∃ (x : MvPowerSeries σ R),
      ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
          Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
rw₆ :
  ∀ (inhabited_h : Inhabited σ),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ (X default) ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ (X default))
⊢ Ne (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
have rw₇ : ∀ (inhabited_h : Inhabited σ) (x : R),
  ¬Eq (α := MvPowerSeries σ R) ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R)
      (X default : MvPowerSeries σ R)
Tactic: classical
      rw [Ne, SetLike.ext_iff, not_forall]
      inhabit σ
      refine ⟨X default, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
      intro x
      rw [MvPowerSeries.ext_iff, not_forall]
      refine ⟨Finsupp.single default 1, ?_⟩
      simp [algebraMap_apply, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
rw : ¬Eq (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
rw₁ :
  ¬∀ (x : MvPowerSeries σ R),
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x
rw₂ rw₃ rw₄ :
  ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
rw₅ :
  ∀ (inhabited_h : Inhabited σ),
    ∃ (x : MvPowerSeries σ R),
      ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
          Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
rw₆ :
  ∀ (inhabited_h : Inhabited σ),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ (X default) ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ (X default))
rw₇ rw₈ :
  ∀ (inhabited_h : Inhabited σ) (x : R),
    ¬Eq (α := MvPowerSeries σ R)
        ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R)
        (X default : MvPowerSeries σ R)
⊢ Ne (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
have rw₉ : ∀ (inhabited_h : Inhabited σ) (x : R),
  ∃ (x_1 : σ →₀ ℕ),
    ¬Eq.{u_2 + 1} (α := R)
        ((coeff x_1 : (a : MvPowerSeries σ R) → R)
            ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
          R)
        ((coeff x_1 : (a : MvPowerSeries σ R) → R) (X default) : R)
Tactic: classical
      rw [Ne, SetLike.ext_iff, not_forall]
      inhabit σ
      refine ⟨X default, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
      intro x
      rw [MvPowerSeries.ext_iff, not_forall]
      refine ⟨Finsupp.single default 1, ?_⟩
      simp [algebraMap_apply, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
rw : ¬Eq (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
rw₁ :
  ¬∀ (x : MvPowerSeries σ R),
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x
rw₂ rw₃ rw₄ :
  ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
rw₅ :
  ∀ (inhabited_h : Inhabited σ),
    ∃ (x : MvPowerSeries σ R),
      ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
          Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
rw₆ :
  ∀ (inhabited_h : Inhabited σ),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ (X default) ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ (X default))
rw₇ rw₈ :
  ∀ (inhabited_h : Inhabited σ) (x : R),
    ¬Eq (α := MvPowerSeries σ R)
        ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R)
        (X default : MvPowerSeries σ R)
rw₉ :
  ∀ (inhabited_h : Inhabited σ) (x : R),
    ∃ (x_1 : σ →₀ ℕ),
      ¬Eq.{u_2 + 1} (α := R)
          ((coeff x_1 : (a : MvPowerSeries σ R) → R)
              ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
            R)
          ((coeff x_1 : (a : MvPowerSeries σ R) → R) (X default) : R)
⊢ Ne (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
have rw₁₀ : ∀ (inhabited_h : Inhabited σ) (x : R),
  ¬Eq.{u_2 + 1} (α := R)
      ((coeff (single default 1) : (a : MvPowerSeries σ R) → R)
          ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
      ((coeff (single default 1) : (a : MvPowerSeries σ R) → R) (X default) : R)
Tactic: classical
      rw [Ne, SetLike.ext_iff, not_forall]
      inhabit σ
      refine ⟨X default, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
      intro x
      rw [MvPowerSeries.ext_iff, not_forall]
      refine ⟨Finsupp.single default 1, ?_⟩
      simp [algebraMap_apply, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
        (↑((monomial n : (a : R) → MvPolynomial σ R) a) : MvPowerSeries σ R) :
      R)
    ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
        ((MvPowerSeries.monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
      R)
have rw : (if n = m then a else 0) = if m = n then a else 0
Tactic: rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if n = m then a else 0) = if m = n then a else 0
have pos : ∀ (h₁ : n = m) (h₂ : m = n), a = a
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
pos : ∀ (h₁ : n = m) (h₂ : m = n), a = a
⊢ (if n = m then a else 0) = if m = n then a else 0
have neg : ∀ (h₁ : n = m) (h₂ : ¬m = n), a = 0
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
pos : ∀ (h₁ : n = m) (h₂ : m = n), a = a
neg : ∀ (h₁ : n = m) (h₂ : ¬m = n), a = 0
⊢ (if n = m then a else 0) = if m = n then a else 0
have pos₁ : ∀ (h₁ : ¬n = m), m = n → 0 = a
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
pos : ∀ (h₁ : n = m) (h₂ : m = n), a = a
neg : ∀ (h₁ : n = m) (h₂ : ¬m = n), a = 0
pos₁ : ∀ (h₁ : ¬n = m), m = n → 0 = a
⊢ (if n = m then a else 0) = if m = n then a else 0
have neg₁ : ∀ (h₁ : ¬n = m), ¬m = n → Eq.{u_2 + 1} (α := R) 0 0
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : n = m
h₂ : ¬m = n
⊢ a = 0
have h₃ : ¬n = n
Tactic: subst m
Cleared hypotheses: m, h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : n = m
h₂ : ¬m = n
⊢ a = 0
have neg : ∀ (h₂ : ¬n = n), a = 0
Tactic: first | rfl | subst m; contradiction
Cleared hypotheses: m, h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h : m = n
⊢ 0 = a
have h₂ : ¬n = n
Tactic: subst m
Cleared hypotheses: m, h₁, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h : m = n
⊢ 0 = a
have pos : ∀ (h₁ : ¬n = n), 0 = a
Tactic: first | rfl | subst m; contradiction
Cleared hypotheses: m, h₁, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
        (↑((monomial n : (a : R) → MvPolynomial σ R) a) : MvPowerSeries σ R) :
      R)
    ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
        ((MvPowerSeries.monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
      R)
have rw : Eq.{u_2 + 1} (α := R) (coeff m ((monomial n : (a : R) → MvPolynomial σ R) a) : R)
  ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
      ((MvPowerSeries.monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
    R)
Tactic: classical
    rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]
    split_ifs with h₁ h₂ <;> first | rfl | subst m; contradiction
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
rw :
  Eq.{u_2 + 1} (α := R) (coeff m ((monomial n : (a : R) → MvPolynomial σ R) a) : R)
    ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
        ((MvPowerSeries.monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
        (↑((monomial n : (a : R) → MvPolynomial σ R) a) : MvPowerSeries σ R) :
      R)
    ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
        ((MvPowerSeries.monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
      R)
have rw₁ : (if n = m then a else 0) =
  (MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
    ((MvPowerSeries.monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
Tactic: classical
    rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]
    split_ifs with h₁ h₂ <;> first | rfl | subst m; contradiction
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
rw :
  Eq.{u_2 + 1} (α := R) (coeff m ((monomial n : (a : R) → MvPolynomial σ R) a) : R)
    ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
        ((MvPowerSeries.monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
      R)
rw₁ :
  (if n = m then a else 0) =
    (MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
      ((MvPowerSeries.monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
⊢ Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
        (↑((monomial n : (a : R) → MvPolynomial σ R) a) : MvPowerSeries σ R) :
      R)
    ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R)
        ((MvPowerSeries.monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
      R)
have rw₂ : (if n = m then a else 0) = if m = n then a else 0
Tactic: classical
    rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]
    split_ifs with h₁ h₂ <;> first | rfl | subst m; contradiction
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x y : MvPolynomial σ R
h : (↑x : MvPowerSeries σ R) = (↑y : MvPowerSeries σ R)
⊢ x = y
have a : ∀ (m : σ →₀ ℕ), coeff m x = coeff m y
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x y : MvPolynomial σ R
h : (↑x : MvPowerSeries σ R) = (↑y : MvPowerSeries σ R)
m : σ →₀ ℕ
⊢ coeff m x = coeff m y
have a : Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R) (↑x : MvPowerSeries σ R) : R)
  ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R) (↑y : MvPowerSeries σ R) : R)
Tactic: simp_rw [← coeff_coe, h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
⊢ (↑φ : MvPowerSeries σ R) = 0 ↔ φ = 0
have rw : (↑φ : MvPowerSeries σ R) = (↑0 : MvPowerSeries σ R) ↔ φ = 0
Tactic: rw [← coe_zero, coe_inj]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
rw : (↑φ : MvPowerSeries σ R) = (↑0 : MvPowerSeries σ R) ↔ φ = 0
⊢ (↑φ : MvPowerSeries σ R) = 0 ↔ φ = 0
have rw₁ : φ = 0 ↔ φ = 0
Tactic: rw [← coe_zero, coe_inj]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
⊢ (↑φ : MvPowerSeries σ R) = 1 ↔ φ = 1
have rw : (↑φ : MvPowerSeries σ R) = (↑1 : MvPowerSeries σ R) ↔ φ = 1
Tactic: rw [← coe_one, coe_inj]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
rw : (↑φ : MvPowerSeries σ R) = (↑1 : MvPowerSeries σ R) ↔ φ = 1
⊢ (↑φ : MvPowerSeries σ R) = 1 ↔ φ = 1
have rw₁ : φ = 1 ↔ φ = 1
Tactic: rw [← coe_one, coe_inj]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
⊢ Eq (α := MvPowerSeries σ R) ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
    (e.prod fun (s : σ) (n : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) n)
have simp : Eq (α := MvPowerSeries σ R)
  (↑(e.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e) : MvPowerSeries σ R)
  (e.prod fun (s : σ) (n : ℕ) ↦ (↑(HPow.hPow (α := MvPolynomial σ R) (X s) n) : MvPowerSeries σ R))
Tactic: simp only [← coe_X, ← coe_pow, ← coe_monomial, monomial_eq, map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : R
| ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
have rw : ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (r * 1) : MvPowerSeries σ R)
Tactic: rw [← mul_one r]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) r =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e : MvPowerSeries σ R)
have conv_lhs : (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (r * 1) =
  HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
    ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
    (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e : MvPowerSeries σ R)
Tactic: conv_lhs => rw [← mul_one r]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (r * 1) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e : MvPowerSeries σ R)
have rw : (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (HSMul.hSMul (β := R) r 1) =
  HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
    ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
    (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e : MvPowerSeries σ R)
Tactic: rw [← smul_eq_mul, ← MvPowerSeries.smul_eq_C_mul, LinearMap.CompatibleSMul.map_smul,
    MvPowerSeries.monomial_one_eq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : R
rw :
  (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (HSMul.hSMul (β := R) r 1) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e : MvPowerSeries σ R)
⊢ (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (r * 1) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e : MvPowerSeries σ R)
have rw₁ : (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (HSMul.hSMul (β := R) r 1) =
  HSMul.hSMul (β := MvPowerSeries σ R) r
    (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e)
Tactic: rw [← smul_eq_mul, ← MvPowerSeries.smul_eq_C_mul, LinearMap.CompatibleSMul.map_smul,
    MvPowerSeries.monomial_one_eq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : R
rw :
  (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (HSMul.hSMul (β := R) r 1) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e : MvPowerSeries σ R)
rw₁ :
  (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (HSMul.hSMul (β := R) r 1) =
    HSMul.hSMul (β := MvPowerSeries σ R) r
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e)
⊢ (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (r * 1) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e : MvPowerSeries σ R)
have rw₂ : HSMul.hSMul (β := MvPowerSeries σ R) r ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1) =
  HSMul.hSMul (β := MvPowerSeries σ R) r
    (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e)
Tactic: rw [← smul_eq_mul, ← MvPowerSeries.smul_eq_C_mul, LinearMap.CompatibleSMul.map_smul,
    MvPowerSeries.monomial_one_eq]