case refine'_1
F : Type ?u.16149
α : Type u_1
β : Type u_2
γ : Type ?u.16158
ι : Type ?u.16161
κ : Type ?u.16164
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
⊢ sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g

case refine'_2
F : Type ?u.16149
α : Type u_1
β : Type u_2
γ : Type ?u.16158
ι : Type ?u.16161
κ : Type ?u.16164
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
b : β
t : Finset β
x✝ : ¬b ∈ t
h : sup t (f ⊔ g) = sup t f ⊔ sup t g
⊢ sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) g
F : Type ?u.16149
α : Type u_1
β : Type u_2
γ : Type ?u.16158
ι : Type ?u.16161
κ : Type ?u.16164
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
⊢ sup s (f ⊔ g) = sup s f ⊔ sup s g
refine' Finset.cons_induction_on s _ fun b t _ h => _
no goals
case refine'_1
F : Type ?u.16149
α : Type u_1
β : Type u_2
γ : Type ?u.16158
ι : Type ?u.16161
κ : Type ?u.16164
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
⊢ sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
case refine'_2
F : Type ?u.16149
α : Type u_1
β : Type u_2
γ : Type ?u.16158
ι : Type ?u.16161
κ : Type ?u.16164
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
b : β
t : Finset β
x✝ : ¬b ∈ t
h : sup t (f ⊔ g) = sup t f ⊔ sup t g
⊢ (f ⊔ g) b ⊔ (sup t f ⊔ sup t g) = f b ⊔ sup t f ⊔ (g b ⊔ sup t g)
case refine'_2
F : Type ?u.16149
α : Type u_1
β : Type u_2
γ : Type ?u.16158
ι : Type ?u.16161
κ : Type ?u.16164
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
b : β
t : Finset β
x✝ : ¬b ∈ t
h : sup t (f ⊔ g) = sup t f ⊔ sup t g
⊢ sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) g
rw [sup_cons, sup_cons, sup_cons, h]
no goals
case refine'_2
F : Type ?u.16149
α : Type u_1
β : Type u_2
γ : Type ?u.16158
ι : Type ?u.16161
κ : Type ?u.16164
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
b : β
t : Finset β
x✝ : ¬b ∈ t
h : sup t (f ⊔ g) = sup t f ⊔ sup t g
⊢ (f ⊔ g) b ⊔ (sup t f ⊔ sup t g) = f b ⊔ sup t f ⊔ (g b ⊔ sup t g)
exact sup_sup_sup_comm _ _ _ _