awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ ≠ 0
a : 𝕜
ha₀ : a ≠ 0
har : ‖a • x‖ < (↑r : ℝ)
hainv : ‖a‖⁻¹ ≤ (↑r : ℝ)⁻¹ * ‖c‖ * ‖x‖
⊢ (↑(‖c‖₊ * ‖x‖₊) : ℝ≥0∞) / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)

Tactic:
simp [ENNReal.coe_mul, enorm]

Premises used: ENNReal.coe_mul, ENorm.enorm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ ≠ 0
a : 𝕜
ha₀ : a ≠ 0
har : ‖a • x‖ < (↑r : ℝ)
hainv : ‖a‖⁻¹ ≤ (↑r : ℝ)⁻¹ * ‖c‖ * ‖x‖
egauge : (↑‖a‖₊⁻¹ : ℝ≥0∞) ≤ (↑(‖c‖₊ * ‖x‖₊ / r) : ℝ≥0∞)
⊢ _root_.egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)

Tactic:
calc
        egauge 𝕜 (ball 0 r) x ≤ ↑(‖a‖₊⁻¹) :=
          egauge_le_of_smul_mem_of_ne (mem_ball_zero_iff.2 har) ha₀
        _ ≤ ↑(‖c‖₊ * ‖x‖₊ / r) := by rwa [ENNReal.coe_le_coe, div_eq_inv_mul, ← mul_assoc]
        _ ≤ ‖c‖ₑ * ‖x‖ₑ / r := ENNReal.coe_div_le.trans <| by simp [ENNReal.coe_mul, enorm]

Premises used: Iff.mpr, HMul.hMul, NNNorm.nnnorm, HDiv.hDiv, Metric.ball, Inv.inv, LE.le.trans, ENNReal.coe_div_le, OfNat.ofNat, egauge, NNReal.toReal, mem_ball_zero_iff, egauge_le_of_smul_mem_of_ne
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
x : E
⊢ egauge 𝕜 (ball 0 1) x ≤ ‖c‖ₑ * ‖x‖ₑ

Tactic:
simpa using egauge_ball_le_of_one_lt_norm hc (.inl one_ne_zero)

Premises used: egauge_ball_le_of_one_lt_norm, Or.inl, one_ne_zero
-- 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
l : StrongDual 𝕜 E
A : Set E
⊢ IsExposed 𝕜 A (toExposed l A)

Tactic:
fun _ => ⟨l, rfl⟩

Premises used: IsExposed, 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 : Set E
h : Set.Nonempty.{u_2} (α := E) ∅
w : E
hx : Membership.mem (γ := Set E) ∅ w
exfalso : False
⊢ ∃ (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 : 𝕜)}

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
h : Set.Nonempty.{u_2} (α := E) ∅
w : E
hx : Membership.mem (γ := Set E) ∅ w
⊢ False

Tactic:
hx

Premises used: Set.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
h : Set.Nonempty.{u_2} (α := E) ∅
w : E
hx : Membership.mem (γ := Set E) ∅ w
⊢ False

Tactic:
exact hx
-- 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
hAB : IsExposed 𝕜 A B
x : E
hx : x ∈ B
obtain :
  ∀ (w : StrongDual 𝕜 E)
    (hAB :
      IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((w : (a : E) → 𝕜) y : 𝕜) ((w : (a : E) → 𝕜) x : 𝕜)})
    (hx :
      Membership.mem (γ := Set E)
        {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((w : (a : E) → 𝕜) y : 𝕜) ((w : (a : E) → 𝕜) x : 𝕜)} x),
    x ∈ A
⊢ x ∈ A

Tactic:
obtain ⟨_, rfl⟩ := hAB ⟨x, hx⟩

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 : Set E
x : E
w : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((w : (a : E) → 𝕜) y : 𝕜) ((w : (a : E) → 𝕜) x : 𝕜)}
hx :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((w : (a : E) → 𝕜) y : 𝕜) ((w : (a : E) → 𝕜) x : 𝕜)} x
⊢ x ∈ A

Tactic:
hx.1

Premises used: And.left
-- 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
x : E
w : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((w : (a : E) → 𝕜) y : 𝕜) ((w : (a : E) → 𝕜) x : 𝕜)}
hx :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((w : (a : E) → 𝕜) y : 𝕜) ((w : (a : E) → 𝕜) x : 𝕜)} x
⊢ x ∈ A

Tactic:
exact hx.1

Premises used: And.left
-- 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
⊢ IsExposed 𝕜 A A

Tactic:
fun ⟨_, _⟩ =>
  ⟨0, Subset.antisymm (fun _ hx => ⟨hx, fun _ _ => le_refl 0⟩) fun _ hx => hx.1⟩

Premises used: Set.Subset.antisymm, le_refl, setOf, Membership.mem, Exists, _private.0.IsExposed.refl.match_1, IsExposed, And, And.left, And.intro, Exists.intro, OfNat.ofNat, Eq
-- 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
hB : IsExposed 𝕜 A B
hA : IsExposed 𝕜 B A
⊢ A = B

Tactic:
hA.subset.antisymm hB.subset

Premises used: IsExposed.subset, HasSubset.Subset.antisymm
-- 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
hBA : B ⊆ A
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 ∈ B ∧ ∀ y ∈ B, LE.le.{u_1} (α := 𝕜) ((l_1 : (a : E) → 𝕜) y : 𝕜) ((l_1 : (a : E) → 𝕜) x : 𝕜)}
⊢ ∃ (l : StrongDual 𝕜 E),
    C = {x : E | x ∈ B ∧ ∀ y ∈ 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
hBA : B ⊆ A
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 ∈ B ∧ ∀ y ∈ B, LE.le.{u_1} (α := 𝕜) ((l_1 : (a : E) → 𝕜) y : 𝕜) ((l_1 : (a : E) → 𝕜) x : 𝕜)}

Tactic:
⟨l, Subset.antisymm (fun x hx => ⟨hCB hx, fun y hy => hx.2 y (hBA hy)⟩) fun x hx =>
    ⟨hBA hx.1, fun y hy => (hw.2 y hy).trans (hx.2 w (hCB hw))⟩⟩

Premises used: Set.Subset.antisymm, 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
hBA : B ⊆ A
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 ∈ B ∧ ∀ y ∈ B, LE.le.{u_1} (α := 𝕜) ((l_1 : (a : E) → 𝕜) y : 𝕜) ((l_1 : (a : E) → 𝕜) x : 𝕜)}

Tactic:
exact ⟨l, Subset.antisymm (fun x hx => ⟨hCB hx, fun y hy => hx.2 y (hBA hy)⟩) fun x hx =>
    ⟨hBA hx.1, fun y hy => (hw.2 y hy).trans (hx.2 w (hCB hw))⟩⟩
-- 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
hAB : IsExposed 𝕜 A B
hB : B.Nonempty
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 : 𝕜)})
    (hB :
      Set.Nonempty.{u_2} (α := E)
        {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}),
    ∃ (l_1 : StrongDual 𝕜 E) (a : 𝕜),
      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 ∧ a ≤ (l_1 : (a : E) → 𝕜) x}
⊢ ∃ (l : StrongDual 𝕜 E) (a : 𝕜), B = {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}

Tactic:
obtain ⟨l, rfl⟩ := hAB hB

Premises used: 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 : Set E
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 : 𝕜)}
obtain :
  ∀ (w : E)
    (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) (a : 𝕜),
      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 ∧ a ≤ (l_1 : (a : E) → 𝕜) x}
⊢ ∃ (l_1 : StrongDual 𝕜 E) (a : 𝕜),
    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 ∧ a ≤ (l_1 : (a : E) → 𝕜) x}

Tactic:
obtain ⟨w, hw⟩ := hB
-- 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
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
w : E
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) (a : 𝕜),
    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 ∧ a ≤ (l_1 : (a : E) → 𝕜) x}

Tactic:
⟨l, l w, Subset.antisymm (fun x hx => ⟨hx.1, hx.2 w hw.1⟩) fun x hx =>
    ⟨hx.1, fun y hy => (hw.2 y hy).trans hx.2⟩⟩

Premises used: Set.Subset.antisymm, And.right, And.left, And.intro, Exists.intro, 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
A : Set E
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
w : E
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) (a : 𝕜),
    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 ∧ a ≤ (l_1 : (a : E) → 𝕜) x}

Tactic:
exact ⟨l, l w, Subset.antisymm (fun x hx => ⟨hx.1, hx.2 w hw.1⟩) fun x hx =>
    ⟨hx.1, fun y hy => (hw.2 y hy).trans hx.2⟩⟩
-- 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 : Nontrivial 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
inl :
  ∀ (hAB : IsExposed 𝕜 A ∅),
    ∃ (l : StrongDual 𝕜 E) (a : 𝕜), Eq.{u_2 + 1} (α := Set E) ∅ {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
inr : ∀ (hB : B.Nonempty), ∃ (l : StrongDual 𝕜 E) (a : 𝕜), B = {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
⊢ ∃ (l : StrongDual 𝕜 E) (a : 𝕜), B = {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}

Tactic:
obtain rfl | hB := B.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, 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
inst_6 : IsOrderedRing 𝕜
inst_7 : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∃ (l : StrongDual 𝕜 E) (a : 𝕜), Eq.{u_2 + 1} (α := Set E) ∅ {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}

Tactic:
⟨0, 1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- 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 : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
inl : Eq.{u_2 + 1} (α := Set E) ∅ {x : E | x ∈ A ∧ LE.le.{u_1} (α := 𝕜) (1 : 𝕜) ((0 : (a : E) → 𝕜) x : 𝕜)}
⊢ ∃ (l : StrongDual 𝕜 E) (a : 𝕜), Eq.{u_2 + 1} (α := Set E) ∅ {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}

Tactic:
refine ⟨0, 1, ?_⟩
-- 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 : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
inl : ∀ (x : E), x ∉ {x : E | x ∈ A ∧ LE.le.{u_1} (α := 𝕜) (1 : 𝕜) ((0 : (a : E) → 𝕜) x : 𝕜)}
⊢ Eq.{u_2 + 1} (α := Set E) ∅ {x : E | x ∈ A ∧ LE.le.{u_1} (α := 𝕜) (1 : 𝕜) ((0 : (a : E) → 𝕜) x : 𝕜)}

Tactic:
rw [eq_comm, eq_empty_iff_forall_notMem]

Premises used: eq_comm, Set.eq_empty_iff_forall_notMem
-- 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 : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : LE.le.{u_1} (α := 𝕜) (1 : 𝕜) ((0 : (a : E) → 𝕜) x : 𝕜)
⊢ LE.le.{u_1} (α := 𝕜) 1 0

Tactic:
rw [ContinuousLinearMap.zero_apply] at h

Premises used: ContinuousLinearMap.zero_apply
-- 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 : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : LE.le.{u_1} (α := 𝕜) 1 0
⊢ ¬LE.le.{u_1} (α := 𝕜) 1 0

Tactic:
have : ¬(1 : 𝕜) ≤ 0 := not_le_of_gt zero_lt_one
-- 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 : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : LE.le.{u_1} (α := 𝕜) 1 0
this : ¬LE.le.{u_1} (α := 𝕜) 1 0
⊢ False

Tactic:
contradiction
-- 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 : Nontrivial 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hB : B.Nonempty
⊢ ∃ (l : StrongDual 𝕜 E) (a : 𝕜), B = {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}

Tactic:
hAB.eq_inter_halfSpace' hB

Premises used: IsExposed.eq_inter_halfSpace'
-- 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 : Nontrivial 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hB : B.Nonempty
⊢ ∃ (l : StrongDual 𝕜 E) (a : 𝕜), B = {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}

Tactic:
exact hAB.eq_inter_halfSpace' hB

Premises used: IsExposed.eq_inter_halfSpace'
-- 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 B C : Set E
hB : IsExposed 𝕜 A B
hC : IsExposed 𝕜 A C
w : E
hwB : w ∈ B
hwC : w ∈ C
obtain :
  ∀ (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),
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩ C =
        {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
⊢ ∃ (l : StrongDual 𝕜 E),
    B ∩ C = {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}

Tactic:
obtain ⟨l₁, rfl⟩ := hB ⟨w, hwB⟩

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
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
A C : Set E
hC : IsExposed 𝕜 A C
w : E
hwC : w ∈ C
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
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 : 𝕜)})
    (hwC :
      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),
      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 : 𝕜)}
⊢ ∃ (l : StrongDual 𝕜 E),
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩ C =
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}

Tactic:
obtain ⟨l₂, rfl⟩ := hC ⟨w, hwC⟩

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
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
⊢ ∃ (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 : 𝕜)}

Tactic:
⟨l₁ + l₂, Subset.antisymm ?_ ?_⟩

Premises used: Set.Subset.antisymm, HAdd.hAdd, Exists.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
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 : 𝕜)}
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 : 𝕜)})
⊢ ∃ (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 : 𝕜)}

Tactic:
refine ⟨l₁ + l₂, Subset.antisymm ?_ ?_⟩