-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : AddCommMonoid A
inst_3 : Module F K
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
inst_7 : StrongRankCondition F
inst_8 : StrongRankCondition K
inst_9 : Free F K
inst_10 : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
rw : lift.{w, v} (lift.{v, v} (Module.rank F K)) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
rw₁ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
rw₂ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (lift.{w, w} (Module.rank K A)) =
    lift.{v, w} (Module.rank F A)
rw₃ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{v, w} (Module.rank F A)
rw₄ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{max w v, w} (Module.rank F A)
rw₅ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} #(Prod.{v, w} (Free.ChooseBasisIndex F K) (Free.ChooseBasisIndex K A))
rw₆ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₇ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₈ :
  lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₉ :
  lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₁₀ :
  lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₁₁ :
  lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A)
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
have rw₁₂ : lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
  lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A)
Tactic: rw [← (Module.rank F K).lift_id, ← b.mk_eq_rank, ← (Module.rank K A).lift_id, ← c.mk_eq_rank,
    ← lift_umax.{w, v}, ← (b.smulTower c).mk_eq_rank, mk_prod, lift_mul, lift_lift, lift_lift,
    lift_lift, lift_lift, lift_umax.{v, w}]