awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Cone.Closure
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
E : Type u_2
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : Module 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
K : PointedCone 𝕜 E
⊢ (↑K : ConvexCone 𝕜 E).closure.Pointed

Tactic:
subset_closure <| PointedCone.pointed_toConvexCone _

Premises used: Set.Mem, subset_closure, setOf, PointedCone.pointed_toConvexCone, closure, ConvexCone.Pointed, Set.sInter
-- Module: Mathlib.Analysis.Convex.Cone.Closure
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
E : Type u_2
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : Module 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
K : PointedCone 𝕜 E
⊢ (↑K.closure : Set E) = closure (↑K : Set E)

Tactic:
rfl

Premises used: Set.Mem, setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Closure
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
E : Type u_2
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : Module 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
K : PointedCone 𝕜 E
a : E
⊢ a ∈ K.closure ↔ a ∈ closure (↑K : Set E)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, closure, Set.sInter
-- Module: Mathlib.Analysis.Convex.Cone.Closure
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
E : Type u_2
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : Module 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
K L : PointedCone 𝕜 E
⊢ K.closure = L ↔ closure (↑K : Set E) = (↑L : Set E)

Tactic:
SetLike.ext'_iff

Premises used: Set.Mem, setOf, closure, SetLike.ext'_iff, Set.sInter
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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)
rw : IsClosed (↑(dual p (⋃ x ∈ s, {x})) : Set N)
⊢ IsClosed (↑(dual p s) : Set N)

Tactic:
rw [← s.biUnion_of_singleton]

Premises used: Set.biUnion_of_singleton
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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)
simp_rw : IsClosed.{u_3} (X := N) (⋂ i ∈ s, (↑(comap ((p : (a : M) → N →ₗ[R] R) i) (positive R R)) : Set N))
⊢ IsClosed (↑(dual p (⋃ x ∈ s, {x})) : Set N)

Tactic:
simp_rw [dual_iUnion, Submodule.coe_iInf, dual_singleton]

Premises used: Submodule.coe_iInf, PointedCone.dual_iUnion, PointedCone.dual_singleton
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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.{u_3} (X := N) (⋂ i ∈ s, (↑(comap ((p : (a : M) → N →ₗ[R] R) i) (positive R R)) : Set N))

Tactic:
isClosed_biInter fun x hx ↦ isClosed_Ici.preimage <| hp _

Premises used: isClosed_biInter, IsClosed.preimage, isClosed_Ici
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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.{u_3} (X := N) (⋂ i ∈ s, (↑(comap ((p : (a : M) → N →ₗ[R] R) i) (positive R R)) : Set N))

Tactic:
exact isClosed_biInter fun x hx ↦ isClosed_Ici.preimage <| hp _

Premises used: isClosed_biInter, IsClosed.preimage, isClosed_Ici
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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 M
y : N
⊢ Membership.mem (γ := ProperCone R N) (dual p s) y ↔
    ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
h : ∀ (x : N), Membership.mem (γ := ProperCone R N) (dual p ∅) x ↔ Membership.mem (γ := ProperCone R N) ⊤ x
⊢ Eq (α := ProperCone R N) (dual p ∅) ⊤

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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 : N
⊢ Membership.mem (γ := ProperCone R N) (dual p ∅) x ↔ Membership.mem (γ := ProperCone R N) ⊤ x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
h : ∀ (x : N), Membership.mem (γ := ProperCone R N) (dual p 0) x ↔ Membership.mem (γ := ProperCone R N) ⊤ x
⊢ Eq (α := ProperCone R N) (dual p 0) ⊤

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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 : N
⊢ Membership.mem (γ := ProperCone R N) (dual p 0) x ↔ Membership.mem (γ := ProperCone R N) ⊤ x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
⊢ LE.le (α := ProperCone R N) ⊥ (dual p univ)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
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)
⊢ Eq (α := ProperCone R N) (dual p univ) ⊥

Tactic:
refine le_antisymm (fun y hy ↦ (_root_.map_eq_zero_iff _ p.flip.toContPerfPair.injective).1 ?_)
    (by simp)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
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)
⊢ 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:
ext x
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
x : M
⊢ LE.le.{u_1} (α := R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R) (0 : R)

Tactic:
simpa using hy <| mem_univ (-x)

Premises used: Set.mem_univ, Neg.neg
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
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:
exact (hy <| mem_univ x).antisymm' <| by simpa using hy <| mem_univ (-x)

Premises used: LE.le.antisymm', Set.mem_univ
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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 t : Set M
h : t ⊆ s
⊢ LE.le (α := ProperCone R N) (dual p s) (dual p t)

Tactic:
fun _y hy _x hx ↦ hy (h hx)

Premises used: Set.Mem, setOf
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
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
⊢ Eq (α := ProperCone R N) (dual p {x})
    (comap (((p.toContPerfPair : M ≃ₗ[R] StrongDual R N) : (a : M) → StrongDual R N) x) (positive R R))

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
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:
simp
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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 t : Set M
⊢ Eq (α := ProperCone R N) (dual p (s ∪ t)) (dual p s ⊓ dual p t)

Tactic:
aesop
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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)
rw₁ rw₂ : Eq (α := ProperCone R N) (dual p {x} ⊓ dual p s) (dual p {x} ⊓ dual p s)
⊢ Eq (α := ProperCone R N) (dual p (insert x s)) (dual p {x} ⊓ dual p s)

Tactic:
rw [insert_eq, dual_union]

Premises used: Set.insert_eq, ProperCone.dual_union
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
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
⊢ Eq (α := ProperCone R N) (dual p (⋃ (i : ι), f i)) (⨅ (i : ι), dual p (f i))

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
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:
simp [forall_comm (α := M)]

Premises used: forall_comm
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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)
h :
  ∀ (x : N),
    Membership.mem (γ := ProperCone R N) (dual p (⋃₀ S)) x ↔ Membership.mem (γ := ProperCone R N) (sInf (dual p '' S)) x
⊢ Eq (α := ProperCone R N) (dual p (⋃₀ S)) (sInf (dual p '' S))

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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)
x : N
⊢ Membership.mem (γ := ProperCone R N) (dual p (⋃₀ S)) x ↔ Membership.mem (γ := ProperCone R N) (sInf (dual p '' S)) x

Tactic:
simp [forall_comm (α := M)]

Premises used: forall_comm
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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 M
⊢ s ⊆ (↑(dual p.flip (↑(dual p s) : Set N)) : Set M)

Tactic:
fun _x hx _y hy ↦ hy hx

Premises used: Set.Mem, setOf, Set.Subset
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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 : ℝ)
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 : ℝ)
⊢ ∃ (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

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
C : ProperCone ℝ E
hKconv : Convex.{0, u_1} ℝ (E := E) ∅
hKcomp : IsCompact.{u_1} (X := E) ∅
hKC : Disjoint ∅ (↑C : Set E)
⊢ (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((0 : (a : E) → ℝ) x : ℝ)) ∧
    ∀ (x : E), Membership.mem (γ := Set E) ∅ x → LT.lt (α := ℝ) ((0 : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
C : ProperCone ℝ E
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:
exact ⟨0, by simp⟩
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
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 : ℝ)
⊢ ∃ (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

Premises used: ProperCone.convex, geometric_hahn_banach_compact_closed, ProperCone.isClosed
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
⊢ v < 0

Tactic:
simpa using hv 0 C.zero_mem

Premises used: ClosedSubmodule.toSubmodule, Submodule.zero_mem, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
⊢ v < 0

Tactic:
have hv₀ : v < 0 := by simpa using hv 0 C.zero_mem
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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 : ℝ)

Tactic:
⟨f, fun x hx ↦ ?_, fun x hx ↦ (hu x hx).trans_le <| huv.le.trans hv₀.le⟩

Premises used: LT.lt.le, LT.lt.trans_le, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Cone.Dual
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
inr : ∀ (x : E) (hx : x ∈ C), LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)
⊢ ∃ (f : StrongDual ℝ E),
    (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) ∧
      ∀ x ∈ K, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
refine ⟨f, fun x hx ↦ ?_, fun x hx ↦ (hu x hx).trans_le <| huv.le.trans hv₀.le⟩