awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), (↑u : Set (Fin (n + 1))).indicator w i) 1
i : Fin (n + 1)
⊢ Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)
have pos : ∀ (hi : i ∈ (↑u : Set (Fin (n + 1)))), Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)
Tactic: by_cases hi : i ∈ (u : Set (Fin (n + 1)))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), (↑u : Set (Fin (n + 1))).indicator w i) 1
i : Fin (n + 1)
pos :
  ∀ (hi : i ∈ (↑u : Set (Fin (n + 1)))), Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)
⊢ Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)
have neg : ∀ (hi : i ∉ (↑u : Set (Fin (n + 1)))), Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)
Tactic: by_cases hi : i ∈ (u : Set (Fin (n + 1)))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
h : p ∈ s.closedInterior
⊢ ∃ (s_1 : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜),
    (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w = p
have h₁ : ∀ (w : Fin (n + 1) → 𝕜) (hw1 : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), w i) 1)
  (h :
    Membership.mem (α := V) s.closedInterior
      ((Finset.affineCombination 𝕜 Finset.univ s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)),
  ∃ (s_1 : Finset (Fin (n + 1))) (w_1 : Fin (n + 1) → 𝕜),
    (∀ i ∈ s_1, 0 ≤ w_1 i) ∧
      s_1.sum w_1 = 1 ∧
        Eq.{u_2 + 1} (α := V) ((Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w_1 : V)
          ((Finset.affineCombination 𝕜 Finset.univ s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)
Tactic: obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype <|
      Set.mem_of_mem_of_subset h s.closedInterior_subset_affineSpan
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
w : Fin (n + 1) → 𝕜
hw1 : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), w i) 1
h :
  Membership.mem (α := V) s.closedInterior
    ((Finset.affineCombination 𝕜 Finset.univ s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)
⊢ ∃ (s_1 : Finset (Fin (n + 1))) (w_1 : Fin (n + 1) → 𝕜),
    (∀ i ∈ s_1, 0 ≤ w_1 i) ∧
      s_1.sum w_1 = 1 ∧
        Eq.{u_2 + 1} (α := V) ((Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w_1 : V)
          ((Finset.affineCombination 𝕜 Finset.univ s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)
have h₁ : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set 𝕜) (Icc 0 1) (w i)
Tactic: rw [affineCombination_mem_closedInterior_iff hw1] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : AddCommMonoid E
inst_1 : TopologicalSpace E
inst_2 : Semifield 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : DenselyOrdered 𝕜
inst_8 : NoMaxOrder 𝕜
inst_9 : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hC : (↑C : Set E).Nonempty
hSclos : IsClosed (↑C : Set E)
⊢ C.Pointed
have obtain : ∀ (x : E) (hx : x ∈ (↑C : Set E)), C.Pointed
Tactic: obtain ⟨x, hx⟩ := hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : AddCommMonoid E
inst_1 : TopologicalSpace E
inst_2 : Semifield 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : DenselyOrdered 𝕜
inst_8 : NoMaxOrder 𝕜
inst_9 : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed (↑C : Set E)
x : E
hx : x ∈ (↑C : Set E)
f : 𝕜 → E := fun (x_1 : 𝕜) ↦ x_1 • x
⊢ C.Pointed
have hfS : closure (f '' Ioi 0) ⊆ (↑C : Set E)
Tactic: have hfS : closure (f '' Set.Ioi 0) ⊆ C :=
    hSclos.closure_subset_iff.2 <| by rintro _ ⟨_, h, rfl⟩; exact C.smul_mem h hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : AddCommMonoid E
inst_1 : TopologicalSpace E
inst_2 : Semifield 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : DenselyOrdered 𝕜
inst_8 : NoMaxOrder 𝕜
inst_9 : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed (↑C : Set E)
x : E
hx : x ∈ (↑C : Set E)
f : 𝕜 → E := fun (x_1 : 𝕜) ↦ x_1 • x
hfS : closure (f '' Ioi 0) ⊆ (↑C : Set E)
⊢ C.Pointed
have fc : ContinuousWithinAt f (Ioi 0) 0
Tactic: have fc : ContinuousWithinAt f (Set.Ioi (0 : 𝕜)) 0 := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : TopologicalSpace R
inst_3 : ClosedIciTopology R
inst_4 : IsOrderedRing R
inst_5 : AddCommGroup M
inst_6 : AddCommGroup N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hp : ∀ (x : M), Continuous.{u_3, u_1} (X := N) (Y := R) (⇑((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
⊢ IsClosed (↑(dual p s) : Set N)
have rw : IsClosed (↑(dual p (⋃ x ∈ s, {x})) : Set N)
Tactic: rw [← s.biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : TopologicalSpace R
inst_3 : ClosedIciTopology R
inst_4 : IsOrderedRing R
inst_5 : AddCommGroup M
inst_6 : AddCommGroup N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hp : ∀ (x : M), Continuous.{u_3, u_1} (X := N) (Y := R) (⇑((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
⊢ IsClosed (↑(dual p (⋃ x ∈ s, {x})) : Set N)
have simp_rw : IsClosed.{u_3} (X := N) (⋂ i ∈ s, (↑(comap ((p : (a : M) → N →ₗ[R] R) i) (positive R R)) : Set N))
Tactic: simp_rw [dual_iUnion, Submodule.coe_iInf, dual_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : TopologicalSpace R
inst_4 : ClosedIciTopology R
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : TopologicalSpace M
inst_8 : AddCommGroup N
inst_9 : Module R N
inst_10 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst_11 : p.IsContPerfPair
⊢ Eq (α := ProperCone R N) (dual p ∅) ⊤
have h : ∀ (x : N), Membership.mem (γ := ProperCone R N) (dual p ∅) x ↔ Membership.mem (γ := ProperCone R N) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : TopologicalSpace R
inst_4 : ClosedIciTopology R
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : TopologicalSpace M
inst_8 : AddCommGroup N
inst_9 : Module R N
inst_10 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst_11 : p.IsContPerfPair
⊢ Eq (α := ProperCone R N) (dual p 0) ⊤
have h : ∀ (x : N), Membership.mem (γ := ProperCone R N) (dual p 0) x ↔ Membership.mem (γ := ProperCone R N) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : TopologicalSpace R
inst_4 : ClosedIciTopology R
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : TopologicalSpace M
inst_8 : AddCommGroup N
inst_9 : Module R N
inst_10 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst_11 : p.IsContPerfPair
inst_12 : IsTopologicalRing R
inst_13 : T1Space N
⊢ Eq (α := ProperCone R N) (dual p univ) ⊥
have refine : ∀ (y : N) (hy : Membership.mem (γ := ProperCone R N) (dual p univ) y),
  Eq (α := StrongDual R M)
    (((p.flip.toContPerfPair : N ≃ₗ[R] StrongDual R M) : (a : N) → StrongDual R M) y : StrongDual R M)
    (0 : StrongDual R M)
Tactic: refine le_antisymm (fun y hy ↦ (_root_.map_eq_zero_iff _ p.flip.toContPerfPair.injective).1 ?_)
    (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : TopologicalSpace R
inst_4 : ClosedIciTopology R
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : TopologicalSpace M
inst_8 : AddCommGroup N
inst_9 : Module R N
inst_10 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst_11 : p.IsContPerfPair
inst_12 : IsTopologicalRing R
inst_13 : T1Space N
y : N
hy : Membership.mem (γ := ProperCone R N) (dual p univ) y
⊢ Eq (α := StrongDual R M)
    (((p.flip.toContPerfPair : N ≃ₗ[R] StrongDual R M) : (a : N) → StrongDual R M) y : StrongDual R M)
    (0 : StrongDual R M)
have h : ∀ (x : M),
  Eq.{u_1 + 1} (α := R)
    (((((p.flip.toContPerfPair : N ≃ₗ[R] StrongDual R M) : (a : N) → StrongDual R M) y : StrongDual R M) : (a : M) → R)
        x :
      R)
    ((0 : (a : M) → R) x : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : TopologicalSpace R
inst_4 : ClosedIciTopology R
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : TopologicalSpace M
inst_8 : AddCommGroup N
inst_9 : Module R N
inst_10 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst_11 : p.IsContPerfPair
inst_12 : IsTopologicalRing R
inst_13 : OrderClosedTopology R
x : M
⊢ Eq (α := ProperCone R N) (dual p {x})
    (comap (((p.toContPerfPair : M ≃ₗ[R] StrongDual R N) : (a : M) → StrongDual R N) x) (positive R R))
have h : ∀ (x_1 : N),
  Membership.mem (γ := ProperCone R N) (dual p {x}) x_1 ↔
    Membership.mem (γ := ProperCone R N)
      (comap (((p.toContPerfPair : M ≃ₗ[R] StrongDual R N) : (a : M) → StrongDual R N) x) (positive R R)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : TopologicalSpace R
inst_4 : ClosedIciTopology R
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : TopologicalSpace M
inst_8 : AddCommGroup N
inst_9 : Module R N
inst_10 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst_11 : p.IsContPerfPair
x : M
s : Set M
⊢ Eq (α := ProperCone R N) (dual p (insert x s)) (dual p {x} ⊓ dual p s)
have rw : Eq (α := ProperCone R N) (dual p ({x} ∪ s)) (dual p {x} ⊓ dual p s)
Tactic: rw [insert_eq, dual_union]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : TopologicalSpace R
inst_4 : ClosedIciTopology R
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : TopologicalSpace M
inst_8 : AddCommGroup N
inst_9 : Module R N
inst_10 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst_11 : p.IsContPerfPair
x : M
s : Set M
rw : Eq (α := ProperCone R N) (dual p ({x} ∪ s)) (dual p {x} ⊓ dual p s)
⊢ Eq (α := ProperCone R N) (dual p (insert x s)) (dual p {x} ⊓ dual p s)
have rw₁ : Eq (α := ProperCone R N) (dual p {x} ⊓ dual p s) (dual p {x} ⊓ dual p s)
Tactic: rw [insert_eq, dual_union]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : TopologicalSpace R
inst_4 : ClosedIciTopology R
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : TopologicalSpace M
inst_8 : AddCommGroup N
inst_9 : Module R N
inst_10 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst_11 : p.IsContPerfPair
ι : Sort u_4
f : ι → Set M
⊢ Eq (α := ProperCone R N) (dual p (⋃ (i : ι), f i)) (⨅ (i : ι), dual p (f i))
have h : ∀ (x : N),
  Membership.mem (γ := ProperCone R N) (dual p (⋃ (i : ι), f i)) x ↔
    Membership.mem (γ := ProperCone R N) (⨅ (i : ι), dual p (f i)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : TopologicalSpace R
inst_4 : ClosedIciTopology R
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : TopologicalSpace M
inst_8 : AddCommGroup N
inst_9 : Module R N
inst_10 : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst_11 : p.IsContPerfPair
S : Set (Set M)
⊢ Eq (α := ProperCone R N) (dual p (⋃₀ S)) (sInf (dual p '' S))
have h : ∀ (x : N),
  Membership.mem (γ := ProperCone R N) (dual p (⋃₀ S)) x ↔ Membership.mem (γ := ProperCone R N) (sInf (dual p '' S)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K (↑C : Set E)
⊢ ∃ (f : StrongDual ℝ E),
    (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) ∧
      ∀ x ∈ K, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
have inl : ∀ (hKconv : Convex.{0, u_1} ℝ (E := E) ∅) (hKcomp : IsCompact.{u_1} (X := E) ∅) (hKC : Disjoint ∅ (↑C : Set E)),
  ∃ (f : StrongDual ℝ E),
    (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) ∧
      ∀ (x : E), Membership.mem (γ := Set E) ∅ x → LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
Tactic: obtain rfl | ⟨x₀, hx₀⟩ := K.eq_empty_or_nonempty
Cleared hypotheses: K, hKconv, hKcomp, hKC
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K (↑C : Set E)
inl :
  ∀ (hKconv : Convex.{0, u_1} ℝ (E := E) ∅) (hKcomp : IsCompact.{u_1} (X := E) ∅) (hKC : Disjoint ∅ (↑C : Set E)),
    ∃ (f : StrongDual ℝ E),
      (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) ∧
        ∀ (x : E), Membership.mem (γ := Set E) ∅ x → LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∃ (f : StrongDual ℝ E),
    (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) ∧
      ∀ x ∈ K, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
have inr : ∀ (x₀ : E) (hx₀ : x₀ ∈ K),
  ∃ (f : StrongDual ℝ E),
    (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) ∧
      ∀ x ∈ K, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
Tactic: obtain rfl | ⟨x₀, hx₀⟩ := K.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K (↑C : Set E)
x₀ : E
hx₀ : x₀ ∈ K
⊢ ∃ (f : StrongDual ℝ E),
    (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) ∧
      ∀ x ∈ K, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
have inr : ∀ (f : StrongDual ℝ E) (u v : ℝ) (hu : ∀ a ∈ K, (f : (a : E) → ℝ) a < u) (huv : u < v)
  (hv : ∀ b ∈ (↑C : Set E), v < (f : (a : E) → ℝ) b),
  ∃ (f : StrongDual ℝ E),
    (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) ∧
      ∀ x ∈ K, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
Tactic: obtain ⟨f, u, v, hu, huv, hv⟩ :=
    geometric_hahn_banach_compact_closed hKconv hKcomp C.convex C.isClosed hKC
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (hypothesis)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K (↑C : Set E)
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, (f : (a : E) → ℝ) a < u
huv : u < v
hv : ∀ b ∈ (↑C : Set E), v < (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E),
    (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) ∧
      ∀ x ∈ K, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
have hv₀ : v < 0
Tactic: have hv₀ : v < 0 := by simpa using hv 0 C.zero_mem
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K (↑C : Set E)
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, (f : (a : E) → ℝ) a < u
huv : u < v
hv : ∀ b ∈ (↑C : Set E), v < (f : (a : E) → ℝ) b
hv₀ : v < 0
⊢ ∃ (f : StrongDual ℝ E),
    (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) ∧
      ∀ x ∈ K, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
have inr : ∀ (x : E) (hx : x ∈ C), LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)
Tactic: refine ⟨f, fun x hx ↦ ?_, fun x hx ↦ (hu x hx).trans_le <| huv.le.trans hv₀.le⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K (↑C : Set E)
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, (f : (a : E) → ℝ) a < u
huv : u < v
hv : ∀ b ∈ (↑C : Set E), v < (f : (a : E) → ℝ) b
hv₀ : v < 0
x : E
hx : x ∈ C
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)
have inr : ∀ (hx₀ : LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)), False
Tactic: by_contra! hx₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup F
inst_5 : Module ℝ E
inst_6 : ContinuousSMul ℝ E
inst_7 : LocallyConvexSpace ℝ E
inst_8 : Module ℝ F
p : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)
inst_9 : p.IsContPerfPair
C : ProperCone ℝ E
⊢ dual p.flip (↑(dual p (↑C : Set E)) : Set F) = C
have refine : ∀ (x : E), Membership.mem (γ := ProperCone ℝ E) (dual p.flip (↑(dual p (↑C : Set E)) : Set F)) x → x ∈ C
Tactic: refine le_antisymm (fun x ↦ ?_) subset_dual_dual
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup F
inst_5 : Module ℝ E
inst_6 : ContinuousSMul ℝ E
inst_7 : LocallyConvexSpace ℝ E
inst_8 : Module ℝ F
p : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)
inst_9 : p.IsContPerfPair
C : ProperCone ℝ E
x : E
⊢ Membership.mem (γ := ProperCone ℝ E) (dual p.flip (↑(dual p (↑C : Set E)) : Set F)) x → x ∈ C
have simp : (∀ ⦃x_1 : F⦄,
    (∀ ⦃x : E⦄, x ∈ C → LE.le (α := ℝ) (0 : ℝ) ((((p : (a : E) → F →ₗ[ℝ] ℝ) x : F →ₗ[ℝ] ℝ) : (a : F) → ℝ) x_1 : ℝ)) →
      LE.le (α := ℝ) (0 : ℝ) ((((p.flip : (a : F) → E →ₗ[ℝ] ℝ) x_1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)) →
  x ∈ C
Tactic: simp only [mem_dual, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Dual (goal)
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup F
inst_5 : Module ℝ E
inst_6 : ContinuousSMul ℝ E
inst_7 : LocallyConvexSpace ℝ E
inst_8 : Module ℝ F
p : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)
inst_9 : p.IsContPerfPair
C : ProperCone ℝ E
x : E
⊢ (∀ ⦃x_1 : F⦄,
      (∀ ⦃x : E⦄, x ∈ C → LE.le (α := ℝ) (0 : ℝ) ((((p : (a : E) → F →ₗ[ℝ] ℝ) x : F →ₗ[ℝ] ℝ) : (a : F) → ℝ) x_1 : ℝ)) →
        LE.le (α := ℝ) (0 : ℝ) ((((p.flip : (a : F) → E →ₗ[ℝ] ℝ) x_1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)) →
    x ∈ C
have contrapose! : x ∉ C →
  ∃ (x_1 : F),
    (∀ ⦃x : E⦄, x ∈ C → LE.le (α := ℝ) (0 : ℝ) ((((p : (a : E) → F →ₗ[ℝ] ℝ) x : F →ₗ[ℝ] ℝ) : (a : F) → ℝ) x_1 : ℝ)) ∧
      LT.lt (α := ℝ) ((((p.flip : (a : F) → E →ₗ[ℝ] ℝ) x_1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (0 : ℝ)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
⊢ ∃ (g : E →ₗ.[ℝ] ℝ), f < g ∧ ∀ (x : ↥g.domain), (↑x : E) ∈ s → 0 ≤ (↑g : ↥g.domain → ℝ) x
have obtain : ∀ (y : E) (hy : y ∉ f.domain), ∃ (g : E →ₗ.[ℝ] ℝ), f < g ∧ ∀ (x : ↥g.domain), (↑x : E) ∈ s → 0 ≤ (↑g : ↥g.domain → ℝ) x
Tactic: obtain ⟨y, -, hy⟩ : ∃ y ∈ ⊤, y ∉ f.domain := SetLike.exists_of_lt (lt_top_iff_ne_top.2 hdom)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
⊢ ∃ (c : ℝ),
    (∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c) ∧
      ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x
have suffices : (upperBounds Sn ∩ lowerBounds Sp).Nonempty
Tactic: suffices (upperBounds Sn ∩ lowerBounds Sp).Nonempty by
      simpa only [Sp, Sn, Set.Nonempty, upperBounds, lowerBounds, forall_mem_image] using this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
⊢ (upperBounds Sn ∩ lowerBounds Sp).Nonempty
have refine_1 : Set.Nonempty.{u_2} (α := ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s}
Tactic: refine exists_between_of_forall_le (Nonempty.image f ?_) (Nonempty.image f (dense y)) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
refine_1 : Set.Nonempty.{u_2} (α := ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s}
⊢ (upperBounds Sn ∩ lowerBounds Sp).Nonempty
have refine_2 : ∀ x ∈ Sn, ∀ y ∈ Sp, x ≤ y
Tactic: refine exists_between_of_forall_le (Nonempty.image f ?_) (Nonempty.image f (dense y)) ?_