awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
inst_3 : CommSemiring R'
S' : Type v
inst_4 : Semiring S'
inst_5 : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective.{w + 1, w' + 1} (α := R) (β := R') (⇑i : (a : R) → R')
hj : Injective (α := S) (β := S') (⇑j : (a : S) → S')
hc : RingHom.comp (algebraMap R' S') i = j.comp (algebraMap R S)
⊢ Module.rank R S ≤ Module.rank R' S'

Tactic:
simpa only [lift_id] using lift_rank_le_of_surjective_injective i j hi hj hc

Premises used: Algebra.lift_rank_le_of_surjective_injective, Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
inst_3 : CommSemiring R'
S' : Type v
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)
⊢ Module.rank R S = Module.rank R' S'

Tactic:
simpa only [lift_id] using lift_rank_eq_of_equiv_equiv i j hc

Premises used: Algebra.lift_rank_eq_of_equiv_equiv, Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
i : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')

Tactic:
lift_rank_le_of_injective_injectiveₛ (RingHom.id R) f (fun _ _ h ↦ h) i f.map_smul

Premises used: AddMonoidHomClass.toAddMonoidHom, LinearMap.map_smul, lift_rank_le_of_injective_injectiveₛ, RingHom.id, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
f : M →ₗ[R] M₁
i : Injective (α := M) (β := M₁) (⇑f : (a : M) → M₁)
⊢ Module.rank R M ≤ Module.rank R M₁

Tactic:
Cardinal.lift_le.1 (f.lift_rank_le_of_injective i)

Premises used: LinearMap.lift_rank_le_of_injective, Iff.mp, Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
simp :
  lift.{v, v'} (⨆ (ι : { s : Set ↥f.range // LinearIndepOn R id s }), #(↑(↑ι : Set ↥f.range) : Type v')) ≤
    lift.{v', v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
⊢ lift.{v, v'} (Module.rank R ↥f.range) ≤ lift.{v', v} (Module.rank R M)

Tactic:
simp only [Module.rank_def]

Premises used: Module.rank_def
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
rw :
  ⨆ (i : { s : Set ↥f.range // LinearIndepOn R id s }), lift.{v, v'} #(↑(↑i : Set ↥f.range) : Type v') ≤
    lift.{v', v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
⊢ lift.{v, v'} (⨆ (ι : { s : Set ↥f.range // LinearIndepOn R id s }), #(↑(↑ι : Set ↥f.range) : Type v')) ≤
    lift.{v', v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))

Tactic:
rw [Cardinal.lift_iSup Cardinal.bddAbove_of_small]

Premises used: Cardinal.lift_iSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
h :
  ∀ (i : { s : Set ↥f.range // LinearIndepOn R id s }),
    lift.{v, v'} #(↑(↑i : Set ↥f.range) : Type v') ≤
      lift.{v', v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
⊢ ⨆ (i : { s : Set ↥f.range // LinearIndepOn R id s }), lift.{v, v'} #(↑(↑i : Set ↥f.range) : Type v') ≤
    lift.{v', v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))

Tactic:
apply ciSup_le'

Premises used: ciSup_le'
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
h :
  lift.{v, v'} #(↑(↑(Subtype.mk (p := fun (s : Set ↥f.range) ↦ LinearIndepOn R id s) s li) : Set ↥f.range) : Type v') ≤
    lift.{v', v}
      #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (rangeSplitting (⇑f : (a : M) → M') '' s) ⋯) :
              Set M) :
          Type v)
h₁ :
  lift.{v', v}
      #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (rangeSplitting (⇑f : (a : M) → M') '' s) ⋯) :
              Set M) :
          Type v) ≤
    lift.{v', v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
h₂ : Cardinal.{max v' v}
⊢ lift.{v, v'} #(↑(↑(Subtype.mk (p := fun (s : Set ↥f.range) ↦ LinearIndepOn R id s) s li) : Set ↥f.range) : Type v') ≤
    lift.{v', v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))

Tactic:
apply le_trans

Premises used: le_trans
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
h :
  #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (rangeSplitting (⇑f : (a : M) → M') '' s) ⋯) : Set M) :
        Type v) ≤
    ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
apply : Cardinal.{v}
⊢ lift.{v', v}
      #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (rangeSplitting (⇑f : (a : M) → M') '' s) ⋯) :
              Set M) :
          Type v) ≤
    lift.{v', v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))

Tactic:
apply Cardinal.lift_le.mpr

Premises used: Iff.mpr, Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (rangeSplitting (⇑f : (a : M) → M') '' s) ⋯) : Set M) :
        Type v) ≤
    ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)

Tactic:
le_ciSup Cardinal.bddAbove_of_small ⟨rangeSplitting f '' s, ?_⟩

Premises used: le_ciSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
h :
  LinearIndependent.{v, u, v'} (ι := (↑(rangeSplitting (⇑f : (a : M) → M') '' s) : Type v)) R (M := ↥f.range)
    (comp (β := M) (⇑f.rangeRestrict : (a : M) → ↥f.range)
      fun (x : (↑(rangeSplitting (⇑f : (a : M) → M') '' s) : Type v)) ↦ id (↑x : M))
⊢ LinearIndepOn R id (rangeSplitting (⇑f : (a : M) → M') '' s)

Tactic:
apply LinearIndependent.of_comp f.rangeRestrict

Premises used: LinearMap.rangeRestrict, LinearIndependent.of_comp
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ LinearIndependent.{v, u, v'} (ι := (↑(rangeSplitting (⇑f : (a : M) → M') '' s) : Type v)) R (M := ↥f.range)
    ((fun (x : (↑s : Type v')) ↦ id (↑x : ↥f.range)) ∘
      (⇑(Equiv.Set.rangeSplittingImageEquiv (⇑f : (a : M) → M') s) :
        (a : (↑(rangeSplitting (⇑f : (a : M) → M') '' s) : Type v)) → (↑s : Type v')))

Tactic:
li.comp (Equiv.Set.rangeSplittingImageEquiv f s) (Equiv.injective _)

Premises used: Equiv.injective, Equiv.Set.rangeSplittingImageEquiv, DFunLike.coe, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ LinearIndependent.{v, u, v'} (ι := (↑(rangeSplitting (⇑f : (a : M) → M') '' s) : Type v)) R (M := ↥f.range)
    (comp (β := M) (⇑f.rangeRestrict : (a : M) → ↥f.range)
      fun (x : (↑(rangeSplitting (⇑f : (a : M) → M') '' s) : Type v)) ↦ id (↑x : M))

Tactic:
convert! li.comp (Equiv.Set.rangeSplittingImageEquiv f s) (Equiv.injective _) using 1

Premises used: Equiv.injective, Equiv.Set.rangeSplittingImageEquiv, DFunLike.coe, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ lift.{v, v'} #(↑(↑(Subtype.mk (p := fun (s : Set ↥f.range) ↦ LinearIndepOn R id s) s li) : Set ↥f.range) : Type v') ≤
    lift.{v', v}
      #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (rangeSplitting (⇑f : (a : M) → M') '' s) ⋯) :
              Set M) :
          Type v)

Tactic:
(Cardinal.lift_mk_eq'.mpr ⟨Equiv.Set.rangeSplittingImageEquiv f s⟩).ge

Premises used: Iff.mpr, Eq.ge, Set.Mem, setOf, Cardinal.lift_mk_eq', Nonempty.intro, Set.image, Set.range, Equiv.Set.rangeSplittingImageEquiv, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ lift.{v, v'} #(↑(↑(Subtype.mk (p := fun (s : Set ↥f.range) ↦ LinearIndepOn R id s) s li) : Set ↥f.range) : Type v') ≤
    lift.{v', v}
      #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (rangeSplitting (⇑f : (a : M) → M') '' s) ⋯) :
              Set M) :
          Type v)

Tactic:
exact (Cardinal.lift_mk_eq'.mpr ⟨Equiv.Set.rangeSplittingImageEquiv f s⟩).ge

Premises used: Iff.mpr, Eq.ge, Cardinal.lift_mk_eq', Nonempty.intro, Equiv.Set.rangeSplittingImageEquiv, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
f : M →ₗ[R] M₁
⊢ Module.rank R ↥f.range ≤ Module.rank R M

Tactic:
simpa using lift_rank_range_le f

Premises used: lift_rank_range_le
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
p : Submodule R M
⊢ lift.{v, v'} (Module.rank R ↥(f ∘ₗ p.subtype).range) ≤ lift.{v', v} (Module.rank R ↥p)

Tactic:
have h := lift_rank_range_le (f.comp (Submodule.subtype p))
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
p : Submodule R M
h : lift.{v, v'} (Module.rank R ↥(f ∘ₗ p.subtype).range) ≤ lift.{v', v} (Module.rank R ↥p)
rwa :
  ∀ (h : lift.{v, v'} (Module.rank R ↥(Submodule.map f p.subtype.range)) ≤ lift.{v', v} (Module.rank R ↥p)),
    lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h : lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)),
    lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)

Tactic:
rwa [LinearMap.range_comp, range_subtype] at h

Premises used: LinearMap.range_comp, Submodule.range_subtype
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
f : M →ₗ[R] M₁
p : Submodule R M
⊢ Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p

Tactic:
simpa using lift_rank_map_le f p

Premises used: lift_rank_map_le
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
f : M →ₗ[R] M₁
hf : Injective (α := M) (β := M₁) (⇑f : (a : M) → M₁)
p : Submodule R M
⊢ Module.rank R ↥(Submodule.map f p) = Module.rank R ↥p

Tactic:
le_antisymm (rank_map_le f p)
    ((f.submoduleMap p).rank_le_of_injective <| LinearMap.submoduleMap_injective hf p)

Premises used: rank_map_le, LinearMap.rank_le_of_injective, LinearMap.submoduleMap, le_antisymm, LinearMap.submoduleMap_injective
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Submodule R M
h : s ≤ t
⊢ Module.rank R ↥s ≤ Module.rank R ↥t

Tactic:
(Submodule.inclusion h).rank_le_of_injective fun ⟨x, _⟩ ⟨y, _⟩ eq =>
    Subtype.ext <| show x = y from Subtype.ext_iff.1 eq

Premises used: _private.0.Submodule.rank_mono.match_2, LinearMap.rank_le_of_injective, Subtype.ext_iff, Subtype.mk, Submodule.inclusion, Iff.mp, Eq, _private.0.Submodule.rank_mono.match_1, Subtype.ext
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M ≃ₗ[R] M'
a : lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')
a₁ : lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)
⊢ lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')

Tactic:
f.toLinearMap.lift_rank_le_of_injective f.injective

Premises used: LinearMap.lift_rank_le_of_injective, LinearEquiv.toLinearMap, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')

Tactic:
exact f.toLinearMap.lift_rank_le_of_injective f.injective

Premises used: LinearMap.lift_rank_le_of_injective, LinearEquiv.toLinearMap, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)

Tactic:
f.symm.toLinearMap.lift_rank_le_of_injective f.symm.injective

Premises used: LinearEquiv.symm, LinearMap.lift_rank_le_of_injective, LinearEquiv.toLinearMap, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)

Tactic:
exact f.symm.toLinearMap.lift_rank_le_of_injective f.symm.injective

Premises used: LinearEquiv.symm, LinearMap.lift_rank_le_of_injective, LinearEquiv.toLinearMap, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
f : M ≃ₗ[R] M₁
⊢ Module.rank R M = Module.rank R M₁

Tactic:
Cardinal.lift_inj.1 f.lift_rank_eq

Premises used: LinearEquiv.lift_rank_eq, Cardinal.lift_inj, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
h : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ lift.{v, v'} (Module.rank R ↥f.range) = lift.{v', v} (Module.rank R M)

Tactic:
(LinearEquiv.ofInjective f h).lift_rank_eq.symm

Premises used: Set.Mem, LinearEquiv.lift_rank_eq, LinearEquiv.ofInjective, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
f : M →ₗ[R] M₁
h : Injective (α := M) (β := M₁) (⇑f : (a : M) → M₁)
⊢ Module.rank R ↥f.range = Module.rank R M

Tactic:
(LinearEquiv.ofInjective f h).rank_eq.symm

Premises used: Set.Mem, LinearEquiv.ofInjective, LinearEquiv.rank_eq, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M ≃ₗ[R] M'
p : Submodule R M
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map (↑f : M →ₗ[R] M') p)) = lift.{v', v} (Module.rank R ↥p)

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

Premises used: Set.Mem, LinearEquiv.lift_rank_eq, LinearEquiv.submoduleMap, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
f : M ≃ₗ[R] M₁
p : Submodule R M
⊢ Module.rank R ↥(Submodule.map (↑f : M →ₗ[R] M₁) p) = Module.rank R ↥p

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

Premises used: Set.Mem, LinearEquiv.submoduleMap, LinearEquiv.rank_eq, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Module.rank R ↥⊤ = Module.rank R M

Tactic:
(LinearEquiv.ofTop ⊤ rfl).rank_eq

Premises used: LinearEquiv.ofTop, LinearEquiv.rank_eq, Top.top, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
h : Surjective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')
rw : Module.rank R ↥⊤ = Module.rank R M'
rw₁ rw₂ : Module.rank R M' = Module.rank R M'
⊢ Module.rank R ↥f.range = Module.rank R M'

Tactic:
rw [LinearMap.range_eq_top.2 h, rank_top]

Premises used: Iff.mpr, LinearMap.range_eq_top, rank_top
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Submodule R M
rw : Module.rank R ↥s ≤ Module.rank R ↥⊤
⊢ Module.rank R ↥s ≤ Module.rank R M

Tactic:
rw [← rank_top R M]

Premises used: rank_top
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R ↥⊤

Tactic:
rank_mono le_top

Premises used: Submodule.rank_mono, le_top
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R ↥⊤

Tactic:
exact rank_mono le_top

Premises used: Submodule.rank_mono, le_top
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
h : Surjective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')
rw : lift.{v, v'} (Module.rank R ↥f.range) ≤ lift.{v', v} (Module.rank R M)
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)

Tactic:
rw [← rank_range_of_surjective f h]

Premises used: rank_range_of_surjective
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
h : Surjective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ lift.{v, v'} (Module.rank R ↥f.range) ≤ lift.{v', v} (Module.rank R M)

Tactic:
apply lift_rank_range_le

Premises used: lift_rank_range_le
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
f : M →ₗ[R] M₁
h : Surjective (α := M) (β := M₁) (⇑f : (a : M) → M₁)
rw : Module.rank R ↥f.range ≤ Module.rank R M
⊢ Module.rank R M₁ ≤ Module.rank R M

Tactic:
rw [← rank_range_of_surjective f h]

Premises used: rank_range_of_surjective
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
f : M →ₗ[R] M₁
h : Surjective (α := M) (β := M₁) (⇑f : (a : M) → M₁)
⊢ Module.rank R ↥f.range ≤ Module.rank R M

Tactic:
apply rank_range_le

Premises used: rank_range_le
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_1
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
L L' : Submodule R M
s : S
hr : IsSMulRegular M s
h_1 : ∀ x ∈ L, s • x ∈ L'
x x_1 : ↥L
h :
  Eq (α := ↥L')
    ((LinearMap.restrict
            (((Algebra.lsmul S R M : AlgHom.{u_1, u_1, v} S S (Module.End R M)) : (a : S) → Module.End R M) s) h_1 :
          (a : ↥L) → ↥L')
        x :
      ↥L')
    ((LinearMap.restrict
            (((Algebra.lsmul S R M : AlgHom.{u_1, u_1, v} S S (Module.End R M)) : (a : S) → Module.End R M) s) h_1 :
          (a : ↥L) → ↥L')
        x_1 :
      ↥L')
⊢ x = x_1

Tactic:
simpa using hr (Subtype.ext_iff.mp h)

Premises used: Subtype.ext_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : Module R' M
inst_5 : SMulWithZero R R'
inst_6 : IsScalarTower R R' M
inst_7 : FaithfulSMul R R'
inst_8 : IsScalarTower R R' R'
rw :
  LE.le.{v + 1} (α := 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:
rw [Module.rank, Module.rank]

Premises used: Module.rank
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : Module R' M
inst_5 : SMulWithZero R R'
inst_6 : IsScalarTower R R' M
inst_7 : FaithfulSMul R R'
inst_8 : IsScalarTower R R' R'
x : { s : Set M // LinearIndepOn R' id s }
s : Set M
hs : LinearIndepOn R' id s
⊢ Injective.{u + 1, u' + 1} (β := R') fun (r : R) ↦ HSMul.hSMul (β := R') r 1

Tactic:
simpa [← faithfulSMul_iff_injective_smul_one]

Premises used: faithfulSMul_iff_injective_smul_one
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : Module R' M
inst_5 : SMulWithZero R R'
inst_6 : IsScalarTower R R' M
inst_7 : FaithfulSMul R R'
inst_8 : IsScalarTower R R' R'
⊢ LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (ι : { s : Set M // LinearIndepOn R' id s }), #(↑(↑ι : Set M) : Type v))
    (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))

Tactic:
exact ciSup_le' fun ⟨s, hs⟩ ↦ le_ciSup_of_le Cardinal.bddAbove_of_small
    ⟨s, hs.restrict_scalars (by simpa [← faithfulSMul_iff_injective_smul_one])⟩ le_rfl

Premises used: ciSup_le'