-- Mathlib/RingTheory/HahnSeries/PowerSeries.lean
theorem ofPowerSeries_C (r : R) : ofPowerSeries Γ R (PowerSeries.C R r) = HahnSeries.C r

Proof state:
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
hn : ¬n = 0
x✝ : ℕ
⊢ ¬((if x✝ = 0 then r else 0) ≠ 0 ∧ { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } x✝ = n)

Tactic:
simp +contextual [Ne.symm hn]

Result:
no goals

Proof state:
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
hn : ¬n = 0
⊢ n ∉ ⇑{ toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } '' (toPowerSeries.symm ((PowerSeries.C R) r)).support

Tactic:
simp only [not_exists, Set.mem_image, toPowerSeries_symm_apply_coeff, mem_support,
  PowerSeries.coeff_C]

Result:
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
hn : ¬n = 0
⊢ ∀ (x : ℕ), ¬((if x = 0 then r else 0) ≠ 0 ∧ { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } x = n)

Proof state:
case pos
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
⊢ (embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (toPowerSeries.symm ((PowerSeries.C R) r))).coeff 0 = r

Tactic:
convert embDomain_coeff (a := 0) <;> simp

Result:
no goals

Proof state:
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
hn : ¬n = 0
⊢ ∀ (x : ℕ), ¬((if x = 0 then r else 0) ≠ 0 ∧ { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } x = n)

Tactic:
intro

Result:
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
hn : ¬n = 0
x✝ : ℕ
⊢ ¬((if x✝ = 0 then r else 0) ≠ 0 ∧ { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } x✝ = n)

Proof state:
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
hn : ¬n = 0
⊢ (embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (toPowerSeries.symm ((PowerSeries.C R) r))).coeff n = 0

Tactic:
rw [embDomain_notin_image_support]

Result:
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
hn : ¬n = 0
⊢ n ∉ ⇑{ toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } '' (toPowerSeries.symm ((PowerSeries.C R) r)).support

Proof state:
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
⊢ (ofPowerSeries Γ R) ((PowerSeries.C R) r) = C r

Tactic:
ext n

Result:
case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
⊢ ((ofPowerSeries Γ R) ((PowerSeries.C R) r)).coeff n = (C r).coeff n

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
⊢ (embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (toPowerSeries.symm ((PowerSeries.C R) r))).coeff n =
    if n = 0 then r else 0

Tactic:
split_ifs with hn

Result:
case pos
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
hn : n = 0
⊢ (embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (toPowerSeries.symm ((PowerSeries.C R) r))).coeff n = r

case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
hn : ¬n = 0
⊢ (embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (toPowerSeries.symm ((PowerSeries.C R) r))).coeff n = 0

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
⊢ ((ofPowerSeries Γ R) ((PowerSeries.C R) r)).coeff n = (C r).coeff n

Tactic:
simp only [ofPowerSeries_apply, C, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, ne_eq,
  coeff_single]

Result:
case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
⊢ (embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (toPowerSeries.symm ((PowerSeries.C R) r))).coeff n =
    if n = 0 then r else 0

Proof state:
case pos
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
n : Γ
hn : n = 0
⊢ (embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (toPowerSeries.symm ((PowerSeries.C R) r))).coeff n = r

Tactic:
subst hn

Result:
case pos
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
r : R
⊢ (embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (toPowerSeries.symm ((PowerSeries.C R) r))).coeff 0 = r