awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (hypothesis)
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 ⋯
⊢ Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
have h_coord_dual : ∀ (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]))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
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)
⊢ Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
have apply : LE.le (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
  (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
Tactic: apply le_antisymm (minTensorProduct_le_maxTensorProduct C₁ C₂.toPointedCone)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
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)) z
have 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)
Tactic: rw [← (equivFinsuppOfBasisLeft b).symm_apply_apply z,
    TensorProduct.equivFinsuppOfBasisLeft_symm_apply, Finsupp.sum_fintype _ _ (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
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)
have 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)
Tactic: refine Submodule.sum_mem _ fun i _ => tmul_mem_minTensorProduct ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
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)
⊢ 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)
have 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)
Tactic: refine Submodule.sum_mem _ fun i _ => tmul_mem_minTensorProduct ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
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 (α := 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)
have 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)
Tactic: simp only [equivFinsuppOfBasisLeft_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
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 (α := F) (↑C₂ : PointedCone ℝ F)
    ((TensorProduct.lid ℝ F : (a : ℝ ⊗[ℝ] F) → F)
        ((LinearMap.rTensor F (b.coord i) : (a : E ⊗[ℝ] F) → ℝ ⊗[ℝ] F) z : ℝ ⊗[ℝ] F) :
      F)
have 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)
Tactic: rw [← ProperCone.dual_dual_flip (topDualPairing ℝ F) C₂]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
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[ℝ] ℝ
⊢ 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) :
        ℝ)
have 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) :
      ℝ)
Tactic: (hf : (f : F →ₗ[ℝ] ℝ) ∈ dual (Dual.eval ℝ F) (C₂ : Set F))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (hypothesis)
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 →ₗ[ℝ] ℝ)
⊢ 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) :
      ℝ)
have 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 :
            ℝ)
Tactic: simp only [mem_maxTensorProduct] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (hypothesis)
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 : ℝ)
    ((((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) :
      ℝ)
have 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 :
    ℝ)
Tactic: have h_nonneg := hz (b.coord i) (h_coord_dual i) (f : F →ₗ[ℝ] ℝ) hf
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
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 :
      ℝ)
⊢ (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)
have 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 :
      ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (hypothesis)
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 :
      ℝ)
⊢ 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) :
      ℝ)
have h_eq : (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: 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]