F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ ↑(g (sup' s H f)) = sup s (WithBot.some ∘ g ∘ f)
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ g (sup' s H f) = sup' s H (g ∘ f)
rw [← WithBot.coe_eq_coe, coe_sup']
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ ↑(g (sup' s H f)) = sup s (WithBot.some ∘ g ∘ f)
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ ↑(g (sup' s H f)) = sup s (WithBot.some ∘ g ∘ f)
let g' := WithBot.map g
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ g' ↑(sup' s H f) = sup s fun a => g' ↑(f a)
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ ↑(g (sup' s H f)) = sup s (WithBot.some ∘ g ∘ f)
show g' ↑(s.sup' H f) = s.sup fun a => g' ↑(f a)
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ g' (sup s (WithBot.some ∘ f)) = sup s fun a => g' ↑(f a)
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ g' ↑(sup' s H f) = sup s fun a => g' ↑(f a)
rw [coe_sup']
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ ∀ (x y : WithBot α), g' (x ⊔ y) = g' x ⊔ g' y
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ g' (sup s (WithBot.some ∘ f)) = sup s fun a => g' ↑(f a)
refine' comp_sup_eq_sup_comp g' _ rfl
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₁ f₂ : WithBot α
⊢ g' (f₁ ⊔ f₂) = g' f₁ ⊔ g' f₂
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ ∀ (x y : WithBot α), g' (x ⊔ y) = g' x ⊔ g' y
intro f₁ f₂
no goals
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₁ f₂ : WithBot α
⊢ g' (f₁ ⊔ f₂) = g' f₁ ⊔ g' f₂
cases f₁ using WithBot.recBotCoe with
| bot =>
  rw [bot_sup_eq]
  exact bot_sup_eq.symm
| coe f₁ =>
  cases f₂ using WithBot.recBotCoe with
  | bot => rfl
  | coe f₂ => exact congr_arg _ (g_sup f₁ f₂)
case bot
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₂ : WithBot α
⊢ g' f₂ = g' ⊥ ⊔ g' f₂
case bot
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₂ : WithBot α
⊢ g' (⊥ ⊔ f₂) = g' ⊥ ⊔ g' f₂
rw [bot_sup_eq]
no goals
case bot
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₂ : WithBot α
⊢ g' f₂ = g' ⊥ ⊔ g' f₂
exact bot_sup_eq.symm
no goals
case coe
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₂ : WithBot α
f₁ : α
⊢ g' (↑f₁ ⊔ f₂) = g' ↑f₁ ⊔ g' f₂
cases f₂ using WithBot.recBotCoe with
| bot => rfl
| coe f₂ => exact congr_arg _ (g_sup f₁ f₂)
no goals
case coe.bot
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₁ : α
⊢ g' (↑f₁ ⊔ ⊥) = g' ↑f₁ ⊔ g' ⊥
rfl
no goals
case coe.coe
F : Type ?u.259369
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.259381
κ : Type ?u.259384
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₁ f₂ : α
⊢ g' (↑f₁ ⊔ ↑f₂) = g' ↑f₁ ⊔ g' ↑f₂
exact congr_arg _ (g_sup f₁ f₂)