case empty
F : Type ?u.75184
α : Type u_1
β : Type u_2
γ : Type ?u.75193
ι : Type ?u.75196
κ : Type ?u.75199
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s → p (f b)
hs : ∀ (b : β), b ∈ ∅ → p (f b)
⊢ p (sup ∅ f)

case cons
F : Type ?u.75184
α : Type u_1
β : Type u_2
γ : Type ?u.75193
ι : Type ?u.75196
κ : Type ?u.75199
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (sup (cons c s hc) f)
F : Type ?u.75184
α : Type u_1
β : Type u_2
γ : Type ?u.75193
ι : Type ?u.75196
κ : Type ?u.75199
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ p (sup s f)
induction' s using Finset.cons_induction with c s hc ih
no goals
case empty
F : Type ?u.75184
α : Type u_1
β : Type u_2
γ : Type ?u.75193
ι : Type ?u.75196
κ : Type ?u.75199
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s → p (f b)
hs : ∀ (b : β), b ∈ ∅ → p (f b)
⊢ p (sup ∅ f)
exact hb
case cons
F : Type ?u.75184
α : Type u_1
β : Type u_2
γ : Type ?u.75193
ι : Type ?u.75196
κ : Type ?u.75199
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (f c ⊔ sup s f)
case cons
F : Type ?u.75184
α : Type u_1
β : Type u_2
γ : Type ?u.75193
ι : Type ?u.75196
κ : Type ?u.75199
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (sup (cons c s hc) f)
rw [sup_cons]
case cons.a
F : Type ?u.75184
α : Type u_1
β : Type u_2
γ : Type ?u.75193
ι : Type ?u.75196
κ : Type ?u.75199
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (f c)

case cons.a
F : Type ?u.75184
α : Type u_1
β : Type u_2
γ : Type ?u.75193
ι : Type ?u.75196
κ : Type ?u.75199
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (sup s f)
case cons
F : Type ?u.75184
α : Type u_1
β : Type u_2
γ : Type ?u.75193
ι : Type ?u.75196
κ : Type ?u.75199
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (f c ⊔ sup s f)
apply hp
no goals
case cons.a
F : Type ?u.75184
α : Type u_1
β : Type u_2
γ : Type ?u.75193
ι : Type ?u.75196
κ : Type ?u.75199
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (f c)
exact hs c (mem_cons.2 (Or.inl rfl))
no goals
case cons.a
F : Type ?u.75184
α : Type u_1
β : Type u_2
γ : Type ?u.75193
ι : Type ?u.75196
κ : Type ?u.75199
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (sup s f)
exact ih fun b h => hs b (mem_cons.2 (Or.inr h))