awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
x : ℕ → F
seq : (x : ℕ) → E
hmem : ∀ (x : ℕ), seq x ∈ C
hx : ∀ (x_1 : ℕ), (f : (a : E) → F) (seq x_1) = x x_1
htends : Filter.Tendsto x Filter.atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ C → 0 ≤ ⟪(f : (a : E) → F) x, y⟫_ℝ
hx₁ : ∀ (x : ℕ), Eq.{u_3 + 1} (α := F) ((f : (a : E) → F) (seq x) : F) (((⇑f : (a : E) → F) ∘ seq) x : F)
⊢ Filter.Tendsto ((⇑f : (a : E) → F) ∘ seq) Filter.atTop (nhds b)

Tactic:
obtain rfl : f ∘ seq = x := funext hx

Premises used: funext, rfl
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : (x : ℕ) → E
hmem : ∀ (x : ℕ), seq x ∈ C
y : F
hinner : ∀ ⦃x : E⦄, x ∈ C → 0 ≤ ⟪(f : (a : E) → F) x, y⟫_ℝ
hx : ∀ (x : ℕ), Eq.{u_3 + 1} (α := F) ((f : (a : E) → F) (seq x) : F) (((⇑f : (a : E) → F) ∘ seq) x : F)
htends : Filter.Tendsto ((⇑f : (a : E) → F) ∘ seq) Filter.atTop (nhds b)
n : ℕ
⊢ 0 ≤ ⟪(f : (a : E) → F) (seq n), y⟫_ℝ

Tactic:
simpa [real_inner_comm] using hinner (hmem n)

Premises used: real_inner_comm
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : (x : ℕ) → E
hmem : ∀ (x : ℕ), seq x ∈ C
y : F
hinner : ∀ ⦃x : E⦄, x ∈ C → 0 ≤ ⟪(f : (a : E) → F) x, y⟫_ℝ
hx : ∀ (x : ℕ), Eq.{u_3 + 1} (α := F) ((f : (a : E) → F) (seq x) : F) (((⇑f : (a : E) → F) ∘ seq) x : F)
htends : Filter.Tendsto ((⇑f : (a : E) → F) ∘ seq) Filter.atTop (nhds b)
⊢ ∀ (n : ℕ), 0 ≤ ⟪(f : (a : E) → F) (seq n), y⟫_ℝ

Tactic:
have h n : 0 ≤ ⟪f (seq n), y⟫_ℝ := by simpa [real_inner_comm] using hinner (hmem n)
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : (x : ℕ) → E
hmem : ∀ (x : ℕ), seq x ∈ C
y : F
hinner : ∀ ⦃x : E⦄, x ∈ C → 0 ≤ ⟪(f : (a : E) → F) x, y⟫_ℝ
hx : ∀ (x : ℕ), Eq.{u_3 + 1} (α := F) ((f : (a : E) → F) (seq x) : F) (((⇑f : (a : E) → F) ∘ seq) x : F)
htends : Filter.Tendsto ((⇑f : (a : E) → F) ∘ seq) Filter.atTop (nhds b)
h : ∀ (n : ℕ), 0 ≤ ⟪(f : (a : E) → F) (seq n), y⟫_ℝ
⊢ 0 ≤ ⟪b, y⟫_ℝ

Tactic:
ge_of_tendsto' ((continuous_id.inner continuous_const).seqContinuous htends) h

Premises used: continuous_const, ge_of_tendsto', Continuous.seqContinuous, continuous_id, Continuous.inner
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : (x : ℕ) → E
hmem : ∀ (x : ℕ), seq x ∈ C
y : F
hinner : ∀ ⦃x : E⦄, x ∈ C → 0 ≤ ⟪(f : (a : E) → F) x, y⟫_ℝ
hx : ∀ (x : ℕ), Eq.{u_3 + 1} (α := F) ((f : (a : E) → F) (seq x) : F) (((⇑f : (a : E) → F) ∘ seq) x : F)
htends : Filter.Tendsto ((⇑f : (a : E) → F) ∘ seq) Filter.atTop (nhds b)
h : ∀ (n : ℕ), 0 ≤ ⟪(f : (a : E) → F) (seq n), y⟫_ℝ
⊢ 0 ≤ ⟪b, y⟫_ℝ

Tactic:
exact ge_of_tendsto' ((continuous_id.inner continuous_const).seqContinuous htends) h

Premises used: continuous_const, ge_of_tendsto', Continuous.seqContinuous, continuous_id, Continuous.inner
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h :
  ∀ (y : F),
    Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑C : Set E))
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) →
      0 ≤ ⟪b, y⟫_ℝ
contrapose! :
  ∀ (h : b ∉ map f C),
    ∃ (y : F),
      Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑C : Set E))
          ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) ∧
        ⟪b, y⟫_ℝ < 0
⊢ b ∈ map f C

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f C
obtain :
  ∀ (y : F) (hxy : ∀ x ∈ map f C, 0 ≤ ⟪x, y⟫_ℝ) (hyb : ⟪b, y⟫_ℝ < 0),
    ∃ (y : F),
      Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑C : Set E))
          ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) ∧
        ⟪b, y⟫_ℝ < 0
⊢ ∃ (y : F),
    Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑C : Set E))
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) ∧
      ⟪b, y⟫_ℝ < 0

Tactic:
obtain ⟨y, hxy, hyb⟩ := (C.map f).hyperplane_separation' h

Premises used: ProperCone.hyperplane_separation', ProperCone.map
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f C
y : F
hxy : ∀ x ∈ map f C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪b, y⟫_ℝ < 0
⊢ ∃ (y : F),
    Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑C : Set E))
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) ∧
      ⟪b, y⟫_ℝ < 0

Tactic:
⟨y, fun x hx ↦ ?_, hyb⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f C
y : F
hxy : ∀ x ∈ map f C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪b, y⟫_ℝ < 0
refine :
  ∀ (x : E) (hx : x ∈ (↑C : Set E)),
    LE.le (α := ℝ) (0 : ℝ)
      (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
          ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) :
        ℝ)
⊢ ∃ (y : F),
    Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑C : Set E))
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) ∧
      ⟪b, y⟫_ℝ < 0

Tactic:
refine ⟨y, fun x hx ↦ ?_, hyb⟩
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f C
y : F
hxy : ∀ x ∈ map f C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪b, y⟫_ℝ < 0
x : E
hx : x ∈ (↑C : Set E)
⊢ LE.le (α := ℝ) (0 : ℝ)
    (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) :
      ℝ)

Tactic:
simpa [ContinuousLinearMap.adjoint_inner_right]
      using hxy (f x) (subset_closure <| mem_image_of_mem _ hx)

Premises used: subset_closure, Set.mem_image_of_mem, ContinuousLinearMap.adjoint_inner_right, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : b ∉ map f K
contrapose! :
  ∀
    (disj :
      ∀ (y : F)
        (_ :
          Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑K : Set E))
            ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E)),
        0 ≤ ⟪b, y⟫_ℝ),
    b ∈ map f K
⊢ ∃ (y : F),
    Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑K : Set E))
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) ∧
      ⟪b, y⟫_ℝ < 0

Tactic:
contrapose! disj
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj :
  ∀ (y : F)
    (_ :
      Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑K : Set E))
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E)),
    0 ≤ ⟪b, y⟫_ℝ
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (y : F),
    Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑K : Set E))
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) →
      0 ≤ ⟪b, y⟫_ℝ
⊢ b ∈ map f K

Tactic:
rwa [K.relative_hyperplane_separation]

Premises used: ProperCone.relative_hyperplane_separation
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
b : Basis ι R M
C : PointedCone R M
hC : (↑C : Set M) ⊆ (↑(hull R (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → M))) : Set M)
i : ι
⊢ Membership.mem (γ := PointedCone R (Dual R M)) (dual (Dual.eval R M) (↑C : Set M)) (b.coord i)

Tactic:
dual_le_dual hC ?_

Premises used: Set.Mem, setOf, PointedCone.dual_le_dual
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
b : Basis ι R M
C : PointedCone R M
hC : (↑C : Set M) ⊆ (↑(hull R (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → M))) : Set M)
i : ι
refine :
  Membership.mem (γ := Submodule { c : R // 0 ≤ c } (M →ₗ[R] R))
    (dual (Dual.eval R M) (↑(hull R (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → M))) : Set M)) (b.coord i)
⊢ Membership.mem (γ := PointedCone R (Dual R M)) (dual (Dual.eval R M) (↑C : Set M)) (b.coord i)

Tactic:
refine dual_le_dual hC ?_

Premises used: PointedCone.dual_le_dual
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
b : Basis ι R M
C : PointedCone R M
hC : (↑C : Set M) ⊆ (↑(hull R (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → M))) : Set M)
i : ι
⊢ Membership.mem (γ := Submodule { c : R // 0 ≤ c } (M →ₗ[R] R))
    (dual (Dual.eval R M) (↑(hull R (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → M))) : Set M)) (b.coord i)

Tactic:
simp [Finsupp.single_apply, ite_nonneg zero_le_one le_rfl]

Premises used: ite_nonneg, le_rfl, zero_le_one, Finsupp.single_apply
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
b : Basis ι R M
C : PointedCone R M
hC : (↑C : Set M) ⊆ (↑(hull R (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → M))) : Set M)
i : ι
refine :
  Membership.mem (γ := Submodule { c : R // 0 ≤ c } (M →ₗ[R] R))
    (dual (Dual.eval R M) (↑(hull R (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → M))) : Set M)) (b.coord i)
⊢ Membership.mem (γ := PointedCone R (Dual R M)) (dual (Dual.eval R M) (↑C : Set M)) (b.coord i)

Tactic:
classical
  refine dual_le_dual hC ?_
  simp [Finsupp.single_apply, ite_nonneg zero_le_one le_rfl]

Premises used: ite_nonneg, le_rfl, zero_le_one, PointedCone.dual_le_dual, Finsupp.single_apply
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_simp : C₁.IsSimplicial
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
obtain :
  ∀ (s : Set E) (hs_fin : s.Finite) (hs_lin : LinearIndepOn ℝ id s) (hs_span : hull ℝ s = C₁),
    Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
      (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
⊢ Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))

Tactic:
obtain ⟨s, hs_fin, hs_lin, hs_span⟩ := h₁_simp
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
haveI :
  ∀ (this : Fintype (↑s : Type u_1)),
    Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
      (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
⊢ Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))

Tactic:
haveI : Fintype s := hs_fin.fintype
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
x : E
hx : x ∈ (↑(hull ℝ s) : Set E)
⊢ ∃ (c : E →₀ ℝ),
    (↑c.support : Set E) ⊆ s ∧
      (∀ (y : E), LE.le (α := ℝ) (0 : ℝ) ((c : (a : E) → ℝ) y : ℝ)) ∧ (c.sum fun (m : E) (r : ℝ) ↦ r • m) = x

Tactic:
rw [SetLike.mem_coe, PointedCone.mem_hull_set] at hx

Premises used: SetLike.mem_coe, PointedCone.mem_hull_set
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
x : E
hx :
  ∃ (c : E →₀ ℝ),
    (↑c.support : Set E) ⊆ s ∧
      (∀ (y : E), LE.le (α := ℝ) (0 : ℝ) ((c : (a : E) → ℝ) y : ℝ)) ∧ (c.sum fun (m : E) (r : ℝ) ↦ r • m) = x
obtain :
  ∀ (c : E →₀ ℝ) (hc_supp : (↑c.support : Set E) ⊆ s),
    (∀ (y : E), LE.le (α := ℝ) (0 : ℝ) ((c : (a : E) → ℝ) y : ℝ)) →
      ∀ (hc_sum : (c.sum fun (m : E) (r : ℝ) ↦ r • m) = x), x ∈ (↑(Submodule.span ℝ s) : Set E)
⊢ x ∈ (↑(Submodule.span ℝ s) : Set E)

Tactic:
obtain ⟨c, hc_supp, _, hc_sum⟩ := hx
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
x : E
c : E →₀ ℝ
hc_supp : (↑c.support : Set E) ⊆ s
left : ∀ (y : E), LE.le (α := ℝ) (0 : ℝ) ((c : (a : E) → ℝ) y : ℝ)
hc_sum : (c.sum fun (m : E) (r : ℝ) ↦ r • m) = x
⊢ x ∈ (↑(Submodule.span ℝ s) : Set E)

Tactic:
hc_sum ▸ Submodule.sum_mem _ fun m hm =>
      Submodule.smul_mem _ _ (Submodule.subset_span (hc_supp hm))

Premises used: Real, Submodule.sum_mem, Eq.rec, Submodule.span, Submodule.subset_span, DFunLike.coe, Submodule.smul_mem
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
x : E
c : E →₀ ℝ
hc_supp : (↑c.support : Set E) ⊆ s
left : ∀ (y : E), LE.le (α := ℝ) (0 : ℝ) ((c : (a : E) → ℝ) y : ℝ)
hc_sum : (c.sum fun (m : E) (r : ℝ) ↦ r • m) = x
⊢ x ∈ (↑(Submodule.span ℝ s) : Set E)

Tactic:
exact hc_sum ▸ Submodule.sum_mem _ fun m hm =>
      Submodule.smul_mem _ _ (Submodule.subset_span (hc_supp hm))
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
⊢ (↑(hull ℝ s) : Set E) ⊆ (↑(Submodule.span ℝ s) : Set E)

Tactic:
have hull_sub_span : (hull ℝ s : Set E) ⊆ Submodule.span ℝ s := by
    intro x hx
    rw [SetLike.mem_coe, PointedCone.mem_hull_set] at hx
    obtain ⟨c, hc_supp, _, hc_sum⟩ := hx
    exact hc_sum ▸ Submodule.sum_mem _ fun m hm =>
      Submodule.smul_mem _ _ (Submodule.subset_span (hc_supp hm))
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
hull_sub_span : (↑(hull ℝ s) : Set E) ⊆ (↑(Submodule.span ℝ s) : Set E)
⊢ LE.le.{u_1} (α := Submodule ℝ E) ⊤ (Submodule.span ℝ (Set.range fun (x : (↑s : Type u_1)) ↦ id (↑x : E)))

Tactic:
simpa only [id_eq, Subtype.range_coe] using
      h₁_gen ▸ hs_span ▸ Submodule.span_le.mpr hull_sub_span

Premises used: Subtype.range_coe, id_eq
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
hull_sub_span : (↑(hull ℝ s) : Set E) ⊆ (↑(Submodule.span ℝ s) : Set E)
b : Basis (↑s : Type u_1) ℝ E := Basis.mk hs_lin ⋯
⊢ s ⊆ Set.range (ι := (↑s : Type u_1)) (⇑b : (a : (↑s : Type u_1)) → E)

Tactic:
simp [b]
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
hull_sub_span : (↑(hull ℝ s) : Set E) ⊆ (↑(Submodule.span ℝ s) : Set E)
b : Basis (↑s : Type u_1) ℝ E := Basis.mk hs_lin ⋯
⊢ ∀ (i : (↑s : Type u_1)),
    Membership.mem (γ := PointedCone ℝ (Dual ℝ E)) (dual (Dual.eval ℝ E) (↑C₁ : Set E)) (b.coord i)

Tactic:
have h_coord_dual : ∀ i, b.coord i ∈ dual (Dual.eval ℝ E) C₁ :=
    basis_coord_mem_dual _ _ (hs_span ▸ (Submodule.span_mono <| by simp [b]))
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
hull_sub_span : (↑(hull ℝ s) : Set E) ⊆ (↑(Submodule.span ℝ s) : Set E)
b : Basis (↑s : Type u_1) ℝ E := Basis.mk hs_lin ⋯
h_coord_dual :
  ∀ (i : (↑s : Type u_1)),
    Membership.mem (γ := PointedCone ℝ (Dual ℝ E)) (dual (Dual.eval ℝ E) (↑C₁ : Set E)) (b.coord i)
apply :
  LE.le (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
⊢ Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))

Tactic:
apply le_antisymm (minTensorProduct_le_maxTensorProduct C₁ C₂.toPointedCone)

Premises used: PointedCone.minTensorProduct_le_maxTensorProduct, le_antisymm, ProperCone.toPointedCone