-- 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 :
  ∀ (φ : 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'
hφ : Membership.mem (γ := PointedCone R (Dual R G')) (dual (Dual.eval R G') (↑(map f C₁) : Set G')) φ
ψ : Dual R H'
hψ : Membership.mem (γ := PointedCone R (Dual R H')) (dual (Dual.eval R H') (↑(map g C₂) : Set H')) ψ
h_eq :
  Eq (α := G ⊗[R] H →ₗ[R] R)
    ((dualDistrib R G' H' : (a : Dual R G' ⊗[R] Dual R H') → Dual R (G' ⊗[R] H')) (φ ⊗ₜ[R] ψ) ∘ₗ TensorProduct.map f g)
    ((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g)))
⊢ 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)
have h : Eq.{u_1 + 1} (α := 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)
  ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g)) :
          Dual R (G ⊗[R] H)) :
        (a : G ⊗[R] H) → R)
      w :
    R)
Tactic: convert! hw (φ.comp f) (fun x hx ↦ hφ ⟨x, hx, rfl⟩) (ψ.comp g) (fun y hy ↦ hψ ⟨y, hy, rfl⟩)