awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h : Eq (α := MvPowerSeries σ R) (X s) (X t)
⊢ Eq.{u_2 + 1} (α := R) ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X s) : R)
    ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X t) : R)

Tactic:
replace h := congr_arg (coeff (single s 1)) h
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h :
  Eq.{u_2 + 1} (α := R) ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X s) : R)
    ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X t) : R)
⊢ Eq.{u_2 + 1} (α := R) 1 (if Eq (α := σ →₀ ℕ) (single s 1) (single t 1) then 1 else 0)

Tactic:
rw [coeff_X, if_pos rfl, coeff_X] at h

Premises used: MvPowerSeries.coeff_X, if_pos, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h : Eq.{u_2 + 1} (α := R) 1 (if Eq (α := σ →₀ ℕ) (single s 1) (single t 1) then 1 else 0)
pos : ∀ (H : Eq (α := σ →₀ ℕ) (single s 1) (single t 1)) (h : Eq.{u_2 + 1} (α := R) 1 1), s = t
neg : ∀ (H : ¬Eq (α := σ →₀ ℕ) (single s 1) (single t 1)) (h : Eq.{u_2 + 1} (α := R) 1 0), s = t
⊢ s = t

Tactic:
split_ifs at h with H
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
H : Eq (α := σ →₀ ℕ) (single s 1) (single t 1)
h : Eq.{u_2 + 1} (α := R) 1 1
⊢ s = t ∧ Eq (α := ℕ) 1 1 ∨ Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0

Tactic:
rw [Finsupp.single_eq_single_iff] at H

Premises used: Finsupp.single_eq_single_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
H : Eq (α := σ →₀ ℕ) (single s 1) (single t 1)
h : Eq.{u_2 + 1} (α := R) 1 1
H₁ : s = t ∧ Eq (α := ℕ) 1 1 ∨ Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0
⊢ Eq.{u_2 + 1} (α := R) 1 1

Tactic:
rw [Finsupp.single_eq_single_iff] at H

Premises used: Finsupp.single_eq_single_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
H : s = t ∧ Eq (α := ℕ) 1 1 ∨ Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0
h : Eq.{u_2 + 1} (α := R) 1 1
pos : ∀ (H : s = t ∧ Eq (α := ℕ) 1 1), s = t
pos₁ : ∀ (H : Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0), s = t
⊢ s = t

Tactic:
rcases H with H | H
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h : Eq.{u_2 + 1} (α := R) 1 1
H : s = t ∧ Eq (α := ℕ) 1 1
⊢ s = t

Tactic:
H.1

Premises used: And.left
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h : Eq.{u_2 + 1} (α := R) 1 1
H : s = t ∧ Eq (α := ℕ) 1 1
⊢ s = t

Tactic:
exact H.1

Premises used: And.left
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h : Eq.{u_2 + 1} (α := R) 1 1
H : Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0
pos : False
⊢ s = t

Tactic:
exfalso
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h : Eq.{u_2 + 1} (α := R) 1 1
H : Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0
⊢ False

Tactic:
one_ne_zero H.1

Premises used: And.left, one_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h : Eq.{u_2 + 1} (α := R) 1 1
H : Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0
⊢ False

Tactic:
exact one_ne_zero H.1

Premises used: And.left, one_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
H : ¬Eq (α := σ →₀ ℕ) (single s 1) (single t 1)
h : Eq.{u_2 + 1} (α := R) 1 0
neg : False
⊢ s = t

Tactic:
exfalso
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
H : ¬Eq (α := σ →₀ ℕ) (single s 1) (single t 1)
h : Eq.{u_2 + 1} (α := R) 1 0
⊢ False

Tactic:
one_ne_zero h

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
H : ¬Eq (α := σ →₀ ℕ) (single s 1) (single t 1)
h : Eq.{u_2 + 1} (α := R) 1 0
⊢ False

Tactic:
exact one_ne_zero h

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
intro : ∀ (h : Eq (α := MvPowerSeries σ R) (X s) (X t)), s = t
intro₁ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := R) ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X s) : R)
        ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X t) : R)),
    s = t
intro₂ : ∀ (h : Eq.{u_2 + 1} (α := R) 1 (if Eq (α := σ →₀ ℕ) (single s 1) (single t 1) then 1 else 0)), s = t
pos : ∀ (H : Eq (α := σ →₀ ℕ) (single s 1) (single t 1)) (h : Eq.{u_2 + 1} (α := R) 1 1), s = t
neg neg₁ : ∀ (H : ¬Eq (α := σ →₀ ℕ) (single s 1) (single t 1)) (h : Eq.{u_2 + 1} (α := R) 1 0), s = t
⊢ Eq (α := MvPowerSeries σ R) (X s) (X t) → s = t

Tactic:
classical
    intro h
    replace h := congr_arg (coeff (single s 1)) h
    rw [coeff_X, if_pos rfl, coeff_X] at h
    split_ifs at h with H
    · rw [Finsupp.single_eq_single_iff] at H
      rcases H with H | H
      · exact H.1
      · exfalso
        exact one_ne_zero H.1
    · exfalso
      exact one_ne_zero h

Premises used: Finsupp.single_eq_single_iff, MvPowerSeries.coeff_X, if_pos, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
rw : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) (if n = 0 then 1 else 0 : S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)

Tactic:
rw [coeff_one, coeff_one]

Premises used: MvPowerSeries.coeff_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
pos : ∀ (h : n = 0), Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
neg : ∀ (h : ¬n = 0), Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) (if n = 0 then 1 else 0 : S)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
h : n = 0
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)

Tactic:
simp only [map_one]

Premises used: map_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
h : ¬n = 0
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
rw :
  Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)
rw₁ rw₂ rw₃ : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) (if n = 0 then 1 else 0 : S)
pos : ∀ (h : n = 0), Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
neg neg₁ : ∀ (h : ¬n = 0), Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)

Tactic:
classical
        rw [coeff_one, coeff_one]
        split_ifs with h
        · simp only [map_one]
        · simp only [map_zero]

Premises used: map_zero, MvPowerSeries.coeff_one, map_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
rw :
  Eq.{u_3 + 1} (α := S)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
      (f : (a : R) → S)
        (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)))
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
      HMul.hMul (α := S) (β := S)
        ((coeff p.1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
          S)
        ((coeff p.2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
          S))
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)

Tactic:
rw [coeff_mul, map_sum, coeff_mul]

Premises used: map_sum, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
apply :
  ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
    (f : (a : R) → S)
        (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)) =
      HMul.hMul (α := S) (β := S)
        ((coeff x.1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
          S)
        ((coeff x.2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
          S)
⊢ Eq.{u_3 + 1} (α := S)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
      (f : (a : R) → S)
        (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)))
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
      HMul.hMul (α := S) (β := S)
        ((coeff p.1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
          S)
        ((coeff p.2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
          S))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n i j : σ →₀ ℕ
h : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
rw :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R) : S)
      ((f : (a : R) → S) ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) ψ : R) : S) =
    HMul.hMul (α := S) (β := S)
      ((coeff (i, j).1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
        S)
      ((coeff (i, j).2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
        S)
⊢ (f : (a : R) → S)
      (HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) ψ : R)) =
    HMul.hMul (α := S) (β := S)
      ((coeff (i, j).1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
        S)
      ((coeff (i, j).2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
        S)

Tactic:
rw [f.map_mul]

Premises used: RingHom.map_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n i j : σ →₀ ℕ
h : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R) : S)
      ((f : (a : R) → S) ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) ψ : R) : S) =
    HMul.hMul (α := S) (β := S)
      ((coeff (i, j).1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
        S)
      ((coeff (i, j).2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
        S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) (φ + ψ) : R) =
    HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) : S)
      ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (map (RingHom.id R)) (RingHom.id (MvPowerSeries σ R))

Tactic:
rfl

Premises used: MvPowerSeries.map, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ T) (map (g.comp f)) (RingHom.comp (map g) (map f))

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
φ : MvPowerSeries σ R
⊢ Eq.{u_3 + 1} (α := S)
    ((constantCoeff : (a : MvPowerSeries σ S) → S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
h :
  ∀ (m : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := S)
      ((coeff m : (a : MvPowerSeries σ S) → S)
          ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) ((monomial n : (a : R) → MvPowerSeries σ R) a) :
            MvPowerSeries σ S) :
        S)
      ((coeff m : (a : MvPowerSeries σ S) → S)
          ((monomial n : (a : S) → MvPowerSeries σ S) ((f : (a : R) → S) a) : MvPowerSeries σ S) :
        S)
⊢ Eq (α := MvPowerSeries σ S)
    ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) ((monomial n : (a : R) → MvPowerSeries σ R) a) :
      MvPowerSeries σ S)
    ((monomial n : (a : S) → MvPowerSeries σ S) ((f : (a : R) → S) a) : MvPowerSeries σ S)

Tactic:
ext m
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := S)
    ((coeff m : (a : MvPowerSeries σ S) → S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) ((monomial n : (a : R) → MvPowerSeries σ R) a) :
          MvPowerSeries σ S) :
      S)
    ((coeff m : (a : MvPowerSeries σ S) → S)
        ((monomial n : (a : S) → MvPowerSeries σ S) ((f : (a : R) → S) a) : MvPowerSeries σ S) :
      S)

Tactic:
simp [coeff_monomial, apply_ite f]

Premises used: apply_ite, MvPowerSeries.coeff_monomial, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
h :
  ∀ (m : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := S)
      ((coeff m : (a : MvPowerSeries σ S) → S)
          ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) ((monomial n : (a : R) → MvPowerSeries σ R) a) :
            MvPowerSeries σ S) :
        S)
      ((coeff m : (a : MvPowerSeries σ S) → S)
          ((monomial n : (a : S) → MvPowerSeries σ S) ((f : (a : R) → S) a) : MvPowerSeries σ S) :
        S)
⊢ Eq (α := MvPowerSeries σ S)
    ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) ((monomial n : (a : R) → MvPowerSeries σ R) a) :
      MvPowerSeries σ S)
    ((monomial n : (a : S) → MvPowerSeries σ S) ((f : (a : R) → S) a) : MvPowerSeries σ S)

Tactic:
classical
  ext m
  simp [coeff_monomial, apply_ite f]

Premises used: apply_ite, MvPowerSeries.coeff_monomial, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
a : R
⊢ Eq (α := MvPowerSeries σ S)
    ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) ((C : (a : R) → MvPowerSeries σ R) a) : MvPowerSeries σ S)
    ((C : (a : S) → MvPowerSeries σ S) ((f : (a : R) → S) a) : MvPowerSeries σ S)

Tactic:
map_monomial _ _ _

Premises used: Function.update, Pi.single, dite, MvPowerSeries.map_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
s : σ
⊢ Eq (α := MvPowerSeries σ S) ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) (X s) : MvPowerSeries σ S)
    (X s : MvPowerSeries σ S)

Tactic:
simp [MvPowerSeries.X]

Premises used: MvPowerSeries.X
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
S₁ : Type u_5
S₂ : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
f : R →+* S₁
g : S₁ →+* S₂
p : MvPowerSeries σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_6 + 1} (α := S₂)
      ((coeff n : (a : MvPowerSeries σ S₂) → S₂)
          ((map g : (a : MvPowerSeries σ S₁) → MvPowerSeries σ S₂)
              ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S₁) p) :
            MvPowerSeries σ S₂) :
        S₂)
      ((coeff n : (a : MvPowerSeries σ S₂) → S₂)
          ((map (g.comp f) : (a : MvPowerSeries σ R) → MvPowerSeries σ S₂) p : MvPowerSeries σ S₂) :
        S₂)
⊢ Eq (α := MvPowerSeries σ S₂)
    ((map g : (a : MvPowerSeries σ S₁) → MvPowerSeries σ S₂)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S₁) p) :
      MvPowerSeries σ S₂)
    ((map (g.comp f) : (a : MvPowerSeries σ R) → MvPowerSeries σ S₂) p : MvPowerSeries σ S₂)

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
S₁ : Type u_5
S₂ : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
f : R →+* S₁
g : S₁ →+* S₂
p : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_6 + 1} (α := S₂)
    ((coeff n : (a : MvPowerSeries σ S₂) → S₂)
        ((map g : (a : MvPowerSeries σ S₁) → MvPowerSeries σ S₂)
            ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S₁) p) :
          MvPowerSeries σ S₂) :
      S₂)
    ((coeff n : (a : MvPowerSeries σ S₂) → S₂)
        ((map (g.comp f) : (a : MvPowerSeries σ R) → MvPowerSeries σ S₂) p : MvPowerSeries σ S₂) :
      S₂)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((↑((coeff n : (a : MvPowerSeries σ ↥T) → ↥T) (p.toSubring T hp)) : R) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) p : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
⊢ Eq.{u_2 + 1} (α := R) ((↑((constantCoeff : (a : MvPowerSeries σ ↥T) → ↥T) (p.toSubring T hp)) : R) : R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) p : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
⊢ (map T.subtype : (a : MvPowerSeries σ ↥T) → MvPowerSeries σ R) (p.toSubring T hp) = p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionSemiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
simp :
  (∀ (n : σ →₀ ℕ),
      Eq.{u_3 + 1} (α := S)
        ((coeff n : (a : MvPowerSeries σ S) → S)
            ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
          S)
        ((coeff n : (a : MvPowerSeries σ S) → S) 0 : S)) ↔
    ∀ (n : σ →₀ ℕ),
      Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ Eq (α := MvPowerSeries σ S) ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S)
      (0 : MvPowerSeries σ S) ↔
    φ = 0

Tactic:
simp only [MvPowerSeries.ext_iff]

Premises used: MvPowerSeries.ext_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionSemiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
a :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := S)
        ((coeff n : (a : MvPowerSeries σ S) → S)
            ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
          S)
        ((coeff n : (a : MvPowerSeries σ S) → S) 0 : S) ↔
      Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ (∀ (n : σ →₀ ℕ),
      Eq.{u_3 + 1} (α := S)
        ((coeff n : (a : MvPowerSeries σ S) → S)
            ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
          S)
        ((coeff n : (a : MvPowerSeries σ S) → S) 0 : S)) ↔
    ∀ (n : σ →₀ ℕ),
      Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
congr! with n
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionSemiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := S)
      ((coeff n : (a : MvPowerSeries σ S) → S)
          ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
        S)
      ((coeff n : (a : MvPowerSeries σ S) → S) 0 : S) ↔
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
simp