-- 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))
obtain₁ :
  ∀ (s : Set E) (hs_fin : s.Finite) (hs_lin : LinearIndepOn ℝ id s) (hs_span : hull ℝ s = C₁)
    (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))
obtain₂ obtain₃ :
  ∀ (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)),
    Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
      (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
obtain₄ :
  ∀ (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)),
    let b := 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)),
      Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
        (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
obtain₅ :
  ∀ (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)),
    let b := 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)),
      LE.le (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
        (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
obtain₆ :
  ∀ (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)),
    let b := 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))
      ⦃z : E ⊗[ℝ] F⦄
      (hz :
        Membership.mem (γ := Submodule { c : ℝ // 0 ≤ c } (E ⊗[ℝ] F))
          (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F)) z),
      Membership.mem (γ := Submodule { c : ℝ // 0 ≤ c } (E ⊗[ℝ] F))
        (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F)) z
obtain₇ :
  ∀ (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)),
    let b := 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))
      ⦃z : E ⊗[ℝ] F⦄
      (hz :
        Membership.mem (γ := Submodule { c : ℝ // 0 ≤ c } (E ⊗[ℝ] F))
          (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F)) z),
      Membership.mem (γ := Submodule { c : ℝ // 0 ≤ c } (E ⊗[ℝ] F))
        (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
        (∑ i : (↑s : Type u_1),
          (b : (a : (↑s : Type u_1)) → E) i ⊗ₜ[ℝ]
            (((equivFinsuppOfBasisLeft b : (a : E ⊗[ℝ] F) → (↑s : Type u_1) →₀ F) z :
                  Finsupp.{u_1, u_2} (↑s : Type u_1) F) :
                (a : (↑s : Type u_1)) → F)
              i)
refine_1 :
  ∀ (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)),
    let b := 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))
      ⦃z : E ⊗[ℝ] F⦄
      (hz :
        Membership.mem (γ := Submodule { c : ℝ // 0 ≤ c } (E ⊗[ℝ] F))
          (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F)) z)
      (i : (↑s : Type u_1)),
      Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i →
        Membership.mem (α := E) C₁ ((b : (a : (↑s : Type u_1)) → E) i : E)
refine_2 refine_2₁ :
  ∀ (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)),
    let b := 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))
      ⦃z : E ⊗[ℝ] F⦄
      (hz :
        Membership.mem (γ := Submodule { c : ℝ // 0 ≤ c } (E ⊗[ℝ] F))
          (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F)) z)
      (i : (↑s : Type u_1)),
      Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i →
        Membership.mem (α := F) (↑C₂ : PointedCone ℝ F)
          ((((equivFinsuppOfBasisLeft b : (a : E ⊗[ℝ] F) → (↑s : Type u_1) →₀ F) z :
                  Finsupp.{u_1, u_2} (↑s : Type u_1) F) :
                (a : (↑s : Type u_1)) → F)
              i :
            F)
⊢ Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))

Tactic:
classical
  obtain ⟨s, hs_fin, hs_lin, hs_span⟩ := h₁_simp
  haveI : Fintype s := hs_fin.fintype
  -- The conic hull (R≥0-span) is contained in the linear span (ℝ-span)
  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))
  -- Extract basis from `C₁.IsSimplicial` + generating
  let b := Basis.mk hs_lin <| by
    simpa only [id_eq, Subtype.range_coe] using
      h₁_gen ▸ hs_span ▸ Submodule.span_le.mpr hull_sub_span
  -- Dual basis elements are in C₁*
  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]))
  -- Reduce to proving z ∈ max → z ∈ min
  apply le_antisymm (minTensorProduct_le_maxTensorProduct C₁ C₂.toPointedCone)
  intro z hz
  -- Express z using basis: z = ∑ b_i ⊗ y_i
  rw [← (equivFinsuppOfBasisLeft b).symm_apply_apply z,
    TensorProduct.equivFinsuppOfBasisLeft_symm_apply, Finsupp.sum_fintype _ _ (by simp)]
  -- Show z ∈ min by showing b_i ∈ C₁ and y_i ∈ C₂
  refine Submodule.sum_mem _ fun i _ => tmul_mem_minTensorProduct ?_ ?_
  · simpa only [b, Basis.coe_mk] using (hs_span ▸ subset_hull) i.prop
  · simp only [equivFinsuppOfBasisLeft_apply]
    rw [← ProperCone.dual_dual_flip (topDualPairing ℝ F) C₂]
    intro f (hf : (f : F →ₗ[ℝ] ℝ) ∈ dual (Dual.eval ℝ F) (C₂ : Set F))
    simp only [mem_maxTensorProduct] at hz
    have h_nonneg := hz (b.coord i) (h_coord_dual i) (f : F →ₗ[ℝ] ℝ) hf
    have h_eq : dualDistrib ℝ E F ((b.coord i) ⊗ₜ[ℝ] (f : F →ₗ[ℝ] ℝ)) =
        (f : F →ₗ[ℝ] ℝ) ∘ₗ (TensorProduct.lid ℝ F) ∘ₗ (b.coord i).rTensor F := by
      ext; simp [mul_comm]
    simpa only [h_eq, LinearMap.comp_apply, LinearEquiv.coe_coe] using h_nonneg

Premises used: TensorProduct.equivFinsuppOfBasisLeft_symm_apply, Real, Finsupp.sum_fintype, Submodule.sum_mem, LinearMap.comp_apply, PointedCone.minTensorProduct_le_maxTensorProduct, le_antisymm, topDualPairing, Module.Basis.coe_mk, ProperCone.dual_dual_flip, PointedCone.tmul_mem_minTensorProduct, TensorProduct.equivFinsuppOfBasisLeft_apply, PointedCone.mem_maxTensorProduct, ProperCone.toPointedCone, LinearEquiv.coe_coe