awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
left : Module.Finite R M
right : Finite ι
⊢ Module.Finite R (ι →₀ M)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
simp : IsEmpty ι → Subsingleton R ∨ Finite ι
⊢ Module.Finite R (ι →₀ R) ↔ Subsingleton R ∨ Finite ι

Tactic:
simp only [finite_finsupp_iff, Finite.self, true_and, or_iff_right_iff_imp]

Premises used: Module.Finite.self, Module.finite_finsupp_iff, or_iff_right_iff_imp, true_and
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
⊢ IsEmpty ι → Subsingleton R ∨ Finite ι

Tactic:
fun _ ↦ .inr inferInstance

Premises used: inferInstance, Or.inr
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
⊢ IsEmpty ι → Subsingleton R ∨ Finite ι

Tactic:
exact fun _ ↦ .inr inferInstance
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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 : ℕ)
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ finrank R M = 1

Tactic:
rw [finrank, rank_subsingleton, map_one]

Premises used: map_one, Module.finrank, rank_subsingleton
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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

Tactic:
simp [finrank, h]

Premises used: Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Module.rank R M = 1 ↔ finrank R M = 1

Tactic:
Cardinal.toNat_eq_one.symm

Premises used: Cardinal.toNat_eq_one, Iff.symm, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
inst_3 : n.AtLeastTwo
⊢ Module.rank R M = OfNat.ofNat n ↔ finrank R M = OfNat.ofNat n

Tactic:
Cardinal.toNat_eq_ofNat.symm

Premises used: Iff.symm, Module.finrank, Cardinal.toNat_eq_ofNat
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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 < ℵ₀
hd : (↑n : Cardinal.{v}) < ℵ₀
⊢ finrank R M ≤ n

Tactic:
rwa [← Cardinal.toNat_le_iff_le_of_lt_aleph0, toNat_natCast] at h

Premises used: Cardinal.toNat_le_iff_le_of_lt_aleph0, Cardinal.toNat_natCast
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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})
⊢ Module.rank R M < ℵ₀

Tactic:
h.trans_lt natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0, LE.le.trans_lt
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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})
⊢ Module.rank R M < ℵ₀

Tactic:
exact h.trans_lt natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0, LE.le.trans_lt
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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})
⊢ (↑n : Cardinal.{v}) < ℵ₀

Tactic:
natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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})
⊢ (↑n : Cardinal.{v}) < ℵ₀

Tactic:
exact natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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 < ℵ₀
hd : (↑n : Cardinal.{v}) < ℵ₀
⊢ finrank R M < n

Tactic:
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast] at h

Premises used: Cardinal.toNat_lt_iff_lt_of_lt_aleph0, Cardinal.toNat_natCast
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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})
⊢ Module.rank R M < ℵ₀

Tactic:
h.trans natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0, LT.lt.trans
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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})
⊢ Module.rank R M < ℵ₀

Tactic:
exact h.trans natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0, LT.lt.trans
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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})
⊢ (↑n : Cardinal.{v}) < ℵ₀

Tactic:
natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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})
⊢ (↑n : Cardinal.{v}) < ℵ₀

Tactic:
exact natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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}) < ℵ₀
hd : Module.rank R M < ℵ₀
⊢ (↑n : Cardinal.{v}) < Module.rank R M

Tactic:
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast]

Premises used: Cardinal.toNat_lt_iff_lt_of_lt_aleph0, Cardinal.toNat_natCast
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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}) < ℵ₀

Tactic:
natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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}) < ℵ₀

Tactic:
exact natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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
hd : ∀ (h : ℵ₀ ≤ Module.rank R M), finrank R M ≤ n
⊢ Module.rank R M < ℵ₀

Tactic:
contrapose! h
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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
hd : 0 ≤ n
⊢ finrank R M ≤ n

Tactic:
rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]

Premises used: Cardinal.toNat_apply_of_aleph0_le, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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
⊢ 0 ≤ n

Tactic:
n.zero_le

Premises used: Nat.zero_le
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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
⊢ 0 ≤ n

Tactic:
exact n.zero_le

Premises used: Nat.zero_le
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : 1 < finrank R M
⊢ 1 < Module.rank R M

Tactic:
simpa using lt_rank_of_lt_finrank h

Premises used: Module.lt_rank_of_lt_finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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
h : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} (Module.rank R N)
h' : Module.rank R N < ℵ₀
⊢ finrank R M ≤ finrank R N

Tactic:
simpa only [toNat_lift] using toNat_le_toNat h (lift_lt_aleph0.mpr h')

Premises used: Iff.mpr, Cardinal.toNat_le_toNat, Cardinal.toNat_lift, Cardinal.lift_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
Goal:
R : Type u_1
inst : CommSemiring R
⊢ finrank R R = 1

Tactic:
finrank_eq_of_rank_eq (rank_self R)

Premises used: CommSemiring.rank_self, Module.finrank_eq_of_rank_eq
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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) : ℕ)
rw₂ rw₃ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{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) : ℕ)

Tactic:
rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]

Premises used: LinearEquiv.lift_rank_eq, Cardinal.toNat_lift
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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
p : Submodule R M
⊢ finrank.{u, w} R ↥(Submodule.map (↑f : M →ₗ[R] N) p) = finrank.{u, v} R ↥p

Tactic:
(f.submoduleMap p).finrank_eq.symm

Premises used: Set.Mem, LinearEquiv.finrank_eq, LinearEquiv.submoduleMap, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
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)
rw rw₁ : finrank.{u, w} R ↥f.range = finrank.{u, w} R ↥f.range
⊢ finrank.{u, w} R ↥f.range = finrank R M

Tactic:
rw [(LinearEquiv.ofInjective f hf).finrank_eq]

Premises used: LinearEquiv.finrank_eq, LinearEquiv.ofInjective
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
q : Submodule R ↥p
⊢ finrank.{u, v} R ↥(map p.subtype q) = finrank.{u, v} R ↥q

Tactic:
(Submodule.equivSubtypeMap p q).symm.finrank_eq

Premises used: LinearEquiv.symm, LinearEquiv.finrank_eq, Submodule.equivSubtypeMap
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R ↥⊤) : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Finrank
Goal:
R₀ : Type u_1
S₀ : Type u_2
inst : CommSemiring R₀
inst_1 : Semiring S₀
inst_2 : Algebra R₀ S₀
R₁ : Type u_3
S₁ : Type u_4
inst_3 : CommSemiring R₁
inst_4 : Semiring S₁
inst_5 : Algebra R₁ S₁
i : R₀ ≃+* R₁
j : S₀ ≃+* S₁
hc : RingHom.comp (algebraMap R₁ S₁) i.toRingHom = j.toRingHom.comp (algebraMap R₀ S₀)
⊢ finrank R₀ S₀ = finrank R₁ S₁

Tactic:
simpa using (congr_arg Cardinal.toNat (lift_rank_eq_of_equiv_equiv i j hc))

Premises used: Cardinal.toNat, Algebra.lift_rank_eq_of_equiv_equiv, congr_arg, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
F : Type u
K : Type v
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : StrongRankCondition F
inst_4 : StrongRankCondition K
inst_5 : Free F K
A : Type v
inst_6 : AddCommMonoid A
inst_7 : Module K A
inst_8 : Module F A
inst_9 : IsScalarTower F K A
inst_10 : Free K A
⊢ lift.{v, v} (Module.rank F K) * lift.{v, v} (Module.rank K A) = lift.{v, v} (Module.rank F A)

Tactic:
lift_rank_mul_lift_rank F K A

Premises used: lift_rank_mul_lift_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
F : Type u
K : Type v
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : StrongRankCondition F
inst_4 : StrongRankCondition K
inst_5 : Free F K
A : Type v
inst_6 : AddCommMonoid A
inst_7 : Module K A
inst_8 : Module F A
inst_9 : IsScalarTower F K A
inst_10 : Free K A
h : Module.rank F K = lift.{v, v} (Module.rank F K)
h₁ : Module.rank K A = lift.{v, v} (Module.rank K A)
h₂ : Module.rank F A = lift.{v, v} (Module.rank F A)
⊢ Module.rank F K * Module.rank K A = Module.rank F A

Tactic:
convert! lift_rank_mul_lift_rank F K A

Premises used: lift_rank_mul_lift_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
F : Type u
K : Type v
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : StrongRankCondition F
inst_4 : StrongRankCondition K
inst_5 : Free F K
A : Type v
inst_6 : AddCommMonoid A
inst_7 : Module K A
inst_8 : Module F A
inst_9 : IsScalarTower F K A
inst_10 : Free K A
h h₁ : Module.rank F K = Module.rank F K
⊢ Module.rank F K = lift.{v, v} (Module.rank F K)

Tactic:
rw [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
F : Type u
K : Type v
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : StrongRankCondition F
inst_4 : StrongRankCondition K
inst_5 : Free F K
A : Type v
inst_6 : AddCommMonoid A
inst_7 : Module K A
inst_8 : Module F A
inst_9 : IsScalarTower F K A
inst_10 : Free K A
h h₁ : Module.rank K A = Module.rank K A
⊢ Module.rank K A = lift.{v, v} (Module.rank K A)

Tactic:
rw [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
F : Type u
K : Type v
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : StrongRankCondition F
inst_4 : StrongRankCondition K
inst_5 : Free F K
A : Type v
inst_6 : AddCommMonoid A
inst_7 : Module K A
inst_8 : Module F A
inst_9 : IsScalarTower F K A
inst_10 : Free K A
h h₁ : Module.rank F A = Module.rank F A
⊢ Module.rank F A = lift.{v, v} (Module.rank F A)

Tactic:
rw [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.Free
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
rw :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank F K)) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
rw₁ :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank F K)) : ℕ)
      ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{v, w} (Module.rank K A)) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
rw₂ :
  Eq (α := ℕ)
    ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A)) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A) : ℕ)
rw₃ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{v, w} (Module.rank F A)) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A) : ℕ)
rw₄ rw₅ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A) : ℕ)
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F K) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)

Tactic:
rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul,
    lift_rank_mul_lift_rank, toNat_lift]

Premises used: lift_rank_mul_lift_rank, Cardinal.toNat_mul, Cardinal.toNat_lift
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
⊢ Nontrivial M

Tactic:
nontriviality M
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
h : Nontrivial M
⊢ Nontrivial R

Tactic:
have := Module.nontrivial R M
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
h : Nontrivial M
this : Nontrivial R
rcases :
  ∀ (w : Set M) (B : Basis (↑w : Type v) R M),
    ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')

Tactic:
rcases Module.Free.exists_set R M with ⟨_, ⟨B⟩⟩

Premises used: Module.Free.exists_set
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
h : Nontrivial M
this : Nontrivial R
w : Set M
B : Basis (↑w : Type v) R M
⊢ lift.{w, v} #(↑w : Type v) ≤ lift.{v, w} #ι

Tactic:
replace cnd := (Cardinal.lift_le.2 B.linearIndependent.cardinal_le_rank).trans cnd
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
h : Nontrivial M
this : Nontrivial R
w : Set M
B : Basis (↑w : Type v) R M
cnd : lift.{w, v} #(↑w : Type v) ≤ lift.{v, w} #ι
⊢ Nonempty (Embedding.{v + 1, w + 1} (↑w : Type v) ι)

Tactic:
rw [Cardinal.lift_mk_le'] at cnd

Premises used: Cardinal.lift_mk_le'
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
h : Nontrivial M
this : Nontrivial R
w : Set M
B : Basis (↑w : Type v) R M
cnd : Nonempty (Embedding.{v + 1, w + 1} (↑w : Type v) ι)
rcases :
  ∀ (i : (↑w : Type v) → ι) (hi : Injective i),
    ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')

Tactic:
rcases cnd with ⟨i, hi⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
h : Nontrivial M
this : Nontrivial R
w : Set M
B : Basis (↑w : Type v) R M
i : (↑w : Type v) → ι
hi : Injective i
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')

Tactic:
⟨B.constr ℕ (v ∘ i), B.injective_constr_of_linearIndependent (hv.comp _ hi)⟩

Premises used: Function.comp, Module.Basis.injective_constr_of_linearIndependent, Nat, Exists.intro, DFunLike.coe, LinearIndependent.comp, Module.Basis.constr
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
h : Nontrivial M
this : Nontrivial R
w : Set M
B : Basis (↑w : Type v) R M
i : (↑w : Type v) → ι
hi : Injective i
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')

Tactic:
refine ⟨B.constr ℕ (v ∘ i), B.injective_constr_of_linearIndependent (hv.comp _ hi)⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N : Type v
inst_4 : AddCommMonoid N
inst_5 : Module R N
ι : Type v
v : ι → N
hv : LinearIndependent R v
cnd : Module.rank R M ≤ #ι
⊢ lift.{v, v} (Module.rank R M) ≤ lift.{v, v} #ι

Tactic:
simpa using cnd
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
cnd : lift.{v', v} (Module.rank R M) < lift.{v, v'} (Module.rank R N')
rcases :
  ∀ (s : Set N') (hs : lift.{v, v'} #(↑s : Type v') = lift.{v', v} (Module.rank R M)) (hs₂ : LinearIndepOn R id s),
    ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')

Tactic:
rcases exists_set_linearIndependent_of_lt_lift_rank cnd with ⟨s, hs, hs₂⟩

Premises used: Module.exists_set_linearIndependent_of_lt_lift_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
cnd : lift.{v', v} (Module.rank R M) < lift.{v, v'} (Module.rank R N')
s : Set N'
hs : lift.{v, v'} #(↑s : Type v') = lift.{v', v} (Module.rank R M)
hs₂ : LinearIndepOn R id s
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')

Tactic:
exists_linearMap_injective_of_linearIndependent_of_lift_rank_le
    hs₂.linearIndependent hs.symm.le

Premises used: LinearIndepOn.linearIndependent, Eq.le, Module.Free.exists_linearMap_injective_of_linearIndependent_of_lift_rank_le, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
cnd : lift.{v', v} (Module.rank R M) < lift.{v, v'} (Module.rank R N')
s : Set N'
hs : lift.{v, v'} #(↑s : Type v') = lift.{v', v} (Module.rank R M)
hs₂ : LinearIndepOn R id s
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')

Tactic:
exact exists_linearMap_injective_of_linearIndependent_of_lift_rank_le
    hs₂.linearIndependent hs.symm.le

Premises used: LinearIndepOn.linearIndependent, Eq.le, Module.Free.exists_linearMap_injective_of_linearIndependent_of_lift_rank_le, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N : Type v
inst_4 : AddCommMonoid N
inst_5 : Module R N
cnd : Module.rank R M < Module.rank R N
⊢ lift.{v, v} (Module.rank R M) < lift.{v, v} (Module.rank R N)

Tactic:
simpa using cnd
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
⊢ Module.rank R M = #(ChooseBasisIndex R M)

Tactic:
(chooseBasis R M).mk_eq_rank''.symm

Premises used: Eq.symm, Module.Basis.mk_eq_rank'', Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
⊢ finrank R M = Fintype.card.{v} (ChooseBasisIndex R M)

Tactic:
simp [finrank, rank_eq_card_chooseBasisIndex]

Premises used: Module.Free.rank_eq_card_chooseBasisIndex, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
inst_5 : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
⊢ lift.{u, v} ℵ₀ ≤ lift.{v, u} #R

Tactic:
simp