awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
inst : Semiring R
inst_1 : Semiring R'
T : Type w
inst_2 : Module R R'
inst_3 : NonAssocSemiring T
inst_4 : Module R T
inst_5 : Module R' T
inst_6 : IsScalarTower R' T T
inst_7 : FaithfulSMul R' T
inst_8 : IsScalarTower R R' T
⊢ lift.{w, u'} (Module.rank R R') ≤ lift.{u', w} (Module.rank R T)

Tactic:
LinearMap.lift_rank_le_of_injective ((LinearMap.toSpanSingleton R' T 1).restrictScalars R) <|
    (faithfulSMul_iff_injective_smul_one R' T).mp ‹_›

Premises used: LinearMap.restrictScalars, LinearMap.lift_rank_le_of_injective, Iff.mp, faithfulSMul_iff_injective_smul_one, OfNat.ofNat, LinearMap.toSpanSingleton
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
inst : Semiring R
inst_1 : Semiring R'
T : Type u'
inst_2 : Module R R'
inst_3 : NonAssocSemiring T
inst_4 : Module R T
inst_5 : Module R' T
inst_6 : IsScalarTower R' T T
inst_7 : FaithfulSMul R' T
inst_8 : IsScalarTower R R' T
⊢ Module.rank R R' ≤ Module.rank R T

Tactic:
simpa using Module.lift_rank_bot_le_lift_rank_of_isScalarTower R R' T

Premises used: Module.lift_rank_bot_le_lift_rank_of_isScalarTower
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
N : Submodule R M
⊢ Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M

Tactic:
HasRankNullity.rank_quotient_add_rank N

Premises used: HasRankNullity.rank_quotient_add_rank
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
⊢ ∃ (s : Set M),
    #(↑s : Type u) = Module.rank R M ∧
      LinearIndependent.{u, u_1, u} (ι := (↑s : Type u)) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
HasRankNullity.exists_set_linearIndependent M

Premises used: HasRankNullity.exists_set_linearIndependent, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
inst : Ring R
inst_1 : HasRankNullity.{u, u_1} R
⊢ Nontrivial R

Tactic:
(subsingleton_or_nontrivial R).resolve_left fun H ↦ ?_

Premises used: subsingleton_or_nontrivial, Or.resolve_left
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
inst : Ring R
inst_1 : HasRankNullity.{u, u_1} R
refine : ∀ (H : Subsingleton R), False
⊢ Nontrivial R

Tactic:
refine (subsingleton_or_nontrivial R).resolve_left fun H ↦ ?_

Premises used: subsingleton_or_nontrivial, Or.resolve_left
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
inst : Ring R
inst_1 : HasRankNullity.{u, u_1} R
H : Subsingleton R
⊢ Module.rank R (HasQuotient.Quotient PUnit.{u + 1} (B := Submodule R PUnit.{u + 1}) ⊥) + Module.rank R ↥⊥ =
    Module.rank R PUnit.{u + 1}

Tactic:
have := rank_quotient_add_rank (R := R) (M := PUnit) ⊥
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
inst : Ring R
inst_1 : HasRankNullity.{u, u_1} R
H : Subsingleton R
this :
  Module.rank R (HasQuotient.Quotient PUnit.{u + 1} (B := Submodule R PUnit.{u + 1}) ⊥) + Module.rank R ↥⊥ =
    Module.rank R PUnit.{u + 1}
⊢ False

Tactic:
simp [one_add_one_eq_two] at this

Premises used: one_add_one_eq_two
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
haveI :
  ∀ (this : (p : Submodule R M) → DecidableEq (M ⧸ p)),
    lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker) = lift.{v, u} (Module.rank R M)
⊢ lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker) = lift.{v, u} (Module.rank R M)

Tactic:
haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p)
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
this : (p : Submodule R M) → DecidableEq (M ⧸ p)
rw : lift.{v, u} (Module.rank R (M ⧸ f.ker)) + lift.{v, u} (Module.rank R ↥f.ker) = lift.{v, u} (Module.rank R M)
rw₁ : lift.{v, u} (Module.rank R (M ⧸ f.ker) + Module.rank R ↥f.ker) = lift.{v, u} (Module.rank R M)
rw₂ rw₃ : lift.{v, u} (Module.rank R M) = lift.{v, u} (Module.rank R M)
⊢ lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker) = lift.{v, u} (Module.rank R M)

Tactic:
rw [← f.quotKerEquivRange.lift_rank_eq, ← lift_add, rank_quotient_add_rank]

Premises used: LinearEquiv.lift_rank_eq, Submodule.rank_quotient_add_rank, LinearMap.quotKerEquivRange, Cardinal.lift_add
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M M₁ : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M₁
haveI :
  ∀ (this : (p : Submodule R M) → DecidableEq (M ⧸ p)), Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M
⊢ Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M

Tactic:
haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p)
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M M₁ : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M₁
this : (p : Submodule R M) → DecidableEq (M ⧸ p)
rw : Module.rank R (M ⧸ f.ker) + Module.rank R ↥f.ker = Module.rank R M
rw₁ rw₂ : Module.rank R M = Module.rank R M
⊢ Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M

Tactic:
rw [← f.quotKerEquivRange.rank_eq, rank_quotient_add_rank]

Premises used: Submodule.rank_quotient_add_rank, LinearEquiv.rank_eq, LinearMap.quotKerEquivRange
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
h : Surjective.{u + 1, v + 1} (α := M) (β := M') (⇑f : (a : M) → M')
rw :
  lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker) =
    lift.{u, v} (Module.rank R M') + lift.{v, u} (Module.rank R ↥f.ker)
rw₁ rw₂ :
  lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker) =
    lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker)
⊢ lift.{v, u} (Module.rank R M) = lift.{u, v} (Module.rank R M') + lift.{v, u} (Module.rank R ↥f.ker)

Tactic:
rw [← lift_rank_range_add_rank_ker f, ← rank_range_of_surjective f h]

Premises used: LinearMap.lift_rank_range_add_rank_ker, rank_range_of_surjective
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M M₁ : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M₁
h : Surjective (α := M) (β := M₁) (⇑f : (a : M) → M₁)
rw : Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M₁ + Module.rank R ↥f.ker
rw₁ rw₂ : Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R ↥f.range + Module.rank R ↥f.ker
⊢ Module.rank R M = Module.rank R M₁ + Module.rank R ↥f.ker

Tactic:
rw [← rank_range_add_rank_ker f, ← rank_range_of_surjective f h]

Premises used: LinearMap.rank_range_add_rank_ker, rank_range_of_surjective
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
⊢ ∀ x ∈ comap f p, Membership.mem (α := M') p ((f : (a : M) → M') x : M')

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : LinearMap.{u_1, u_1, u, v} (RingHom.id R) ↥(comap f p) ↥p := f.restrict ⋯
rw : Module.rank R ↥(Submodule.map (comap f p).subtype f'.ker) ≤ Module.rank R ↥f.ker
⊢ Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker

Tactic:
rw [← rank_map_eq (injective_subtype (comap f p))]

Premises used: Submodule.injective_subtype, Submodule.comap, rank_map_eq
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : LinearMap.{u_1, u_1, u, v} (RingHom.id R) ↥(comap f p) ↥p := f.restrict ⋯
x : M
hx : x ∈ Submodule.map (comap f p).subtype f'.ker
⊢ x ∈ f.ker

Tactic:
aesop (add simp Subtype.ext_iff)

Premises used: Subtype.ext_iff
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : LinearMap.{u_1, u_1, u, v} (RingHom.id R) ↥(comap f p) ↥p := f.restrict ⋯
⊢ Module.rank R ↥(Submodule.map (comap f p).subtype f'.ker) ≤ Module.rank R ↥f.ker

Tactic:
exact rank_mono fun x hx ↦ by aesop (add simp Subtype.ext_iff)

Premises used: Submodule.rank_mono
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : LinearMap.{u_1, u_1, u, v} (RingHom.id R) ↥(comap f p) ↥p := f.restrict ⋯
⊢ Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker

Tactic:
have hk : Module.rank R f'.ker ≤ Module.rank R f.ker := by
    rw [← rank_map_eq (injective_subtype (comap f p))]
    exact rank_mono fun x hx ↦ by aesop (add simp Subtype.ext_iff)
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : LinearMap.{u_1, u_1, u, v} (RingHom.id R) ↥(comap f p) ↥p := f.restrict ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
grw grw₁ : Module.rank R ↥p ≤ Module.rank R ↥p
⊢ Module.rank R ↥f'.range ≤ Module.rank R ↥p

Tactic:
grw [Submodule.rank_le f'.range]

Premises used: Submodule.rank_le, LinearMap.range
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : LinearMap.{u_1, u_1, u, v} (RingHom.id R) ↥(comap f p) ↥p := f.restrict ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
⊢ Module.rank R ↥f'.range ≤ Module.rank R ↥p

Tactic:
have hr : Module.rank R f'.range ≤ Module.rank R p := by grw [Submodule.rank_le f'.range]
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : LinearMap.{u_1, u_1, u, v} (RingHom.id R) ↥(comap f p) ↥p := f.restrict ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
hr : Module.rank R ↥f'.range ≤ Module.rank R ↥p
rw :
  lift.{u, v} (Module.rank R ↥f'.range) + lift.{v, u} (Module.rank R ↥f'.ker) ≤
    lift.{u, v} (Module.rank R ↥p) + lift.{v, u} (Module.rank R ↥f.ker)
⊢ lift.{v, u} (Module.rank R ↥(comap f p)) ≤ lift.{u, v} (Module.rank R ↥p) + lift.{v, u} (Module.rank R ↥f.ker)

Tactic:
rw [← f'.lift_rank_range_add_rank_ker]

Premises used: LinearMap.lift_rank_range_add_rank_ker
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : LinearMap.{u_1, u_1, u, v} (RingHom.id R) ↥(comap f p) ↥p := f.restrict ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
hr : Module.rank R ↥f'.range ≤ Module.rank R ↥p
h₁ : lift.{u, v} (Module.rank R ↥f'.range) ≤ lift.{u, v} (Module.rank R ↥p)
h₂ : lift.{v, u} (Module.rank R ↥f'.ker) ≤ lift.{v, u} (Module.rank R ↥f.ker)
⊢ lift.{u, v} (Module.rank R ↥f'.range) + lift.{v, u} (Module.rank R ↥f'.ker) ≤
    lift.{u, v} (Module.rank R ↥p) + lift.{v, u} (Module.rank R ↥f.ker)

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : LinearMap.{u_1, u_1, u, v} (RingHom.id R) ↥(comap f p) ↥p := f.restrict ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
hr : Module.rank R ↥f'.range ≤ Module.rank R ↥p
h₁ h₂ h₃ h₄ : Module.rank R ↥f'.range ≤ Module.rank R ↥p
⊢ lift.{u, v} (Module.rank R ↥f'.range) ≤ lift.{u, v} (Module.rank R ↥p)

Tactic:
rwa [lift_le]

Premises used: Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : LinearMap.{u_1, u_1, u, v} (RingHom.id R) ↥(comap f p) ↥p := f.restrict ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
hr : Module.rank R ↥f'.range ≤ Module.rank R ↥p
h₂ h₃ h₄ h₅ : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
⊢ lift.{v, u} (Module.rank R ↥f'.ker) ≤ lift.{v, u} (Module.rank R ↥f.ker)

Tactic:
rwa [lift_le]

Premises used: Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
rw : Submodule.map (Submodule.map f p).mkQ f.range = Submodule.map (Submodule.map f p).mkQ (comap id f.range)
⊢ Submodule.map (Submodule.map f p).mkQ f.range = f'.ker

Tactic:
rw [ker_mapQ]

Premises used: Submodule.ker_mapQ
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
⊢ Submodule.map (Submodule.map f p).mkQ f.range = Submodule.map (Submodule.map f p).mkQ (comap id f.range)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
g : ↥f.range →ₗ[R] ↥f'.ker :=
  (↑(LinearEquiv.ofEq (Submodule.map (Submodule.map f p).mkQ f.range) f'.ker ⋯) :
      ↥(Submodule.map (Submodule.map f p).mkQ f.range) →ₗ[R] ↥f'.ker) ∘ₗ
    (Submodule.map f p).mkQ.submoduleMap f.range
⊢ Surjective (α := ↥f.range) (β := ↥f'.ker) (⇑g : (a : ↥f.range) → ↥f'.ker)

Tactic:
simpa [g] using submoduleMap_surjective (map f p).mkQ f.range

Premises used: LinearMap.range, Submodule.mkQ, Submodule.map, LinearMap.submoduleMap_surjective
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
g : ↥f.range →ₗ[R] ↥f'.ker :=
  (↑(LinearEquiv.ofEq (Submodule.map (Submodule.map f p).mkQ f.range) f'.ker ⋯) :
      ↥(Submodule.map (Submodule.map f p).mkQ f.range) →ₗ[R] ↥f'.ker) ∘ₗ
    (Submodule.map f p).mkQ.submoduleMap f.range
⊢ Surjective (α := ↥f.range) (β := ↥f'.ker) (⇑g : (a : ↥f.range) → ↥f'.ker)

Tactic:
have g_surj : Surjective g := by simpa [g] using submoduleMap_surjective (map f p).mkQ f.range
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
g : ↥f.range →ₗ[R] ↥f'.ker :=
  (↑(LinearEquiv.ofEq (Submodule.map (Submodule.map f p).mkQ f.range) f'.ker ⋯) :
      ↥(Submodule.map (Submodule.map f p).mkQ f.range) →ₗ[R] ↥f'.ker) ∘ₗ
    (Submodule.map f p).mkQ.submoduleMap f.range
g_surj : Surjective (α := ↥f.range) (β := ↥f'.ker) (⇑g : (a : ↥f.range) → ↥f'.ker)
⊢ g.ker = Submodule.map f.rangeRestrict p

Tactic:
simp [g, submoduleMap, ker_restrict, map_codRestrict]

Premises used: LinearMap.submoduleMap, LinearMap.map_codRestrict, LinearMap.ker_restrict
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
g : ↥f.range →ₗ[R] ↥f'.ker :=
  (↑(LinearEquiv.ofEq (Submodule.map (Submodule.map f p).mkQ f.range) f'.ker ⋯) :
      ↥(Submodule.map (Submodule.map f p).mkQ f.range) →ₗ[R] ↥f'.ker) ∘ₗ
    (Submodule.map f p).mkQ.submoduleMap f.range
g_surj : Surjective (α := ↥f.range) (β := ↥f'.ker) (⇑g : (a : ↥f.range) → ↥f'.ker)
⊢ g.ker = Submodule.map f.rangeRestrict p

Tactic:
have g_ker : g.ker = map f.rangeRestrict p := by
      simp [g, submoduleMap, ker_restrict, map_codRestrict]
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
g : ↥f.range →ₗ[R] ↥f'.ker :=
  (↑(LinearEquiv.ofEq (Submodule.map (Submodule.map f p).mkQ f.range) f'.ker ⋯) :
      ↥(Submodule.map (Submodule.map f p).mkQ f.range) →ₗ[R] ↥f'.ker) ∘ₗ
    (Submodule.map f p).mkQ.submoduleMap f.range
g_surj : Surjective (α := ↥f.range) (β := ↥f'.ker) (⇑g : (a : ↥f.range) → ↥f'.ker)
g_ker : g.ker = Submodule.map f.rangeRestrict p
e : (↥f.range ⧸ g.ker) ≃ₗ[R] ↥f'.ker := g.quotKerEquivOfSurjective g_surj
rwa rwa₁ rwa₂ rwa₃ :
  (e : HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker) →
    HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
⊢ HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker

Tactic:
rwa [g_ker] at e
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
let :
  ∀ (e : HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker),
    Module.rank R (M' ⧸ Submodule.map f p) =
      Module.rank R (M' ⧸ f.range) +
        Module.rank R (HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p))
⊢ Module.rank R (M' ⧸ Submodule.map f p) =
    Module.rank R (M' ⧸ f.range) +
      Module.rank R (HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p))

Tactic:
let +nondep e : (f.range ⧸ map f.rangeRestrict p) ≃ₗ[R] f'.ker := by
    let g : f.range →ₗ[R] f'.ker :=
      (LinearEquiv.ofEq (map (map f p).mkQ f.range) f'.ker) (by rw [ker_mapQ]; rfl) ∘ₗ
        (map f p).mkQ.submoduleMap f.range
    have g_surj : Surjective g := by simpa [g] using submoduleMap_surjective (map f p).mkQ f.range
    have g_ker : g.ker = map f.rangeRestrict p := by
      simp [g, submoduleMap, ker_restrict, map_codRestrict]
    let e := g.quotKerEquivOfSurjective g_surj
    rwa [g_ker] at e
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
e : HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
⊢ Module.rank R (M' ⧸ Submodule.map f p) = Module.rank R (M' ⧸ f.range) + Module.rank R ↥f'.ker

Tactic:
have := f'.rank_eq_of_surjective <| factor_surjective map_le_range
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
e : HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
this : Module.rank R (M' ⧸ Submodule.map f p) = Module.rank R (M' ⧸ f.range) + Module.rank R ↥f'.ker
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Module.rank R (M' ⧸ Submodule.map f p) =
        Module.rank R (M' ⧸ f.range) +
          Module.rank R (HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p))),
    Module.rank R (M' ⧸ Submodule.map f p) =
      Module.rank R (M' ⧸ f.range) +
        Module.rank R (HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p))
⊢ Module.rank R (M' ⧸ Submodule.map f p) =
    Module.rank R (M' ⧸ f.range) +
      Module.rank R (HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p))

Tactic:
rwa [← e.rank_eq] at this

Premises used: LinearEquiv.rank_eq
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
rw :
  lift.{u, v} (Module.rank R (M' ⧸ f.range)) +
      lift.{u, v}
        (Module.rank R (HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p))) ≤
    lift.{u, v} (Module.rank R (M' ⧸ f.range)) + lift.{v, u} (Module.rank R (M ⧸ p))
⊢ lift.{u, v} (Module.rank R (M' ⧸ Submodule.map f p)) ≤
    lift.{u, v} (Module.rank R (M' ⧸ f.range)) + lift.{v, u} (Module.rank R (M ⧸ p))

Tactic:
rw [rank_quot_submodule_map_eq, lift_add]

Premises used: LinearMap.rank_quot_submodule_map_eq, Cardinal.lift_add
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_1
M : Type u
M' : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
bc :
  lift.{u, v}
      (Module.rank R (HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p))) ≤
    lift.{v, u} (Module.rank R (M ⧸ p))
⊢ lift.{u, v} (Module.rank R (M' ⧸ f.range)) +
      lift.{u, v}
        (Module.rank R (HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p))) ≤
    lift.{u, v} (Module.rank R (M' ⧸ f.range)) + lift.{v, u} (Module.rank R (M ⧸ p))

Tactic:
gcongr