Theorem: MvPolynomial.coeff_single_X_pow (FormalSnarksProject/ToMathlib/ForTransformations.lean)

State before:
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ coeff (Finsupp.single j n) (X x ^ k) = if n = k ∧ j = x ∨ k = 0 ∧ n = 0 then 1 else 0
Tactic:
rw [MvPolynomial.X_pow_eq_monomial, MvPolynomial.coeff_monomial]
State after:
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ (if Finsupp.single x k = Finsupp.single j n then 1 else 0) = if n = k ∧ j = x ∨ k = 0 ∧ n = 0 then 1 else 0

State before:
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ (if Finsupp.single x k = Finsupp.single j n then 1 else 0) = if n = k ∧ j = x ∨ k = 0 ∧ n = 0 then 1 else 0
Tactic:
congr
State after:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ (Finsupp.single x k = Finsupp.single j n) = (n = k ∧ j = x ∨ k = 0 ∧ n = 0)

State before:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ (Finsupp.single x k = Finsupp.single j n) = (n = k ∧ j = x ∨ k = 0 ∧ n = 0)
Tactic:
simp only [Finsupp.single_eq_single_iff, eq_iff_iff]
State after:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ x = j ∧ k = n ∨ k = 0 ∧ n = 0 ↔ n = k ∧ j = x ∨ k = 0 ∧ n = 0

State before:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ x = j ∧ k = n ∨ k = 0 ∧ n = 0 ↔ n = k ∧ j = x ∨ k = 0 ∧ n = 0
Tactic:
tauto
State after:
no goals