awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
h :
  Eq (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g' : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ Eq (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
⊢ g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)

Tactic:
have H' := g'.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
⊢ (g * g').IsWeierstrassFactorization ((g * g').weierstrassDistinguished hg) ((g * g').weierstrassUnit hg)

Tactic:
have H'' := (g * g').isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
H'' : (g * g').IsWeierstrassFactorization ((g * g').weierstrassDistinguished hg) ((g * g').weierstrassUnit hg)
⊢ (g * g').weierstrassDistinguished hg =
    HMul.hMul (α := A[X]) (g.weierstrassDistinguished ⋯) (g'.weierstrassDistinguished ⋯)

Tactic:
(H''.elim (H.mul H')).1

Premises used: PowerSeries.IsWeierstrassFactorization.elim, And.left, PowerSeries.IsWeierstrassFactorizationAt.mul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
H'' : (g * g').IsWeierstrassFactorization ((g * g').weierstrassDistinguished hg) ((g * g').weierstrassUnit hg)
⊢ (g * g').weierstrassDistinguished hg =
    HMul.hMul (α := A[X]) (g.weierstrassDistinguished ⋯) (g'.weierstrassDistinguished ⋯)

Tactic:
exact (H''.elim (H.mul H')).1

Premises used: PowerSeries.IsWeierstrassFactorization.elim, And.left, PowerSeries.IsWeierstrassFactorizationAt.mul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
H'' : (g * g').IsWeierstrassFactorization ((g * g').weierstrassDistinguished hg) ((g * g').weierstrassUnit hg)
⊢ (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯

Tactic:
(H''.elim (H.mul H')).2

Premises used: PowerSeries.IsWeierstrassFactorization.elim, And.right, PowerSeries.IsWeierstrassFactorizationAt.mul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
H'' : (g * g').IsWeierstrassFactorization ((g * g').weierstrassDistinguished hg) ((g * g').weierstrassUnit hg)
⊢ (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯

Tactic:
exact (H''.elim (H.mul H')).2

Premises used: PowerSeries.IsWeierstrassFactorization.elim, And.right, PowerSeries.IsWeierstrassFactorizationAt.mul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g g' : A⟦X⟧
f : A[X]
h_1 : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
h :
  Eq (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ Eq (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)

Tactic:
simp [Algebra.smul_def, h]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
h :
  Eq (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ Eq (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)

Tactic:
simp [Algebra.smul_def, h]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)

Tactic:
have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [Algebra.smul_def, h]))
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
⊢ (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)

Tactic:
have H' := (a • g).isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
h :
  Eq (α := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) a : IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)
⊢ Eq (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)

Tactic:
simp [Algebra.smul_def, h]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
⊢ Ne (α := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) a : IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)

Tactic:
have ha : IsLocalRing.residue A a ≠ 0 := fun h ↦ hg (by simp [Algebra.smul_def, h])
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
ha :
  Ne (α := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) a : IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)
⊢ IsUnit a

Tactic:
simpa using ha
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
ha :
  Ne (α := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) a : IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)
⊢ (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯

Tactic:
exact (H'.elim (H.smul (by simpa using ha))).1

Premises used: PowerSeries.IsWeierstrassFactorization.elim, And.left, PowerSeries.IsWeierstrassFactorizationAt.smul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
ha :
  Ne (α := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) a : IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)
⊢ (a • g).weierstrassUnit hg = a • g.weierstrassUnit ⋯

Tactic:
exact (H'.elim (H.smul (by simpa using ha))).2

Premises used: PowerSeries.IsWeierstrassFactorization.elim, And.right, PowerSeries.IsWeierstrassFactorizationAt.smul
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
R : Type u_1
inst : Ring R
u : Rˣ
n : ℕ
⊢ (coeff n : (a : R⟦X⟧) → R) (invUnitsSub u) = 1 /ₚ u ^ (n + 1)

Tactic:
coeff_mk _ _

Premises used: PowerSeries.coeff_mk, PowerSeries.invUnitsSub
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
R : Type u_1
inst : Ring R
u : Rˣ
rw : (coeff 0 : (a : R⟦X⟧) → R) (invUnitsSub u) = 1 /ₚ u
rw₁ : 1 /ₚ u ^ HAdd.hAdd (α := ℕ) 0 1 = 1 /ₚ u
rw₂ : 1 /ₚ HPow.hPow (β := ℕ) u 1 = 1 /ₚ u
rw₃ rw₄ : 1 /ₚ u = 1 /ₚ u
⊢ (constantCoeff : (a : R⟦X⟧) → R) (invUnitsSub u) = 1 /ₚ u

Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_invUnitsSub, zero_add, pow_one]

Premises used: PowerSeries.coeff_invUnitsSub, zero_add, PowerSeries.coeff_zero_eq_constantCoeff_apply, pow_one
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
R : Type u_1
inst : Ring R
u : Rˣ
h :
  Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) (invUnitsSub u * X) : R)
    ((coeff 0 : (a : R⟦X⟧) → R) (HMul.hMul (β := R⟦X⟧) (invUnitsSub u) ((C : (a : R) → R⟦X⟧) (↑u : R) : R⟦X⟧) - 1) : R)
h₁ :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (invUnitsSub u * X) : R)
      ((coeff (n + 1) : (a : R⟦X⟧) → R)
          (HMul.hMul (β := R⟦X⟧) (invUnitsSub u) ((C : (a : R) → R⟦X⟧) (↑u : R) : R⟦X⟧) - 1) :
        R)
⊢ invUnitsSub u * X = HMul.hMul (β := R⟦X⟧) (invUnitsSub u) ((C : (a : R) → R⟦X⟧) (↑u : R) : R⟦X⟧) - 1

Tactic:
ext (_ | n)
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
R : Type u_1
inst : Ring R
u : Rˣ
⊢ Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) (invUnitsSub u * X) : R)
    ((coeff 0 : (a : R⟦X⟧) → R) (HMul.hMul (β := R⟦X⟧) (invUnitsSub u) ((C : (a : R) → R⟦X⟧) (↑u : R) : R⟦X⟧) - 1) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
R : Type u_1
inst : Ring R
u : Rˣ
n : ℕ
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (invUnitsSub u * X) : R)
    ((coeff (n + 1) : (a : R⟦X⟧) → R)
        (HMul.hMul (β := R⟦X⟧) (invUnitsSub u) ((C : (a : R) → R⟦X⟧) (↑u : R) : R⟦X⟧) - 1) :
      R)

Tactic:
simp [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
R : Type u_1
inst : Ring R
u : Rˣ
⊢ invUnitsSub u * HSub.hSub (α := R⟦X⟧) (β := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (↑u : R) : R⟦X⟧) X = 1

Tactic:
simp [mul_sub, sub_sub_cancel]

Premises used: mul_sub, sub_sub_cancel
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
u : Rˣ
h :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := S) ((coeff n : (a : S⟦X⟧) → S) ((map f : (a : R⟦X⟧) → S⟦X⟧) (invUnitsSub u) : S⟦X⟧) : S)
      ((coeff n : (a : S⟦X⟧) → S)
          (invUnitsSub (((Units.map (↑f : R →* S) : MonoidHom.{u_1, u_2} Rˣ Sˣ) : (a : Rˣ) → Sˣ) u)) :
        S)
⊢ Eq.{u_2 + 1} (α := S⟦X⟧) ((map f : (a : R⟦X⟧) → S⟦X⟧) (invUnitsSub u) : S⟦X⟧)
    (invUnitsSub (((Units.map (↑f : R →* S) : MonoidHom.{u_1, u_2} Rˣ Sˣ) : (a : Rˣ) → Sˣ) u) : S⟦X⟧)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
u : Rˣ
n : ℕ
h :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (↑(u ^ (n + 1))⁻¹ : R) : S)
    ((↑(((Units.map (↑f : R →* S) : MonoidHom.{u_1, u_2} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (u ^ (n + 1)))⁻¹ : S) : S)
⊢ Eq.{u_2 + 1} (α := S) ((coeff n : (a : S⟦X⟧) → S) ((map f : (a : R⟦X⟧) → S⟦X⟧) (invUnitsSub u) : S⟦X⟧) : S)
    ((coeff n : (a : S⟦X⟧) → S)
        (invUnitsSub (((Units.map (↑f : R →* S) : MonoidHom.{u_1, u_2} Rˣ Sˣ) : (a : Rˣ) → Sˣ) u)) :
      S)

Tactic:
simp only [← map_pow, coeff_map, coeff_invUnitsSub, one_divp]

Premises used: PowerSeries.coeff_invUnitsSub, map_pow, one_divp, PowerSeries.coeff_map
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
u : Rˣ
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (↑(u ^ (n + 1))⁻¹ : R) : S)
    ((↑(((Units.map (↑f : R →* S) : MonoidHom.{u_1, u_2} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (u ^ (n + 1)))⁻¹ : S) : S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
rw :
  ∀ (n : ℕ),
    Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S) ((coeff n : (a : S⟦X⟧) → S) 1 : S)
⊢ mk 1 * HSub.hSub (α := S⟦X⟧) 1 X = 1

Tactic:
rw [mul_comm, PowerSeries.ext_iff]

Premises used: PowerSeries.ext_iff, mul_comm
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
⊢ Eq (α := S) ((coeff 0 : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S) ((coeff 0 : (a : S⟦X⟧) → S) 1 : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
n : ℕ
⊢ Eq (α := S) ((coeff (n + 1) : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S)
    ((coeff (n + 1) : (a : S⟦X⟧) → S) 1 : S)

Tactic:
simp [sub_mul]

Premises used: sub_mul
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
n : ℕ
zero :
  Eq (α := S) ((coeff 0 : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S) ((coeff 0 : (a : S⟦X⟧) → S) 1 : S)
succ :
  ∀ (n : ℕ),
    Eq (α := S) ((coeff (n + 1) : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S)
      ((coeff (n + 1) : (a : S⟦X⟧) → S) 1 : S)
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S) ((coeff n : (a : S⟦X⟧) → S) 1 : S)

Tactic:
cases n with
  | zero => simp
  | succ n => simp [sub_mul]

Premises used: sub_mul
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
zero :
  ∀ (n : ℕ),
    Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HPow.hPow (α := S⟦X⟧) (mk 1) (HAdd.hAdd (α := ℕ) 0 1)) : S)
      ((coeff n : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((0 + n).choose 0) : S)) : S)
⊢ HPow.hPow (α := S⟦X⟧) (mk 1) (HAdd.hAdd (α := ℕ) 0 1) = mk fun (n : ℕ) ↦ (↑((0 + n).choose 0) : S)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d n : ℕ
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HPow.hPow (α := S⟦X⟧) (mk 1) (HAdd.hAdd (α := ℕ) 0 1)) : S)
    ((coeff n : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((0 + n).choose 0) : S)) : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
succ :
  ∀ (n : ℕ),
    Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1 + 1)) : S)
      ((coeff n : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)) : S)
⊢ HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1 + 1) = mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
n : ℕ
succ :
  Eq.{u_1 + 1} (α := S)
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := S) (β := S) ((coeff p.1 : (a : S⟦X⟧) → S) (mk 1) : S)
          ((coeff p.2 : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) : S) :
      S)
    ((coeff n : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)) : S)
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1 + 1)) : S)
    ((coeff n : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)) : S)

Tactic:
rw [pow_add, hd, pow_one, mul_comm, coeff_mul]

Premises used: pow_add, PowerSeries.coeff_mul, pow_one, mul_comm
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
n : ℕ
succ :
  Eq.{u_1 + 1} (α := S) (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (↑((d + x.2).choose d) : S))
    (↑((d + 1 + n).choose (d + 1)) : S)
⊢ Eq.{u_1 + 1} (α := S)
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := S) (β := S) ((coeff p.1 : (a : S⟦X⟧) → S) (mk 1) : S)
          ((coeff p.2 : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) : S) :
      S)
    ((coeff n : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)) : S)

Tactic:
simp_rw [coeff_mk, Pi.one_apply, one_mul]

Premises used: Pi.one_apply, PowerSeries.coeff_mk, one_mul
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
n : ℕ
succ :
  Eq.{u_1 + 1} (α := S) (↑(∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (d + x.2).choose d) : S)
    (↑((d + 1 + n).choose (d + 1)) : S)
⊢ Eq.{u_1 + 1} (α := S) (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (↑((d + x.2).choose d) : S))
    (↑((d + 1 + n).choose (d + 1)) : S)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
n : ℕ
succ : Eq.{u_1 + 1} (α := S) (↑((d + n + 1).choose (d + 1)) : S) (↑((d + 1 + n).choose (d + 1)) : S)
succ₁ succ₂ : Eq.{u_1 + 1} (α := S) (↑((d + 1 + n).choose (d + 1)) : S) (↑((d + 1 + n).choose (d + 1)) : S)
⊢ Eq.{u_1 + 1} (α := S) (↑(∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (d + x.2).choose d) : S)
    (↑((d + 1 + n).choose (d + 1)) : S)

Tactic:
rw [Finset.sum_antidiagonal_choose_add, add_right_comm]

Premises used: add_right_comm, Finset.sum_antidiagonal_choose_add