awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : Infinite M
h : lift.{max u v, v} #M = lift.{v, max u v} #(Finsupp.{v, u} (ChooseBasisIndex R M) R)
⊢ lift.{max u v, v} #M = max (lift.{max u v, v} (Module.rank R M)) (lift.{v, u} #R)

Tactic:
simp only [mk_finsupp_lift_of_infinite', ← rank_eq_card_chooseBasisIndex, lift_max,
    lift_lift] at h

Premises used: Cardinal.lift_lift, Module.Free.rank_eq_card_chooseBasisIndex, Cardinal.mk_finsupp_lift_of_infinite', Cardinal.lift_max
-- 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
this : Infinite M
h : lift.{max u v, v} #M = max (lift.{max u v, v} (Module.rank R M)) (lift.{v, u} #R)
⊢ Module.rank R M = #M

Tactic:
lift_inj.mp ((max_eq_iff.mp h.symm).resolve_right <| not_and_of_not_left _ ?_).left

Premises used: not_and_of_not_left, Cardinal.lift_inj, And.left, Iff.mp, Or.resolve_right, Eq.symm, max_eq_iff
-- 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
this : Infinite M
h : lift.{max u v, v} #M = max (lift.{max u v, v} (Module.rank R M)) (lift.{v, u} #R)
refine : ¬lift.{v, u} #R = lift.{max u v, v} #M
⊢ Module.rank R M = #M

Tactic:
refine lift_inj.mp ((max_eq_iff.mp h.symm).resolve_right <| not_and_of_not_left _ ?_).left

Premises used: not_and_of_not_left, Cardinal.lift_inj, And.left, Iff.mp, Or.resolve_right, Eq.symm, max_eq_iff
-- 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
this : Infinite M
h : lift.{max u v, v} #M = max (lift.{max u v, v} (Module.rank R M)) (lift.{v, u} #R)
⊢ ¬lift.{v, u} #R = lift.{max u v, v} #M

Tactic:
exact (lift_umax.{v, u}.symm ▸ h_lt).ne
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
h : lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')
rcases :
  ∀ (w : Set M') (B : Basis (↑w : Type v') R M'),
    ∃ (f : M →ₗ[R] M'), Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ ∃ (f : M →ₗ[R] M'), Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')

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
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
h : lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')
w : Set M'
B : Basis (↑w : Type v') R M'
⊢ ∃ (f : M →ₗ[R] M'), Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')

Tactic:
exists_linearMap_injective_of_linearIndependent_of_lift_rank_le B.linearIndependent
      (B.mk_eq_rank''.symm ▸ h)

Premises used: Eq.rec, Module.Basis.linearIndependent, Module.Free.exists_linearMap_injective_of_linearIndependent_of_lift_rank_le, Eq.symm, Module.Basis.mk_eq_rank''
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
h : lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')
w : Set M'
B : Basis (↑w : Type v') R M'
⊢ ∃ (f : M →ₗ[R] M'), Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')

Tactic:
exact exists_linearMap_injective_of_linearIndependent_of_lift_rank_le B.linearIndependent
      (B.mk_eq_rank''.symm ▸ h)

Premises used: Module.Basis.linearIndependent, Module.Free.exists_linearMap_injective_of_linearIndependent_of_lift_rank_le
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M₁
inst_5 : Module R M₁
inst_6 : Free R M₁
inst_7 : StrongRankCondition R
⊢ Module.rank R M ≤ Module.rank R M₁ ↔ ∃ (f : M →ₗ[R] M₁), Injective (α := M) (β := M₁) (⇑f : (a : M) → M₁)

Tactic:
simp [← lift_rank_le_iff_exists_linearMap]

Premises used: lift_rank_le_iff_exists_linearMap
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
inst_8 : Module.Finite R M
inst_9 : Module.Finite R M'
⊢ finrank R M ≤ finrank R M' ↔ ∃ (f : M →ₗ[R] M'), Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')

Tactic:
simp [← lift_rank_le_iff_exists_linearMap, ← finrank_eq_rank]

Premises used: lift_rank_le_iff_exists_linearMap, Module.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
obtain : ∀ (α : Type v) (B : Basis α R M), Nonempty (M ≃ₗ[R] M')
⊢ Nonempty (M ≃ₗ[R] M')

Tactic:
obtain ⟨⟨α, B⟩⟩ := Module.Free.exists_basis (R := R) (M := M)

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
obtain : ∀ (β : Type v') (B' : Basis β R M'), Nonempty (M ≃ₗ[R] M')
⊢ Nonempty (M ≃ₗ[R] M')

Tactic:
obtain ⟨⟨β, B'⟩⟩ := Module.Free.exists_basis (R := R) (M := M')

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
rw : lift.{v', v} (Module.rank R M) = lift.{v, v'} #β
rw₁ : lift.{v, v'} (Module.rank R M') = lift.{v, v'} #β
rw₂ rw₃ : lift.{v, v'} (Module.rank R M') = lift.{v, v'} (Module.rank R M')
⊢ lift.{v', v} #α = lift.{v, v'} #β

Tactic:
rw [B.mk_eq_rank'', cnd, B'.mk_eq_rank'']

Premises used: Module.Basis.mk_eq_rank''
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
⊢ lift.{v', v} #α = lift.{v, v'} #β

Tactic:
have : Cardinal.lift.{v', v} #α = Cardinal.lift.{v, v'} #β := by
    rw [B.mk_eq_rank'', cnd, B'.mk_eq_rank'']
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
this : lift.{v', v} #α = lift.{v, v'} #β
⊢ Nonempty (M ≃ₗ[R] M')

Tactic:
(Cardinal.lift_mk_eq.{v, v', 0}.1 this).map (B.equiv B')

Premises used: Module.Basis.equiv, Cardinal.lift_mk_eq, Iff.mp, Nonempty.map
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
this : lift.{v', v} #α = lift.{v, v'} #β
⊢ Nonempty (M ≃ₗ[R] M')

Tactic:
exact (Cardinal.lift_mk_eq.{v, v', 0}.1 this).map (B.equiv B')
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M₁
inst_5 : Module R M₁
inst_6 : Free R M₁
inst_7 : StrongRankCondition R
cond : Module.rank R M = Module.rank R M₁
⊢ Nonempty.{v + 1} (M ≃ₗ[R] M₁)

Tactic:
nonempty_linearEquiv_of_lift_rank_eq <| congr_arg _ cond

Premises used: congr_arg, nonempty_linearEquiv_of_lift_rank_eq
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
⊢ Nonempty (M ≃ₗ[R] M') ↔ lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')

Tactic:
⟨fun ⟨h⟩ => LinearEquiv.lift_rank_eq h, fun h => nonempty_linearEquiv_of_lift_rank_eq h⟩

Premises used: LinearEquiv.lift_rank_eq, Cardinal.lift, _private.0.LinearEquiv.nonempty_equiv_iff_lift_rank_eq.match_1, Iff.intro, nonempty_linearEquiv_of_lift_rank_eq, Module.rank, Eq
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M₁
inst_5 : Module R M₁
inst_6 : Free R M₁
inst_7 : StrongRankCondition R
⊢ Nonempty.{v + 1} (M ≃ₗ[R] M₁) ↔ Module.rank R M = Module.rank R M₁

Tactic:
⟨fun ⟨h⟩ => LinearEquiv.rank_eq h, fun h => nonempty_linearEquiv_of_rank_eq h⟩

Premises used: _private.0.LinearEquiv.nonempty_equiv_iff_rank_eq.match_1, LinearEquiv.rank_eq, Iff.intro, Module.rank, Eq, nonempty_linearEquiv_of_rank_eq
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
inst_8 : Module.Finite R M
inst_9 : Module.Finite R M'
cond : finrank R M = finrank R M'
⊢ lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')

Tactic:
simp only [← finrank_eq_rank, cond, lift_natCast]

Premises used: Module.finrank_eq_rank, Cardinal.lift_natCast
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
inst_8 : Module.Finite R M
inst_9 : Module.Finite R M'
⊢ Nonempty (M ≃ₗ[R] M') ↔ finrank R M = finrank R M'

Tactic:
⟨fun ⟨h⟩ => h.finrank_eq, fun h => nonempty_linearEquiv_of_finrank_eq h⟩

Premises used: LinearEquiv.finrank_eq, FiniteDimensional.nonempty_linearEquiv_of_finrank_eq, _private.0.LinearEquiv.nonempty_equiv_iff_lift_rank_eq.match_1, Iff.intro, Eq, 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
h : Module.rank R M = 0
⊢ IsEmpty.{v + 1} (ChooseBasisIndex R M)

Tactic:
rw [← Basis.mk_eq_rank'' (Module.Free.chooseBasis R M), Cardinal.mk_eq_zero_iff] at h

Premises used: Cardinal.mk_eq_zero_iff, 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
h : IsEmpty.{v + 1} (ChooseBasisIndex R M)
⊢ Subsingleton M

Tactic:
(Module.Free.chooseBasis R M).repr.subsingleton

Premises used: LinearEquiv.toAddEquiv, Module.Basis.repr, AddEquiv.toEquiv, Equiv.subsingleton, 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
h : IsEmpty.{v + 1} (ChooseBasisIndex R M)
⊢ Subsingleton M

Tactic:
exact (Module.Free.chooseBasis R M).repr.subsingleton

Premises used: LinearEquiv.toAddEquiv, Module.Basis.repr, AddEquiv.toEquiv, Equiv.subsingleton, 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
rw : Finite.{v + 1} (ChooseBasisIndex R M) ↔ Module.Finite R M
⊢ Module.rank R M < ℵ₀ ↔ Module.Finite R M

Tactic:
rw [Free.rank_eq_card_chooseBasisIndex, mk_lt_aleph0_iff]

Premises used: Cardinal.mk_lt_aleph0_iff, Module.Free.rank_eq_card_chooseBasisIndex
-- 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
⊢ Finite.{v + 1} (ChooseBasisIndex R M) ↔ Module.Finite R M

Tactic:
⟨fun h ↦ Finite.of_basis (Free.chooseBasis R M),
    fun I ↦ Finite.of_fintype (Free.ChooseBasisIndex R M)⟩

Premises used: Finite.of_fintype, Module.Free.ChooseBasisIndex, Iff.intro, Module.Finite.of_basis, 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
⊢ Finite.{v + 1} (ChooseBasisIndex R M) ↔ Module.Finite R M

Tactic:
exact ⟨fun h ↦ Finite.of_basis (Free.chooseBasis R M),
    fun I ↦ Finite.of_fintype (Free.ChooseBasisIndex 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
inst_4 : StrongRankCondition R
h : ¬Module.Finite R M
rw : Module.rank R M = 0 ∨ ¬Module.Finite R M
⊢ finrank R M = 0

Tactic:
rw [finrank, toNat_eq_zero, ← not_lt, Module.rank_lt_aleph0_iff]

Premises used: Module.rank_lt_aleph0_iff, not_lt, Cardinal.toNat_eq_zero, 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
h : ¬Module.Finite R M
⊢ Module.rank R M = 0 ∨ ¬Module.Finite R M

Tactic:
.inr h

Premises used: Or.inr
-- 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
h : ¬Module.Finite R M
⊢ Module.rank R M = 0 ∨ ¬Module.Finite R M

Tactic:
exact .inr h
-- 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
h : 0 < finrank R M
contrapose : ∀ (h : ¬Module.Finite R M), ¬0 < finrank R M
⊢ Module.Finite R M

Tactic:
contrapose h
-- 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
h : ¬Module.Finite R M
⊢ ¬0 < finrank R M

Tactic:
simp [finrank_of_not_finite h]

Premises used: Module.finrank_of_not_finite
-- 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
n : ℕ
hn : finrank R M = n.succ
rw : 0 < n.succ
⊢ 0 < finrank R M

Tactic:
rw [hn]
-- 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
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ

Tactic:
n.succ_pos

Premises used: Nat.succ_pos
-- 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
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ

Tactic:
exact n.succ_pos

Premises used: Nat.succ_pos
-- 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
W : Type v
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Free R W
n : ℕ
hn : n ≠ 0
hVW : Module.rank R M = n • Module.rank R W
⊢ Module.Finite R M ↔ Module.Finite R W

Tactic:
simp only [← rank_lt_aleph0_iff, hVW, nsmul_lt_aleph0_iff_of_ne_zero hn]

Premises used: Module.rank_lt_aleph0_iff, Cardinal.nsmul_lt_aleph0_iff_of_ne_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
pos : ∀ (H : Module.Finite S M), finrank S M ≤ finrank R M
neg : ∀ (H : ¬Module.Finite S M), finrank S M ≤ finrank R M
⊢ finrank S M ≤ finrank R M

Tactic:
by_cases H : Module.Finite S M

Premises used: Module.Finite
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
H : Module.Finite S M
⊢ Module.Finite R M

Tactic:
have := Module.Finite.trans (R := R) S M
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
H : Module.Finite S M
this : Module.Finite R M
⊢ finrank S M ≤ finrank R M

Tactic:
finrank_top_le_finrank_of_isScalarTower R S M

Premises used: Module.finrank_top_le_finrank_of_isScalarTower
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
H : Module.Finite S M
this : Module.Finite R M
⊢ finrank S M ≤ finrank R M

Tactic:
exact finrank_top_le_finrank_of_isScalarTower R S M

Premises used: Module.finrank_top_le_finrank_of_isScalarTower
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
H : ¬Module.Finite S M
neg : 0 ≤ finrank R M
rw : ℵ₀ ≤ Module.rank S M
⊢ finrank S M ≤ finrank R M

Tactic:
rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]

Premises used: Iff.mpr, Cardinal.toNat_eq_zero, Module.finrank, Or.inr
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
H : ¬Module.Finite S M
⊢ 0 ≤ finrank R M

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
H : ¬Module.Finite S M
⊢ 0 ≤ finrank R M

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
H : ¬Module.Finite S M
rwa : ¬Module.rank S M < ℵ₀
rwa₁ rwa₂ rwa₃ rwa₄ : ¬Module.Finite S M
⊢ ℵ₀ ≤ Module.rank S M

Tactic:
rwa [← not_lt, Module.rank_lt_aleph0_iff]

Premises used: Module.rank_lt_aleph0_iff, not_lt
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
S : Type u_2
T : Type u_3
inst_2 : Semiring S
inst_3 : Semiring T
inst_4 : Module R T
inst_5 : Module S T
inst_6 : Module R S
inst_7 : IsScalarTower R S T
inst_8 : IsScalarTower S T T
inst_9 : FaithfulSMul S T
inst_10 : Module.Finite S T
inst_11 : Free R S
pos : ∀ (H : Module.Finite R S), finrank R S ≤ finrank R T
neg : ∀ (H : ¬Module.Finite R S), finrank R S ≤ finrank R T
⊢ finrank R S ≤ finrank R T

Tactic:
by_cases H : Module.Finite R S

Premises used: Module.Finite
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
S : Type u_2
T : Type u_3
inst_2 : Semiring S
inst_3 : Semiring T
inst_4 : Module R T
inst_5 : Module S T
inst_6 : Module R S
inst_7 : IsScalarTower R S T
inst_8 : IsScalarTower S T T
inst_9 : FaithfulSMul S T
inst_10 : Module.Finite S T
inst_11 : Free R S
H : Module.Finite R S
⊢ Module.Finite R T

Tactic:
have := Module.Finite.trans (R := R) S T
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
S : Type u_2
T : Type u_3
inst_2 : Semiring S
inst_3 : Semiring T
inst_4 : Module R T
inst_5 : Module S T
inst_6 : Module R S
inst_7 : IsScalarTower R S T
inst_8 : IsScalarTower S T T
inst_9 : FaithfulSMul S T
inst_10 : Module.Finite S T
inst_11 : Free R S
H : Module.Finite R S
this : Module.Finite R T
⊢ finrank R S ≤ finrank R T

Tactic:
finrank_bot_le_finrank_of_isScalarTower R S T

Premises used: Module.finrank_bot_le_finrank_of_isScalarTower
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
S : Type u_2
T : Type u_3
inst_2 : Semiring S
inst_3 : Semiring T
inst_4 : Module R T
inst_5 : Module S T
inst_6 : Module R S
inst_7 : IsScalarTower R S T
inst_8 : IsScalarTower S T T
inst_9 : FaithfulSMul S T
inst_10 : Module.Finite S T
inst_11 : Free R S
H : Module.Finite R S
this : Module.Finite R T
⊢ finrank R S ≤ finrank R T

Tactic:
exact finrank_bot_le_finrank_of_isScalarTower R S T

Premises used: Module.finrank_bot_le_finrank_of_isScalarTower