α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.804933
inst✝² : MeasurableSpace α
K : Type ?u.804939
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    ¬a_1 ∈ s →
      (↑(Finset.sup s f) a = Finset.sup s fun c => ↑(f c) a) →
        ↑(Finset.sup (insert a_1 s) f) a = Finset.sup (insert a_1 s) fun c => ↑(f c) a
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.804933
inst✝² : MeasurableSpace α
K : Type ?u.804939
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ ↑(Finset.sup s f) a = Finset.sup s fun c => ↑(f c) a
refine' Finset.induction_on s rfl _
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.804933
inst✝² : MeasurableSpace α
K : Type ?u.804939
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s✝ : Finset γ
a✝¹ : α
a : γ
s : Finset γ
a✝ : ¬a ∈ s
ih : ↑(Finset.sup s f) a✝¹ = Finset.sup s fun c => ↑(f c) a✝¹
⊢ ↑(Finset.sup (insert a s) f) a✝¹ = Finset.sup (insert a s) fun c => ↑(f c) a✝¹
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.804933
inst✝² : MeasurableSpace α
K : Type ?u.804939
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    ¬a_1 ∈ s →
      (↑(Finset.sup s f) a = Finset.sup s fun c => ↑(f c) a) →
        ↑(Finset.sup (insert a_1 s) f) a = Finset.sup (insert a_1 s) fun c => ↑(f c) a
intro a s _ ih
no goals
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.804933
inst✝² : MeasurableSpace α
K : Type ?u.804939
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s✝ : Finset γ
a✝¹ : α
a : γ
s : Finset γ
a✝ : ¬a ∈ s
ih : ↑(Finset.sup s f) a✝¹ = Finset.sup s fun c => ↑(f c) a✝¹
⊢ ↑(Finset.sup (insert a s) f) a✝¹ = Finset.sup (insert a s) fun c => ↑(f c) a✝¹
rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]