awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.{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)
have h₁ : lift.{u, v} (Module.rank R ↥f'.range) ≤ lift.{u, v} (Module.rank R ↥p)
Tactic: gcongr
-- 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
h₁ : lift.{u, v} (Module.rank R ↥f'.range) ≤ lift.{u, v} (Module.rank R ↥p)
⊢ 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)
have h₂ : lift.{v, u} (Module.rank R ↥f'.ker) ≤ lift.{v, u} (Module.rank R ↥f.ker)
Tactic: gcongr
-- 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.{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 = f'.ker
have rw : Submodule.map (Submodule.map f p).mkQ f.range = Submodule.map (Submodule.map f p).mkQ (comap id f.range)
Tactic: rw [ker_mapQ]
-- 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.{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
⊢ HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
have g_surj : 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
-- 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.{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)
⊢ HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
have g_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]
-- 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.{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
⊢ HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
have 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
Tactic: rwa [g_ker] at e
Cleared hypotheses: e
-- 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.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
⊢ 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))
have 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))
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
-- 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.{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 (HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p))
have this : 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
-- 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.{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
⊢ 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))
have 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))
Tactic: rwa [← e.rank_eq] at this
Cleared hypotheses: this
-- 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.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
⊢ 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))
have 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))
Tactic: rw [rank_quot_submodule_map_eq, lift_add]
-- 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.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
⊢ 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))
have 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))
Tactic: gcongr
-- 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.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
⊢ p ≤ comap (M₂ := ↥f.range) f.rangeRestrict (Submodule.map f.rangeRestrict p)
have rw : p ≤ p ⊔ ker (M₂ := ↥f.range) f.rangeRestrict
Tactic: rw [comap_map_eq]
-- 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.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : LinearMap.{u_1, u_1, u, v} (RingHom.id R) (M ⧸ p)
  (HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p)) :=
  p.mapQ (Submodule.map f.rangeRestrict p) f.rangeRestrict ⋯
⊢ Surjective.{u + 1, v + 1} (α := M ⧸ p) (β :=
    HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p))
    (⇑f' : (a : M ⧸ p) → ↥f.range ⧸ Submodule.map f.rangeRestrict p)
have rw : Eq (α := Submodule R (HasQuotient.Quotient ↥f.range (B := Submodule R ↥f.range) (Submodule.map f.rangeRestrict p)))
  (Submodule.map (mkQ (Submodule.map f.rangeRestrict p)) (range f.rangeRestrict)) ⊤
Tactic: rw [← range_eq_top, range_mapQ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
⊢ ∃ (t : Set M), s ⊆ t ∧ #(↑t : Type u) = Module.rank R M ∧ LinearIndepOn R _root_.id t
have obtain : ∀ (t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s)))
  (ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s)))
  (ht' :
    LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
      (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))),
  ∃ (t : Set M), s ⊆ t ∧ #(↑t : Type u) = Module.rank R M ∧ LinearIndepOn R _root_.id t
Tactic: obtain ⟨t, ht, ht'⟩ := exists_set_linearIndependent R (M ⧸ Submodule.span R s)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
⊢ ∃ (t : Set M), s ⊆ t ∧ #(↑t : Type u) = Module.rank R M ∧ LinearIndepOn R _root_.id t
have choose : ∀ (sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M)
  (hsec :
    ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)),
      (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b),
  ∃ (t : Set M), s ⊆ t ∧ #(↑t : Type u) = Module.rank R M ∧ LinearIndepOn R _root_.id t
Tactic: choose sec hsec using Submodule.mkQ_surjective (Submodule.span R s)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
⊢ ∃ (t : Set M), s ⊆ t ∧ #(↑t : Type u) = Module.rank R M ∧ LinearIndepOn R _root_.id t
have hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
Tactic: have hsec' : (Submodule.mkQ _) ∘ sec = _root_.id := funext hsec
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
⊢ Disjoint s (sec '' t)
have rw : s ∩ sec '' t ⊆ ∅
Tactic: rw [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
x : HasQuotient.Quotient M (B := Submodule R M) (span R s)
hxt : x ∈ t
hxs : sec x ∈ s
⊢ Membership.mem (γ := Set M) ∅ (sec x)
have apply : (↑(Subtype.mk (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t) x hxt) : M ⧸ span R s) = 0
Tactic: apply ht'.ne_zero ⟨x, hxt⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
x : HasQuotient.Quotient M (B := Submodule R M) (span R s)
hxt : x ∈ t
hxs : sec x ∈ s
⊢ (↑(Subtype.mk (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t) x hxt) : M ⧸ span R s) =
    0
have rw : Membership.mem (γ := Submodule R M) (span R s) (sec x)
Tactic: rw [Subtype.coe_mk, ← hsec x, mkQ_apply, Quotient.mk_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
⊢ ∃ (t : Set M), s ⊆ t ∧ #(↑t : Type u) = Module.rank R M ∧ LinearIndepOn R _root_.id t
have hst : Disjoint s (sec '' t)
Tactic: have hst : Disjoint s (sec '' t) := by
    rw [Set.disjoint_iff]
    rintro _ ⟨hxs, ⟨x, hxt, rfl⟩⟩
    apply ht'.ne_zero ⟨x, hxt⟩
    rw [Subtype.coe_mk, ← hsec x, mkQ_apply, Quotient.mk_eq_zero]
    exact Submodule.subset_span hxs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ ∃ (t : Set M), s ⊆ t ∧ #(↑t : Type u) = Module.rank R M ∧ LinearIndepOn R _root_.id t
have refine_1 : #(↑(s ∪ sec '' t) : Type u) = Module.rank R M
Tactic: refine ⟨s ∪ sec '' t, subset_union_left, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
refine_1 : #(↑(s ∪ sec '' t) : Type u) = Module.rank R M
⊢ ∃ (t : Set M), s ⊆ t ∧ #(↑t : Type u) = Module.rank R M ∧ LinearIndepOn R _root_.id t
have refine_2 : LinearIndepOn R _root_.id (s ∪ sec '' t)
Tactic: refine ⟨s ∪ sec '' t, subset_union_left, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ #(↑(s ∪ sec '' t) : Type u) = Module.rank R M
have refine_1 : Injective sec
Tactic: rw [Cardinal.mk_union_of_disjoint hst, Cardinal.mk_image_eq, ht,
      ← rank_quotient_add_rank (Submodule.span R s), add_comm, rank_span_set hs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ LinearIndepOn R _root_.id (s ∪ sec '' t)
have refine_2 : LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R s))
  (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) (sec '' t)
Tactic: apply LinearIndepOn.union_id_of_quotient Submodule.subset_span hs