Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
⊢ coeff
      { coeff := fun b => if h : b ∈ ↑f '' support x then coeff x (Classical.choose h) else 0,
        isPwo_support' :=
          (_ :
            Set.IsPwo (Function.support fun b => if h : b ∈ ↑f '' support x then coeff x (Classical.choose h) else 0)) }
      (↑f a) =
    coeff x a
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
⊢ coeff (embDomain f x) (↑f a) = coeff x a
rw [embDomain]
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
⊢ (if h : ↑f a ∈ ↑f '' support x then coeff x (Classical.choose h) else 0) = coeff x a
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
⊢ coeff
      { coeff := fun b => if h : b ∈ ↑f '' support x then coeff x (Classical.choose h) else 0,
        isPwo_support' :=
          (_ :
            Set.IsPwo (Function.support fun b => if h : b ∈ ↑f '' support x then coeff x (Classical.choose h) else 0)) }
      (↑f a) =
    coeff x a
dsimp only
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∈ support x
⊢ (if h : ↑f a ∈ ↑f '' support x then coeff x (Classical.choose h) else 0) = coeff x a

case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : ¬a ∈ support x
⊢ (if h : ↑f a ∈ ↑f '' support x then coeff x (Classical.choose h) else 0) = coeff x a
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
⊢ (if h : ↑f a ∈ ↑f '' support x then coeff x (Classical.choose h) else 0) = coeff x a
by_cases ha : a ∈ x.support
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∈ support x
⊢ coeff x (Classical.choose (_ : ↑f a ∈ ↑f '' support x)) = coeff x a
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∈ support x
⊢ (if h : ↑f a ∈ ↑f '' support x then coeff x (Classical.choose h) else 0) = coeff x a
rw [dif_pos (Set.mem_image_of_mem f ha)]
no goals
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : a ∈ support x
⊢ coeff x (Classical.choose (_ : ↑f a ∈ ↑f '' support x)) = coeff x a
exact congr rfl (f.injective (Classical.choose_spec (Set.mem_image_of_mem f ha)).2)
case neg.hnc
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : ¬a ∈ support x
⊢ ¬↑f a ∈ ↑f '' support x
case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : ¬a ∈ support x
⊢ (if h : ↑f a ∈ ↑f '' support x then coeff x (Classical.choose h) else 0) = coeff x a
rw [dif_neg, Classical.not_not.1 fun c => ha ((mem_support _ _).2 c)]
case neg.hnc
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : ↑f a ∈ ↑f '' support x
⊢ a ∈ support x
case neg.hnc
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : ¬a ∈ support x
⊢ ¬↑f a ∈ ↑f '' support x
contrapose! ha
case neg.hnc.intro.intro
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b✝ : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : ↑f a ∈ ↑f '' support x
b : Γ
hb1 : b ∈ support x
hb2 : ↑f b = ↑f a
⊢ a ∈ support x
case neg.hnc
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : ↑f a ∈ ↑f '' support x
⊢ a ∈ support x
obtain ⟨b, hb1, hb2⟩ := (Set.mem_image _ _ _).1 ha
no goals
case neg.hnc.intro.intro
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a✝ b✝ : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
a : Γ
ha : ↑f a ∈ ↑f '' support x
b : Γ
hb1 : b ∈ support x
hb2 : ↑f b = ↑f a
⊢ a ∈ support x
rwa [f.injective hb2] at hb1