awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
⊢ Eq (α := ℕ) ((constantCoeff : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ) (1 : ℕ)

Tactic:
simp only [← coeff_zero_eq_constantCoeff_apply, coeff_largeSchroderSeries, largeSchroder_zero]

Premises used: PowerSeries.coeff_largeSchroderSeries, PowerSeries.coeff_zero_eq_constantCoeff_apply, Nat.largeSchroder_zero
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
simp :
  ∑ k ∈ range (n + 1), HMul.hMul (α := ℕ) ((coeff k : (a : ℕ⟦X⟧) → ℕ) X : ℕ) (n - k).largeSchroder =
    (n - 1).largeSchroder
⊢ (coeff n : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) = (n - 1).largeSchroder

Tactic:
simp only [coeff_mul, coeff_largeSchroderSeries,
    Nat.sum_antidiagonal_eq_sum_range_succ (coeff · X * largeSchroder ·),
    succ_eq_add_one]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, Nat.largeSchroder, HMul.hMul, Nat.succ_eq_add_one, PowerSeries.coeff, PowerSeries.coeff_largeSchroderSeries, PowerSeries.X, PowerSeries.coeff_mul, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
simp : n = 0 → 0 = (n - 1).largeSchroder
⊢ ∑ k ∈ range (n + 1), HMul.hMul (α := ℕ) ((coeff k : (a : ℕ⟦X⟧) → ℕ) X : ℕ) (n - k).largeSchroder =
    (n - 1).largeSchroder

Tactic:
simp only [coeff_X, ite_mul, one_mul, zero_mul, sum_ite_eq', mem_range, lt_add_iff_pos_left,
    ite_eq_left_iff, not_lt, nonpos_iff_eq_zero]

Premises used: Finset.sum_ite_eq', ite_eq_left_iff, MulZeroClass.zero_mul, Finset.mem_range, PowerSeries.coeff_X, not_lt, ite_mul, lt_add_iff_pos_left, one_mul, nonpos_iff_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
hn : LT.lt (α := ℕ) 0 0
⊢ 0 = (HSub.hSub (α := ℕ) 0 1).largeSchroder

Tactic:
simp_all only [lt_self_iff_false]

Premises used: lt_self_iff_false
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
rw :
  Eq (α := ℕ)
    (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := ℕ) (β := ℕ) ((coeff p.1 : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
        ((coeff p.2 : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ))
    (∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder)
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
    (∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder : ℕ)

Tactic:
rw [pow_two, ← mul_assoc, coeff_mul]

Premises used: pow_two, mul_assoc, PowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
rw :
  ∑ x ∈ range n,
        HMul.hMul (α := ℕ) (β := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
          ((coeff (n - x) : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ) +
      HMul.hMul (α := ℕ) (β := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
        ((coeff (n - n) : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ) =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
⊢ Eq (α := ℕ)
    (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := ℕ) (β := ℕ) ((coeff p.1 : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
        ((coeff p.2 : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ))
    (∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder)

Tactic:
rw [Nat.sum_antidiagonal_eq_sum_range_succ
    (fun x y => (coeff x) (X * largeSchroderSeries) * (coeff y) largeSchroderSeries) n,
    Nat.succ_eq_add_one, sum_range_succ]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, HMul.hMul, Nat.succ_eq_add_one, PowerSeries.largeSchroderSeries, PowerSeries.coeff, PowerSeries.X, DFunLike.coe, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
simp :
  ∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder +
      (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
⊢ ∑ x ∈ range n,
        HMul.hMul (α := ℕ) (β := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
          ((coeff (n - x) : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ) +
      HMul.hMul (α := ℕ) (β := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
        ((coeff (n - n) : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ) =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
simp only [coeff_largeSchroderSeries, coeff_X_mul_largeSchroderSeries n hn, tsub_self,
    largeSchroder_zero, mul_one]

Premises used: PowerSeries.coeff_X_mul_largeSchroderSeries, tsub_self, PowerSeries.coeff_largeSchroderSeries, Nat.largeSchroder_zero, mul_one
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
apply :
  ∀ x ∈ range n,
    HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
      if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
⊢ Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
x : ℕ
a : x ∈ range n
⊢ x < n

Tactic:
simp_all only [mem_range]

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
x : ℕ
a : x < n
isTrue :
  0 < x →
    HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
      (x - 1).largeSchroder * (n - x).largeSchroder
isFalse :
  ¬0 < x → HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder = 0
⊢ HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
    if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0

Tactic:
split
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h : 0 < x
simp_all : (coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) = (x - 1).largeSchroder ∨ (n - x).largeSchroder = 0
⊢ HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
    (x - 1).largeSchroder * (n - x).largeSchroder

Tactic:
simp_all only [mul_eq_mul_right_iff]

Premises used: mul_eq_mul_right_iff
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h : 0 < x
⊢ 0 < x

Tactic:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h : 0 < x
⊢ (coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) = (x - 1).largeSchroder ∨ (n - x).largeSchroder = 0

Tactic:
simp [coeff_X_mul_largeSchroderSeries x (by lia)]

Premises used: PowerSeries.coeff_X_mul_largeSchroderSeries
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h : 0 < x
⊢ HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
    (x - 1).largeSchroder * (n - x).largeSchroder

Tactic:
next h =>
      simp_all only [mul_eq_mul_right_iff]
      simp [coeff_X_mul_largeSchroderSeries x (by lia)]

Premises used: PowerSeries.coeff_X_mul_largeSchroderSeries, mul_eq_mul_right_iff
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h : ¬0 < x
⊢ HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder = 0

Tactic:
simp_all only [not_lt, nonpos_iff_eq_zero, coeff_zero_eq_constantCoeff, map_mul,
      constantCoeff_X, constantCoeff_largeSchroderSeries, mul_one, tsub_zero, zero_mul]

Premises used: PowerSeries.constantCoeff_X, MulZeroClass.zero_mul, tsub_zero, PowerSeries.constantCoeff_largeSchroderSeries, map_mul, not_lt, PowerSeries.coeff_zero_eq_constantCoeff, mul_one, nonpos_iff_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
⊢ Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)

Tactic:
have : ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * largeSchroder (n - x) =
      ∑ x ∈ range n, if 0 < x then largeSchroder (x - 1) * largeSchroder (n - x) else 0 := by
    apply sum_congr rfl
    intro x a
    simp_all only [mem_range]
    split
    next h =>
      simp_all only [mul_eq_mul_right_iff]
      simp [coeff_X_mul_largeSchroderSeries x (by lia)]
    next h =>
      simp_all only [not_lt, nonpos_iff_eq_zero, coeff_zero_eq_constantCoeff, map_mul,
      constantCoeff_X, constantCoeff_largeSchroderSeries, mul_one, tsub_zero, zero_mul]
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
rw :
  ((if LT.lt (α := ℕ) 0 0 then (HSub.hSub (α := ℕ) 0 1).largeSchroder * (n - 0).largeSchroder else 0) +
        ∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) +
      (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
⊢ ∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder +
      (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
rw [this, sum_range_eq_add_Ico _ (by lia)]

Premises used: Finset.sum_range_eq_add_Ico
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
simp :
  (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) + (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
⊢ ((if LT.lt (α := ℕ) 0 0 then (HSub.hSub (α := ℕ) 0 1).largeSchroder * (n - 0).largeSchroder else 0) +
        ∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) +
      (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
simp only [lt_self_iff_false, reduceIte, zero_add]

Premises used: zero_add, lt_self_iff_false, reduceIte
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
apply :
  ∀ x ∈ Ico 1 n,
    (if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) = (x - 1).largeSchroder * (n - x).largeSchroder
⊢ Eq (α := ℕ) (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
    (∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
x : ℕ
hx : x ∈ Ico 1 n
⊢ 0 < x

Tactic:
grind
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
x : ℕ
hx : x ∈ Ico 1 n
⊢ 0 < x

Tactic:
have hx' : 0 < x := by grind
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
x : ℕ
hx : x ∈ Ico 1 n
hx' : 0 < x
rw rw₁ : (x - 1).largeSchroder * (n - x).largeSchroder = (x - 1).largeSchroder * (n - x).largeSchroder
⊢ (if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) = (x - 1).largeSchroder * (n - x).largeSchroder

Tactic:
rw [if_pos hx']

Premises used: if_pos
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
⊢ Eq (α := ℕ) (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
    (∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder)

Tactic:
have : (∑ x ∈ Ico 1 n, if 0 < x then largeSchroder (x - 1) * largeSchroder (n - x) else 0) =
    ∑ x ∈ Ico 1 n, largeSchroder (x - 1) * largeSchroder (n - x) := by
    apply sum_congr rfl
    intros x hx
    have hx' : 0 < x := by grind
    rw [if_pos hx']
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
this_1 :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
this :
  Eq (α := ℕ) (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
    (∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder)
⊢ n = n - 1 + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
this_1 :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
this :
  Eq (α := ℕ) (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
    (∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder)
rw :
  ∑ k ∈ range (n - 1 + 1 - 1), (1 + k - 1).largeSchroder * (n - 1 + 1 - (1 + k)).largeSchroder +
      (n - 1 + 1 - 1).largeSchroder =
    ∑ x ∈ range (n - 1), x.largeSchroder * (n - 1 + 1 - 1 - x).largeSchroder +
      (n - 1).largeSchroder * (n - 1 + 1 - 1 - (n - 1)).largeSchroder
⊢ (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) + (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
rw [this, sum_Ico_eq_sum_range, show n = n - 1 + 1 by lia,
    sum_range_succ]

Premises used: Finset.sum_Ico_eq_sum_range, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : 0 < n
this_1 :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
this :
  Eq (α := ℕ) (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
    (∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder)
⊢ ∑ k ∈ range (n - 1 + 1 - 1), (1 + k - 1).largeSchroder * (n - 1 + 1 - (1 + k)).largeSchroder +
      (n - 1 + 1 - 1).largeSchroder =
    ∑ x ∈ range (n - 1), x.largeSchroder * (n - 1 + 1 - 1 - x).largeSchroder +
      (n - 1).largeSchroder * (n - 1 + 1 - 1 - (n - 1)).largeSchroder

Tactic:
grind [largeSchroder_zero]

Premises used: Nat.largeSchroder_zero
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
h :
  ∀ (n : ℕ),
    Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
      ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
⊢ largeSchroderSeries = 1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
pos :
  ∀ (hn : n = 0),
    Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
      ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
neg :
  ∀ (hn : ¬n = 0),
    Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
      ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : n = 0
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)

Tactic:
aesop
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : ¬n = 0
⊢ 0 < n

Tactic:
omega
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : ¬n = 0
⊢ 0 < n

Tactic:
have hn' : 0 < n := by omega
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : ¬n = 0
hn' : 0 < n
neg :
  n.largeSchroder =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
      ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)

Tactic:
simp only [coeff_largeSchroderSeries, map_add, coeff_one, hn, ↓reduceIte, zero_add]

Premises used: map_add, PowerSeries.coeff_largeSchroderSeries, zero_add, PowerSeries.coeff_one, reduceIte
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ n = n - 1 + 1

Tactic:
omega
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : ¬n = 0
hn' : 0 < n
neg :
  (n - 1).largeSchroder + ∑ i ∈ Iic (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder =
    (n - 1 + 1 - 1).largeSchroder + ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 + 1 - 1 - i).largeSchroder
⊢ n.largeSchroder =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
      ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)

Tactic:
rw [coeff_X_mul_largeSchroderSeriesSeries_sq _ hn', coeff_X_mul_largeSchroderSeries _ hn',
      show n = n - 1 + 1 by omega, largeSchroder_succ (n - 1)]

Premises used: PowerSeries.coeff_X_mul_largeSchroderSeries, Nat.largeSchroder_succ, PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : ¬n = 0
hn' : 0 < n
neg :
  Eq (α := ℕ) (∑ i ∈ Iic (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
    (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
⊢ (n - 1).largeSchroder + ∑ i ∈ Iic (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder =
    (n - 1 + 1 - 1).largeSchroder + ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 + 1 - 1 - i).largeSchroder

Tactic:
simp only [add_tsub_cancel_right, Nat.add_left_cancel_iff]

Premises used: Nat.add_left_cancel_iff, add_tsub_cancel_right
-- Module: Mathlib.RingTheory.PowerSeries.Schroder
Goal:
n : ℕ
hn : ¬n = 0
hn' : 0 < n
neg :
  Eq (α := ℕ) (∑ i ∈ Icc ⊥ (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
    (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
neg₁ :
  Eq (α := ℕ) (∑ i ∈ Icc 0 (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
    (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
neg₂ neg₃ :
  Eq (α := ℕ) (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
    (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
⊢ Eq (α := ℕ) (∑ i ∈ Iic (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
    (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)

Tactic:
rw [Iic_eq_Icc, Nat.bot_eq_zero, ← range_succ_eq_Icc_zero]

Premises used: Finset.Iic_eq_Icc, Nat.range_succ_eq_Icc_zero, Nat.bot_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
a : MvPowerSeries τ S
⊢ HasSubst a ↔ MvPowerSeries.HasSubst (Function.const Unit a)

Tactic:
⟨fun ha ↦ MvPowerSeries.hasSubst_of_constantCoeff_nilpotent (Function.const Unit ha),
   fun ha ↦ (ha.const_coeff ())⟩

Premises used: Unit.unit, MvPowerSeries.hasSubst_of_constantCoeff_nilpotent, MvPowerSeries.HasSubst.const_coeff, Unit, Iff.intro, Function.const
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
a : MvPowerSeries τ S
ha : HasSubst a
⊢ MvPowerSeries.HasSubst.{0, u_3, u_4} (τ := τ) (S := S) fun (x : Unit) ↦ a

Tactic:
hasSubst_iff.mp ha

Premises used: PowerSeries.hasSubst_iff, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : DiscreteTopology S
a : MvPowerSeries τ S
rw : MvPowerSeries.HasSubst (Function.const Unit a) ↔ HasEval a
rw₁ : MvPowerSeries.HasEval (Function.const Unit a) ↔ HasEval a
rw₂ : MvPowerSeries.HasEval (Function.const Unit a) ↔ MvPowerSeries.HasEval (S := MvPowerSeries τ S) fun (x : Unit) ↦ a
rw₃ rw₄ : MvPowerSeries.HasEval (Function.const Unit a) ↔ MvPowerSeries.HasEval (Function.const Unit a)
⊢ HasSubst a ↔ HasEval a

Tactic:
rw [hasSubst_iff, MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, hasEval_iff,
    Function.const_def]

Premises used: MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, PowerSeries.hasSubst_iff, Function.const_def, PowerSeries.hasEval_iff
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : TopologicalSpace S
a : MvPowerSeries τ S
ha : HasSubst a
⊢ HasEval a

Tactic:
isTopologicallyNilpotent_of_constantCoeff_isNilpotent ha

Premises used: MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
a : MvPowerSeries τ S
ha : Eq.{u_4 + 1} (α := S) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S) a : S) (0 : S)
⊢ HasSubst a

Tactic:
simp [HasSubst, ha]

Premises used: PowerSeries.HasSubst
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
S : Type u_4
inst : CommRing S
a : S⟦X⟧
ha : Eq (α := S) ((constantCoeff : (a : S⟦X⟧) → S) a : S) (0 : S)
⊢ HasSubst a

Tactic:
HasSubst.of_constantCoeff_zero ha

Premises used: PowerSeries.HasSubst.of_constantCoeff_zero
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
t : τ
⊢ HasSubst.{u_3, u_4} (S := S) (MvPowerSeries.X t)

Tactic:
simp [HasSubst]

Premises used: PowerSeries.HasSubst
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
⊢ HasSubst.{0, u_2} (S := R) X

Tactic:
HasSubst.X _

Premises used: PowerSeries.X, PowerSeries.HasSubst.X
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
n : ℕ
hn : n ≠ 0
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) (0 : R)

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
n : τ →₀ ℕ
hn : n ≠ 0
s : S
ha :
  Eq.{u_4 + 1} (α := S)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S)
        ((MvPowerSeries.monomial n : (a : S) → MvPowerSeries τ S) s : MvPowerSeries τ S) :
      S)
    (0 : S)
⊢ HasSubst.{u_3, u_4} (τ := τ) (S := S) ((MvPowerSeries.monomial n : (a : S) → MvPowerSeries τ S) s)

Tactic:
apply HasSubst.of_constantCoeff_zero

Premises used: PowerSeries.HasSubst.of_constantCoeff_zero