awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Set M
inst_4 : Fintype (↑s : Type v)
hs : LinearIndepOn R id s
this : Module.rank R ↥(span R s) = #(↑s : Type v)
rwa :
  ∀ (this : Module.rank R ↥(span R s) = (↑(Fintype.card.{v} (↑s : Type v)) : Cardinal.{v})),
    Module.rank R ↥(span R s) = (↑s.toFinset.card : Cardinal.{v})
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Module.rank R ↥(span R s) = (↑s.toFinset.card : Cardinal.{v})),
    Module.rank R ↥(span R s) = (↑s.toFinset.card : Cardinal.{v})
⊢ Module.rank R ↥(span R s) = (↑s.toFinset.card : Cardinal.{v})

Tactic:
rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this

Premises used: Set.toFinset_card, Cardinal.mk_fintype
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Finset M
hs : LinearIndepOn R id (↑s : Set M)
⊢ finrank.{u, v} R ↥(span R (↑s : Set M)) = (↑s : Set M).toFinset.card

Tactic:
finrank_span_set_eq_card (s := (s : Set M)) hs

Premises used: finrank_span_set_eq_card
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Finset M
hs : LinearIndepOn R id (↑s : Set M)
h : s = (↑s : Set M).toFinset
⊢ finrank.{u, v} R ↥(span R (↑s : Set M)) = s.card

Tactic:
convert! finrank_span_set_eq_card (s := (s : Set M)) hs

Premises used: finrank_span_set_eq_card
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Finset M
hs : LinearIndepOn R id (↑s : Set M)
h : ∀ (a : M), a ∈ s ↔ a ∈ (↑s : Set M).toFinset
⊢ s = (↑s : Set M).toFinset

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Finset M
hs : LinearIndepOn R id (↑s : Set M)
a : M
⊢ a ∈ s ↔ a ∈ (↑s : Set M).toFinset

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Set M
inst_4 : Fintype (↑s : Type v)
t : Submodule R M
subset : s ⊆ (↑t : Set M)
card_lt : s.toFinset.card < finrank.{u, v} R ↥t
⊢ span R s < t

Tactic:
lt_of_le_of_finrank_lt_finrank (span_le.mpr subset)
    (lt_of_le_of_lt (finrank_span_le_card _) card_lt)

Premises used: Iff.mpr, lt_of_le_of_lt, finrank_span_le_card, Submodule.lt_of_le_of_finrank_lt_finrank, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Set M
inst_4 : Fintype (↑s : Type v)
card_lt : s.toFinset.card < finrank R M
⊢ LT.lt (α := Submodule R M) (span R s) ⊤

Tactic:
lt_top_of_finrank_lt_finrank (lt_of_le_of_lt (finrank_span_le_card _) card_lt)

Premises used: lt_of_le_of_lt, finrank_span_le_card, Submodule.lt_top_of_finrank_lt_finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
rw : finrank.{u, v} R ↥(span R (range v)) ≤ Fintype.card ι
⊢ finrank R M ≤ Fintype.card ι

Tactic:
rw [← finrank_top, ← hv]

Premises used: finrank_top
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
⊢ Fintype.card.{v} (↑(range v) : Type v) ≤ Fintype.card ι

Tactic:
Fintype.card_range_le v

Premises used: Fintype.card_range_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
h : (range v).toFinset.card = Fintype.card.{v} (↑(range v) : Type v)
⊢ (range v).toFinset.card ≤ Fintype.card ι

Tactic:
convert! Fintype.card_range_le v

Premises used: Fintype.card_range_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
h h₁ : Fintype.card.{v} (↑(range v) : Type v) = Fintype.card.{v} (↑(range v) : Type v)
⊢ (range v).toFinset.card = Fintype.card.{v} (↑(range v) : Type v)

Tactic:
rw [Set.toFinset_card]

Premises used: Set.toFinset_card
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
⊢ finrank.{u, v} R ↥(span R (range v)) ≤ Fintype.card ι

Tactic:
exact (finrank_span_le_card _).trans (by convert! Fintype.card_range_le v; rw [Set.toFinset_card])

Premises used: finrank_span_le_card, LE.le.trans
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
rw : finrank.{u, v} R ↥⊤ ≤ Fintype.card ι
rw₁ rw₂ rw₃ : finrank.{u, v} R ↥(span R (range v)) ≤ Fintype.card ι
⊢ finrank R M ≤ Fintype.card ι

Tactic:
classical
  rw [← finrank_top, ← hv]
  exact (finrank_span_le_card _).trans (by convert! Fintype.card_range_le v; rw [Set.toFinset_card])

Premises used: finrank_span_le_card, finrank_top, LE.le.trans
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
ι : Type w
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Finite ι
inst_3 : Nontrivial R
s : Set ι
have : ∀ (this : Fintype ι), finrank R ↥(spanSubset R s) = s.ncard
⊢ finrank R ↥(spanSubset R s) = s.ncard

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
ι : Type w
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Finite ι
inst_3 : Nontrivial R
s : Set ι
this : Fintype ι
rw : ncard (α := ι → R) ((⇑(basisFun R ι) : (a : ι) → ι → R) '' s) = s.ncard
⊢ finrank R ↥(spanSubset R s) = s.ncard

Tactic:
rw [Pi.spanSubset, finrank_span_set_eq_card <| (Pi.basisFun R ι).linearIndepOn _ |>.id_image,
    Set.toFinset_card, Fintype.card_eq_nat_card, Nat.card_coe_set_eq]

Premises used: finrank_span_set_eq_card, Nat.card_coe_set_eq, Module.Basis.linearIndepOn, Set.toFinset_card, Pi.basisFun, LinearIndepOn.id_image, Pi.spanSubset, Fintype.card_eq_nat_card
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
ι : Type w
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Finite ι
inst_3 : Nontrivial R
s : Set ι
this : Fintype ι
⊢ ncard (α := ι → R) ((⇑(basisFun R ι) : (a : ι) → ι → R) '' s) = s.ncard

Tactic:
Set.ncard_image_of_injective s <| (Pi.basisFun R ι).injective

Premises used: Module.Basis.injective, Set.ncard_image_of_injective, Pi.basisFun
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
ι : Type w
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Finite ι
inst_3 : Nontrivial R
s : Set ι
this : Fintype ι
⊢ ncard (α := ι → R) ((⇑(basisFun R ι) : (a : ι) → ι → R) '' s) = s.ncard

Tactic:
exact Set.ncard_image_of_injective s <| (Pi.basisFun R ι).injective

Premises used: Module.Basis.injective, Set.ncard_image_of_injective, Pi.basisFun
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
ι : Type w
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Finite ι
inst_3 : Nontrivial R
s : Set ι
have have₁ have₂ : ∀ (this : Fintype ι), finrank R ↥(spanSubset R s) = s.ncard
have₃ : ∀ (this : Fintype ι), ncard (α := ι → R) ((⇑(basisFun R ι) : (a : ι) → ι → R) '' s) = s.ncard
⊢ finrank R ↥(spanSubset R s) = s.ncard

Tactic:
classical
  have := Fintype.ofFinite ι
  rw [Pi.spanSubset, finrank_span_set_eq_card <| (Pi.basisFun R ι).linearIndepOn _ |>.id_image,
    Set.toFinset_card, Fintype.card_eq_nat_card, Nat.card_coe_set_eq]
  exact Set.ncard_image_of_injective s <| (Pi.basisFun R ι).injective

Premises used: finrank_span_set_eq_card, Nat.card_coe_set_eq, Module.Basis.injective, Module.Basis.linearIndepOn, Set.toFinset_card, Set.ncard_image_of_injective, Pi.basisFun, LinearIndepOn.id_image, Pi.spanSubset, Fintype.card_eq_nat_card
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
S : Subalgebra F E
⊢ Module.rank F ↥((toSubmodule : (a : Subalgebra F E) → Submodule F E) S : Submodule F E) = Module.rank F ↥S

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
S : Subalgebra F E
⊢ finrank.{u_2, u_3} F ↥((toSubmodule : (a : Subalgebra F E) → Submodule F E) S : Submodule F E) =
    finrank.{u_2, u_3} F ↥S

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F ↥((Subalgebra.toSubmodule : (a : Subalgebra F E) → Submodule F E) ⊤ : Submodule F E)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
⊢ finrank.{u_2, u_3} F ↥⊤ =
    finrank.{u_2, u_3} F ↥((Subalgebra.toSubmodule : (a : Subalgebra F E) → Submodule F E) ⊤ : Submodule F E)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
rw : Module.rank F ↥⊤ = Module.rank F E
⊢ Module.rank F ↥⊤ = Module.rank F E

Tactic:
rw [subalgebra_top_rank_eq_submodule_top_rank]

Premises used: subalgebra_top_rank_eq_submodule_top_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F E

Tactic:
_root_.rank_top F E

Premises used: rank_top
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F E

Tactic:
exact _root_.rank_top F E

Premises used: rank_top
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommRing F
inst_1 : IsDomain F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : StrongRankCondition F
inst_5 : IsTorsionFree F E
inst_6 : Nontrivial E
rw : LinearIndepOn (ι := E) F id {1}
⊢ Module.rank F ↥((toSubmodule : (a : Subalgebra F E) → Submodule F E) ⊥ : Submodule F E) = 1

Tactic:
rw [Algebra.toSubmodule_bot, one_eq_span, rank_span_set, mk_singleton _]

Premises used: rank_span_set, Algebra.toSubmodule_bot, Cardinal.mk_singleton, Submodule.one_eq_span
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommRing F
inst_1 : IsDomain F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : StrongRankCondition F
inst_5 : IsTorsionFree F E
inst_6 : Nontrivial E
⊢ Nontrivial F

Tactic:
have := Module.nontrivial F E
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommRing F
inst_1 : IsDomain F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : StrongRankCondition F
inst_5 : IsTorsionFree F E
inst_6 : Nontrivial E
this : Nontrivial F
⊢ LinearIndepOn (ι := E) F id {1}

Tactic:
.singleton one_ne_zero

Premises used: LinearIndepOn.singleton, one_ne_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommRing F
inst_1 : IsDomain F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : StrongRankCondition F
inst_5 : IsTorsionFree F E
inst_6 : Nontrivial E
this : Nontrivial F
⊢ LinearIndepOn (ι := E) F id {1}

Tactic:
exact .singleton one_ne_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
F : Type u_2
E : Type u_3
inst : CommRing F
inst_1 : IsDomain F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : StrongRankCondition F
inst_5 : IsTorsionFree F E
inst_6 : Nontrivial E
⊢ Module.rank F ↥⊥ = (↑1 : Cardinal.{u_3})

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
h : ∀ (j : n), Eq (α := V ⧸ W) (((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) j : V ⧸ W) ((bQ : (a : n) → V ⧸ W) j : V ⧸ W)
⊢ Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
j : n
⊢ Eq (α := V ⧸ W) (((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) j : V ⧸ W) ((bQ : (a : n) → V ⧸ W) j : V ⧸ W)

Tactic:
apply Function.rightInverse_surjInv W.mkQ_surjective

Premises used: Function.rightInverse_surjInv, Submodule.mkQ_surjective
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
⊢ Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)

Tactic:
have br : W.mkQ ∘ b ∘ Sum.inr = bQ := by
    ext j
    apply Function.rightInverse_surjInv W.mkQ_surjective
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
br : Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)
hli : LinearIndependent R b
hsp : LE.le (α := Submodule R V) ⊤ (span R (range b))
⊢ Basis (m ⊕ n) R V

Tactic:
apply Basis.mk (v := b)

Premises used: Module.Basis.mk
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
br : Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)
hli : LinearIndependent.{u_4, u_2, u_3} (ι := m) R (M := ↥W) (⇑bW : (a : m) → ↥W)
hli₁ :
  LinearIndependent.{u_5, u_2, u_3} (ι := n) R (M := V ⧸ W)
    (Submodule.Quotient.mk ∘ surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
⊢ LinearIndependent R b

Tactic:
apply LinearIndependent.sumElim_of_quotient

Premises used: LinearIndependent.sumElim_of_quotient
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
br : Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)
⊢ LinearIndependent.{u_4, u_2, u_3} (ι := m) R (M := ↥W) (⇑bW : (a : m) → ↥W)

Tactic:
bW.linearIndependent

Premises used: Set.Mem, Module.Basis.linearIndependent
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
br : Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)
⊢ LinearIndependent.{u_4, u_2, u_3} (ι := m) R (M := ↥W) (⇑bW : (a : m) → ↥W)

Tactic:
exact bW.linearIndependent

Premises used: Module.Basis.linearIndependent
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
br : Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)
⊢ LinearIndependent.{u_5, u_2, u_3} (ι := n) R (M := V ⧸ W) (⇑bQ : (a : n) → V ⧸ W)

Tactic:
bQ.linearIndependent

Premises used: Module.Basis.linearIndependent
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
br : Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)
⊢ LinearIndependent.{u_5, u_2, u_3} (ι := n) R (M := V ⧸ W)
    (Submodule.Quotient.mk ∘ surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))

Tactic:
convert! bQ.linearIndependent

Premises used: Module.Basis.linearIndependent
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
br : Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)
hsp :
  LE.le (α := Submodule R V) ⊤
    (span R
      (range (ι := m ⊕ n)
        (Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W)))))
⊢ LE.le (α := Submodule R V) ⊤ (span R (range b))

Tactic:
unfold b
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
br : Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)
⊢ Eq (α := Set V) (range fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V))
    (image (α := ↥W) (⇑W.subtype : (a : ↥W) → V) (range fun (i : m) ↦ (bW : (a : m) → ↥W) i))

Tactic:
aesop