σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : X s = X t
⊢ s = t
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
⊢ X s = X t → s = t
intro h
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
⊢ s = t
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : X s = X t
⊢ s = t
replace h := congr_arg (coeff R (single s 1)) h
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
h : 1 = if single s 1 = single t 1 then 1 else 0
⊢ s = t
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
⊢ s = t
rw [coeff_X, if_pos rfl, coeff_X] at h
case inl
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
H : single s 1 = single t 1
h : 1 = 1
⊢ s = t

case inr
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
H : ¬single s 1 = single t 1
h : 1 = 0
⊢ s = t
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
h : 1 = if single s 1 = single t 1 then 1 else 0
⊢ s = t
split_ifs  at h with H
case inl
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
H : s = t ∧ 1 = 1 ∨ 1 = 0 ∧ 1 = 0
h : 1 = 1
⊢ s = t
case inl
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
H : single s 1 = single t 1
h : 1 = 1
⊢ s = t
rw [Finsupp.single_eq_single_iff] at H
case inl.inl
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
h : 1 = 1
H : s = t ∧ 1 = 1
⊢ s = t

case inl.inr
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
h : 1 = 1
H : 1 = 0 ∧ 1 = 0
⊢ s = t
case inl
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
H : s = t ∧ 1 = 1 ∨ 1 = 0 ∧ 1 = 0
h : 1 = 1
⊢ s = t
cases' H with H H
no goals
case inl.inl
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
h : 1 = 1
H : s = t ∧ 1 = 1
⊢ s = t
exact H.1
case inl.inr.h
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
h : 1 = 1
H : 1 = 0 ∧ 1 = 0
⊢ False
case inl.inr
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
h : 1 = 1
H : 1 = 0 ∧ 1 = 0
⊢ s = t
exfalso
no goals
case inl.inr.h
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
h : 1 = 1
H : 1 = 0 ∧ 1 = 0
⊢ False
exact one_ne_zero H.1
case inr.h
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
H : ¬single s 1 = single t 1
h : 1 = 0
⊢ False
case inr
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
H : ¬single s 1 = single t 1
h : 1 = 0
⊢ s = t
exfalso
no goals
case inr.h
σ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h✝¹ : ↑(coeff R (single s 1)) (X s) = ↑(coeff R (single s 1)) (X t)
h✝ : 1 = ↑(coeff R (single s 1)) (X t)
H : ¬single s 1 = single t 1
h : 1 = 0
⊢ False
exact one_ne_zero h