awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
simp :
  ∀ x < n,
    (x < n → ¬Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) (0 : σ →₀ ℕ)) →
      LE.le (α := ℕ) (1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) : ℕ)
⊢ ∀ x ∈ range n \ s,
    LE.le (α := ℕ) 1 ((fun (x : ℕ) ↦ ((degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) : ℕ)) x)

Tactic:
simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]

Premises used: and_imp, Finset.mem_range, Finset.mem_sdiff, Finset.mem_filter, not_and
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
i : ℕ
hi : i < n
hi' : i < n → ¬Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
rw : ¬Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
⊢ LE.le (α := ℕ) (1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) : ℕ)

Tactic:
rw [← not_lt, Nat.lt_one_iff, degree_eq_zero_iff]

Premises used: not_lt, Nat.lt_one_iff, Finsupp.degree_eq_zero_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
i : ℕ
hi : i < n
hi' : i < n → ¬Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
⊢ ¬Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)

Tactic:
hi' hi
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
i : ℕ
hi : i < n
hi' : i < n → ¬Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
⊢ ¬Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)

Tactic:
exact hi' hi
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
a : R
φ : MvPowerSeries σ A
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := A)
      ((coeff n : (a : MvPowerSeries σ A) → A)
          (HMul.hMul (α := MvPowerSeries σ A)
            ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ A) a : MvPowerSeries σ A) φ) :
        A)
      ((coeff n : (a : MvPowerSeries σ A) → A)
          (HMul.hMul (β := MvPowerSeries σ A) φ
            ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ A) a : MvPowerSeries σ A)) :
        A)
⊢ HMul.hMul (α := MvPowerSeries σ A)
      ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ A) a : MvPowerSeries σ A) φ =
    HMul.hMul (β := MvPowerSeries σ A) φ
      ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ A) a : MvPowerSeries σ A)

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
a : R
φ : MvPowerSeries σ A
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := A)
    ((coeff n : (a : MvPowerSeries σ A) → A)
        (HMul.hMul (α := MvPowerSeries σ A)
          ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ A) a : MvPowerSeries σ A) φ) :
      A)
    ((coeff n : (a : MvPowerSeries σ A) → A)
        (HMul.hMul (β := MvPowerSeries σ A) φ
          ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ A) a : MvPowerSeries σ A)) :
      A)

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ_1 : 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
a : R
σ : MvPowerSeries σ_1 A
h :
  ∀ (n : σ_1 →₀ ℕ),
    Eq.{u_3 + 1} (α := A) ((coeff n : (a : MvPowerSeries σ_1 A) → A) (a • σ) : A)
      ((coeff n : (a : MvPowerSeries σ_1 A) → A)
          (HMul.hMul (α := MvPowerSeries σ_1 A)
            ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ_1 A) a : MvPowerSeries σ_1 A) σ) :
        A)
⊢ a • σ =
    HMul.hMul (α := MvPowerSeries σ_1 A)
      ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ_1 A) a : MvPowerSeries σ_1 A) σ

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ_1 : 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
a : R
σ : MvPowerSeries σ_1 A
n : σ_1 →₀ ℕ
⊢ Eq.{u_3 + 1} (α := A) ((coeff n : (a : MvPowerSeries σ_1 A) → A) (a • σ) : A)
    ((coeff n : (a : MvPowerSeries σ_1 A) → A)
        (HMul.hMul (α := MvPowerSeries σ_1 A)
          ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ_1 A) a : MvPowerSeries σ_1 A) σ) :
      A)

Tactic:
simp [(coeff A n).map_smul_of_tower a, Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
⊢ Eq (α := R →+* MvPowerSeries σ R) C (algebraMap R (MvPowerSeries σ R))

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl, MvPowerSeries.C
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Eq (α := MvPowerSeries σ A)
    ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ A) r : MvPowerSeries σ A)
    ((C : (a : A) → MvPowerSeries σ A) ((algebraMap R A : (a : R) → A) r) : MvPowerSeries σ A)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
φ : A →ₐ[R] B
r : R
⊢ Eq (α := MvPowerSeries σ B)
    (OneHom.toFun
      (↑(↑(map (↑φ : A →+* B)) : MvPowerSeries σ A →* MvPowerSeries σ B) :
        OneHom (MvPowerSeries σ A) (MvPowerSeries σ B))
      ((algebraMap R (MvPowerSeries σ A) : (a : R) → MvPowerSeries σ A) r))
    ((algebraMap R (MvPowerSeries σ B) : (a : R) → MvPowerSeries σ B) r)

Tactic:
simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
      MonoidHom.coe_coe, MvPowerSeries.algebraMap_apply, map_C, RingHom.coe_coe, AlgHom.commutes]

Premises used: RingHom.coe_coe, RingHom.toMonoidHom_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe, AlgHom.commutes, MvPowerSeries.algebraMap_apply, MvPowerSeries.map_C, OneHom.toFun_eq_coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
φ : A →ₐ[R] B
f : MvPowerSeries σ A
⊢ Eq (α := MvPowerSeries σ B) ((mapAlgHom φ : (a : MvPowerSeries σ A) → MvPowerSeries σ B) f : MvPowerSeries σ B)
    ((map (↑φ : A →+* B) : (a : MvPowerSeries σ A) → MvPowerSeries σ B) f : MvPowerSeries σ B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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 :
  ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
⊢ Ne (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤

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

Premises used: Ne, SetLike.ext_iff, Classical.not_forall
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
inhabit :
  ∀ (inhabited_h : Inhabited σ),
    ∃ (x : MvPowerSeries σ R),
      ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
          Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
⊢ ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)

Tactic:
inhabit σ
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
inhabited_h : Inhabited σ
⊢ ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)

Tactic:
⟨X default, ?_⟩

Premises used: Inhabited.default, MvPowerSeries.X, Exists.intro
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
inhabited_h : Inhabited σ
refine :
  ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ (X default) ↔
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ (X default))
⊢ ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)

Tactic:
refine ⟨X default, ?_⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
inhabited_h : Inhabited σ
simp :
  ∀ (x : R),
    ¬Eq (α := MvPowerSeries σ R)
        ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R)
        (X default : MvPowerSeries σ R)
⊢ ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ (X default) ↔
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ (X default))

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

Premises used: Algebra.mem_top, Set.mem_range, Algebra.mem_bot, iff_true, not_exists
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
inhabited_h : Inhabited σ
x : R
rw :
  ∃ (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)
⊢ ¬Eq (α := MvPowerSeries σ R) ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R)
      (X default : MvPowerSeries σ R)

Tactic:
rw [MvPowerSeries.ext_iff, not_forall]

Premises used: MvPowerSeries.ext_iff, Classical.not_forall
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
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:
⟨Finsupp.single default 1, ?_⟩

Premises used: Inhabited.default, Exists.intro, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
inhabited_h : Inhabited σ
x : R
refine :
  ¬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)
⊢ ∃ (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:
refine ⟨Finsupp.single default 1, ?_⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
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:
simp [algebraMap_apply, coeff_C]

Premises used: MvPowerSeries.coeff_C, MvPowerSeries.algebraMap_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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)
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)
⊢ Ne (α := Subalgebra R (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]

Premises used: Algebra.mem_top, Set.mem_range, Algebra.mem_bot, MvPowerSeries.ext_iff, iff_true, not_exists, Ne, SetLike.ext_iff, MvPowerSeries.coeff_C, MvPowerSeries.algebraMap_apply, Classical.not_forall
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
⊢ (↑φ : MvPowerSeries σ R) = fun (n : σ →₀ ℕ) ↦ coeff n φ

Tactic:
rfl

Premises used: MvPolynomial.toMvPowerSeries, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
n : σ →₀ ℕ
⊢ (MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (↑φ : MvPowerSeries σ R) = coeff n φ

Tactic:
rfl

Premises used: MvPolynomial.toMvPowerSeries, MvPolynomial.coeff, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
rw : (if n = m then a else 0) = if m = n then a else 0
⊢ 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)

Tactic:
rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]

Premises used: MvPolynomial.coeff_coe, MvPowerSeries.coeff_monomial, MvPolynomial.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
neg₁ : ∀ (h₁ : ¬n = m), ¬m = n → Eq.{u_2 + 1} (α := R) 0 0
⊢ (if n = m then a else 0) = if m = n then a else 0

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : n = m
h₂ : m = n
⊢ a = a

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : n = m
h₂ : m = n
⊢ a = a

Tactic:
first | rfl | subst m; contradiction
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : n = m
h₂ : ¬m = n
⊢ ¬n = n

Tactic:
subst m
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
h₂ : ¬n = n
⊢ a = 0

Tactic:
contradiction
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : n = m
h₂ : ¬m = n
neg neg₁ : ∀ (h₂ : ¬n = n), a = 0
⊢ a = 0

Tactic:
first | rfl | subst m; contradiction
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h : m = n
⊢ ¬n = n

Tactic:
subst m
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
h₁ : ¬n = n
⊢ 0 = a

Tactic:
contradiction
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h : m = n
pos pos₁ : ∀ (h₁ : ¬n = n), 0 = a
⊢ 0 = a

Tactic:
first | rfl | subst m; contradiction
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h : ¬m = n
⊢ Eq.{u_2 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h : ¬m = n
⊢ Eq.{u_2 + 1} (α := R) 0 0

Tactic:
first | rfl | subst m; contradiction
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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)
rw₂ rw₃ rw₄ : (if n = m then a else 0) = if m = n then a else 0
⊢ 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)

Tactic:
classical
    rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]
    split_ifs with h₁ h₂ <;> first | rfl | subst m; contradiction

Premises used: MvPolynomial.coeff_coe, MvPowerSeries.coeff_monomial, MvPolynomial.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
⊢ Eq (α := MvPowerSeries σ R) (↑0 : MvPowerSeries σ R) 0

Tactic:
rfl

Premises used: MvPolynomial.toMvPowerSeries, MvPolynomial.coeff, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
⊢ Eq (α := MvPowerSeries σ R) (↑1 : MvPowerSeries σ R) 1

Tactic:
coe_monomial _ _

Premises used: MvPolynomial.coe_monomial, Finsupp.single