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

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

State before:
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n : ℕ
x : σ
⊢ (if x = j ∧ 1 = n ∨ False ∧ n = 0 then 1 else 0) = if n = 1 ∧ j = x 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 : ℕ
x : σ
⊢ (x = j ∧ 1 = n ∨ False ∧ n = 0) = (n = 1 ∧ j = x)

State before:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n : ℕ
x : σ
⊢ (x = j ∧ 1 = n ∨ False ∧ n = 0) = (n = 1 ∧ j = x)
Tactic:
simp_rw [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 : ℕ
x : σ
⊢ x = j ∧ 1 = n ∨ False ∧ n = 0 ↔ n = 1 ∧ j = x

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