awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type w
fst : Type v
bs : Basis fst R M
rw : Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} #fst
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)
have rw₁ : #((_ : ι) × fst) = lift.{v, w} #ι * lift.{w, v} #fst
Tactic: rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma,
    Cardinal.sum_const]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type w
fst : Type v
bs : Basis fst R M
rw : Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} #fst
rw₁ : #((_ : ι) × fst) = lift.{v, w} #ι * lift.{w, v} #fst
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)
have rw₂ : (sum.{w, v} fun (i : ι) ↦ #fst) = lift.{v, w} #ι * lift.{w, v} #fst
Tactic: rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma,
    Cardinal.sum_const]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type w
fst : Type v
bs : Basis fst R M
rw : Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} #fst
rw₁ : #((_ : ι) × fst) = lift.{v, w} #ι * lift.{w, v} #fst
rw₂ : (sum.{w, v} fun (i : ι) ↦ #fst) = lift.{v, w} #ι * lift.{w, v} #fst
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)
have rw₃ : lift.{v, w} #ι * lift.{w, v} #fst = lift.{v, w} #ι * lift.{w, v} #fst
Tactic: rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma,
    Cardinal.sum_const]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
m : Type w
n : Type w'
inst_5 : Finite m
inst_6 : Finite n
⊢ Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)
have intro : ∀ (val : Fintype m),
  Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)
Tactic: cases nonempty_fintype m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
m : Type w
n : Type w'
inst_5 : Finite m
inst_6 : Finite n
val : Fintype m
⊢ Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)
have intro : ∀ (val : Fintype n),
  Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)
Tactic: cases nonempty_fintype n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
m : Type w
n : Type w'
inst_5 : Finite m
inst_6 : Finite n
val : Fintype m
val_1 : Fintype n
⊢ Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)
have intro : ∀ (I : Type v) (b : Basis I R M),
  Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)
Tactic: obtain ⟨I, b⟩ := Module.Free.exists_basis (R := R) (M := M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
m : Type w
n : Type w'
inst_5 : Finite m
inst_6 : Finite n
val : Fintype m
val_1 : Fintype n
I : Type v
b : Basis I R M
⊢ Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)
have intro : #(m × n × I) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)
Tactic: rw [← (b.matrix m n).mk_eq_rank'']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
m n : Type w
inst_5 : Finite m
inst_6 : Finite n
⊢ Module.rank R (Matrix m n M) = lift.{v, w} (#m * #n) * lift.{w, v} (Module.rank R M)
have rw : lift.{max v w, w} #m * lift.{max v w, w} #n * lift.{w, v} (Module.rank R M) =
  lift.{v, w} (#m * #n) * lift.{w, v} (Module.rank R M)
Tactic: rw [rank_matrix_module, lift_mul, lift_umax.{w, v}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
m n : Type w
inst_5 : Finite m
inst_6 : Finite n
rw :
  lift.{max v w, w} #m * lift.{max v w, w} #n * lift.{w, v} (Module.rank R M) =
    lift.{v, w} (#m * #n) * lift.{w, v} (Module.rank R M)
⊢ Module.rank R (Matrix m n M) = lift.{v, w} (#m * #n) * lift.{w, v} (Module.rank R M)
have rw₁ : lift.{max v w, w} #m * lift.{max v w, w} #n * lift.{w, v} (Module.rank R M) =
  lift.{v, w} #m * lift.{v, w} #n * lift.{w, v} (Module.rank R M)
Tactic: rw [rank_matrix_module, lift_mul, lift_umax.{w, v}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
m n : Type w
inst_5 : Finite m
inst_6 : Finite n
rw :
  lift.{max v w, w} #m * lift.{max v w, w} #n * lift.{w, v} (Module.rank R M) =
    lift.{v, w} (#m * #n) * lift.{w, v} (Module.rank R M)
rw₁ :
  lift.{max v w, w} #m * lift.{max v w, w} #n * lift.{w, v} (Module.rank R M) =
    lift.{v, w} #m * lift.{v, w} #n * lift.{w, v} (Module.rank R M)
⊢ Module.rank R (Matrix m n M) = lift.{v, w} (#m * #n) * lift.{w, v} (Module.rank R M)
have rw₂ : lift.{v, w} #m * lift.{v, w} #n * lift.{w, v} (Module.rank R M) =
  lift.{v, w} #m * lift.{v, w} #n * lift.{w, v} (Module.rank R M)
Tactic: rw [rank_matrix_module, lift_mul, lift_umax.{w, v}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m : Type v
n : Type w
inst_2 : Finite m
inst_3 : Finite n
⊢ Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
have rw : lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} (Module.rank R R) =
  lift.{max v w u, v} #m * lift.{max v w u, w} #n
Tactic: rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id,
    ← lift_lift.{w, max u v}, lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m : Type v
n : Type w
inst_2 : Finite m
inst_3 : Finite n
rw :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} (Module.rank R R) =
    lift.{max v w u, v} #m * lift.{max v w u, w} #n
⊢ Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
have rw₁ : lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
Tactic: rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id,
    ← lift_lift.{w, max u v}, lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m : Type v
n : Type w
inst_2 : Finite m
inst_3 : Finite n
rw :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} (Module.rank R R) =
    lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₁ :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
⊢ Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
have rw₂ : lift.{max u w, v} #m * lift.{max u v, w} #n * 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
Tactic: rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id,
    ← lift_lift.{w, max u v}, lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m : Type v
n : Type w
inst_2 : Finite m
inst_3 : Finite n
rw :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} (Module.rank R R) =
    lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₁ :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₂ : lift.{max u w, v} #m * lift.{max u v, w} #n * 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
⊢ Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
have rw₃ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max v w u, v} #m * lift.{max v w u, w} #n
Tactic: rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id,
    ← lift_lift.{w, max u v}, lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m : Type v
n : Type w
inst_2 : Finite m
inst_3 : Finite n
rw :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} (Module.rank R R) =
    lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₁ :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₂ : lift.{max u w, v} #m * lift.{max u v, w} #n * 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₃ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max v w u, v} #m * lift.{max v w u, w} #n
⊢ Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
have rw₄ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} (lift.{v, v} #m) * lift.{max v w u, w} #n
Tactic: rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id,
    ← lift_lift.{w, max u v}, lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m : Type v
n : Type w
inst_2 : Finite m
inst_3 : Finite n
rw :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} (Module.rank R R) =
    lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₁ :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₂ : lift.{max u w, v} #m * lift.{max u v, w} #n * 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₃ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₄ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} (lift.{v, v} #m) * lift.{max v w u, w} #n
⊢ Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
have rw₅ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} #m * lift.{max v w u, w} #n
Tactic: rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id,
    ← lift_lift.{w, max u v}, lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m : Type v
n : Type w
inst_2 : Finite m
inst_3 : Finite n
rw :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} (Module.rank R R) =
    lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₁ :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₂ : lift.{max u w, v} #m * lift.{max u v, w} #n * 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₃ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₄ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} (lift.{v, v} #m) * lift.{max v w u, w} #n
rw₅ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} #m * lift.{max v w u, w} #n
⊢ Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
have rw₆ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} #m * lift.{max u v, w} (lift.{w, w} #n)
Tactic: rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id,
    ← lift_lift.{w, max u v}, lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m : Type v
n : Type w
inst_2 : Finite m
inst_3 : Finite n
rw :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} (Module.rank R R) =
    lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₁ :
  lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₂ : lift.{max u w, v} #m * lift.{max u v, w} #n * 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₃ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max v w u, v} #m * lift.{max v w u, w} #n
rw₄ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} (lift.{v, v} #m) * lift.{max v w u, w} #n
rw₅ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} #m * lift.{max v w u, w} #n
rw₆ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} #m * lift.{max u v, w} (lift.{w, w} #n)
⊢ Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
have rw₇ : lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} #m * lift.{max u v, w} #n
Tactic: rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id,
    ← lift_lift.{w, max u v}, lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m n : Type v
inst_2 : Finite m
inst_3 : Finite n
⊢ Module.rank R (Matrix m n R) = lift.{u, v} (#m * #n)
have rw : lift.{max v u, v} #m * lift.{max v u, v} #n = lift.{u, v} (#m * #n)
Tactic: rw [rank_matrix, lift_mul, lift_umax.{v, u}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m n : Type v
inst_2 : Finite m
inst_3 : Finite n
rw : lift.{max v u, v} #m * lift.{max v u, v} #n = lift.{u, v} (#m * #n)
⊢ Module.rank R (Matrix m n R) = lift.{u, v} (#m * #n)
have rw₁ : lift.{max v u, v} #m * lift.{max v u, v} #n = lift.{u, v} #m * lift.{u, v} #n
Tactic: rw [rank_matrix, lift_mul, lift_umax.{v, u}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m n : Type v
inst_2 : Finite m
inst_3 : Finite n
rw : lift.{max v u, v} #m * lift.{max v u, v} #n = lift.{u, v} (#m * #n)
rw₁ : lift.{max v u, v} #m * lift.{max v u, v} #n = lift.{u, v} #m * lift.{u, v} #n
⊢ Module.rank R (Matrix m n R) = lift.{u, v} (#m * #n)
have rw₂ : lift.{u, v} #m * lift.{u, v} #n = lift.{u, v} #m * lift.{u, v} #n
Tactic: rw [rank_matrix, lift_mul, lift_umax.{v, u}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type v
inst_5 : Fintype ι
⊢ finrank.{u, v} R (ι →₀ M) = card ι * finrank R M
have rw : (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) = card ι * finrank R M
Tactic: rw [finrank, finrank, rank_finsupp, ← mk_toNat_eq_card, toNat_mul, toNat_lift, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type v
inst_5 : Fintype ι
rw : (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) = card ι * finrank R M
⊢ finrank.{u, v} R (ι →₀ M) = card ι * finrank R M
have rw₁ : (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) =
  HMul.hMul (β := ℕ) (card ι) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
Tactic: rw [finrank, finrank, rank_finsupp, ← mk_toNat_eq_card, toNat_mul, toNat_lift, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type v
inst_5 : Fintype ι
rw : (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) = card ι * finrank R M
rw₁ :
  (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) =
    HMul.hMul (β := ℕ) (card ι) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
⊢ finrank.{u, v} R (ι →₀ M) = card ι * finrank R M
have rw₂ : (toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι * lift.{v, v} (Module.rank R M)) =
  HMul.hMul (β := ℕ) (card ι) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
Tactic: rw [finrank, finrank, rank_finsupp, ← mk_toNat_eq_card, toNat_mul, toNat_lift, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type v
inst_5 : Fintype ι
rw : (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) = card ι * finrank R M
rw₁ :
  (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) =
    HMul.hMul (β := ℕ) (card ι) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
rw₂ :
  (toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι * lift.{v, v} (Module.rank R M)) =
    HMul.hMul (β := ℕ) (card ι) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
⊢ finrank.{u, v} R (ι →₀ M) = card ι * finrank R M
have rw₃ : (toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι * lift.{v, v} (Module.rank R M)) =
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
Tactic: rw [finrank, finrank, rank_finsupp, ← mk_toNat_eq_card, toNat_mul, toNat_lift, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type v
inst_5 : Fintype ι
rw : (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) = card ι * finrank R M
rw₁ :
  (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) =
    HMul.hMul (β := ℕ) (card ι) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
rw₂ :
  (toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι * lift.{v, v} (Module.rank R M)) =
    HMul.hMul (β := ℕ) (card ι) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
rw₃ :
  (toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι * lift.{v, v} (Module.rank R M)) =
    HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
      ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
⊢ finrank.{u, v} R (ι →₀ M) = card ι * finrank R M
have rw₄ : HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι) : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} (Module.rank R M)) : ℕ) =
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
Tactic: rw [finrank, finrank, rank_finsupp, ← mk_toNat_eq_card, toNat_mul, toNat_lift, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type v
inst_5 : Fintype ι
rw : (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) = card ι * finrank R M
rw₁ :
  (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) =
    HMul.hMul (β := ℕ) (card ι) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
rw₂ :
  (toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι * lift.{v, v} (Module.rank R M)) =
    HMul.hMul (β := ℕ) (card ι) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
rw₃ :
  (toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι * lift.{v, v} (Module.rank R M)) =
    HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
      ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
rw₄ :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι) : ℕ)
      ((toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} (Module.rank R M)) : ℕ) =
    HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
      ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
⊢ finrank.{u, v} R (ι →₀ M) = card ι * finrank R M
have rw₅ : HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} (Module.rank R M)) : ℕ) =
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
Tactic: rw [finrank, finrank, rank_finsupp, ← mk_toNat_eq_card, toNat_mul, toNat_lift, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type v
inst_5 : Fintype ι
rw : (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) = card ι * finrank R M
rw₁ :
  (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R (ι →₀ M)) =
    HMul.hMul (β := ℕ) (card ι) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
rw₂ :
  (toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι * lift.{v, v} (Module.rank R M)) =
    HMul.hMul (β := ℕ) (card ι) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
rw₃ :
  (toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι * lift.{v, v} (Module.rank R M)) =
    HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
      ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
rw₄ :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} #ι) : ℕ)
      ((toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} (Module.rank R M)) : ℕ) =
    HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
      ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
rw₅ :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
      ((toNat : (a : Cardinal.{v}) → ℕ) (lift.{v, v} (Module.rank R M)) : ℕ) =
    HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
      ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
⊢ finrank.{u, v} R (ι →₀ M) = card ι * finrank R M
have rw₆ : HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) =
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
Tactic: rw [finrank, finrank, rank_finsupp, ← mk_toNat_eq_card, toNat_mul, toNat_lift, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
ι : Type v
inst_2 : Fintype ι
⊢ finrank R (ι →₀ R) = card ι
have rw : (toNat : (a : Cardinal.{max u v}) → ℕ) (Module.rank R (ι →₀ R)) = card ι
Tactic: rw [finrank, rank_finsupp_self, ← mk_toNat_eq_card, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
ι : Type v
inst_2 : Fintype ι
rw : (toNat : (a : Cardinal.{max u v}) → ℕ) (Module.rank R (ι →₀ R)) = card ι
⊢ finrank R (ι →₀ R) = card ι
have rw₁ : (toNat : (a : Cardinal.{max u v}) → ℕ) (lift.{u, v} #ι) = card ι
Tactic: rw [finrank, rank_finsupp_self, ← mk_toNat_eq_card, toNat_lift]