awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s_1 t : Set M
y_1 : N
s : Set M
c : R≥0
y : N
hy :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃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)}
    y
x : M
hx : x ∈ s
⊢ 0 ≤ HSMul.hSMul (β := R) (↑c : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)

Tactic:
exact mul_nonneg c.2 (hy hx)

Premises used: mul_nonneg, Subtype.property
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
y : N
⊢ Membership.mem (γ := PointedCone 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.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
h : ∀ (x : N), Membership.mem (γ := PointedCone R N) (dual p ∅) x ↔ Membership.mem (γ := PointedCone R N) ⊤ x
⊢ Eq (α := PointedCone R N) (dual p ∅) ⊤

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : N
⊢ Membership.mem (γ := PointedCone R N) (dual p ∅) x ↔ Membership.mem (γ := PointedCone R N) ⊤ x

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
h : ∀ (x : N), Membership.mem (γ := PointedCone R N) (dual p 0) x ↔ Membership.mem (γ := PointedCone R N) ⊤ x
⊢ Eq (α := PointedCone R N) (dual p 0) ⊤

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : N
⊢ Membership.mem (γ := PointedCone R N) (dual p 0) x ↔ Membership.mem (γ := PointedCone R N) ⊤ x

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
⊢ Eq (α := PointedCone R N) (dual p {0}) ⊤

Tactic:
dual_zero

Premises used: PointedCone.dual_zero
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
h :
  ∀ (x : N),
    Membership.mem (γ := PointedCone R N) (dual p (↑p.ker : Set M)) x ↔ Membership.mem (γ := PointedCone R N) ⊤ x
⊢ Eq (α := PointedCone R N) (dual p (↑p.ker : Set M)) ⊤

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : N
⊢ Membership.mem (γ := PointedCone R N) (dual p (↑p.ker : Set M)) x ↔ Membership.mem (γ := PointedCone R N) ⊤ x

Tactic:
simp +contextual
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s t : Set M
h : t ⊆ s
⊢ LE.le (α := PointedCone R N) (dual p s) (dual p t)

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

Premises used: Set.Mem, setOf
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
⊢ Antitone (β := PointedCone R N) (dual p)

Tactic:
fun _ _ h => dual_anti h

Premises used: Antitone, PointedCone.dual_anti
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : M
h :
  ∀ (x_1 : N),
    Membership.mem (γ := PointedCone R N) (dual p {x}) x_1 ↔
      Membership.mem (γ := PointedCone R N) (comap ((p : (a : M) → N →ₗ[R] R) x) (positive R R)) x_1
⊢ Eq (α := PointedCone R N) (dual p {x}) (comap ((p : (a : M) → N →ₗ[R] R) x) (positive R R))

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : M
x_1 : N
⊢ Membership.mem (γ := PointedCone R N) (dual p {x}) x_1 ↔
    Membership.mem (γ := PointedCone R N) (comap ((p : (a : M) → N →ₗ[R] R) x) (positive R R)) x_1

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s t : Set M
⊢ Eq (α := PointedCone R N) (dual p (s ∪ t)) (dual p s ⊓ dual p t)

Tactic:
aesop
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : M
s : Set M
rw : Eq (α := PointedCone R N) (dual p ({x} ∪ s)) (dual p {x} ⊓ dual p s)
rw₁ rw₂ : Eq (α := PointedCone R N) (dual p {x} ⊓ dual p s) (dual p {x} ⊓ dual p s)
⊢ Eq (α := PointedCone R N) (dual p (insert x s)) (dual p {x} ⊓ dual p s)

Tactic:
rw [insert_eq, dual_union]

Premises used: Set.insert_eq, PointedCone.dual_union
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
ι : Sort u_4
f : ι → Set M
h :
  ∀ (x : N),
    Membership.mem (γ := PointedCone R N) (dual p (⋃ (i : ι), f i)) x ↔
      Membership.mem (γ := PointedCone R N) (⨅ (i : ι), dual p (f i)) x
⊢ Eq (α := PointedCone R N) (dual p (⋃ (i : ι), f i)) (⨅ (i : ι), dual p (f i))

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
ι : Sort u_4
f : ι → Set M
x : N
⊢ Membership.mem (γ := PointedCone R N) (dual p (⋃ (i : ι), f i)) x ↔
    Membership.mem (γ := PointedCone R N) (⨅ (i : ι), dual p (f i)) x

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

Premises used: forall_comm
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
S : Set (Set M)
h :
  ∀ (x : N),
    Membership.mem (γ := PointedCone R N) (dual p (⋃₀ S)) x ↔
      Membership.mem (γ := PointedCone R N) (sInf (dual p '' S)) x
⊢ Eq (α := PointedCone R N) (dual p (⋃₀ S)) (sInf (dual p '' S))

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
S : Set (Set M)
x : N
⊢ Membership.mem (γ := PointedCone R N) (dual p (⋃₀ S)) x ↔ Membership.mem (γ := PointedCone R N) (sInf (dual p '' S)) x

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

Premises used: forall_comm
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
h :
  ∀ (x : N),
    x ∈ (↑(dual p s) : Set N) ↔ Membership.mem (γ := Set N) (⋂ (i : (↑s : Type u_2)), (↑(dual p {(↑i : M)}) : Set N)) x
⊢ (↑(dual p s) : Set N) = ⋂ (i : (↑s : Type u_2)), (↑(dual p {(↑i : M)}) : Set N)

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
⊢ x ∈ (↑(dual p s) : Set N) ↔ Membership.mem (γ := Set N) (⋂ (i : (↑s : Type u_2)), (↑(dual p {(↑i : M)}) : Set N)) x

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
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.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
t : Set N
mp : s ⊆ (↑(dual p.flip t) : Set M) → t ⊆ (↑(dual p s) : Set N)
mpr : t ⊆ (↑(dual p s) : Set N) → s ⊆ (↑(dual p.flip t) : Set M)
⊢ s ⊆ (↑(dual p.flip t) : Set M) ↔ t ⊆ (↑(dual p s) : Set N)

Tactic:
constructor
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
t : Set N
⊢ s ⊆ (↑(dual p.flip t) : Set M) → t ⊆ (↑(dual p s) : Set N)

Tactic:
(le_trans subset_dual_dual <| dual_antitone ·)

Premises used: PointedCone.subset_dual_dual, PointedCone.dual_antitone, le_trans
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
t : Set N
⊢ s ⊆ (↑(dual p.flip t) : Set M) → t ⊆ (↑(dual p s) : Set N)

Tactic:
exact (le_trans subset_dual_dual <| dual_antitone ·)

Premises used: PointedCone.subset_dual_dual, PointedCone.dual_antitone, le_trans
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
t : Set N
⊢ t ⊆ (↑(dual p s) : Set N) → s ⊆ (↑(dual p.flip t) : Set M)

Tactic:
(le_trans subset_dual_dual <| dual_antitone ·)

Premises used: PointedCone.subset_dual_dual, PointedCone.dual_antitone, le_trans
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
t : Set N
⊢ t ⊆ (↑(dual p s) : Set N) → s ⊆ (↑(dual p.flip t) : Set M)

Tactic:
exact (le_trans subset_dual_dual <| dual_antitone ·)

Premises used: PointedCone.subset_dual_dual, PointedCone.dual_antitone, le_trans
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
⊢ Eq (α := PointedCone R N) (dual p (↑(dual p.flip (↑(dual p s) : Set N)) : Set M)) (dual p s)

Tactic:
le_antisymm (dual_anti subset_dual_dual) subset_dual_dual

Premises used: PointedCone.subset_dual_dual, le_antisymm, PointedCone.dual_anti
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set N
⊢ Eq (α := PointedCone R M) (dual p.flip (↑(dual p (↑(dual p.flip s) : Set M)) : Set N)) (dual p.flip s)

Tactic:
dual_dual_flip_dual _

Premises used: setOf, PointedCone.dual_dual_flip_dual
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
⊢ Eq (α := PointedCone R N) (dual p (↑(hull R s) : Set M)) (dual p s)

Tactic:
le_antisymm (dual_anti Submodule.subset_span) (fun x hx y hy => ?_)

Premises used: le_antisymm, Submodule.subset_span, PointedCone.dual_anti
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
refine :
  ∀ (x : N) (hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x) (y : M)
    (hy : y ∈ (↑(hull R s) : Set M)),
    LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ Eq (α := PointedCone R N) (dual p (↑(hull R s) : Set M)) (dual p s)

Tactic:
refine le_antisymm (dual_anti Submodule.subset_span) (fun x hx y hy => ?_)

Premises used: le_antisymm, Submodule.subset_span, PointedCone.dual_anti
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y _y : M
h : _y ∈ s
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) _y : N →ₗ[R] R) : (a : N) → R) x : R)

Tactic:
hx h
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y _y : M
h : _y ∈ s
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) _y : N →ₗ[R] R) : (a : N) → R) x : R)

Tactic:
exact hx h
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y : M
⊢ LE.le.{u_1} (α := R) (0 : R) (((p : (a : M) → N →ₗ[R] R) 0 : (a : N) → R) x : R)

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y_1 y z : M
_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y
_hz : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) z
hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
hz : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) z : N →ₗ[R] R) : (a : N) → R) x : R)
add :
  0 ≤
    HAdd.hAdd (α := R) (β := R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
      ((((p : (a : M) → N →ₗ[R] R) z : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) (y + z) : N →ₗ[R] R) : (a : N) → R) x : R)

Tactic:
rw [map_add, add_apply]

Premises used: LinearMap.add_apply, map_add
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y_1 y z : M
_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y
_hz : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) z
hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
hz : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) z : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ 0 ≤
    HAdd.hAdd (α := R) (β := R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
      ((((p : (a : M) → N →ₗ[R] R) z : N →ₗ[R] R) : (a : N) → R) x : R)

Tactic:
add_nonneg hy hz

Premises used: add_nonneg
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y_1 y z : M
_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y
_hz : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) z
hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
hz : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) z : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ 0 ≤
    HAdd.hAdd (α := R) (β := R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
      ((((p : (a : M) → N →ₗ[R] R) z : N →ₗ[R] R) : (a : N) → R) x : R)

Tactic:
exact add_nonneg hy hz

Premises used: add_nonneg
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y_1 : M
t : R≥0
y : M
_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y
hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
smul : 0 ≤ HSMul.hSMul (β := R) (↑t : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) (t • y) : N →ₗ[R] R) : (a : N) → R) x : R)

Tactic:
rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]

Premises used: LinearMap.smul_apply, Nonneg.mk_smul, LinearMap.map_smul_of_tower
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y_1 : M
t : R≥0
y : M
_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y
hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ 0 ≤ HSMul.hSMul (β := R) (↑t : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)

Tactic:
mul_nonneg t.2 hy

Premises used: mul_nonneg, Subtype.property
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y_1 : M
t : R≥0
y : M
_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y
hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ 0 ≤ HSMul.hSMul (β := R) (↑t : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)

Tactic:
exact mul_nonneg t.2 hy

Premises used: mul_nonneg, Subtype.property
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : Membership.mem (γ := Submodule.{u_1, u_3} R≥0 N) (dual p s) x
y : M
hy : y ∈ (↑(hull R s) : Set M)
mem :
  ∀ (_y : M) (h : _y ∈ s),
    LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) _y : N →ₗ[R] R) : (a : N) → R) x : R)
zero : LE.le.{u_1} (α := R) (0 : R) (((p : (a : M) → N →ₗ[R] R) 0 : (a : N) → R) x : R)
add :
  ∀ (y z : M) (_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y)
    (_hz : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) z)
    (hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R))
    (hz : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) z : N →ₗ[R] R) : (a : N) → R) x : R)),
    LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) (y + z) : N →ₗ[R] R) : (a : N) → R) x : R)
smul :
  ∀ (t : R≥0) (y : M) (_hy : Membership.mem (γ := Submodule.{u_1, u_2} R≥0 M) (Submodule.span R≥0 s) y)
    (hy : LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)),
    LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) (t • y) : N →ₗ[R] R) : (a : N) → R) x : R)
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) x : R)

Tactic:
induction hy using Submodule.span_induction with
  | mem _y h => exact hx h
  | zero => simp
  | add y z _hy _hz hy hz => rw [map_add, add_apply]; exact add_nonneg hy hz
  | smul t y _hy hy => rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]; exact mul_nonneg t.2 hy

Premises used: LinearMap.smul_apply, LinearMap.add_apply, map_add, Nonneg.mk_smul, LinearMap.map_smul_of_tower
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C D : PointedCone R M
⊢ Eq (α := PointedCone R N) (dual p (↑(C ⊔ D) : Set M)) (dual p ((↑C : Set M) ∪ (↑D : Set M)))

Tactic:
simp [← dual_hull]

Premises used: PointedCone.dual_hull