awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Exposed
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
hxB : ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)
hxC : ∀ 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₁ + l₂ : (a : E) → 𝕜) y : 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) x : 𝕜)} x

Tactic:
⟨hxA, fun z hz => add_le_add (hxB z hz) (hxC z hz)⟩

Premises used: Set.Mem, add_le_add, setOf, And.intro
-- Module: Mathlib.Analysis.Convex.Exposed
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
hxB : ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)
hxC : ∀ 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₁ + l₂ : (a : E) → 𝕜) y : 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) x : 𝕜)} x

Tactic:
exact ⟨hxA, fun z hz => add_le_add (hxB z hz) (hxC z hz)⟩
-- Module: Mathlib.Analysis.Convex.Exposed
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

Tactic:
⟨⟨hxA, fun y hy => ?_⟩, hxA, fun y hy => ?_⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Analysis.Convex.Exposed
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 : 𝕜)
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

Tactic:
refine ⟨⟨hxA, fun y hy => ?_⟩, hxA, fun y hy => ?_⟩
-- Module: Mathlib.Analysis.Convex.Exposed
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 : 𝕜)
y : E
hy : y ∈ A
⊢ LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)

Tactic:
(add_le_add_iff_right (l₂ x)).1 ((add_le_add (hwB.2 y hy) (hwC.2 x hxA)).trans (hx w hwB.1))

Premises used: add_le_add, add_le_add_iff_right, And.right, And.left, Iff.mp, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Exposed
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 : 𝕜)
y : E
hy : y ∈ A
⊢ LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)

Tactic:
exact
      (add_le_add_iff_right (l₂ x)).1 ((add_le_add (hwB.2 y hy) (hwC.2 x hxA)).trans (hx w hwB.1))

Premises used: add_le_add, add_le_add_iff_right, And.right, And.left, Iff.mp, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Exposed
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 : 𝕜)
y : E
hy : y ∈ A
⊢ LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)

Tactic:
(add_le_add_iff_left (l₁ x)).1 (le_trans (add_le_add (hwB.2 x hxA) (hwC.2 y hy)) (hx w hwB.1))

Premises used: add_le_add, add_le_add_iff_left, And.right, And.left, Iff.mp, DFunLike.coe, le_trans
-- Module: Mathlib.Analysis.Convex.Exposed
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 : 𝕜)
y : E
hy : y ∈ A
⊢ LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)

Tactic:
exact
      (add_le_add_iff_left (l₁ x)).1 (le_trans (add_le_add (hwB.2 x hxA) (hwC.2 y hy)) (hx w hwB.1))

Premises used: add_le_add, add_le_add_iff_left, And.right, And.left, Iff.mp, DFunLike.coe, le_trans
-- Module: Mathlib.Analysis.Convex.Exposed
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
empty : False
⊢ IsExposed 𝕜 A (⋂₀ (↑∅ : Set (Set E)))

Tactic:
exfalso
-- Module: Mathlib.Analysis.Convex.Exposed
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
⊢ False

Tactic:
Finset.not_nonempty_empty hF

Premises used: Finset.not_nonempty_empty
-- Module: Mathlib.Analysis.Convex.Exposed
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
⊢ False

Tactic:
exact Finset.not_nonempty_empty hF

Premises used: Finset.not_nonempty_empty
-- Module: Mathlib.Analysis.Convex.Exposed
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 : IsExposed 𝕜 A (C ∩ ⋂₀ (↑F : Set (Set E)))
⊢ IsExposed 𝕜 A (⋂₀ (↑(Insert.insert C F) : Set (Set E)))

Tactic:
rw [Finset.coe_insert, sInter_insert]

Premises used: Set.sInter_insert, Finset.coe_insert
-- Module: Mathlib.Analysis.Convex.Exposed
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)))
insert₁ : ∀ (hFnemp : F.Nonempty), IsExposed 𝕜 A (C ∩ ⋂₀ (↑F : Set (Set E)))
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ (↑F : Set (Set E)))

Tactic:
obtain rfl | hFnemp := F.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Analysis.Convex.Exposed
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.insert C ∅)
hAF : ∀ (B : Set E), Membership.mem (γ := Finset (Set E)) (Insert.insert C ∅) B → IsExposed 𝕜 A B
insert : IsExposed 𝕜 A C
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ (↑∅ : Set (Set E)))

Tactic:
rw [Finset.coe_empty, sInter_empty, inter_univ]

Premises used: Finset.coe_empty, Set.sInter_empty, Set.inter_univ
-- Module: Mathlib.Analysis.Convex.Exposed
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

Tactic:
hAF C (Finset.mem_singleton_self C)

Premises used: Finset.mem_singleton_self
-- Module: Mathlib.Analysis.Convex.Exposed
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

Tactic:
exact hAF C (Finset.mem_singleton_self C)

Premises used: Finset.mem_singleton_self
-- Module: Mathlib.Analysis.Convex.Exposed
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
hFnemp : F.Nonempty
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ (↑F : Set (Set E)))

Tactic:
(hAF C (Finset.mem_insert_self C F)).inter
        (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))

Premises used: Finset.mem_insert_self, IsExposed.inter, Finset.mem_insert_of_mem
-- Module: Mathlib.Analysis.Convex.Exposed
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
hFnemp : F.Nonempty
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ (↑F : Set (Set E)))

Tactic:
exact (hAF C (Finset.mem_insert_self C F)).inter
        (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))

Premises used: Finset.mem_insert_self, IsExposed.inter, Finset.mem_insert_of_mem
-- Module: Mathlib.Analysis.Convex.Exposed
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)))
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.insert C F).Nonempty) (hAF : ∀ B ∈ Insert.insert C F, IsExposed 𝕜 A B),
        IsExposed 𝕜 A (⋂₀ (↑(Insert.insert C F) : Set (Set E)))
⊢ IsExposed 𝕜 A (⋂₀ (↑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))

Premises used: Finset.coe_empty, Set.sInter_empty, Set.inter_univ, Set.sInter_insert, Insert.insert, Finset.coe_insert, rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Analysis.Convex.Exposed
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)))
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.insert C F).Nonempty) (hAF : ∀ B ∈ Insert.insert C F, IsExposed 𝕜 A B),
        IsExposed 𝕜 A (⋂₀ (↑(Insert.insert C F) : Set (Set E)))
⊢ IsExposed 𝕜 A (⋂₀ (↑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))

Premises used: Finset.coe_empty, Set.sInter_empty, Set.inter_univ, Set.sInter_insert, Insert.insert, Finset.coe_insert, rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Analysis.Convex.Exposed
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
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 : 𝕜)}
⊢ ∃ (l : StrongDual 𝕜 E),
    C = {x : E | x ∈ A ∩ B ∧ ∀ y ∈ A ∩ B, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}

Tactic:
obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Analysis.Convex.Exposed
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 : Set E
w : E
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:
⟨l, Subset.antisymm (fun x hx => ⟨⟨hx.1, hCB hx⟩, fun y hy => hx.2 y hy.1⟩)
    fun x ⟨⟨hxC, _⟩, hx⟩ => ⟨hxC, fun y hy => (hw.2 y hy).trans (hx w ⟨hC.subset hw, hCB hw⟩)⟩⟩

Premises used: Set.Subset.antisymm, IsExposed.subset, _private.0.IsExposed.inter_left.match_1, setOf, Membership.mem, And, And.right, And.left, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Exposed
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 : Set E
w : E
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:
exact ⟨l, Subset.antisymm (fun x hx => ⟨⟨hx.1, hCB hx⟩, fun y hy => hx.2 y hy.1⟩)
    fun x ⟨⟨hxC, _⟩, hx⟩ => ⟨hxC, fun y hy => (hw.2 y hy).trans (hx w ⟨hC.subset hw, hCB hw⟩)⟩⟩