F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ WithBot.recBotCoe True p ↑(sup' s H f)
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ p (sup' s H f)
show @WithBot.recBotCoe α (fun _ => Prop) True p ↑(s.sup' H f)
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ WithBot.recBotCoe True p (sup s (WithBot.some ∘ f))
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ WithBot.recBotCoe True p ↑(sup' s H f)
rw [coe_sup']
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ ∀ (a₁ : WithBot α),
    WithBot.recBotCoe True p a₁ → ∀ (a₂ : WithBot α), WithBot.recBotCoe True p a₂ → WithBot.recBotCoe True p (a₁ ⊔ a₂)
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ WithBot.recBotCoe True p (sup s (WithBot.some ∘ f))
refine' sup_induction trivial _ hs
case none
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
h₁ : WithBot.recBotCoe True p none
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p (none ⊔ a₂)

case some
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
a₁ : α
h₁ : WithBot.recBotCoe True p (some a₁)
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p (some a₁ ⊔ a₂)
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ ∀ (a₁ : WithBot α),
    WithBot.recBotCoe True p a₁ → ∀ (a₂ : WithBot α), WithBot.recBotCoe True p a₂ → WithBot.recBotCoe True p (a₁ ⊔ a₂)
rintro (_ | a₁) h₁ a₂ h₂
case none
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
h₁ : WithBot.recBotCoe True p none
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p a₂
case none
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
h₁ : WithBot.recBotCoe True p none
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p (none ⊔ a₂)
rw [WithBot.none_eq_bot, bot_sup_eq]
no goals
case none
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
h₁ : WithBot.recBotCoe True p none
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p a₂
exact h₂
no goals
case some
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
a₁ : α
h₁ : WithBot.recBotCoe True p (some a₁)
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p (some a₁ ⊔ a₂)
cases a₂ using WithBot.recBotCoe with
| bot => exact h₁
| coe a₂ => exact hp a₁ h₁ a₂ h₂
no goals
case some.bot
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
a₁ : α
h₁ : WithBot.recBotCoe True p (some a₁)
h₂ : WithBot.recBotCoe True p ⊥
⊢ WithBot.recBotCoe True p (some a₁ ⊔ ⊥)
exact h₁
no goals
case some.coe
F : Type ?u.260693
α : Type u_1
β : Type u_2
γ : Type ?u.260702
ι : Type ?u.260705
κ : Type ?u.260708
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
a₁ : α
h₁ : WithBot.recBotCoe True p (some a₁)
a₂ : α
h₂ : WithBot.recBotCoe True p ↑a₂
⊢ WithBot.recBotCoe True p (some a₁ ⊔ ↑a₂)
exact hp a₁ h₁ a₂ h₂