awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)), Eq (α := E ⊗[ℝ] F) ((b : (a : (↑s : Type u_1)) → E) i ⊗ₜ[ℝ] 0 : E ⊗[ℝ] F) (0 : E ⊗[ℝ] F)

Tactic:
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₁
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)
z : E ⊗[ℝ] F
hz :
  Membership.mem (γ := Submodule { c : ℝ // 0 ≤ c } (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F)) z
rw :
  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)
⊢ Membership.mem (γ := Submodule { c : ℝ // 0 ≤ c } (E ⊗[ℝ] F))
    (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F)) z

Tactic:
rw [← (equivFinsuppOfBasisLeft b).symm_apply_apply z,
    TensorProduct.equivFinsuppOfBasisLeft_symm_apply, Finsupp.sum_fintype _ _ (by simp)]

Premises used: TensorProduct.equivFinsuppOfBasisLeft_symm_apply, Finsupp.sum_fintype, LinearEquiv.symm_apply_apply, TensorProduct.equivFinsuppOfBasisLeft
-- 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)
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)

Tactic:
Submodule.sum_mem _ fun i _ => tmul_mem_minTensorProduct ?_ ?_

Premises used: Set.Mem, Submodule.sum_mem, PointedCone.tmul_mem_minTensorProduct
-- 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)
z : E ⊗[ℝ] F
hz :
  Membership.mem (γ := Submodule { c : ℝ // 0 ≤ c } (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F)) z
refine_1 :
  ∀ (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 :
  ∀ (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)
⊢ 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)

Tactic:
refine Submodule.sum_mem _ fun i _ => tmul_mem_minTensorProduct ?_ ?_

Premises used: Submodule.sum_mem, PointedCone.tmul_mem_minTensorProduct
-- 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)
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)
h : Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i
⊢ Membership.mem (α := E) C₁ ((b : (a : (↑s : Type u_1)) → E) i : E)

Tactic:
simpa only [b, Basis.coe_mk] using (hs_span ▸ subset_hull) i.prop

Premises used: Module.Basis.coe_mk
-- 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)
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)
h : Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i
refine_2 :
  Membership.mem (α := F) (↑C₂ : PointedCone ℝ F)
    ((TensorProduct.lid ℝ F : (a : ℝ ⊗[ℝ] F) → F)
        ((LinearMap.rTensor F (b.coord i) : (a : E ⊗[ℝ] F) → ℝ ⊗[ℝ] F) z : ℝ ⊗[ℝ] F) :
      F)
⊢ 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)

Tactic:
simp only [equivFinsuppOfBasisLeft_apply]

Premises used: TensorProduct.equivFinsuppOfBasisLeft_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₁_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)
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)
h : Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i
refine_2 :
  Membership.mem (α := F) (γ := PointedCone ℝ F)
    (↑(ProperCone.dual (topDualPairing ℝ F)
          (↑(ProperCone.dual (LinearMap.flip (topDualPairing ℝ F)) (↑C₂ : Set F)) : Set (F →L[ℝ] ℝ))) :
      PointedCone ℝ F)
    ((TensorProduct.lid ℝ F : (a : ℝ ⊗[ℝ] F) → F)
        ((LinearMap.rTensor F (b.coord i) : (a : E ⊗[ℝ] F) → ℝ ⊗[ℝ] F) z : ℝ ⊗[ℝ] F) :
      F)
⊢ Membership.mem (α := F) (↑C₂ : PointedCone ℝ F)
    ((TensorProduct.lid ℝ F : (a : ℝ ⊗[ℝ] F) → F)
        ((LinearMap.rTensor F (b.coord i) : (a : E ⊗[ℝ] F) → ℝ ⊗[ℝ] F) z : ℝ ⊗[ℝ] F) :
      F)

Tactic:
rw [← ProperCone.dual_dual_flip (topDualPairing ℝ F) C₂]

Premises used: Real, topDualPairing, ProperCone.dual_dual_flip
-- 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)
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)
h : Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i
f : F →L[ℝ] ℝ
refine_2 :
  ∀ (hf : Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑C₂ : Set F)) (↑f : F →ₗ[ℝ] ℝ)),
    LE.le (α := ℝ) (0 : ℝ)
      ((((topDualPairing ℝ F : (a : F →L[ℝ] ℝ) → F →ₗ[ℝ] ℝ) f : F →ₗ[ℝ] ℝ) : (a : F) → ℝ)
          ((TensorProduct.lid ℝ F : (a : ℝ ⊗[ℝ] F) → F)
              ((LinearMap.rTensor F (b.coord i) : (a : E ⊗[ℝ] F) → ℝ ⊗[ℝ] F) z : ℝ ⊗[ℝ] F) :
            F) :
        ℝ)
⊢ f ∈ (↑(ProperCone.dual (LinearMap.flip (topDualPairing ℝ F)) (↑C₂ : Set F)) : Set (F →L[ℝ] ℝ)) →
    LE.le (α := ℝ) (0 : ℝ)
      ((((topDualPairing ℝ F : (a : F →L[ℝ] ℝ) → F →ₗ[ℝ] ℝ) f : F →ₗ[ℝ] ℝ) : (a : F) → ℝ)
          ((TensorProduct.lid ℝ F : (a : ℝ ⊗[ℝ] F) → F)
              ((LinearMap.rTensor F (b.coord i) : (a : E ⊗[ℝ] F) → ℝ ⊗[ℝ] F) z : ℝ ⊗[ℝ] F) :
            F) :
        ℝ)

Tactic:
(hf : (f : F →ₗ[ℝ] ℝ) ∈ dual (Dual.eval ℝ F) (C₂ : Set F))
-- 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)
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)
h : Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i
f : F →L[ℝ] ℝ
hf : Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑C₂ : Set F)) (↑f : F →ₗ[ℝ] ℝ)
⊢ ∀ (φ : Dual ℝ E),
    Membership.mem (γ := PointedCone ℝ (Dual ℝ E)) (dual (Dual.eval ℝ E) (↑C₁ : Set E)) φ →
      ∀ (ψ : Dual ℝ F),
        Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑(↑C₂ : PointedCone ℝ F) : Set F)) ψ →
          LE.le (α := ℝ) (0 : ℝ)
            ((((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (φ ⊗ₜ[ℝ] ψ) : Dual ℝ (E ⊗[ℝ] F)) :
                  (a : E ⊗[ℝ] F) → ℝ)
                z :
              ℝ)

Tactic:
simp only [mem_maxTensorProduct] at hz

Premises used: PointedCone.mem_maxTensorProduct
-- 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)
z : E ⊗[ℝ] F
i : (↑s : Type u_1)
h : Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i
f : F →L[ℝ] ℝ
hf : Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑C₂ : Set F)) (↑f : F →ₗ[ℝ] ℝ)
hz :
  ∀ (φ : Dual ℝ E),
    Membership.mem (γ := PointedCone ℝ (Dual ℝ E)) (dual (Dual.eval ℝ E) (↑C₁ : Set E)) φ →
      ∀ (ψ : Dual ℝ F),
        Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑(↑C₂ : PointedCone ℝ F) : Set F)) ψ →
          LE.le (α := ℝ) (0 : ℝ)
            ((((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (φ ⊗ₜ[ℝ] ψ) : Dual ℝ (E ⊗[ℝ] F)) :
                  (a : E ⊗[ℝ] F) → ℝ)
                z :
              ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (b.coord i ⊗ₜ[ℝ] (↑f : F →ₗ[ℝ] ℝ)) :
            Dual ℝ (E ⊗[ℝ] F)) :
          (a : E ⊗[ℝ] F) → ℝ)
        z :
      ℝ)

Tactic:
have h_nonneg := hz (b.coord i) (h_coord_dual i) (f : F →ₗ[ℝ] ℝ) hf
-- 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)
z : E ⊗[ℝ] F
i : (↑s : Type u_1)
h : Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i
f : F →L[ℝ] ℝ
hf : Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑C₂ : Set F)) (↑f : F →ₗ[ℝ] ℝ)
hz :
  ∀ (φ : Dual ℝ E),
    Membership.mem (γ := PointedCone ℝ (Dual ℝ E)) (dual (Dual.eval ℝ E) (↑C₁ : Set E)) φ →
      ∀ (ψ : Dual ℝ F),
        Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑(↑C₂ : PointedCone ℝ F) : Set F)) ψ →
          LE.le (α := ℝ) (0 : ℝ)
            ((((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (φ ⊗ₜ[ℝ] ψ) : Dual ℝ (E ⊗[ℝ] F)) :
                  (a : E ⊗[ℝ] F) → ℝ)
                z :
              ℝ)
h_nonneg :
  LE.le (α := ℝ) (0 : ℝ)
    ((((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (b.coord i ⊗ₜ[ℝ] (↑f : F →ₗ[ℝ] ℝ)) :
            Dual ℝ (E ⊗[ℝ] F)) :
          (a : E ⊗[ℝ] F) → ℝ)
        z :
      ℝ)
a :
  ∀ (x : E) (x_1 : F),
    Eq (α := ℝ)
      (((((AlgebraTensorModule.curry
                      ((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F))
                        (b.coord i ⊗ₜ[ℝ] (↑f : F →ₗ[ℝ] ℝ))) :
                    LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)) :
                  (a : E) → F →ₗ[ℝ] ℝ)
                x :
              F →ₗ[ℝ] ℝ) :
            (a : F) → ℝ)
          x_1 :
        ℝ)
      (((((AlgebraTensorModule.curry
                      ((↑f : F →ₗ[ℝ] ℝ) ∘ₗ
                        (↑(TensorProduct.lid ℝ F) : ℝ ⊗[ℝ] F →ₗ[ℝ] F) ∘ₗ LinearMap.rTensor F (b.coord i)) :
                    LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)) :
                  (a : E) → F →ₗ[ℝ] ℝ)
                x :
              F →ₗ[ℝ] ℝ) :
            (a : F) → ℝ)
          x_1 :
        ℝ)
⊢ (dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (b.coord i ⊗ₜ[ℝ] (↑f : F →ₗ[ℝ] ℝ)) =
    (↑f : F →ₗ[ℝ] ℝ) ∘ₗ (↑(TensorProduct.lid ℝ F) : ℝ ⊗[ℝ] F →ₗ[ℝ] F) ∘ₗ LinearMap.rTensor F (b.coord i)

Tactic:
ext
-- 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)
z : E ⊗[ℝ] F
i : (↑s : Type u_1)
h : Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i
f : F →L[ℝ] ℝ
hf : Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑C₂ : Set F)) (↑f : F →ₗ[ℝ] ℝ)
hz :
  ∀ (φ : Dual ℝ E),
    Membership.mem (γ := PointedCone ℝ (Dual ℝ E)) (dual (Dual.eval ℝ E) (↑C₁ : Set E)) φ →
      ∀ (ψ : Dual ℝ F),
        Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑(↑C₂ : PointedCone ℝ F) : Set F)) ψ →
          LE.le (α := ℝ) (0 : ℝ)
            ((((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (φ ⊗ₜ[ℝ] ψ) : Dual ℝ (E ⊗[ℝ] F)) :
                  (a : E ⊗[ℝ] F) → ℝ)
                z :
              ℝ)
h_nonneg :
  LE.le (α := ℝ) (0 : ℝ)
    ((((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (b.coord i ⊗ₜ[ℝ] (↑f : F →ₗ[ℝ] ℝ)) :
            Dual ℝ (E ⊗[ℝ] F)) :
          (a : E ⊗[ℝ] F) → ℝ)
        z :
      ℝ)
x : E
x_1 : F
⊢ Eq (α := ℝ)
    (((((AlgebraTensorModule.curry
                    ((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F))
                      (b.coord i ⊗ₜ[ℝ] (↑f : F →ₗ[ℝ] ℝ))) :
                  LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)) :
                (a : E) → F →ₗ[ℝ] ℝ)
              x :
            F →ₗ[ℝ] ℝ) :
          (a : F) → ℝ)
        x_1 :
      ℝ)
    (((((AlgebraTensorModule.curry
                    ((↑f : F →ₗ[ℝ] ℝ) ∘ₗ
                      (↑(TensorProduct.lid ℝ F) : ℝ ⊗[ℝ] F →ₗ[ℝ] F) ∘ₗ LinearMap.rTensor F (b.coord i)) :
                  LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)) :
                (a : E) → F →ₗ[ℝ] ℝ)
              x :
            F →ₗ[ℝ] ℝ) :
          (a : F) → ℝ)
        x_1 :
      ℝ)

Tactic:
simp [mul_comm]

Premises used: mul_comm