case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r✝ : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
⊢ coeff (embDomain f (↑(single g) r)) g' = coeff (↑(single (↑f g)) r) g'
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r✝ : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
⊢ embDomain f (↑(single g) r) = ↑(single (↑f g)) r
ext g'
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 Γ'
g : Γ
r : R
g' : Γ'
h : g' = ↑f g
⊢ coeff (embDomain f (↑(single g) r)) g' = coeff (↑(single (↑f g)) r) g'

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 Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = ↑f g
⊢ coeff (embDomain f (↑(single g) r)) g' = coeff (↑(single (↑f g)) r) g'
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r✝ : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
⊢ coeff (embDomain f (↑(single g) r)) g' = coeff (↑(single (↑f g)) r) g'
by_cases h : g' = f g
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 Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = ↑f g
⊢ ¬g' ∈ ↑f '' support (↑(single g) r)
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 Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = ↑f g
⊢ coeff (embDomain f (↑(single g) r)) g' = coeff (↑(single (↑f g)) r) g'
rw [embDomain_notin_image_support, single_coeff_of_ne h]
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 Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = ↑f g
hr : r = 0
⊢ ¬g' ∈ ↑f '' support (↑(single g) r)

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 Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = ↑f g
hr : ¬r = 0
⊢ ¬g' ∈ ↑f '' support (↑(single g) r)
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 Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = ↑f g
⊢ ¬g' ∈ ↑f '' support (↑(single g) r)
by_cases hr : r = 0
no goals
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 Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = ↑f g
hr : ¬r = 0
⊢ ¬g' ∈ ↑f '' support (↑(single g) r)
rwa [support_single_of_ne hr, Set.image_singleton, Set.mem_singleton_iff]
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 Γ'
g : Γ
r : R
g' : Γ'
h : g' = ↑f g
⊢ coeff (embDomain f (↑(single g) r)) g' = coeff (↑(single (↑f g)) r) g'
simp [h]
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 Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = ↑f g
hr : r = 0
⊢ ¬g' ∈ ↑f '' support (↑(single g) r)
simp [hr]