-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
G' : Type u_4
H' : Type u_5
inst_7 : AddCommGroup G'
inst_8 : Module R G'
inst_9 : AddCommGroup H'
inst_10 : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw : w ∈ (↑(C₁.maxTensorProduct C₂ : PointedCone R (G ⊗[R] H)) : Set (G ⊗[R] H))
simp :
  ∀
    (hw :
      ∀ (φ : Dual R G),
        Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) φ →
          ∀ (ψ : Dual R H),
            Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ →
              LE.le.{u_1} (α := R) (0 : R)
                ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) (φ ⊗ₜ[R] ψ) :
                        Dual R (G ⊗[R] H)) :
                      (a : G ⊗[R] H) → R)
                    w :
                  R))
    (φ : Dual R G'),
    Membership.mem (γ := PointedCone R (Dual R G')) (dual (Dual.eval R G') (↑(map f C₁) : Set G')) φ →
      ∀ (ψ : Dual R H'),
        Membership.mem (γ := PointedCone R (Dual R H')) (dual (Dual.eval R H') (↑(map g C₂) : Set H')) ψ →
          LE.le.{u_1} (α := R) (0 : R)
            ((((dualDistrib R G' H' : (a : Dual R G' ⊗[R] Dual R H') → Dual R (G' ⊗[R] H')) (φ ⊗ₜ[R] ψ) :
                    Dual R (G' ⊗[R] H')) :
                  (a : G' ⊗[R] H') → R)
                (((↑{ c : R // 0 ≤ c } :
                          {S : Type u_1} →
                            {M : Type (max u_3 u_2)} →
                              {M₂ : Type (max u_5 u_4)} →
                                [inst_11 : Semiring { c : R // 0 ≤ c }] →
                                  [inst_12 : Semiring S] →
                                    [inst_13 : AddCommMonoid M] →
                                      [inst_14 : AddCommMonoid M₂] →
                                        [inst_15 : Module { c : R // 0 ≤ c } M] →
                                          [inst_16 : Module { c : R // 0 ≤ c } M₂] →
                                            [inst_17 : Module S M] →
                                              [inst_18 : Module S M₂] →
                                                [LinearMap.CompatibleSMul M M₂ { c : R // 0 ≤ c } S] →
                                                  (fₗ : M →ₗ[S] M₂) → M →ₗ[{ c : R // 0 ≤ c }] M₂)
                        (TensorProduct.map f g) :
                      (a : G ⊗[R] H) → G' ⊗[R] H')
                    w :
                  G' ⊗[R] H') :
              R)
⊢ Membership.mem (α := G' ⊗[R] H') (γ := Submodule { c : R // 0 ≤ c } (G' ⊗[R] H'))
    ((map f C₁).maxTensorProduct (map g C₂) : PointedCone R (G' ⊗[R] H'))
    (((↑{ c : R // 0 ≤ c } :
              {S : Type u_1} →
                {M : Type (max u_3 u_2)} →
                  {M₂ : Type (max u_5 u_4)} →
                    [inst_11 : Semiring { c : R // 0 ≤ c }] →
                      [inst_12 : Semiring S] →
                        [inst_13 : AddCommMonoid M] →
                          [inst_14 : AddCommMonoid M₂] →
                            [inst_15 : Module { c : R // 0 ≤ c } M] →
                              [inst_16 : Module { c : R // 0 ≤ c } M₂] →
                                [inst_17 : Module S M] →
                                  [inst_18 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ { c : R // 0 ≤ c } S] →
                                      (fₗ : M →ₗ[S] M₂) → M →ₗ[{ c : R // 0 ≤ c }] M₂)
            (TensorProduct.map f g) :
          (a : G ⊗[R] H) → G' ⊗[R] H')
        w :
      G' ⊗[R] H')

Tactic:
simp only [SetLike.mem_coe, mem_maxTensorProduct] at hw ⊢

Premises used: SetLike.mem_coe, PointedCone.mem_maxTensorProduct