Fixing Finset.induction

Stream: mathlib4

[Jeremy Tan]

How do I get the Finset.induction line here to work and the interₛ function to compile?

import Mathlib.Analysis.Convex.Extreme
import Mathlib.Analysis.Convex.Function
import Mathlib.Topology.Algebra.Module.Basic
import Mathlib.Topology.Order.Basic

open Classical Affine BigOperators Set

section PreorderSemiring

variable (𝕜 : Type _) {E : Type _} [TopologicalSpace 𝕜] [Semiring 𝕜] [Preorder 𝕜] [AddCommMonoid E]
  [TopologicalSpace E] [Module 𝕜 E] {A B : Set E}

def IsExposed (A B : Set E) : Prop :=
  B.Nonempty → ∃ l : E →L[𝕜] 𝕜, B = { x ∈ A | ∀ y ∈ A, l y ≤ l x }

end PreorderSemiring

variable {𝕜 : Type _} {E : Type _} [TopologicalSpace 𝕜] [OrderedRing 𝕜] [AddCommMonoid E]
  [TopologicalSpace E] [Module 𝕜 E] {A B : Set E}

theorem interₛ [ContinuousAdd 𝕜] {F : Finset (Set E)} (hF : F.Nonempty)
    (hAF : ∀ B ∈ F, IsExposed 𝕜 A B) : IsExposed 𝕜 A (⋂₀ F) := by
  revert hF F
  refine' Finset.induction _ _ -- here
  · rintro h
    exfalso
    exact not_nonempty_empty h
  rintro C F _ hF _ hCF
  rw [Finset.coe_insert, interₛ_insert]
  obtain rfl | hFnemp := F.eq_empty_or_nonempty
  · rw [Finset.coe_empty, interₛ_empty, inter_univ]
    exact hCF C (Finset.mem_singleton_self C)
  exact (hCF C (Finset.mem_insert_self C F)).inter
    (hF hFnemp fun B hB => hCF B (Finset.mem_insert_of_mem hB))

[Eric Wieser]

I would recommend induction F using finset.induction (and dropping the revert too)

[Jeremy Tan]

It's from !4#3453. With the original code (refine' Finset.induction _ _) I get the error message

type mismatch
  fun s => Finset.induction ?m.24263 ?m.24264 s
has type
  Finset ?m.24260 → (∀ (B : Set E), B ∈ F✝ → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F✝) : Prop
but is expected to have type
  Finset.Nonempty F✝ → (∀ (B : Set E), B ∈ F✝ → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F✝) : Prop
the following variables have been introduced by the implicit lambda feature
  F✝ : Finset (Set E)
you can disable implicit lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.

which suggests to me that deleting an implicit variable somewhere should solve everything, but how do I do that?

[Jeremy Tan]

Or how can I go on with the code I already have in !4#3453?

[Eric Wieser]

Did you try my suggestion above?