Theorem: PowerSeries.coeff_add_pow (DividedPowers/ExponentialModule/Basic.lean)

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
⊢ MvPolynomial.coeff d ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ n) =
    ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)
Tactic:
rw [Commute.add_pow' (Commute.all _ _), MvPolynomial.coeff_sum]
State after:
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
⊢ ∑ x ∈ Finset.antidiagonal n, MvPolynomial.coeff d (n.choose x.1 • (MvPolynomial.X 0 ^ x.1 * MvPolynomial.X 1 ^ x.2)) =
    ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)

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
⊢ ∑ x ∈ Finset.antidiagonal n, MvPolynomial.coeff d (n.choose x.1 • (MvPolynomial.X 0 ^ x.1 * MvPolynomial.X 1 ^ x.2)) =
    ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)
Tactic:
simp only [nsmul_eq_smul, MvPolynomial.coeff_smul]
State after:
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
⊢ ∑ x ∈ Finset.antidiagonal n, n.choose x.1 • MvPolynomial.coeff d (MvPolynomial.X 0 ^ x.1 * MvPolynomial.X 1 ^ x.2) =
    ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)

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
⊢ ∑ x ∈ Finset.antidiagonal n, n.choose x.1 • MvPolynomial.coeff d (MvPolynomial.X 0 ^ x.1 * MvPolynomial.X 1 ^ x.2) =
    ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)
Tactic:
simp only [Fin.isValue, Nat.cast_ite, Nat.cast_zero, hmon]
State after:
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
⊢ ∑ x ∈ Finset.antidiagonal n,
      n.choose x.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 x.1 + Finsupp.single 1 x.2)) 1) =
    if (d 0, d 1) ∈ Finset.antidiagonal n then ↑(n.choose (d 0)) else 0

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
⊢ ∑ x ∈ Finset.antidiagonal n,
      n.choose x.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 x.1 + Finsupp.single 1 x.2)) 1) =
    if (d 0, d 1) ∈ Finset.antidiagonal n then ↑(n.choose (d 0)) else 0
Tactic:
split_ifs with hd
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
⊢ ∑ 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))

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

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 : ℕ
⊢ ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
Tactic:
intro u v
State after:
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 u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1

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 u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
Tactic:
rw [MvPolynomial.monomial_eq]
State after:
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 u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.C 1 * (Finsupp.single 0 u + Finsupp.single 1 v).prod fun n e => MvPolynomial.X n ^ e

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 u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.C 1 * (Finsupp.single 0 u + Finsupp.single 1 v).prod fun n e => MvPolynomial.X n ^ e
Tactic:
rw [Finsupp.prod_of_support_subset _ (Finset.subset_univ _)]
State after:
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 u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.C 1 * ∏ x : Fin 2, MvPolynomial.X x ^ (Finsupp.single 0 u + Finsupp.single 1 v) x

case 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 u v : ℕ
⊢ ∀ i ∈ Finset.univ, MvPolynomial.X i ^ 0 = 1

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 u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.C 1 * ∏ x : Fin 2, MvPolynomial.X x ^ (Finsupp.single 0 u + Finsupp.single 1 v) x
Tactic:
simp only [map_one, Fin.prod_univ_two, Fin.isValue, one_mul]
State after:
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 u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.X 0 ^ (Finsupp.single 0 u + Finsupp.single 1 v) 0 *
      MvPolynomial.X 1 ^ (Finsupp.single 0 u + Finsupp.single 1 v) 1

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 u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.X 0 ^ (Finsupp.single 0 u + Finsupp.single 1 v) 0 *
      MvPolynomial.X 1 ^ (Finsupp.single 0 u + Finsupp.single 1 v) 1
Tactic:
simp only [Fin.isValue, Finsupp.coe_add, Pi.add_apply,
  Finsupp.single_eq_same, ne_eq, one_ne_zero, not_false_eq_true,
  Finsupp.single_eq_of_ne, add_zero, zero_ne_one, zero_add]
State after:
no goals

State before:
case 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 u v : ℕ
⊢ ∀ i ∈ Finset.univ, MvPolynomial.X i ^ 0 = 1
Tactic:
exact fun i _ ↦ by simp only [pow_zero]
State after:
no goals

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 u v : ℕ
i : Fin 2
x✝ : i ∈ Finset.univ
⊢ MvPolynomial.X i ^ 0 = 1
Tactic:
simp only [pow_zero]
State after:
no goals

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)]
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

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]
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

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]
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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]
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

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
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

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
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)

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]
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)

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
State after:
no goals

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'
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

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
State after:
no goals

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
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

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
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

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
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

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]
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

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
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

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
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

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]
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

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
State after:
no goals