awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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 ↥f.range) ≤ lift.{v', v} (Module.rank R M)
have 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))
Tactic: simp only [Module.rank_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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'} (⨆ (ι : { 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))
have 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))
Tactic: rw [Cardinal.lift_iSup Cardinal.bddAbove_of_small]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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 : { 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))
have 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))
Tactic: apply ciSup_le'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
have 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) sorry) :
            Set M) :
        Type v)
Tactic: apply le_trans
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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)
⊢ 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))
have h₁ : lift.{v', v}
    #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (rangeSplitting (⇑f : (a : M) → M') '' s) sorry) :
            Set M) :
        Type v) ≤
  lift.{v', v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
Tactic: apply le_trans
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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))
⊢ 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))
have h₂ : Cardinal.{max v' v}
Tactic: apply le_trans
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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 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))
have h : #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (rangeSplitting (⇑f : (a : M) → M') '' s) sorry) : Set M) :
      Type v) ≤
  ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
Tactic: apply Cardinal.lift_le.mpr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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)
⊢ 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))
have apply : Cardinal.{v}
Tactic: apply Cardinal.lift_le.mpr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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
⊢ LinearIndepOn R id (rangeSplitting (⇑f : (a : M) → M') '' s)
have 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))
Tactic: apply LinearIndependent.of_comp f.rangeRestrict
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
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 p)) ≤ lift.{v', v} (Module.rank R ↥p)
have h : 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))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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)
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)
have 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)
Tactic: rwa [LinearMap.range_comp, range_subtype] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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)
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)
have 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)
Tactic: rwa [LinearMap.range_comp, range_subtype] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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')
have a : lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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')
⊢ lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
have a₁ : lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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')
⊢ Module.rank R ↥f.range = Module.rank R M'
have rw : Module.rank R ↥⊤ = Module.rank R M'
Tactic: rw [LinearMap.range_eq_top.2 h, rank_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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'
⊢ Module.rank R ↥f.range = Module.rank R M'
have rw₁ : Module.rank R M' = Module.rank R M'
Tactic: rw [LinearMap.range_eq_top.2 h, rank_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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 M
have rw : Module.rank R ↥s ≤ Module.rank R ↥⊤
Tactic: rw [← rank_top R M]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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 M') ≤ lift.{v', v} (Module.rank R M)
have rw : lift.{v, v'} (Module.rank R ↥f.range) ≤ lift.{v', v} (Module.rank R M)
Tactic: rw [← rank_range_of_surjective f h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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 M₁ ≤ Module.rank R M
have rw : Module.rank R ↥f.range ≤ Module.rank R M
Tactic: rw [← rank_range_of_surjective f h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
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'
⊢ Module.rank R' M ≤ Module.rank R M
have 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))
Tactic: rw [Module.rank, Module.rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : HasRankNullity.{u, u_1} R
⊢ Nontrivial R
have refine : ∀ (H : Subsingleton R), False
Tactic: refine (subsingleton_or_nontrivial R).resolve_left fun H ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : HasRankNullity.{u, u_1} R
H : Subsingleton R
⊢ False
have this : 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) ⊥
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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'
⊢ lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker) = lift.{v, u} (Module.rank R M)
have 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)
Tactic: haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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)
⊢ lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker) = lift.{v, u} (Module.rank R M)
have 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)
Tactic: rw [← f.quotKerEquivRange.lift_rank_eq, ← lift_add, rank_quotient_add_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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)
⊢ lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker) = lift.{v, u} (Module.rank R M)
have rw₁ : lift.{v, u} (Module.rank R (M ⧸ f.ker) + 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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)
⊢ lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker) = lift.{v, u} (Module.rank R M)
have rw₂ : lift.{v, u} (Module.rank R M) = lift.{v, u} (Module.rank R M)
Tactic: rw [← f.quotKerEquivRange.lift_rank_eq, ← lift_add, rank_quotient_add_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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₁
⊢ Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M
have haveI : ∀ (this : (p : Submodule R M) → DecidableEq (M ⧸ p)), 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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)
⊢ Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M
have rw : Module.rank R (M ⧸ f.ker) + Module.rank R ↥f.ker = Module.rank R M
Tactic: rw [← f.quotKerEquivRange.rank_eq, rank_quotient_add_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
⊢ Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M
have rw₁ : Module.rank R M = Module.rank R M
Tactic: rw [← f.quotKerEquivRange.rank_eq, rank_quotient_add_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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')
⊢ lift.{v, u} (Module.rank R M) = lift.{u, v} (Module.rank R M') + lift.{v, u} (Module.rank R ↥f.ker)
have 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)
Tactic: rw [← lift_rank_range_add_rank_ker f, ← rank_range_of_surjective f h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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)
⊢ lift.{v, u} (Module.rank R M) = lift.{u, v} (Module.rank R M') + lift.{v, u} (Module.rank R ↥f.ker)
have 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)
Tactic: rw [← lift_rank_range_add_rank_ker f, ← rank_range_of_surjective f h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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₁)
⊢ Module.rank R M = Module.rank R M₁ + Module.rank R ↥f.ker
have rw : Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M₁ + Module.rank R ↥f.ker
Tactic: rw [← rank_range_add_rank_ker f, ← rank_range_of_surjective f h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
⊢ Module.rank R M = Module.rank R M₁ + Module.rank R ↥f.ker
have rw₁ : Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R ↥f.range + Module.rank R ↥f.ker
Tactic: rw [← rank_range_add_rank_ker f, ← rank_range_of_surjective f h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
have rw : Module.rank R ↥(Submodule.map (comap f p).subtype f'.ker) ≤ Module.rank R ↥f.ker
Tactic: rw [← rank_map_eq (injective_subtype (comap f p))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
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 ⋯
⊢ lift.{v, u} (Module.rank R ↥(comap f p)) ≤ lift.{u, v} (Module.rank R ↥p) + lift.{v, u} (Module.rank R ↥f.ker)
have hk : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
have grw : Module.rank R ↥p ≤ Module.rank R ↥p
Tactic: grw [Submodule.rank_le f'.range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
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
⊢ lift.{v, u} (Module.rank R ↥(comap f p)) ≤ lift.{u, v} (Module.rank R ↥p) + lift.{v, u} (Module.rank R ↥f.ker)
have hr : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
⊢ lift.{v, u} (Module.rank R ↥(comap f p)) ≤ lift.{u, v} (Module.rank R ↥p) + lift.{v, u} (Module.rank R ↥f.ker)
have 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)
Tactic: rw [← f'.lift_rank_range_add_rank_ker]