awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
rw₁ : (toNat : (a : Cardinal.{max u v}) → ℕ) (lift.{u, v} #ι) = card ι
⊢ finrank R (ι →₀ R) = card ι
have rw₂ : Eq (α := ℕ) ((toNat : (a : Cardinal.{max u v}) → ℕ) (lift.{u, v} #ι) : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
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 ι
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}) → ℕ) #ι : ℕ)
⊢ finrank R (ι →₀ R) = card ι
have rw₃ : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #ι : ℕ)
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
η : 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 η
⊢ Module.rank R ((i : η) → φ i) = sum.{u₁', u_1} fun (i : η) ↦ Module.rank R (φ i)
have intro : ∀ (val : Fintype η), Module.rank R ((i : η) → φ i) = sum.{u₁', u_1} fun (i : η) ↦ Module.rank R (φ i)
Tactic: cases nonempty_fintype η
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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
⊢ Module.rank R (η → M) = (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M
have rw : (sum fun (i : η) ↦ Module.rank R M) = (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M
Tactic: rw [rank_pi, Cardinal.sum_const', Cardinal.mk_fintype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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
⊢ Module.rank R (η → M) = (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M
have rw₁ : #η * Module.rank R M = (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M
Tactic: rw [rank_pi, Cardinal.sum_const', Cardinal.mk_fintype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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
⊢ Module.rank R (η → M) = (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M
have rw₂ : (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M = (↑(Fintype.card η) : Cardinal.{u}) * Module.rank R M
Tactic: rw [rank_pi, Cardinal.sum_const', Cardinal.mk_fintype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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 η
⊢ Module.rank R (η → M) = (↑(Fintype.card η) : Cardinal.{max u₁' v}) * lift.{u₁', v} (Module.rank R M)
have rw : (sum.{u₁', v} fun (i : η) ↦ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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)
⊢ Module.rank R (η → M) = (↑(Fintype.card η) : Cardinal.{max u₁' v}) * lift.{u₁', v} (Module.rank R M)
have rw₁ : lift.{v, u₁'} #η * lift.{u₁', v} (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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)
⊢ Module.rank R (η → M) = (↑(Fintype.card η) : Cardinal.{max u₁' v}) * lift.{u₁', v} (Module.rank R M)
have 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)
Tactic: rw [rank_pi, Cardinal.sum_const, Cardinal.mk_fintype, Cardinal.lift_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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)
⊢ Module.rank R (η → M) = (↑(Fintype.card η) : Cardinal.{max u₁' v}) * lift.{u₁', v} (Module.rank R M)
have 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)
Tactic: rw [rank_pi, Cardinal.sum_const, Cardinal.mk_fintype, Cardinal.lift_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
η : Type u₁'
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Fintype η
⊢ Module.rank R (η → R) = (↑(Fintype.card η) : Cardinal.{max u u₁'})
have rw : (↑(Fintype.card η) : Cardinal.{max u₁' u}) * lift.{u₁', u} (Module.rank R R) =
  (↑(Fintype.card η) : Cardinal.{max u u₁'})
Tactic: rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
η : Type u₁'
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Fintype η
rw :
  (↑(Fintype.card η) : Cardinal.{max u₁' u}) * lift.{u₁', u} (Module.rank R R) =
    (↑(Fintype.card η) : Cardinal.{max u u₁'})
⊢ Module.rank R (η → R) = (↑(Fintype.card η) : Cardinal.{max u u₁'})
have rw₁ : (↑(Fintype.card η) : Cardinal.{max u₁' u}) * lift.{u₁', u} 1 = (↑(Fintype.card η) : Cardinal.{max u u₁'})
Tactic: rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
η : Type u₁'
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Fintype η
rw :
  (↑(Fintype.card η) : Cardinal.{max u₁' u}) * lift.{u₁', u} (Module.rank R R) =
    (↑(Fintype.card η) : Cardinal.{max u u₁'})
rw₁ : (↑(Fintype.card η) : Cardinal.{max u₁' u}) * lift.{u₁', u} 1 = (↑(Fintype.card η) : Cardinal.{max u u₁'})
⊢ Module.rank R (η → R) = (↑(Fintype.card η) : Cardinal.{max u u₁'})
have rw₂ : HMul.hMul (α := Cardinal.{max u₁' u}) (↑(Fintype.card η) : Cardinal.{max u₁' u}) 1 =
  (↑(Fintype.card η) : Cardinal.{max u u₁'})
Tactic: rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
η : Type u₁'
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Fintype η
rw :
  (↑(Fintype.card η) : Cardinal.{max u₁' u}) * lift.{u₁', u} (Module.rank R R) =
    (↑(Fintype.card η) : Cardinal.{max u u₁'})
rw₁ : (↑(Fintype.card η) : Cardinal.{max u₁' u}) * lift.{u₁', u} 1 = (↑(Fintype.card η) : Cardinal.{max u u₁'})
rw₂ :
  HMul.hMul (α := Cardinal.{max u₁' u}) (↑(Fintype.card η) : Cardinal.{max u₁' u}) 1 =
    (↑(Fintype.card η) : Cardinal.{max u u₁'})
⊢ Module.rank R (η → R) = (↑(Fintype.card η) : Cardinal.{max u u₁'})
have rw₃ : Eq (α := Cardinal.{max u u₁'}) (↑(Fintype.card η) : Cardinal.{max u₁' u}) (↑(Fintype.card η) : Cardinal.{max u u₁'})
Tactic: rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn : Module.rank R M = (↑n : Cardinal.{v})
⊢ M ≃ₗ[R] Fin n → R
have this : Nontrivial R
Tactic: haveI := nontrivial_of_invariantBasisNumber R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn : Module.rank R M = (↑n : Cardinal.{v})
this : Nontrivial R
⊢ M ≃ₗ[R] Fin n → R
have this₁ : lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})
Tactic: have : Cardinal.lift.{u} (n : Cardinal.{v}) = Cardinal.lift.{v} (n : Cardinal.{u}) := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn : Module.rank R M = (↑n : Cardinal.{v})
this_1 : Nontrivial R
this : lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})
⊢ M ≃ₗ[R] Fin n → R
have hn₁ : lift.{u, v} (Module.rank R M) = lift.{u, v} (↑n : Cardinal.{v})
Tactic: have hn := Cardinal.lift_inj.{v, u}.2 hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn_1 : Module.rank R M = (↑n : Cardinal.{v})
this_1 : Nontrivial R
this : lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})
hn : lift.{u, v} (Module.rank R M) = lift.{u, v} (↑n : Cardinal.{v})
⊢ M ≃ₗ[R] Fin n → R
have hn₁ : lift.{u, v} (Module.rank R M) = lift.{v, u} (↑n : Cardinal.{u})
Tactic: rw [this] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn_1 : Module.rank R M = (↑n : Cardinal.{v})
this_1 : Nontrivial R
this : lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})
hn : lift.{u, v} (Module.rank R M) = lift.{v, u} (↑n : Cardinal.{u})
⊢ M ≃ₗ[R] Fin n → R
have hn₁ : lift.{u, v} (Module.rank R M) = lift.{v, u} (Module.rank R (Fin n → R))
Tactic: rw [← @rank_fin_fun R _ _ n] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn_1 : Module.rank R M = (↑n : Cardinal.{v})
this_1 : Nontrivial R
this : lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})
hn : lift.{u, v} (Module.rank R M) = lift.{v, u} (Module.rank R (Fin n → R))
⊢ M ≃ₗ[R] Fin n → R
have this₁ : Free R (Fin n → R)
Tactic: haveI : Module.Free R (Fin n → R) := Module.Free.pi _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : StrongRankCondition R
inst_6 : StrongRankCondition S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : Free S M'
inst_10 : Algebra S R
inst_11 : IsScalarTower S R M
inst_12 : Free R M
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
have obtain : ∀ (fst : Type v) (bM : Basis fst R M),
  Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
Tactic: obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : StrongRankCondition R
inst_6 : StrongRankCondition S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : Free S M'
inst_10 : Algebra S R
inst_11 : IsScalarTower S R M
inst_12 : Free R M
fst : Type v
bM : Basis fst R M
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
have obtain : ∀ (fst : Type v') (bN : Basis fst S M'),
  Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
Tactic: obtain ⟨⟨_, bN⟩⟩ := Module.Free.exists_basis (R := S) (M := M')
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : StrongRankCondition R
inst_6 : StrongRankCondition S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : Free S M'
inst_10 : Algebra S R
inst_11 : IsScalarTower S R M
inst_12 : Free R M
fst : Type v
bM : Basis fst R M
fst_1 : Type v'
bN : Basis fst_1 S M'
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
have rw : Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} (Module.rank S M')
Tactic: rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : StrongRankCondition R
inst_6 : StrongRankCondition S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : Free S M'
inst_10 : Algebra S R
inst_11 : IsScalarTower S R M
inst_12 : Free R M
fst : Type v
bM : Basis fst R M
fst_1 : Type v'
bN : Basis fst_1 S M'
rw : Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} (Module.rank S M')
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
have rw₁ : Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} #fst_1
Tactic: rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : StrongRankCondition R
inst_6 : StrongRankCondition S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : Free S M'
inst_10 : Algebra S R
inst_11 : IsScalarTower S R M
inst_12 : Free R M
fst : Type v
bM : Basis fst R M
fst_1 : Type v'
bN : Basis fst_1 S M'
rw : Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} (Module.rank S M')
rw₁ : Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} #fst_1
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
have rw₂ : #(fst × fst_1) = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} #fst_1
Tactic: rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : StrongRankCondition R
inst_6 : StrongRankCondition S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : Free S M'
inst_10 : Algebra S R
inst_11 : IsScalarTower S R M
inst_12 : Free R M
fst : Type v
bM : Basis fst R M
fst_1 : Type v'
bN : Basis fst_1 S M'
rw : Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} (Module.rank S M')
rw₁ : Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} #fst_1
rw₂ : #(fst × fst_1) = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} #fst_1
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
have rw₃ : Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} #fst_1 = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} #fst_1
Tactic: rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]
-- 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
s t : Submodule R M
le : s ≤ t
lt : finrank.{u, v} R ↥s < finrank.{u, v} R ↥t
h : s = t
⊢ finrank.{u, v} R ↥s = finrank.{u, v} R ↥t
have rw : finrank.{u, v} R ↥t = finrank.{u, v} R ↥t
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Submodule R M
lt : finrank.{u, v} R ↥s < finrank R M
⊢ s < ⊤
have lt₁ : finrank.{u, v} R ↥s < finrank.{u, v} R ↥⊤
Tactic: rw [← finrank_top R M] at lt
Cleared hypotheses: lt
-- 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
s : Set M
⊢ Module.rank R ↥(span R s) ≤ #(↑s : Type v)
have rw : lift.{max u v, v}
    (Module.rank R
      ↥(LinearMap.range (M := Finsupp.{v, u} { x : M // x ∈ s } R)
          (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))) ≤
  lift.{max u v, v} #(↑s : Type v)
Tactic: rw [Finsupp.span_eq_range_linearCombination, ← lift_strictMono.le_iff_le]
-- 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
s : Set M
⊢ lift.{max u v, v}
      (Module.rank R
        ↥(LinearMap.range (M := Finsupp.{v, u} { x : M // x ∈ s } R)
            (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))) ≤
    lift.{max u v, v} #(↑s : Type v)
have refine : lift.{v, max u v} (Module.rank R (Finsupp.{v, u} { x : M // x ∈ s } R)) ≤ lift.{max u v, v} #(↑s : Type v)
Tactic: refine (lift_rank_range_le _).trans ?_
-- 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
s : Set M
⊢ lift.{v, max u v} (Module.rank R (Finsupp.{v, u} { x : M // x ∈ s } R)) ≤ lift.{max u v, v} #(↑s : Type v)
have rw : lift.{v, max u v} (lift.{u, v} #{ x : M // x ∈ s }) ≤ lift.{max u v, v} #(↑s : Type v)
Tactic: rw [rank_finsupp_self]
-- 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
ι : Type u_2
inst_4 : Fintype ι
b : ι → M
⊢ Set.finrank R (range b) ≤ Fintype.card ι
have refine : (range b).toFinset.card ≤ Fintype.card ι
Tactic: refine (finrank_span_le_card _).trans ?_
-- 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
ι : Type u_2
inst_4 : Fintype ι
b : ι → M
⊢ (range b).toFinset.card ≤ Fintype.card ι
have rw : (Finset.image b Finset.univ).card ≤ Fintype.card ι
Tactic: rw [Set.toFinset_range]
-- 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
ι : Type u_2
inst_4 : Fintype ι
b : ι → M
⊢ Set.finrank R (range b) ≤ Fintype.card ι
have refine : (range b).toFinset.card ≤ Fintype.card ι
Tactic: classical
  refine (finrank_span_le_card _).trans ?_
  rw [Set.toFinset_range]
  exact Finset.card_image_le
-- 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
ι : Type u_2
inst_4 : Fintype ι
b : ι → M
refine : (range b).toFinset.card ≤ Fintype.card ι
⊢ Set.finrank R (range b) ≤ Fintype.card ι
have refine₁ : (Finset.image b Finset.univ).card ≤ Fintype.card ι
Tactic: classical
  refine (finrank_span_le_card _).trans ?_
  rw [Set.toFinset_range]
  exact Finset.card_image_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
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 : Nontrivial R
ι : Type u_2
inst_5 : Fintype ι
b : ι → M
hb : LinearIndependent R b
⊢ Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
have this : Module.rank R ↥(span R (range b)) = #(↑(range b) : Type v)
Tactic: have : Module.rank R (span R (Set.range b)) = #(Set.range b) := rank_span hb