awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton R
rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) (1 : ℕ)
rw₁ : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) 1 : ℕ) (1 : ℕ)
⊢ finrank R M = 1
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [finrank, rank_subsingleton, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
h : Module.rank R M ≤ (↑n : Cardinal.{v})
⊢ finrank R M ≤ n
have hc : Module.rank R M < ℵ₀
Tactic: rwa [← Cardinal.toNat_le_iff_le_of_lt_aleph0, toNat_natCast] at h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
h : Module.rank R M ≤ (↑n : Cardinal.{v})
hc : Module.rank R M < ℵ₀
⊢ finrank R M ≤ n
have hd : (↑n : Cardinal.{v}) < ℵ₀
Tactic: rwa [← Cardinal.toNat_le_iff_le_of_lt_aleph0, toNat_natCast] at h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
h : Module.rank R M < (↑n : Cardinal.{v})
⊢ finrank R M < n
have hc : Module.rank R M < ℵ₀
Tactic: rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast] at h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
h : Module.rank R M < (↑n : Cardinal.{v})
hc : Module.rank R M < ℵ₀
⊢ finrank R M < n
have hd : (↑n : Cardinal.{v}) < ℵ₀
Tactic: rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast] at h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
h : n < finrank R M
⊢ (↑n : Cardinal.{v}) < Module.rank R M
have hc : (↑n : Cardinal.{v}) < ℵ₀
Tactic: rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
h : n < finrank R M
hc : (↑n : Cardinal.{v}) < ℵ₀
⊢ (↑n : Cardinal.{v}) < Module.rank R M
have hd : Module.rank R M < ℵ₀
Tactic: rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
h : n < finrank R M
⊢ Module.rank R M < ℵ₀
have hd : ∀ (h : ℵ₀ ≤ Module.rank R M), finrank R M ≤ n
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
h : ℵ₀ ≤ Module.rank R M
⊢ finrank R M ≤ n
have hd : 0 ≤ n
Tactic: rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M ≃ₗ[R] N
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank R N) : ℕ)
have rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank R M)) : ℕ)
  ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank R N) : ℕ)
Tactic: rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M ≃ₗ[R] N
rw :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank R M)) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank R N) : ℕ)
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank R N) : ℕ)
have rw₁ : Eq (α := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{v, w} (Module.rank R N)) : ℕ)
  ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank R N) : ℕ)
Tactic: rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M ≃ₗ[R] N
rw :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank R M)) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank R N) : ℕ)
rw₁ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{v, w} (Module.rank R N)) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank R N) : ℕ)
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank R N) : ℕ)
have rw₂ : Eq (α := ℕ) ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank R N) : ℕ)
  ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank R N) : ℕ)
Tactic: rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Injective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ finrank.{u, w} R ↥f.range = finrank R M
have rw : finrank.{u, w} R ↥f.range = finrank.{u, w} R ↥f.range
Tactic: rw [(LinearEquiv.ofInjective f hf).finrank_eq]
-- 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
⊢ 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} (lift.{v, v} (Module.rank F K)) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F 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}]
-- 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)
⊢ 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} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F 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}]
-- 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)
⊢ 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} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (lift.{w, w} (Module.rank K A)) =
  lift.{v, w} (Module.rank F 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}]
-- 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)
⊢ 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} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
  lift.{v, w} (Module.rank F 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}]
-- 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)
⊢ 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} (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)
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}]
-- 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)
⊢ 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} (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))
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}]
-- 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))
⊢ 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} (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))
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}]
-- 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))
⊢ 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} (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))
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}]
-- 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))
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
have 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))
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}]
-- 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))
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
have 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))
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}]