internlm/Lean-Github huggingface dataset:
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ ∑ x ∈ Finset.antidiagonal n,
      n.choose x.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 x.1 + Finsupp.single 1 x.2)) 1) =
    ↑(n.choose (d 0))
Tactic:
rw [Finset.sum_eq_single (d 0, d 1)]
Proof state after:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ n.choose (d 0, d 1).1 •
      MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2)) 1) =
    ↑(n.choose (d 0))

case pos.h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ ∀ b ∈ Finset.antidiagonal n,
    b ≠ (d 0, d 1) →
      n.choose b.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 b.1 + Finsupp.single 1 b.2)) 1) = 0

case pos.h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ (d 0, d 1) ∉ Finset.antidiagonal n →
    n.choose (d 0, d 1).1 •
        MvPolynomial.coeff d
          ((MvPolynomial.monomial (Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2)) 1) =
      0
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ n.choose (d 0, d 1).1 •
      MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2)) 1) =
    ↑(n.choose (d 0))
Tactic:
rw [MvPolynomial.coeff_monomial, if_pos]
Proof state after:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ n.choose (d 0, d 1).1 • 1 = ↑(n.choose (d 0))

case pos.hc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2 = d
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ n.choose (d 0, d 1).1 • 1 = ↑(n.choose (d 0))

case pos.hc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2 = d
Tactic:
simp only [Fin.isValue, nsmul_eq_mul, mul_one]
Proof state after:
case pos.hc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2 = d
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos.hc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2 = d
Tactic:
ext i
Proof state after:
case pos.hc.h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
i : Fin 2
⊢ (Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2) i = d i
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos.hc.h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
i : Fin 2
⊢ (Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2) i = d i
Tactic:
match i with
| 0 => simp
| 1 => simp
Proof state after:
no goals
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
i : Fin 2
⊢ (Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2) 0 = d 0
Tactic:
simp
Proof state after:
no goals
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
i : Fin 2
⊢ (Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2) 1 = d 1
Tactic:
simp
Proof state after:
no goals
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos.h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ ∀ b ∈ Finset.antidiagonal n,
    b ≠ (d 0, d 1) →
      n.choose b.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 b.1 + Finsupp.single 1 b.2)) 1) = 0
Tactic:
intro e _ hed
Proof state after:
case pos.h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
e : ℕ × ℕ
a✝ : e ∈ Finset.antidiagonal n
hed : e ≠ (d 0, d 1)
⊢ n.choose e.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 e.1 + Finsupp.single 1 e.2)) 1) = 0
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos.h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
e : ℕ × ℕ
a✝ : e ∈ Finset.antidiagonal n
hed : e ≠ (d 0, d 1)
⊢ n.choose e.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 e.1 + Finsupp.single 1 e.2)) 1) = 0
Tactic:
rw [MvPolynomial.coeff_monomial, if_neg, smul_zero]
Proof state after:
case pos.h₀.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
e : ℕ × ℕ
a✝ : e ∈ Finset.antidiagonal n
hed : e ≠ (d 0, d 1)
⊢ ¬Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos.h₀.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
e : ℕ × ℕ
a✝ : e ∈ Finset.antidiagonal n
hed : e ≠ (d 0, d 1)
⊢ ¬Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
Tactic:
intro hde
Proof state after:
case pos.h₀.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
e : ℕ × ℕ
a✝ : e ∈ Finset.antidiagonal n
hed : e ≠ (d 0, d 1)
hde : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ False
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos.h₀.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
e : ℕ × ℕ
a✝ : e ∈ Finset.antidiagonal n
hed : e ≠ (d 0, d 1)
hde : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ False
Tactic:
apply hed
Proof state after:
case pos.h₀.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
e : ℕ × ℕ
a✝ : e ∈ Finset.antidiagonal n
hed : e ≠ (d 0, d 1)
hde : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ e = (d 0, d 1)
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos.h₀.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
e : ℕ × ℕ
a✝ : e ∈ Finset.antidiagonal n
hed : e ≠ (d 0, d 1)
hde : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ e = (d 0, d 1)
Tactic:
rw [← hde]
Proof state after:
case pos.h₀.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
e : ℕ × ℕ
a✝ : e ∈ Finset.antidiagonal n
hed : e ≠ (d 0, d 1)
hde : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ e = ((Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 0, (Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 1)
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos.h₀.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
e : ℕ × ℕ
a✝ : e ∈ Finset.antidiagonal n
hed : e ≠ (d 0, d 1)
hde : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ e = ((Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 0, (Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 1)
Tactic:
simp
Proof state after:
no goals
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos.h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ (d 0, d 1) ∉ Finset.antidiagonal n →
    n.choose (d 0, d 1).1 •
        MvPolynomial.coeff d
          ((MvPolynomial.monomial (Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2)) 1) =
      0
Tactic:
intro hd'
Proof state after:
case pos.h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
hd' : (d 0, d 1) ∉ Finset.antidiagonal n
⊢ n.choose (d 0, d 1).1 •
      MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2)) 1) =
    0
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case pos.h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
hd' : (d 0, d 1) ∉ Finset.antidiagonal n
⊢ n.choose (d 0, d 1).1 •
      MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 (d 0, d 1).1 + Finsupp.single 1 (d 0, d 1).2)) 1) =
    0
Tactic:
contradiction
Proof state after:
no goals
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case neg
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
⊢ ∑ x ∈ Finset.antidiagonal n,
      n.choose x.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 x.1 + Finsupp.single 1 x.2)) 1) =
    0
Tactic:
apply Finset.sum_eq_zero
Proof state after:
case neg.h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
⊢ ∀ x ∈ Finset.antidiagonal n,
    n.choose x.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 x.1 + Finsupp.single 1 x.2)) 1) = 0
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case neg.h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
⊢ ∀ x ∈ Finset.antidiagonal n,
    n.choose x.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 x.1 + Finsupp.single 1 x.2)) 1) = 0
Tactic:
intro e he
Proof state after:
case neg.h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e ∈ Finset.antidiagonal n
⊢ n.choose e.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 e.1 + Finsupp.single 1 e.2)) 1) = 0
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case neg.h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e ∈ Finset.antidiagonal n
⊢ n.choose e.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 e.1 + Finsupp.single 1 e.2)) 1) = 0
Tactic:
simp only [Finset.mem_antidiagonal] at he
Proof state after:
case neg.h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e.1 + e.2 = n
⊢ n.choose e.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 e.1 + Finsupp.single 1 e.2)) 1) = 0
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case neg.h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e.1 + e.2 = n
⊢ n.choose e.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 e.1 + Finsupp.single 1 e.2)) 1) = 0
Tactic:
rw [MvPolynomial.coeff_monomial, if_neg, smul_zero]
Proof state after:
case neg.h.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e.1 + e.2 = n
⊢ ¬Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case neg.h.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e.1 + e.2 = n
⊢ ¬Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
Tactic:
intro hed
Proof state after:
case neg.h.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e.1 + e.2 = n
hed : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ False
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case neg.h.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e.1 + e.2 = n
hed : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ False
Tactic:
apply hd
Proof state after:
case neg.h.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e.1 + e.2 = n
hed : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ (d 0, d 1) ∈ Finset.antidiagonal n
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case neg.h.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e.1 + e.2 = n
hed : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ (d 0, d 1) ∈ Finset.antidiagonal n
Tactic:
rw [← hed, Finset.mem_antidiagonal]
Proof state after:
case neg.h.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e.1 + e.2 = n
hed : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ ((Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 0, (Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 1).1 +
      ((Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 0, (Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 1).2 =
    n
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case neg.h.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
e : ℕ × ℕ
he : e.1 + e.2 = n
hed : Finsupp.single 0 e.1 + Finsupp.single 1 e.2 = d
⊢ ((Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 0, (Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 1).1 +
      ((Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 0, (Finsupp.single 0 e.1 + Finsupp.single 1 e.2) 1).2 =
    n
Tactic:
simpa using he
Proof state after:
no goals