awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
S' : Type u_7
inst_2 : CommRing S'
inst_3 : Algebra A S
inst_4 : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A (pb.map e).gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval (pb.map e).gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
x : S
⊢ Eq.{u_7 + 1} (α := S') ((pb.equivOfRoot (pb.map e) h₁ h₂ : (a : S) → S') x : S') ((e : (a : S) → S') x : S')
have h : ∀ (f : A[X]),
  Eq.{u_7 + 1} (α := S') ((pb.equivOfRoot (pb.map e) h₁ h₂ : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) f : S) : S')
    ((e : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) f : S) : S')
Tactic: obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
B : PowerBasis R S
⊢ Eq (α := Subalgebra R S) R[B.gen] ⊤
have rw : Set.range (ι := Fin B.dim) (⇑B.basis : (a : Fin B.dim) → S) ⊆
  (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[B.gen] : Submodule R S) : Set S)
Tactic: rw [← toSubmodule_eq_top, _root_.eq_top_iff, ← B.basis.span_eq, Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
B : PowerBasis R S
i : Fin B.dim
⊢ Membership.mem (α := S)
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[B.gen] : Submodule R S) : Set S)
    ((B.basis : (a : Fin B.dim) → S) i : S)
have rw : B.gen ^ (↑i : ℕ) ∈ (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[B.gen] : Submodule R S) : Set S)
Tactic: rw [B.basis_eq_pow i]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
B : PowerBasis R S
x : S
hx : Membership.mem (γ := Subalgebra R S) R[x] B.gen
⊢ Eq (α := Subalgebra R S) R[x] ⊤
have rw : LE.le (α := Subalgebra R S) R[B.gen] R[x]
Tactic: rw [_root_.eq_top_iff, ← B.adjoin_gen_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
B : PowerBasis R S
x : S
hx : Membership.mem (γ := Subalgebra R S) R[x] B.gen
⊢ LE.le (α := Subalgebra R S) R[B.gen] R[x]
have refine : {B.gen} ⊆ (↑R[x] : Set S)
Tactic: refine adjoin_le ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : BinomialRing R
inst_2 : Ring A
inst_3 : Algebra R A
r s : R
⊢ binomialSeries A (r + s) = binomialSeries A r * binomialSeries A s
have h : ∀ (n : ℕ),
  Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (binomialSeries A (r + s)) : A)
    ((coeff n : (a : A⟦X⟧) → A) (binomialSeries A r * binomialSeries A s) : A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : BinomialRing R
inst_2 : Ring A
inst_3 : Algebra R A
r s : R
n : ℕ
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (binomialSeries A (r + s)) : A)
    ((coeff n : (a : A⟦X⟧) → A) (binomialSeries A r * binomialSeries A s) : A)
have h : Eq.{u_2 + 1} (α := A)
  (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ n, HSMul.hSMul (β := A) (Ring.choose r i.1 * Ring.choose s i.2) 1)
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, Ring.choose s x.2 • HSMul.hSMul (β := A) (Ring.choose r x.1) 1)
Tactic: simp only [binomialSeries_coeff, Ring.add_choose_eq n (Commute.all r s), coeff_mul,
    Algebra.mul_smul_comm, mul_one, sum_smul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : BinomialRing R
inst_2 : Ring A
inst_3 : Algebra R A
r s : R
n : ℕ
⊢ Eq.{u_2 + 1} (α := A)
    (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ n, HSMul.hSMul (β := A) (Ring.choose r i.1 * Ring.choose s i.2) 1)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, Ring.choose s x.2 • HSMul.hSMul (β := A) (Ring.choose r x.1) 1)
have h : ∀ (ab : ℕ × ℕ) (hab : ab ∈ @antidiagonal _ Nat.instAddMonoid _ n),
  HSMul.hSMul (β := A) (Ring.choose r ab.1 * Ring.choose s ab.2) 1 =
    Ring.choose s ab.2 • HSMul.hSMul (β := A) (Ring.choose r ab.1) 1
Tactic: refine sum_congr rfl fun ab hab => ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : BinomialRing R
inst_2 : Ring A
inst_3 : Algebra R A
r s : R
n : ℕ
ab : ℕ × ℕ
hab : ab ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ HSMul.hSMul (β := A) (Ring.choose r ab.1 * Ring.choose s ab.2) 1 =
    Ring.choose s ab.2 • HSMul.hSMul (β := A) (Ring.choose r ab.1) 1
have h : HSMul.hSMul (β := A) (Ring.choose s ab.2 * Ring.choose r ab.1) 1 =
  Ring.choose s ab.2 • HSMul.hSMul (β := A) (Ring.choose r ab.1) 1
Tactic: rw [mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : BinomialRing R
inst_2 : Ring A
inst_3 : Algebra R A
r s : R
n : ℕ
ab : ℕ × ℕ
hab : ab ∈ @antidiagonal _ Nat.instAddMonoid _ n
h :
  HSMul.hSMul (β := A) (Ring.choose s ab.2 * Ring.choose r ab.1) 1 =
    Ring.choose s ab.2 • HSMul.hSMul (β := A) (Ring.choose r ab.1) 1
⊢ HSMul.hSMul (β := A) (Ring.choose r ab.1 * Ring.choose s ab.2) 1 =
    Ring.choose s ab.2 • HSMul.hSMul (β := A) (Ring.choose r ab.1) 1
have h₁ : Ring.choose s ab.2 • HSMul.hSMul (β := A) (Ring.choose r ab.1) 1 =
  Ring.choose s ab.2 • HSMul.hSMul (β := A) (Ring.choose r ab.1) 1
Tactic: rw [mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : BinomialRing R
inst_2 : Ring A
inst_3 : Algebra R A
d : ℕ
⊢ binomialSeries.{u_1, u_2} (R := R) A (↑d : R) = HAdd.hAdd (α := A⟦X⟧) 1 X ^ d
have h : ∀ (n : ℕ),
  Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (binomialSeries.{u_1, u_2} (R := R) A (↑d : R)) : A)
    ((coeff n : (a : A⟦X⟧) → A) (HAdd.hAdd (α := A⟦X⟧) 1 X ^ d) : A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : BinomialRing R
inst_2 : Ring A
inst_3 : Algebra R A
d n : ℕ
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (binomialSeries.{u_1, u_2} (R := R) A (↑d : R)) : A)
    ((coeff n : (a : A⟦X⟧) → A) (HAdd.hAdd (α := A⟦X⟧) 1 X ^ d) : A)
have hright : HAdd.hAdd (α := A⟦X⟧) 1 X ^ d = (↑(HAdd.hAdd (α := Polynomial A) 1 Polynomial.X ^ d) : A⟦X⟧)
Tactic: have hright : (1 + X) ^ d = (((1 : Polynomial A) + (Polynomial.X)) ^ d).toPowerSeries := by
    simp
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : BinomialRing R
inst_2 : Ring A
inst_3 : Algebra R A
d n : ℕ
hright : HAdd.hAdd (α := A⟦X⟧) 1 X ^ d = (↑(HAdd.hAdd (α := Polynomial A) 1 Polynomial.X ^ d) : A⟦X⟧)
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (binomialSeries.{u_1, u_2} (R := R) A (↑d : R)) : A)
    ((coeff n : (a : A⟦X⟧) → A) (HAdd.hAdd (α := A⟦X⟧) 1 X ^ d) : A)
have h : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) (Ring.choose (↑d : R) n) 1 = (↑(d.choose n) : A)
Tactic: rw [hright, Polynomial.coeff_coe, binomialSeries_coeff, Polynomial.coeff_one_add_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
A : Type u_2
inst : CommRing A
d : ℕ
⊢ (rescale (-1) : (a : A⟦X⟧) → A⟦X⟧) (↑(invOneSubPow A d) : A⟦X⟧) = binomialSeries (R := ℤ) A (-(↑d : ℤ))
have h : ∀ (n : ℕ),
  Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((rescale (-1) : (a : A⟦X⟧) → A⟦X⟧) (↑(invOneSubPow A d) : A⟦X⟧) : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) (binomialSeries (R := ℤ) A (-(↑d : ℤ))) : A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
A : Type u_2
inst : CommRing A
d n : ℕ
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((rescale (-1) : (a : A⟦X⟧) → A⟦X⟧) (↑(invOneSubPow A d) : A⟦X⟧) : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) (binomialSeries (R := ℤ) A (-(↑d : ℤ))) : A)
have h : HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A d) : A⟦X⟧) : A) =
  HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑d : ℤ)) n) 1
Tactic: rw [coeff_rescale, binomialSeries_coeff, ← Int.cast_negOnePow_natCast, ← zsmul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
A : Type u_2
inst : CommRing A
n : ℕ
⊢ HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A 0) : A⟦X⟧) : A) =
    HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑0 : ℤ)) n) 1
have pos : ∀ (hn : n = 0),
  HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A 0) : A⟦X⟧) : A) =
    HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑0 : ℤ)) n) 1
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
A : Type u_2
inst : CommRing A
n : ℕ
pos :
  ∀ (hn : n = 0),
    HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A 0) : A⟦X⟧) : A) =
      HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑0 : ℤ)) n) 1
⊢ HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A 0) : A⟦X⟧) : A) =
    HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑0 : ℤ)) n) 1
have neg : ∀ (hn : ¬n = 0),
  HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A 0) : A⟦X⟧) : A) =
    HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑0 : ℤ)) n) 1
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
A : Type u_2
inst : CommRing A
n d : ℕ
⊢ HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ)
      ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A (d + 1)) : A⟦X⟧) : A) =
    HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑(d + 1) : ℤ)) n) 1
have h : HMul.hMul (α := A) (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : A) (↑((d + n).choose d) : A) =
  (↑(Ring.choose (HAdd.hAdd (α := ℤ) (-1) (-(↑d : ℤ))) n) : A)
Tactic: simp only [invOneSubPow, coeff_mk, Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg,
      zsmul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
A : Type u_2
inst : CommRing A
n d : ℕ
⊢ HMul.hMul (α := A) (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : A) (↑((d + n).choose d) : A) =
    (↑(Ring.choose (HAdd.hAdd (α := ℤ) (-1) (-(↑d : ℤ))) n) : A)
have h : HMul.hMul (α := A) (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : A) (↑((d + n).choose n) : A) =
  (↑(HSMul.hSMul (β := ℤ) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) (↑((d + n).choose n) : ℤ)) : A)
Tactic: rw [show (-1 : ℤ) + -d = -(d + 1) by abel, Ring.choose_neg, Nat.choose_symm_add, Units.smul_def,
      show (d : ℤ) + 1 + n - 1 = d + n by lia, ← Nat.cast_add, Ring.choose_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
A : Type u_2
inst : CommRing A
n d : ℕ
⊢ HMul.hMul (α := A) (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : A) (↑((d + n).choose n) : A) =
    (↑(HSMul.hSMul (β := ℤ) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) (↑((d + n).choose n) : ℤ)) : A)
have h : Eq.{u_2 + 1} (α := A) (↑((↑(Int.negOnePow (↑n : ℤ)) : ℤ) * (↑((d + n).choose n) : ℤ)) : A)
  (↑(HSMul.hSMul (β := ℤ) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) (↑((d + n).choose n) : ℤ)) : A)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
A : Type u_2
inst : CommRing A
d n : ℕ
⊢ HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A d) : A⟦X⟧) : A) =
    HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑d : ℤ)) n) 1
have h : HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A 0) : A⟦X⟧) : A) =
  HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑0 : ℤ)) n) 1
Tactic: cases d with
  | zero =>
    by_cases hn : n = 0 <;> simp [invOneSubPow, Ring.choose_zero_ite, hn]
  | succ d =>
    simp only [invOneSubPow, coeff_mk, Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg,
      zsmul_eq_mul, mul_one]
    rw [show (-1 : ℤ) + -d = -(d + 1) by abel, Ring.choose_neg, Nat.choose_symm_add, Units.smul_def,
      show (d : ℤ) + 1 + n - 1 = d + n by lia, ← Nat.cast_add, Ring.choose_natCast]
    norm_cast
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Binomial (goal)
Goal:
A : Type u_2
inst : CommRing A
d n : ℕ
h :
  HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A 0) : A⟦X⟧) : A) =
    HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑0 : ℤ)) n) 1
⊢ HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A d) : A⟦X⟧) : A) =
    HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑d : ℤ)) n) 1
have h₁ : ∀ (d : ℕ),
  HSMul.hSMul (β := A) (↑(Int.negOnePow (↑n : ℤ)) : ℤ)
      ((coeff n : (a : A⟦X⟧) → A) (↑(invOneSubPow A (d + 1)) : A⟦X⟧) : A) =
    HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑(d + 1) : ℤ)) n) 1
Tactic: cases d with
  | zero =>
    by_cases hn : n = 0 <;> simp [invOneSubPow, Ring.choose_zero_ite, hn]
  | succ d =>
    simp only [invOneSubPow, coeff_mk, Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg,
      zsmul_eq_mul, mul_one]
    rw [show (-1 : ℤ) + -d = -(d + 1) by abel, Ring.choose_neg, Nat.choose_symm_add, Units.smul_def,
      show (d : ℤ) + 1 + n - 1 = d + n by lia, ← Nat.cast_add, Ring.choose_natCast]
    norm_cast
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
⊢ Eq (α := ℕ) ((constantCoeff : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ) (1 : ℕ)
have rw : Eq (α := ℕ) ((coeff 0 : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ) (1 : ℕ)
Tactic: rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
⊢ HPow.hPow (β := ℕ) catalanSeries 2 * X + 1 = catalanSeries
have h : ∀ (n : ℕ),
  Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
have h : Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (1 + HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
  ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
Tactic: simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
n : ℕ
h :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (1 + HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
⊢ Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
have h₁ : HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) 1 : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
  (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
Tactic: simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
n : ℕ
h :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (1 + HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₁ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) 1 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
⊢ Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
have h₂ : HAdd.hAdd (α := ℕ) (β := ℕ) (if n + 1 = 0 then 1 else 0 : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
  (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
Tactic: simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
n : ℕ
h :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (1 + HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₁ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) 1 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₂ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (if n + 1 = 0 then 1 else 0 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
⊢ Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
have h₃ : HAdd.hAdd (α := ℕ) (β := ℕ) (0 : ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
  (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
Tactic: simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
n : ℕ
h :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (1 + HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₁ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) 1 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₂ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (if n + 1 = 0 then 1 else 0 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₃ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (0 : ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
⊢ Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
have h₄ : Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
  ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
Tactic: simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
n : ℕ
h :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (1 + HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₁ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) 1 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₂ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (if n + 1 = 0 then 1 else 0 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₃ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (0 : ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₄ :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
⊢ Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
have h₅ : Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2) : ℕ)
  ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
Tactic: simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
n : ℕ
h :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (1 + HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₁ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) 1 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₂ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (if n + 1 = 0 then 1 else 0 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₃ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (0 : ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₄ :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₅ :
  Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
⊢ Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
have h₆ : Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (catalanSeries * catalanSeries) : ℕ)
  ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
Tactic: simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
n : ℕ
h :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (1 + HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₁ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) 1 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₂ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (if n + 1 = 0 then 1 else 0 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₃ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (0 : ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₄ :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₅ :
  Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₆ :
  Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (catalanSeries * catalanSeries) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
⊢ Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
have h₇ : Eq (α := ℕ)
  (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := ℕ) (β := ℕ) ((coeff p.1 : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
        ((coeff p.2 : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ) :
    ℕ)
  ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
Tactic: simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']