-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem X_inj [Nontrivial R] {s t : σ} : (X s : MvPowerSeries σ R) = X t ↔ s = t :=
  ⟨by
    classical
    intro h
    replace h := congr_arg (coeff R (single s 1)) h
    rw [coeff_X, if_pos rfl, coeff_X] at h
    split_ifs at h with H
    · rw [Finsupp.single_eq_single_iff] at H
      rcases H with H | H
      · exact H.1
      · exfalso
        exact one_ne_zero H.1
    · exfalso
      exact one_ne_zero h, congr_arg X⟩

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = if single s 1 = single t 1 then 1 else 0
⊢ s = t

Tactic:
split_ifs at h with H

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : single s 1 = single t 1
h : 1 = 1
⊢ s = t

case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : ¬single s 1 = single t 1
h : 1 = 0
⊢ s = t

Proof state:
case pos.inl
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = 1
H : s = t ∧ 1 = 1
⊢ s = t

Tactic:
exact H.1

Result:
no goals

Proof state:
case pos.inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = 1
H : 1 = 0 ∧ 1 = 0
⊢ False

Tactic:
exact one_ne_zero H.1

Result:
no goals

Proof state:
case pos.inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = 1
H : 1 = 0 ∧ 1 = 0
⊢ s = t

Tactic:
exfalso

Result:
case pos.inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = 1
H : 1 = 0 ∧ 1 = 0
⊢ False

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : single s 1 = single t 1
h : 1 = 1
⊢ s = t

Tactic:
rw [Finsupp.single_eq_single_iff] at H

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : s = t ∧ 1 = 1 ∨ 1 = 0 ∧ 1 = 0
h : 1 = 1
⊢ s = t

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : ¬single s 1 = single t 1
h : 1 = 0
⊢ False

Tactic:
exact one_ne_zero h

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : X s = X t
⊢ s = t

Tactic:
replace h := congr_arg (coeff R (single s 1)) h

Result:
σ : Type u_1
R : Type u_2
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

Proof state:
σ : Type u_1
R : Type u_2
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

Tactic:
rw [coeff_X, if_pos rfl, coeff_X] at h

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = if single s 1 = single t 1 then 1 else 0
⊢ s = t

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : s = t ∧ 1 = 1 ∨ 1 = 0 ∧ 1 = 0
h : 1 = 1
⊢ s = t

Tactic:
rcases H with H | H

Result:
case pos.inl
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = 1
H : s = t ∧ 1 = 1
⊢ s = t

case pos.inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = 1
H : 1 = 0 ∧ 1 = 0
⊢ s = t

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
⊢ X s = X t → s = t

Tactic:
intro h

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : X s = X t
⊢ s = t

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : ¬single s 1 = single t 1
h : 1 = 0
⊢ s = t

Tactic:
exfalso

Result:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : ¬single s 1 = single t 1
h : 1 = 0
⊢ False