-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_induction {p : α → Prop} (hp : ∀ a₁, p a₁ → ∀ a₂, p a₂ → p (a₁ ⊔ a₂))
    (hs : ∀ b ∈ s, p (f b)) : p (s.sup' H f)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ WithBot.recBotCoe True p ↑(s.sup' H f)

Tactic:
rw [coe_sup']

Result:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ WithBot.recBotCoe True p (s.sup (WithBot.some ∘ f))

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁✝ a₂ : WithBot α
a₁ : α
h₁ : WithBot.recBotCoe True p ↑a₁
h₂ : WithBot.recBotCoe True p ⊥
⊢ WithBot.recBotCoe True p (↑a₁ ⊔ ⊥)

Tactic:
rwa [sup_bot_eq]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁ : WithBot α
h₁ : WithBot.recBotCoe True p a₁
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p (a₁ ⊔ a₂)

Tactic:
match a₁, a₂ with
| ⊥, _ => rwa [bot_sup_eq]
| (a₁ : α), ⊥ => rwa [sup_bot_eq]
| (a₁ : α), (a₂ : α) => exact hp a₁ h₁ a₂ h₂

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ p (s.sup' H f)

Tactic:
show @WithBot.recBotCoe α (fun _ => Prop) True p ↑(s.sup' H f)

Result:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ WithBot.recBotCoe True p ↑(s.sup' H f)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ WithBot.recBotCoe True p (s.sup (WithBot.some ∘ f))

Tactic:
refine sup_induction trivial (fun a₁ h₁ a₂ h₂ ↦ ?_) hs

Result:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁ : WithBot α
h₁ : WithBot.recBotCoe True p a₁
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p (a₁ ⊔ a₂)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁ a₂ x✝ : WithBot α
h₁ : WithBot.recBotCoe True p ⊥
h₂ : WithBot.recBotCoe True p x✝
⊢ WithBot.recBotCoe True p (⊥ ⊔ x✝)

Tactic:
rwa [bot_sup_eq]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁✝ a₂✝ : WithBot α
a₁ a₂ : α
h₁ : WithBot.recBotCoe True p ↑a₁
h₂ : WithBot.recBotCoe True p ↑a₂
⊢ WithBot.recBotCoe True p (↑a₁ ⊔ ↑a₂)

Tactic:
exact hp a₁ h₁ a₂ h₂

Result:
no goals