-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.TensorProduct (goal)
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))
⊢ 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')
have 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)
Tactic: simp only [SetLike.mem_coe, mem_maxTensorProduct] at hw ⊢
Cleared hypotheses: hw