awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : p ≤ p ⊔ ker (M₂ := ↥f.range) f.rangeRestrict
⊢ p ≤ comap (M₂ := ↥f.range) f.rangeRestrict (Submodule.map f.rangeRestrict p)

Tactic:
rw [comap_map_eq]

Premises used: Submodule.comap_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.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
⊢ p ≤ p ⊔ ker (M₂ := ↥f.range) f.rangeRestrict

Tactic:
le_sup_left

Premises used: le_sup_left
-- 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
⊢ p ≤ p ⊔ ker (M₂ := ↥f.range) f.rangeRestrict

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- 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' : 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 ⋯
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)) ⊤
⊢ 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)

Tactic:
rw [← range_eq_top, range_mapQ]

Premises used: LinearMap.range_eq_top, Submodule.range_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' : 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 ⋯
⊢ 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:
simp
-- 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' : 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 ⋯
⊢ 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:
exact lift_rank_le_of_surjective f' <| by rw [← range_eq_top, range_mapQ]; simp

Premises used: LinearMap.lift_rank_le_of_surjective
-- 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
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
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
⊢ ∃ (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)

Premises used: HasQuotient.Quotient, exists_set_linearIndependent, Submodule.span
-- 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
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))
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
⊢ ∃ (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)

Premises used: Submodule.span, Submodule.mkQ_surjective
-- 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
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
⊢ (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id

Tactic:
have hsec' : (Submodule.mkQ _) ∘ sec = _root_.id := funext hsec
-- 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
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
rw : s ∩ sec '' t ⊆ ∅
⊢ Disjoint s (sec '' t)

Tactic:
rw [Set.disjoint_iff]

Premises used: Set.disjoint_iff
-- 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
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
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
⊢ Membership.mem (γ := Set M) ∅ (sec x)

Tactic:
apply ht'.ne_zero ⟨x, hxt⟩

Premises used: LinearIndependent.ne_zero
-- 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
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
rw : Membership.mem (γ := Submodule R M) (span R s) (sec x)
⊢ (↑(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:
rw [Subtype.coe_mk, ← hsec x, mkQ_apply, Quotient.mk_eq_zero]

Premises used: Subtype.coe_mk, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero
-- 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
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 (γ := Submodule R M) (span R s) (sec x)

Tactic:
Submodule.subset_span hxs

Premises used: Submodule.subset_span
-- 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
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 (γ := Submodule R M) (span R s) (sec x)

Tactic:
exact Submodule.subset_span hxs

Premises used: Submodule.subset_span
-- 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
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)

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
-- 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
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

Tactic:
⟨s ∪ sec '' t, subset_union_left, ?_, ?_⟩

Premises used: Set.subset_union_left, And.intro, Exists.intro, Set.image, Union.union
-- 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
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
refine_2 : LinearIndepOn R _root_.id (s ∪ sec '' t)
⊢ ∃ (t : Set M), s ⊆ t ∧ #(↑t : Type u) = Module.rank R M ∧ LinearIndepOn R _root_.id t

Tactic:
refine ⟨s ∪ sec '' t, subset_union_left, ?_, ?_⟩
-- 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
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 : Injective sec
⊢ #(↑(s ∪ sec '' t) : Type u) = Module.rank R M

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]

Premises used: rank_span_set, Submodule.rank_quotient_add_rank, Cardinal.mk_union_of_disjoint, add_comm, Cardinal.mk_image_eq, Submodule.span
-- 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
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)
⊢ Injective sec

Tactic:
HasLeftInverse.injective ⟨Submodule.Quotient.mk, hsec⟩

Premises used: Function.HasLeftInverse.injective, Submodule.Quotient.mk, Exists.intro
-- 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
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)
⊢ Injective sec

Tactic:
exact HasLeftInverse.injective ⟨Submodule.Quotient.mk, hsec⟩

Premises used: Function.HasLeftInverse.injective, Submodule.Quotient.mk, Exists.intro
-- 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
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_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)
⊢ LinearIndepOn R _root_.id (s ∪ sec '' t)

Tactic:
apply LinearIndepOn.union_id_of_quotient Submodule.subset_span hs

Premises used: LinearIndepOn.union_id_of_quotient, Submodule.subset_span
-- 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
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_2 :
  LinearIndepOn (ι := HasQuotient.Quotient M (B := Submodule R M) (span R s)) R _root_.id
    ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) '' sec '' t)
refine_2₁ :
  LinearIndepOn (ι := HasQuotient.Quotient M (B := Submodule R M) (span R s)) R _root_.id
    ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec '' t)
refine_2₂ : LinearIndepOn R _root_.id (_root_.id '' t)
refine_2₃ refine_2₄ refine_2₅ refine_2₆ : LinearIndepOn R _root_.id t
⊢ 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:
rwa [linearIndepOn_iff_image (hsec'.symm ▸ injective_id).injOn.image_of_comp,
      ← image_comp, hsec', image_id]

Premises used: Set.image_comp, linearIndepOn_iff_image, Set.image_id
-- 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
inst_4 : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
obtain :
  ∀ (t : Set M) (h₁ : Set.range v ⊆ t) (h₂ : #(↑t : Type u) = Module.rank R M) (h₃ : LinearIndepOn R _root_.id t),
    ∃ (x : M),
      LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)
⊢ ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)

Tactic:
obtain ⟨t, h₁, h₂, h₃⟩ := exists_linearIndepOn_of_lt_rank hv.linearIndepOn_id

Premises used: exists_linearIndepOn_of_lt_rank, LinearIndependent.linearIndepOn_id
-- 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
inst_4 : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
⊢ Set.range v ≠ t

Tactic:
fun e ↦ h.ne ?_

Premises used: Not, LT.lt.ne
-- 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
inst_4 : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
refine : ∀ (e : Set.range v = t), (↑n : Cardinal.{u}) = Module.rank R M
⊢ Set.range v ≠ t

Tactic:
refine fun e ↦ h.ne ?_

Premises used: LT.lt.ne
-- 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
inst_4 : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
e : Set.range v = t
⊢ lift.{u, 0} #(Fin n) = lift.{0, u} (Module.rank R M)

Tactic:
rw [← e, ← lift_injective.eq_iff, mk_range_eq_of_injective hv.injective] at h₂

Premises used: Cardinal.mk_range_eq_of_injective, Function.Injective.eq_iff, LinearIndependent.injective, Cardinal.lift_injective