-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem embDomain_coeff {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {a : Γ} :
    (embDomain f x).coeff (f a) = x.coeff a

Proof state:
case neg.hnc
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∉ x.support
⊢ f a ∉ ⇑f '' x.support

Tactic:
contrapose! ha

Result:
case neg.hnc
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : f a ∈ ⇑f '' x.support
⊢ a ∈ x.support

Proof state:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∈ x.support
⊢ x.coeff (Classical.choose ⋯) = x.coeff a

Tactic:
exact congr rfl (f.injective (Classical.choose_spec (Set.mem_image_of_mem f ha)).2)

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
⊢ { coeff := fun b => if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0, isPWO_support' := ⋯ }.coeff
      (f a) =
    x.coeff a

Tactic:
dsimp only

Result:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a

Proof state:
case neg.hnc.intro.intro
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : f a ∈ ⇑f '' x.support
b : Γ
hb1 : b ∈ x.support
hb2 : f b = f a
⊢ a ∈ x.support

Tactic:
rwa [f.injective hb2] at hb1

Result:
no goals

Proof state:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∈ x.support
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a

Tactic:
rw [dif_pos (Set.mem_image_of_mem f ha)]

Result:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∈ x.support
⊢ x.coeff (Classical.choose ⋯) = x.coeff a

Proof state:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∉ x.support
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a

Tactic:
rw [dif_neg, Classical.not_not.1 fun c => ha ((mem_support _ _).2 c)]

Result:
case neg.hnc
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∉ x.support
⊢ f a ∉ ⇑f '' x.support

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a

Tactic:
by_cases ha : a ∈ x.support

Result:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∈ x.support
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a

case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∉ x.support
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a

Proof state:
case neg.hnc
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : f a ∈ ⇑f '' x.support
⊢ a ∈ x.support

Tactic:
obtain ⟨b, hb1, hb2⟩ := (Set.mem_image _ _ _).1 ha

Result:
case neg.hnc.intro.intro
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : f a ∈ ⇑f '' x.support
b : Γ
hb1 : b ∈ x.support
hb2 : f b = f a
⊢ a ∈ x.support

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
⊢ (embDomain f x).coeff (f a) = x.coeff a

Tactic:
rw [embDomain]

Result:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
⊢ { coeff := fun b => if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0, isPWO_support' := ⋯ }.coeff
      (f a) =
    x.coeff a