awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)}
hwB :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} w
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)}
hwC :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)} w
refine_1 :
  Subset.{u_2} (α := Set E)
    ({x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)})
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) y : 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) x : 𝕜)}
⊢ ∃ (l : StrongDual 𝕜 E),
    Eq.{u_2 + 1} (α := Set E)
      ({x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩
        {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)})
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
have refine_2 : Subset.{u_2} (α := Set E)
  {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) y : 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) x : 𝕜)}
  ({x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)})
Tactic: refine ⟨l₁ + l₂, Subset.antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)}
hwB :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} w
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)}
hwC :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)} w
x : E
hxA : x ∈ A
hx : ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) y : 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) x : 𝕜)
⊢ Membership.mem (γ := Set E)
    ({x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)})
    x
have refine_2 : ∀ (y : E) (hy : y ∈ A), LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)
Tactic: refine ⟨⟨hxA, fun y hy => ?_⟩, hxA, fun y hy => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)}
hwB :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} w
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)}
hwC :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)} w
x : E
hxA : x ∈ A
hx : ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) y : 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) x : 𝕜)
refine_2 : ∀ (y : E) (hy : y ∈ A), LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)
⊢ Membership.mem (γ := Set E)
    ({x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)})
    x
have refine_2₁ : ∀ (y : E) (hy : y ∈ A), LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)
Tactic: refine ⟨⟨hxA, fun y hy => ?_⟩, hxA, fun y hy => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
hF : Finset.Nonempty.{u_2} (α := Set E) ∅
hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) ∅ B → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ (↑∅ : Set (Set E)))
have empty : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
h : C ∉ F
hF' : ∀ (hF : F.Nonempty) (hAF : ∀ B ∈ F, IsExposed 𝕜 A B), IsExposed 𝕜 A (⋂₀ (↑F : Set (Set E)))
hF : (insert C F).Nonempty
hAF : ∀ B ∈ insert C F, IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ (↑(insert C F) : Set (Set E)))
have insert : IsExposed 𝕜 A (C ∩ ⋂₀ (↑F : Set (Set E)))
Tactic: rw [Finset.coe_insert, sInter_insert]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
h : C ∉ F
hF' : ∀ (hF : F.Nonempty) (hAF : ∀ B ∈ F, IsExposed 𝕜 A B), IsExposed 𝕜 A (⋂₀ (↑F : Set (Set E)))
hF : (insert C F).Nonempty
hAF : ∀ B ∈ insert C F, IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ (↑F : Set (Set E)))
have insert : C ∉ ∅ →
  ∀
    (hF' :
      ∀ (hF : Finset.Nonempty.{u_2} (α := Set E) ∅)
        (hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) ∅ B → IsExposed 𝕜 A B),
        IsExposed 𝕜 A (⋂₀ (↑∅ : Set (Set E))))
    (hF : Finset.Nonempty (α := Set E) (insert C ∅))
    (hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) (insert C ∅) B → IsExposed 𝕜 A B),
    IsExposed 𝕜 A (C ∩ ⋂₀ (↑∅ : Set (Set E)))
Tactic: obtain rfl | hFnemp := F.eq_empty_or_nonempty
Cleared hypotheses: F, h, hF', hF, hAF
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
h : C ∉ F
hF' : ∀ (hF : F.Nonempty) (hAF : ∀ B ∈ F, IsExposed 𝕜 A B), IsExposed 𝕜 A (⋂₀ (↑F : Set (Set E)))
hF : (Insert.insert C F).Nonempty
hAF : ∀ B ∈ Insert.insert C F, IsExposed 𝕜 A B
insert :
  C ∉ ∅ →
    ∀
      (hF' :
        ∀ (hF : Finset.Nonempty.{u_2} (α := Set E) ∅)
          (hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) ∅ B → IsExposed 𝕜 A B),
          IsExposed 𝕜 A (⋂₀ (↑∅ : Set (Set E))))
      (hF : Finset.Nonempty (α := Set E) (Insert.insert C ∅))
      (hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) (Insert.insert C ∅) B → IsExposed 𝕜 A B),
      IsExposed 𝕜 A (C ∩ ⋂₀ (↑∅ : Set (Set E)))
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ (↑F : Set (Set E)))
have insert₁ : ∀ (hFnemp : F.Nonempty), IsExposed 𝕜 A (C ∩ ⋂₀ (↑F : Set (Set E)))
Tactic: obtain rfl | hFnemp := F.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
C : Set E
h : C ∉ ∅
hF' :
  ∀ (hF : Finset.Nonempty.{u_2} (α := Set E) ∅)
    (hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) ∅ B → IsExposed 𝕜 A B),
    IsExposed 𝕜 A (⋂₀ (↑∅ : Set (Set E)))
hF : Finset.Nonempty (α := Set E) (insert C ∅)
hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) (insert C ∅) B → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ (↑∅ : Set (Set E)))
have insert : IsExposed 𝕜 A C
Tactic: rw [Finset.coe_empty, sInter_empty, inter_univ]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
F : Finset (Set E)
hF : F.Nonempty
hAF : ∀ B ∈ F, IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ (↑F : Set (Set E)))
have empty : ∀ (hF : Finset.Nonempty.{u_2} (α := Set E) ∅)
  (hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) ∅ B → IsExposed 𝕜 A B),
  IsExposed 𝕜 A (⋂₀ (↑∅ : Set (Set E)))
Tactic: induction F using Finset.induction with
  | empty => exfalso; exact Finset.not_nonempty_empty hF
  | insert C F _ hF' =>
    rw [Finset.coe_insert, sInter_insert]
    obtain rfl | hFnemp := F.eq_empty_or_nonempty
    · rw [Finset.coe_empty, sInter_empty, inter_univ]
      exact hAF C (Finset.mem_singleton_self C)
    · exact (hAF C (Finset.mem_insert_self C F)).inter
        (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))
Cleared hypotheses: F, hF, hAF
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
F : Finset (Set E)
hF : F.Nonempty
hAF : ∀ B ∈ F, IsExposed 𝕜 A B
empty :
  ∀ (hF : Finset.Nonempty.{u_2} (α := Set E) ∅)
    (hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) ∅ B → IsExposed 𝕜 A B),
    IsExposed 𝕜 A (⋂₀ (↑∅ : Set (Set E)))
⊢ IsExposed 𝕜 A (⋂₀ (↑F : Set (Set E)))
have insert : ∀ (C : Set E) (F : Finset (Set E)),
  C ∉ F →
    ∀ (hF' : ∀ (hF : F.Nonempty) (hAF : ∀ B ∈ F, IsExposed 𝕜 A B), IsExposed 𝕜 A (⋂₀ (↑F : Set (Set E))))
      (hF : (insert C F).Nonempty) (hAF : ∀ B ∈ insert C F, IsExposed 𝕜 A B),
      IsExposed 𝕜 A (⋂₀ (↑(insert C F) : Set (Set E)))
Tactic: induction F using Finset.induction with
  | empty => exfalso; exact Finset.not_nonempty_empty hF
  | insert C F _ hF' =>
    rw [Finset.coe_insert, sInter_insert]
    obtain rfl | hFnemp := F.eq_empty_or_nonempty
    · rw [Finset.coe_empty, sInter_empty, inter_univ]
      exact hAF C (Finset.mem_singleton_self C)
    · exact (hAF C (Finset.mem_insert_self C F)).inter
        (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))
Cleared hypotheses: F, hF, hAF
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
F : Finset (Set E)
hF : F.Nonempty
hAF : ∀ B ∈ F, IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ (↑F : Set (Set E)))
have empty : ∀ (hF : Finset.Nonempty.{u_2} (α := Set E) ∅)
  (hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) ∅ B → IsExposed 𝕜 A B),
  IsExposed 𝕜 A (⋂₀ (↑∅ : Set (Set E)))
Tactic: classical
  induction F using Finset.induction with
  | empty => exfalso; exact Finset.not_nonempty_empty hF
  | insert C F _ hF' =>
    rw [Finset.coe_insert, sInter_insert]
    obtain rfl | hFnemp := F.eq_empty_or_nonempty
    · rw [Finset.coe_empty, sInter_empty, inter_univ]
      exact hAF C (Finset.mem_singleton_self C)
    · exact (hAF C (Finset.mem_insert_self C F)).inter
        (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))
Cleared hypotheses: F, hF, hAF
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
F : Finset (Set E)
hF : F.Nonempty
hAF : ∀ B ∈ F, IsExposed 𝕜 A B
empty :
  ∀ (hF : Finset.Nonempty.{u_2} (α := Set E) ∅)
    (hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) ∅ B → IsExposed 𝕜 A B),
    IsExposed 𝕜 A (⋂₀ (↑∅ : Set (Set E)))
⊢ IsExposed 𝕜 A (⋂₀ (↑F : Set (Set E)))
have insert : ∀ (C : Set E) (F : Finset (Set E)),
  C ∉ F →
    ∀ (hF' : ∀ (hF : F.Nonempty) (hAF : ∀ B ∈ F, IsExposed 𝕜 A B), IsExposed 𝕜 A (⋂₀ (↑F : Set (Set E))))
      (hF : (insert C F).Nonempty) (hAF : ∀ B ∈ insert C F, IsExposed 𝕜 A B),
      IsExposed 𝕜 A (⋂₀ (↑(insert C F) : Set (Set E)))
Tactic: classical
  induction F using Finset.induction with
  | empty => exfalso; exact Finset.not_nonempty_empty hF
  | insert C F _ hF' =>
    rw [Finset.coe_insert, sInter_insert]
    obtain rfl | hFnemp := F.eq_empty_or_nonempty
    · rw [Finset.coe_empty, sInter_empty, inter_univ]
      exact hAF C (Finset.mem_singleton_self C)
    · exact (hAF C (Finset.mem_insert_self C F)).inter
        (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))
Cleared hypotheses: F, hF, hAF
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hCB : C ⊆ B
w : E
hw : w ∈ C
⊢ ∃ (l : StrongDual 𝕜 E),
    C = {x : E | x ∈ A ∩ B ∧ ∀ y ∈ A ∩ B, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
have obtain : ∀ (l : StrongDual 𝕜 E)
  (hC :
    IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)})
  (hCB : {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} ⊆ B)
  (hw :
    Membership.mem (γ := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} w),
  ∃ (l_1 : StrongDual 𝕜 E),
    Eq.{u_2 + 1} (α := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
      {x : E | x ∈ A ∩ B ∧ ∀ y ∈ A ∩ B, LE.le.{u_1} (α := 𝕜) ((l_1 : (a : E) → 𝕜) y : 𝕜) ((l_1 : (a : E) → 𝕜) x : 𝕜)}
Tactic: obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩
Cleared hypotheses: C, hC, hCB, hw
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (A ∩ B) C
have rw : IsExposed 𝕜 (B ∩ A) C
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
⊢ IsClosed B
have inl : ∀ (hAB : IsExposed 𝕜 A ∅), IsClosed.{u_2} (X := E) ∅
Tactic: obtain rfl | hB := B.eq_empty_or_nonempty
Cleared hypotheses: B, hAB
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
inl : ∀ (hAB : IsExposed 𝕜 A ∅), IsClosed.{u_2} (X := E) ∅
⊢ IsClosed B
have inr : ∀ (hB : B.Nonempty), IsClosed B
Tactic: obtain rfl | hB := B.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
hB : B.Nonempty
⊢ IsClosed B
have inr : ∀ (l : StrongDual 𝕜 E) (a : 𝕜) (hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x})
  (hB : Set.Nonempty.{u_2} (α := E) {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}),
  IsClosed.{u_2} (X := E) {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
Tactic: obtain ⟨l, a, rfl⟩ := hAB.eq_inter_halfSpace' hB
Cleared hypotheses: B, hAB, hB
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
x : E
⊢ x ∈ exposedPoints 𝕜 A ↔ IsExposed 𝕜 A {x}
have mpr : IsExposed 𝕜 A {x} → x ∈ exposedPoints 𝕜 A
Tactic: use fun ⟨hxA, l, hl⟩ _ =>
    ⟨l,
      Eq.symm <|
        eq_singleton_iff_unique_mem.2
          ⟨⟨hxA, fun y hy => (hl y hy).1⟩, fun z hz => (hl z hz.1).2 (hz.2 x hxA)⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
⊢ x ∈ exposedPoints 𝕜 A
have mpr : ∀ (l : StrongDual 𝕜 E)
  (hl :
    Eq (α := Set E) {x}
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}),
  x ∈ exposedPoints 𝕜 A
Tactic: obtain ⟨l, hl⟩ := h ⟨x, mem_singleton _⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
l : StrongDual 𝕜 E
hl :
  Eq (α := Set E) {x}
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
⊢ x ∈ exposedPoints 𝕜 A
have hl₁ : Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x ∧
  ∀ (x_1 : E),
    Membership.mem (γ := Set E)
        {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x_1 →
      x_1 = x
Tactic: rw [eq_comm, eq_singleton_iff_unique_mem] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : AddCommMonoid E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
⊢ Convex 𝕜 B
have inl : ∀ (hAB : IsExposed 𝕜 A ∅), Convex.{u_1, u_2} 𝕜 (E := E) ∅
Tactic: obtain rfl | hB := B.eq_empty_or_nonempty
Cleared hypotheses: B, hAB
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : AddCommMonoid E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
inl : ∀ (hAB : IsExposed 𝕜 A ∅), Convex.{u_1, u_2} 𝕜 (E := E) ∅
⊢ Convex 𝕜 B
have inr : ∀ (hB : B.Nonempty), Convex 𝕜 B
Tactic: obtain rfl | hB := B.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : AddCommMonoid E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
hB : B.Nonempty
⊢ Convex 𝕜 B
have inr : ∀ (l : StrongDual 𝕜 E)
  (hAB :
    IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)})
  (hB :
    Set.Nonempty.{u_2} (α := E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}),
  Convex.{u_1, u_2} 𝕜 (E := E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
Tactic: obtain ⟨l, rfl⟩ := hAB hB
Cleared hypotheses: B, hAB, hB
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : AddCommMonoid E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
⊢ IsExtreme 𝕜 A B
have refine : ∀ (x₁ : E) (hx₁A : x₁ ∈ A) (x₂ : E) (hx₂A : x₂ ∈ A) (x : E) (hxB : x ∈ B) (hx : x ∈ openSegment 𝕜 x₁ x₂), x₁ ∈ B
Tactic: refine ⟨hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxB hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : AddCommMonoid E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ B
have obtain : ∀ (l : StrongDual 𝕜 E)
  (hAB :
    IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)})
  (hxB :
    Membership.mem (γ := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x),
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x₁
Tactic: obtain ⟨l, rfl⟩ := hAB ⟨x, hxB⟩
Cleared hypotheses: B, hAB, hxB
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : AddCommMonoid E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
hxB :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x
⊢ Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x₁
have hl : ConvexOn.{u_1, u_2, u_1} 𝕜 (E := E) (β := 𝕜) univ (⇑l : (a : E) → 𝕜)
Tactic: have hl : ConvexOn 𝕜 univ l := l.toLinearMap.convexOn convex_univ
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : AddCommMonoid E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
hxB :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x
hl : ConvexOn.{u_1, u_2, u_1} 𝕜 (E := E) (β := 𝕜) univ (⇑l : (a : E) → 𝕜)
⊢ Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x₁
have hlx₁ : LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) x₁ : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)
Tactic: have hlx₁ := hxB.2 x₁ hx₁A