awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Module.rank R (ULift.{w, v} M) = lift.{w, v} (Module.rank R M)

Tactic:
Cardinal.lift_injective.{v} <| Eq.symm <| (lift_lift _).trans ULift.moduleEquiv.symm.lift_rank_eq

Premises used: LinearEquiv.symm, Cardinal.lift_lift, LinearEquiv.lift_rank_eq, ULift.moduleEquiv, Eq.symm, Eq.trans, Cardinal.lift_injective
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
simp_rw :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u_2}) → ℕ) (Module.rank R (ULift.{u_2, v} M)) : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
simp_rw₁ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u_2}) → ℕ) (lift.{u_2, v} (Module.rank R M)) : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
⊢ finrank R (ULift.{u_2, v} M) = finrank R M

Tactic:
simp_rw [finrank, rank_ulift, toNat_lift]

Premises used: rank_ulift, Cardinal.toNat_lift, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Nontrivial R
simp :
  HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
    (⨆ (ι : { s : Set M₁ // LinearIndepOn R id s }), #(↑(↑ι : Set M₁) : Type v))
| Module.rank R M + Module.rank R M₁

Tactic:
simp only [Module.rank_def]

Premises used: Module.rank_def
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Nontrivial R
conv_lhs :
  HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
      (⨆ (ι : { s : Set M₁ // LinearIndepOn R id s }), #(↑(↑ι : Set M₁) : Type v)) ≤
    Module.rank R (M × M₁)
⊢ Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁)

Tactic:
conv_lhs => simp only [Module.rank_def]

Premises used: Module.rank_def
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Nontrivial R
rw :
  ⨆ (i : { s : Set M // LinearIndepOn R id s }),
      ⨆ (j : { s : Set M₁ // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) + #(↑(↑j : Set M₁) : Type v) ≤
    Module.rank R (M × M₁)
⊢ HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
      (⨆ (ι : { s : Set M₁ // LinearIndepOn R id s }), #(↑(↑ι : Set M₁) : Type v)) ≤
    Module.rank R (M × M₁)

Tactic:
rw [Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small]

Premises used: Cardinal.bddAbove_of_small, Cardinal.ciSup_add_ciSup
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Nontrivial R
⊢ ⨆ (i : { s : Set M // LinearIndepOn R id s }),
      ⨆ (j : { s : Set M₁ // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) + #(↑(↑j : Set M₁) : Type v) ≤
    Module.rank R (M × M₁)

Tactic:
ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦
    (linearIndependent_inl_union_inr' hs ht).cardinal_le_rank

Premises used: iSup, LinearIndependent.cardinal_le_rank, Cardinal.mk, Set.Elem, linearIndependent_inl_union_inr', LE.le, Subtype.mk, HAdd.hAdd, Module.rank, Prod, _private.0.rank_add_rank_le_rank_prod.match_1, Subtype.val, ciSup_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Nontrivial R
⊢ ⨆ (i : { s : Set M // LinearIndepOn R id s }),
      ⨆ (j : { s : Set M₁ // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) + #(↑(↑j : Set M₁) : Type v) ≤
    Module.rank R (M × M₁)

Tactic:
exact ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦
    (linearIndependent_inl_union_inr' hs ht).cardinal_le_rank

Premises used: ciSup_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : Nontrivial R
rw : Module.rank R (ULift.{v', v} M) + Module.rank R (ULift.{v, v'} M') ≤ Module.rank R (M × M')
⊢ lift.{v', v} (Module.rank R M) + lift.{v, v'} (Module.rank R M') ≤ Module.rank R (M × M')

Tactic:
rw [← rank_ulift, ← rank_ulift]

Premises used: rank_ulift
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : Nontrivial R
⊢ Module.rank R (ULift.{v', v} M) + Module.rank R (ULift.{v, v'} M') ≤ Module.rank R (M × M')

Tactic:
(rank_add_rank_le_rank_prod R _).trans_eq
    (ULift.moduleEquiv.prodCongr ULift.moduleEquiv).rank_eq

Premises used: LE.le.trans_eq, LinearEquiv.prodCongr, ULift.moduleEquiv, LinearEquiv.rank_eq, rank_add_rank_le_rank_prod
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : Nontrivial R
⊢ Module.rank R (ULift.{v', v} M) + Module.rank R (ULift.{v, v'} M') ≤ Module.rank R (M × M')

Tactic:
exact (rank_add_rank_le_rank_prod R _).trans_eq
    (ULift.moduleEquiv.prodCongr ULift.moduleEquiv).rank_eq

Premises used: LE.le.trans_eq, LinearEquiv.prodCongr, ULift.moduleEquiv, LinearEquiv.rank_eq, rank_add_rank_le_rank_prod
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : StrongRankCondition R
inst_6 : Free R M
inst_7 : Free R M'
⊢ Module.rank R (M × M') = lift.{v', v} (Module.rank R M) + lift.{v, v'} (Module.rank R M')

Tactic:
simpa [rank_eq_card_chooseBasisIndex R M, rank_eq_card_chooseBasisIndex R M', lift_umax]
    using ((chooseBasis R M).prod (chooseBasis R M')).mk_eq_rank.symm

Premises used: Module.Basis.mk_eq_rank, Module.Basis.prod, Cardinal.lift_umax, Eq.symm, Module.Free.rank_eq_card_chooseBasisIndex, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : StrongRankCondition R
inst_6 : Free R M
inst_7 : Free R M₁
⊢ Module.rank R (M × M₁) = Module.rank R M + Module.rank R M₁

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : StrongRankCondition R
inst_6 : Free R M
inst_7 : Free R M'
inst_8 : Module.Finite R M
inst_9 : Module.Finite R M'
⊢ finrank R (M × M') = finrank R M + finrank R M'

Tactic:
simp [finrank, rank_lt_aleph0 R M, rank_lt_aleph0 R M']

Premises used: Module.rank_lt_aleph0, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
obtain : ∀ (fst : Type v) (bs : Basis fst R M), Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)

Tactic:
obtain ⟨⟨_, bs⟩⟩ := Module.Free.exists_basis (R := R) (M := M)

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
rw₃ rw₄ : lift.{v, w} #ι * lift.{w, v} #fst = lift.{v, w} #ι * lift.{w, v} #fst
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)

Tactic:
rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma,
    Cardinal.sum_const]

Premises used: Cardinal.mk_sigma, Finsupp.basis, Cardinal.sum_const, Module.Basis.mk_eq_rank''
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
⊢ Module.rank R (ι →₀ M) = #ι * Module.rank R M

Tactic:
simp [rank_finsupp]

Premises used: rank_finsupp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
ι : Type w
⊢ Module.rank R (ι →₀ R) = lift.{u, w} #ι

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
ι : Type u
⊢ Module.rank R (ι →₀ R) = #ι

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
ι : Type v
M : ι → Type w
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u, w} R (M i)
inst_4 : ∀ (i : ι), Free.{u, w} R (M i)
B : (i : ι) → Basis.{w, u, w} (ChooseBasisIndex R (M i)) R (M i) := fun (i : ι) ↦ chooseBasis R (M i)
b : Basis ((i : ι) × ChooseBasisIndex R (M i)) R (⨁ (i : ι), M i) :=
  DFinsupp.basis (M := fun (i : ι) ↦ M i) (η := fun (i : ι) ↦ ChooseBasisIndex R (M i)) fun (i : ι) ↦ B i
⊢ Module.rank R (⨁ (i : ι), M i) = sum.{v, w} fun (i : ι) ↦ Module.rank R (M i)

Tactic:
simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']

Premises used: Module.Basis.mk_eq_rank''
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
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)
⊢ 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

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
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)
⊢ 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

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
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)
⊢ 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)

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
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)
⊢ 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:
rw [← (b.matrix m n).mk_eq_rank'']

Premises used: Module.Basis.matrix, Module.Basis.mk_eq_rank''
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
⊢ #(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:
simp only [mk_prod, lift_mul, lift_lift, ← mul_assoc, b.mk_eq_rank'']

Premises used: Cardinal.lift_lift, mul_assoc, Cardinal.lift_mul, Module.Basis.mk_eq_rank'', Cardinal.mk_prod
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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)
rw₂ 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)
⊢ Module.rank R (Matrix m n M) = lift.{v, w} (#m * #n) * lift.{w, v} (Module.rank R M)

Tactic:
rw [rank_matrix_module, lift_mul, lift_umax.{w, v}]

Premises used: rank_matrix_module, Cardinal.lift_mul
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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)
rw₇ 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
⊢ Module.rank R (Matrix m n 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]

Premises used: rank_matrix_module, Module.rank_self, Cardinal.lift_one, mul_one, Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
rw₂ rw₃ : lift.{u, v} #m * lift.{u, v} #n = lift.{u, v} #m * lift.{u, v} #n
⊢ Module.rank R (Matrix m n R) = lift.{u, v} (#m * #n)

Tactic:
rw [rank_matrix, lift_mul, lift_umax.{v, u}]

Premises used: rank_matrix, Cardinal.lift_mul
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
m n : Type u
inst_2 : Finite m
inst_3 : Finite n
⊢ Module.rank R (Matrix m n R) = #m * #n

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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) : ℕ)
rw₆ 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) : ℕ)
⊢ finrank.{u, v} R (ι →₀ M) = card ι * finrank R M

Tactic:
rw [finrank, finrank, rank_finsupp, ← mk_toNat_eq_card, toNat_mul, toNat_lift, toNat_lift]

Premises used: rank_finsupp, Cardinal.toNat_mul, Cardinal.mk_toNat_eq_card, Cardinal.toNat_lift, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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 ι
rw₁ : (toNat : (a : Cardinal.{max u v}) → ℕ) (lift.{u, v} #ι) = card ι
rw₂ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max u v}) → ℕ) (lift.{u, v} #ι) : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
rw₃ rw₄ : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
⊢ finrank R (ι →₀ R) = card ι

Tactic:
rw [finrank, rank_finsupp_self, ← mk_toNat_eq_card, toNat_lift]

Premises used: rank_finsupp_self, Cardinal.mk_toNat_eq_card, Cardinal.toNat_lift, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
ι : Type v
inst_2 : Fintype ι
M : ι → Type w
inst_3 : (i : ι) → AddCommMonoid (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : ∀ (i : ι), Free.{u, w} R (M i)
inst_6 : ∀ (i : ι), Module.Finite.{u, w} R (M i)
⊢ finrank R (⨁ (i : ι), M i) = ∑ i : ι, finrank.{u, w} R (M i)

Tactic:
simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_directSum, ← mk_sigma,
    mk_toNat_eq_card, card_sigma]

Premises used: rank_directSum, Cardinal.mk_toNat_eq_card, Fintype.card_sigma, Cardinal.mk_sigma, Module.Free.rank_eq_card_chooseBasisIndex, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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 u_2
n : Type u_3
inst_5 : Fintype m
inst_6 : Fintype n
⊢ finrank R (Matrix m n M) = card m * card n * finrank R M

Tactic:
simp [finrank]

Premises used: Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : (i : η) → AddCommMonoid (φ i)
inst_3 : (i : η) → Module.{u, u_1} R (φ i)
inst_4 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_5 : Finite η
intro : ∀ (val : Fintype η), Module.rank R ((i : η) → φ i) = sum.{u₁', u_1} fun (i : η) ↦ Module.rank R (φ i)
⊢ Module.rank R ((i : η) → φ i) = sum.{u₁', u_1} fun (i : η) ↦ Module.rank R (φ i)

Tactic:
cases nonempty_fintype η

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : (i : η) → AddCommMonoid (φ i)
inst_3 : (i : η) → Module.{u, u_1} R (φ i)
inst_4 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_5 : Finite η
val : Fintype η
B : (i : η) → Basis.{u_1, u, u_1} (ChooseBasisIndex R (φ i)) R (φ i) := fun (i : η) ↦ chooseBasis R (φ i)
b : Basis ((j : η) × ChooseBasisIndex R (φ j)) R ((i : η) → φ i) :=
  Pi.basis (ιs := fun (i : η) ↦ ChooseBasisIndex R (φ i)) (Ms := φ) fun (i : η) ↦ B i
⊢ Module.rank R ((i : η) → φ i) = sum.{u₁', u_1} fun (i : η) ↦ Module.rank R (φ i)

Tactic:
simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']

Premises used: Module.Basis.mk_eq_rank''
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
ι : Type v
inst_2 : Fintype ι
⊢ finrank R (ι → R) = Fintype.card ι

Tactic:
simp [finrank]

Premises used: Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
ι : Type v
inst_2 : Fintype ι
M : ι → Type w
inst_3 : (i : ι) → AddCommMonoid (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : ∀ (i : ι), Free.{u, w} R (M i)
inst_6 : ∀ (i : ι), Module.Finite.{u, w} R (M i)
⊢ finrank R ((i : ι) → M i) = ∑ i : ι, finrank.{u, w} R (M i)

Tactic:
simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_pi, ← mk_sigma,
    mk_toNat_eq_card, Fintype.card_sigma]

Premises used: Cardinal.mk_toNat_eq_card, Fintype.card_sigma, Cardinal.mk_sigma, Module.Free.rank_eq_card_chooseBasisIndex, rank_pi, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
M η : Type u
inst_2 : Fintype η
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Free R M
rw : (sum fun (i : η) ↦ Module.rank R M) = (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M
rw₁ : #η * Module.rank R M = (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M
rw₂ rw₃ : (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M = (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M
⊢ Module.rank R (η → M) = (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M

Tactic:
rw [rank_pi, Cardinal.sum_const', Cardinal.mk_fintype]

Premises used: Cardinal.mk_fintype, Cardinal.sum_const', rank_pi
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
η : Type u₁'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
inst_5 : Fintype η
rw :
  (sum.{u₁', v} fun (i : η) ↦ Module.rank R M) =
    (↑(Fintype.card η) : Cardinal.{max u₁' v}) * lift.{u₁', v} (Module.rank R M)
rw₁ :
  lift.{v, u₁'} #η * lift.{u₁', v} (Module.rank R M) =
    (↑(Fintype.card η) : Cardinal.{max u₁' v}) * lift.{u₁', v} (Module.rank R M)
rw₂ :
  lift.{v, u₁'} (↑(Fintype.card η) : Cardinal.{u₁'}) * lift.{u₁', v} (Module.rank R M) =
    (↑(Fintype.card η) : Cardinal.{max u₁' v}) * lift.{u₁', v} (Module.rank R M)
rw₃ rw₄ :
  (↑(Fintype.card η) : Cardinal.{max u₁' v}) * lift.{u₁', v} (Module.rank R M) =
    (↑(Fintype.card η) : Cardinal.{max u₁' v}) * lift.{u₁', v} (Module.rank R M)
⊢ Module.rank R (η → M) = (↑(Fintype.card η) : Cardinal.{max u₁' v}) * lift.{u₁', v} (Module.rank R M)

Tactic:
rw [rank_pi, Cardinal.sum_const, Cardinal.mk_fintype, Cardinal.lift_natCast]

Premises used: Cardinal.mk_fintype, Cardinal.lift_natCast, Cardinal.sum_const, rank_pi