awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ B.gen ^ (↑i : ℕ) ∈
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[B.gen] : Submodule R S) : Set S)

Tactic:
Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _

Premises used: Set.mem_singleton, iInf, Set.Mem, Set.iInter, Algebra.subset_adjoin, setOf, Subalgebra.pow_mem
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ B.gen ^ (↑i : ℕ) ∈
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[B.gen] : Submodule R S) : Set S)

Tactic:
exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _

Premises used: Set.mem_singleton, Algebra.subset_adjoin, Subalgebra.pow_mem
-- Module: Mathlib.RingTheory.PowerBasis
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
rw : LE.le (α := Subalgebra R S) R[B.gen] R[x]
⊢ Eq (α := Subalgebra R S) R[x] ⊤

Tactic:
rw [_root_.eq_top_iff, ← B.adjoin_gen_eq_top]

Premises used: eq_top_iff, PowerBasis.adjoin_gen_eq_top
-- Module: Mathlib.RingTheory.PowerBasis
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]

Tactic:
adjoin_le ?_

Premises used: Algebra.adjoin_le
-- Module: Mathlib.RingTheory.PowerBasis
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
refine : {B.gen} ⊆ (↑R[x] : Set S)
⊢ LE.le (α := Subalgebra R S) R[B.gen] R[x]

Tactic:
refine adjoin_le ?_

Premises used: Algebra.adjoin_le
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ {B.gen} ⊆ (↑R[x] : Set S)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : BinomialRing R
inst_2 : Semiring A
inst_3 : SMul R A
r : R
n : ℕ
⊢ (coeff n : (a : A⟦X⟧) → A) (binomialSeries A r) = HSMul.hSMul (β := A) (Ring.choose r n) 1

Tactic:
coeff_mk n fun n ↦ Ring.choose r n • 1

Premises used: PowerSeries.binomialSeries, PowerSeries.coeff_mk, Ring.choose, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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 : R
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (binomialSeries A r) : A) (1 : A)

Tactic:
simp [← coeff_zero_eq_constantCoeff_apply]

Premises used: PowerSeries.coeff_zero_eq_constantCoeff_apply
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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
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)
⊢ binomialSeries A (r + s) = binomialSeries A r * binomialSeries A s

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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 : ℕ
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)
⊢ 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:
simp only [binomialSeries_coeff, Ring.add_choose_eq n (Commute.all r s), coeff_mul,
    Algebra.mul_smul_comm, mul_one, sum_smul]

Premises used: Finset.sum_smul, Algebra.mul_smul_comm, Ring.add_choose_eq, PowerSeries.binomialSeries_coeff, PowerSeries.coeff_mul, mul_one, Commute.all
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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)

Tactic:
sum_congr rfl fun ab hab => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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 : ℕ
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
⊢ 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:
refine sum_congr rfl fun ab hab => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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
h₁ 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
⊢ 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:
rw [mul_comm, mul_smul]

Premises used: mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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 : ℕ
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)
⊢ binomialSeries.{u_1, u_2} (R := R) A (↑d : R) = HAdd.hAdd (α := A⟦X⟧) 1 X ^ d

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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 : ℕ
⊢ HAdd.hAdd (α := A⟦X⟧) 1 X ^ d = (↑(HAdd.hAdd (α := Polynomial A) 1 Polynomial.X ^ d) : A⟦X⟧)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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 : ℕ
⊢ 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
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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⟧)
h : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) (Ring.choose (↑d : R) n) 1 = (↑(d.choose n) : A)
⊢ 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:
rw [hright, Polynomial.coeff_coe, binomialSeries_coeff, Polynomial.coeff_one_add_X_pow]

Premises used: Polynomial.coeff_one_add_X_pow, PowerSeries.binomialSeries_coeff, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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⟧)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) (Ring.choose (↑d : R) n) 1 = (↑(d.choose n) : A)

Tactic:
simp [Ring.choose_natCast, Nat.cast_smul_eq_nsmul]

Premises used: Ring.choose_natCast, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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
⊢ binomialSeries.{u_1, u_2} (R := R) A 0 = 1

Tactic:
simpa using binomialSeries_nat 0

Premises used: OfNat.ofNat, PowerSeries.binomialSeries_nat
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
Goal:
A : Type u_2
inst : CommRing A
d : ℕ
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)
⊢ (rescale (-1) : (a : A⟦X⟧) → A⟦X⟧) (↑(invOneSubPow A d) : A⟦X⟧) = binomialSeries (R := ℤ) A (-(↑d : ℤ))

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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 d) : A⟦X⟧) : A) =
    HSMul.hSMul (α := ℤ) (β := A) (Ring.choose (-(↑d : ℤ)) n) 1
⊢ 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:
rw [coeff_rescale, binomialSeries_coeff, ← Int.cast_negOnePow_natCast, ← zsmul_eq_mul]

Premises used: PowerSeries.coeff_rescale, zsmul_eq_mul, PowerSeries.binomialSeries_coeff, Int.cast_negOnePow_natCast
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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
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
⊢ 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
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
Goal:
A : Type u_2
inst : CommRing A
n : ℕ
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:
simp [invOneSubPow, Ring.choose_zero_ite, hn]

Premises used: PowerSeries.invOneSubPow, Ring.choose_zero_ite
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
Goal:
A : Type u_2
inst : CommRing A
n : ℕ
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:
simp [invOneSubPow, Ring.choose_zero_ite, hn]

Premises used: PowerSeries.invOneSubPow, Ring.choose_zero_ite
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
Goal:
A : Type u_2
inst : CommRing A
n d : ℕ
h :
  HMul.hMul (α := A) (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : A) (↑((d + n).choose d) : A) =
    (↑(Ring.choose (HAdd.hAdd (α := ℤ) (-1) (-(↑d : ℤ))) n) : A)
⊢ 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:
simp only [invOneSubPow, coeff_mk, Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg,
      zsmul_eq_mul, mul_one]

Premises used: neg_add_rev, zsmul_eq_mul, PowerSeries.invOneSubPow, Int.reduceNeg, PowerSeries.coeff_mk, Nat.cast_add, mul_one, Nat.cast_one
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
Goal:
A : Type u_2
inst : CommRing A
n d : ℕ
⊢ HAdd.hAdd (α := ℤ) (-1) (-(↑d : ℤ)) = -HAdd.hAdd (α := ℤ) (↑d : ℤ) 1

Tactic:
abel
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
Goal:
A : Type u_2
inst : CommRing A
n d : ℕ
⊢ HAdd.hAdd (α := ℤ) (↑d : ℤ) 1 + (↑n : ℤ) - 1 = HAdd.hAdd (α := ℤ) (↑d : ℤ) (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
Goal:
A : Type u_2
inst : CommRing A
n d : ℕ
h :
  HMul.hMul (α := A) (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : A) (↑((d + n).choose n) : A) =
    (↑(HSMul.hSMul (β := ℤ) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) (↑((d + n).choose n) : ℤ)) : A)
⊢ HMul.hMul (α := A) (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : A) (↑((d + n).choose d) : A) =
    (↑(Ring.choose (HAdd.hAdd (α := ℤ) (-1) (-(↑d : ℤ))) 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]

Premises used: Ring.choose_neg, Nat.choose_symm_add, Nat.cast_add, Ring.choose_natCast, Units.smul_def
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
Goal:
A : Type u_2
inst : CommRing A
n d : ℕ
h h₁ h₂ h₃ :
  Eq.{u_2 + 1} (α := A) (↑((↑(Int.negOnePow (↑n : ℤ)) : ℤ) * (↑((d + n).choose n) : ℤ)) : A)
    (↑(HSMul.hSMul (β := ℤ) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) (↑((d + n).choose n) : ℤ)) : A)
⊢ HMul.hMul (α := A) (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : A) (↑((d + n).choose n) : A) =
    (↑(HSMul.hSMul (β := ℤ) (↑(Int.negOnePow (↑n : ℤ)) : ℤ) (↑((d + n).choose n) : ℤ)) : A)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.PowerSeries.Binomial
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
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
⊢ 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:
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

Premises used: neg_add_rev, zsmul_eq_mul, PowerSeries.invOneSubPow, Int.reduceNeg, Ring.choose_neg, Ring.choose_zero_ite, PowerSeries.coeff_mk, Nat.choose_symm_add, Nat.cast_add, Ring.choose_natCast, Units.smul_def, mul_one, Nat.cast_one
-- Module: Mathlib.RingTheory.PowerSeries.Catalan
Goal:
n : ℕ
⊢ (coeff n : (a : ℕ⟦X⟧) → ℕ) catalanSeries = catalan n

Tactic:
simp [catalanSeries]

Premises used: PowerSeries.catalanSeries
-- Module: Mathlib.RingTheory.PowerSeries.Catalan
Goal:
rw : Eq (α := ℕ) ((coeff 0 : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ) (1 : ℕ)
⊢ Eq (α := ℕ) ((constantCoeff : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ) (1 : ℕ)

Tactic:
rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply]

Premises used: PowerSeries.coeff_zero_eq_constantCoeff_apply
-- Module: Mathlib.RingTheory.PowerSeries.Catalan
Goal:
⊢ Eq (α := ℕ) ((coeff 0 : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ) (1 : ℕ)

Tactic:
simp only [catalanSeries_coeff, catalan_zero]

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

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

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Catalan
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 : ℕ)
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 : ℕ)
h₈ : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan x.1 * catalan x.2 = catalan (n + 1)
⊢ Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((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']

Premises used: PowerSeries.catalanSeries_coeff, PowerSeries.coeff_succ_mul_X, map_add, sq, zero_add, add_comm, PowerSeries.coeff_mul, Nat.succ_ne_zero, PowerSeries.coeff_one, catalan_succ', if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Catalan
Goal:
n : ℕ
h :
  Eq (α := ℕ) ((coeff 0 : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff 0 : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₁ :
  ∀ (n : ℕ),
    Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)

Tactic:
cases n with
  | zero => simp
  | succ n =>
    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']

Premises used: PowerSeries.catalanSeries_coeff, PowerSeries.coeff_succ_mul_X, map_add, sq, zero_add, add_comm, PowerSeries.coeff_mul, Nat.succ_ne_zero, PowerSeries.coeff_one, catalan_succ', if_neg
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) f : A)
hg : ∀ i ≤ n, Membership.mem (α := A) J ((coeff i : (a : A⟦X⟧) → A) g : A)
i : ℕ
hi : i ≤ n
rw :
  ∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i,
      HMul.hMul (α := A) (β := A) ((coeff p.1 : (a : A⟦X⟧) → A) f : A) ((coeff p.2 : (a : A⟦X⟧) → A) g : A) ∈
    I * J
⊢ Membership.mem (α := A) (I * J) ((coeff i : (a : A⟦X⟧) → A) (f * g) : A)

Tactic:
rw [coeff_mul]

Premises used: PowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) f : A)
hg : ∀ i ≤ n, Membership.mem (α := A) J ((coeff i : (a : A⟦X⟧) → A) g : A)
i : ℕ
hi : i ≤ n
⊢ ∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i,
      HMul.hMul (α := A) (β := A) ((coeff p.1 : (a : A⟦X⟧) → A) f : A) ((coeff p.2 : (a : A⟦X⟧) → A) g : A) ∈
    I * J

Tactic:
Ideal.sum_mem _ fun p hp ↦ Ideal.mul_mem_mul
    (hf _ ((Finset.antidiagonal.fst_le hp).trans hi))
    (hg _ ((Finset.antidiagonal.snd_le hp).trans hi))

Premises used: Ideal.sum_mem, Ideal.mul_mem_mul, Prod.fst, Finset.antidiagonal.snd_le, Finset.antidiagonal.fst_le, LE.le.trans, Prod.snd
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) f : A)
hg : ∀ i ≤ n, Membership.mem (α := A) J ((coeff i : (a : A⟦X⟧) → A) g : A)
i : ℕ
hi : i ≤ n
⊢ ∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i,
      HMul.hMul (α := A) (β := A) ((coeff p.1 : (a : A⟦X⟧) → A) f : A) ((coeff p.2 : (a : A⟦X⟧) → A) g : A) ∈
    I * J

Tactic:
exact Ideal.sum_mem _ fun p hp ↦ Ideal.mul_mem_mul
    (hf _ ((Finset.antidiagonal.fst_le hp).trans hi))
    (hg _ ((Finset.antidiagonal.snd_le hp).trans hi))

Premises used: Ideal.sum_mem, Ideal.mul_mem_mul, Prod.fst, Finset.antidiagonal.snd_le, Finset.antidiagonal.fst_le, LE.le.trans, Prod.snd
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I J : Ideal A
f g : A⟦X⟧
hf : ∀ (i : ℕ), Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) f : A)
hg : ∀ (i : ℕ), Membership.mem (α := A) J ((coeff i : (a : A⟦X⟧) → A) g : A)
⊢ ∀ (i : ℕ), Membership.mem (α := A) (I * J) ((coeff i : (a : A⟦X⟧) → A) (f * g) : A)

Tactic:
fun i ↦ coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal i
    (fun i _ ↦ hf i) (fun i _ ↦ hg i) i le_rfl

Premises used: le_rfl, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
hg : ∀ i ≤ n, Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) g : A)
⊢ ∀ i ≤ n, Membership.mem (α := A) (γ := Ideal A) ⊤ ((coeff i : (a : A⟦X⟧) → A) f : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
hg : ∀ i ≤ n, Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) g : A)
⊢ ∀ i ≤ n, Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (f * g) : A)

Tactic:
simpa using coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal (I := ⊤) (f := f) n (by simp) hg

Premises used: PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I : Ideal A
f g : A⟦X⟧
hg : ∀ (i : ℕ), Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) g : A)
⊢ ∀ (i : ℕ), Membership.mem (α := A) (γ := Ideal A) ⊤ ((coeff i : (a : A⟦X⟧) → A) f : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I : Ideal A
f g : A⟦X⟧
hg : ∀ (i : ℕ), Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) g : A)
⊢ ∀ (i : ℕ), Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (f * g) : A)

Tactic:
simpa using coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (I := ⊤) (f := f) (by simp) hg

Premises used: PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
inst_1 : I.IsTwoSided
hf : ∀ i ≤ n, Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) f : A)
⊢ ∀ i ≤ n, Membership.mem (α := A) (γ := Ideal A) 1 ((coeff i : (a : A⟦X⟧) → A) g : A)

Tactic:
simp