awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Nontrivial R
ι : Type u_2
inst_5 : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = #(↑(range b) : Type v)
⊢ Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
have rwa : ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{u_2, v} #(↑(range b) : Type v)),
  Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
Tactic: rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
        lift_eq_nat_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Nontrivial R
ι : Type u_2
inst_5 : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = #(↑(range b) : Type v)
rwa :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{u_2, v} #(↑(range b) : Type v)),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
⊢ Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
have rwa₁ : ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{v, u_2} #ι),
  Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
Tactic: rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
        lift_eq_nat_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Nontrivial R
ι : Type u_2
inst_5 : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = #(↑(range b) : Type v)
rwa :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{u_2, v} #(↑(range b) : Type v)),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
rwa₁ :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{v, u_2} #ι),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
⊢ Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
have rwa₂ : ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{v, u_2} (↑(Fintype.card ι) : Cardinal.{u_2})),
  Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
Tactic: rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
        lift_eq_nat_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Nontrivial R
ι : Type u_2
inst_5 : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = #(↑(range b) : Type v)
rwa :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{u_2, v} #(↑(range b) : Type v)),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
rwa₁ :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{v, u_2} #ι),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
rwa₂ :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{v, u_2} (↑(Fintype.card ι) : Cardinal.{u_2})),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
⊢ Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
have rwa₃ : ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = (↑(Fintype.card ι) : Cardinal.{max u_2 v})),
  Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
Tactic: rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
        lift_eq_nat_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Nontrivial R
ι : Type u_2
inst_5 : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = #(↑(range b) : Type v)
rwa :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{u_2, v} #(↑(range b) : Type v)),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
rwa₁ :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{v, u_2} #ι),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
rwa₂ :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{v, u_2} (↑(Fintype.card ι) : Cardinal.{u_2})),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
rwa₃ :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = (↑(Fintype.card ι) : Cardinal.{max u_2 v})),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
⊢ Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
have rwa₄ : ∀ (this : Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})),
  Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
Tactic: rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
        lift_eq_nat_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
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
⊢ Module.rank R ↥(span R s) = (↑s.toFinset.card : Cardinal.{v})
have this : Module.rank R ↥(span R s) = #(↑s : Type v)
Tactic: have : Module.rank R (span R s) = #s := rank_span_set hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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)
⊢ Module.rank R ↥(span R s) = (↑s.toFinset.card : Cardinal.{v})
have 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})
Tactic: rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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})
⊢ Module.rank R ↥(span R s) = (↑s.toFinset.card : Cardinal.{v})
have rwa₁ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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.card
have h : s = (↑s : Set M).toFinset
Tactic: convert! finrank_span_set_eq_card (s := (s : Set M)) hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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)
⊢ s = (↑s : Set M).toFinset
have h : ∀ (a : M), a ∈ s ↔ a ∈ (↑s : Set M).toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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 R M ≤ Fintype.card ι
have rw : finrank.{u, v} R ↥(span R (range v)) ≤ Fintype.card ι
Tactic: rw [← finrank_top, ← hv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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)) ⊤
⊢ (range v).toFinset.card ≤ Fintype.card ι
have h : (range v).toFinset.card = Fintype.card.{v} (↑(range v) : Type v)
Tactic: convert! Fintype.card_range_le v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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)) ⊤
⊢ (range v).toFinset.card = Fintype.card.{v} (↑(range v) : Type v)
have h : Fintype.card.{v} (↑(range v) : Type v) = Fintype.card.{v} (↑(range v) : Type v)
Tactic: rw [Set.toFinset_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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 R M ≤ Fintype.card ι
have rw : finrank.{u, v} R ↥⊤ ≤ 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])
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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 ι
⊢ finrank R M ≤ Fintype.card ι
have rw₁ : finrank.{u, v} R ↥(span R (range v)) ≤ 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])
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
ι : Type w
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Finite ι
inst_3 : Nontrivial R
s : Set ι
⊢ finrank R ↥(spanSubset R s) = s.ncard
have have : ∀ (this : Fintype ι), finrank R ↥(spanSubset R s) = s.ncard
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
ι : Type w
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Finite ι
inst_3 : Nontrivial R
s : Set ι
this : Fintype ι
⊢ finrank R ↥(spanSubset R s) = s.ncard
have rw : ncard (α := ι → R) ((⇑(basisFun R ι) : (a : ι) → ι → 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
ι : Type w
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Finite ι
inst_3 : Nontrivial R
s : Set ι
⊢ finrank R ↥(spanSubset R s) = s.ncard
have have : ∀ (this : Fintype ι), 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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
⊢ finrank R ↥(spanSubset R s) = s.ncard
have have₃ : ∀ (this : Fintype ι), ncard (α := ι → R) ((⇑(basisFun R ι) : (a : ι) → ι → 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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
have rw : Module.rank F ↥⊤ = Module.rank F E
Tactic: rw [subalgebra_top_rank_eq_submodule_top_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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 ↥((toSubmodule : (a : Subalgebra F E) → Submodule F E) ⊥ : Submodule F E) = 1
have rw : LinearIndepOn (ι := E) F id {1}
Tactic: rw [Algebra.toSubmodule_bot, one_eq_span, rank_span_set, mk_singleton _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
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
⊢ LinearIndepOn (ι := E) F id {1}
have this : Nontrivial F
Tactic: have := Module.nontrivial F E
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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)
have 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)
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
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))
⊢ Basis (m ⊕ n) R V
have br : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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)
⊢ Basis (m ⊕ n) R V
have hli : LinearIndependent R b
Tactic: apply Basis.mk (v := b)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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
⊢ Basis (m ⊕ n) R V
have hsp : LE.le (α := Submodule R V) ⊤ (span R (range b))
Tactic: apply Basis.mk (v := b)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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 R b
have hli : LinearIndependent.{u_4, u_2, u_3} (ι := m) R (M := ↥W) (⇑bW : (a : m) → ↥W)
Tactic: apply LinearIndependent.sumElim_of_quotient
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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)
⊢ LinearIndependent R b
have hli₁ : LinearIndependent.{u_5, u_2, u_3} (ι := n) R (M := V ⧸ W) (Submodule.Quotient.mk ∘ surjInv sorry ∘ (⇑bQ : (a : n) → V ⧸ W))
Tactic: apply LinearIndependent.sumElim_of_quotient
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
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)
⊢ 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)))))
have hsp : Eq (α := Submodule R (V ⧸ W))
  (span R (range.{u_3, u_5 + 1} (ι := n) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ surjInv sorry ∘ (⇑bQ : (a : n) → V ⧸ W))))
  (span R (range.{u_3, u_5 + 1} (ι := n) (⇑bQ : (a : n) → V ⧸ W)))
Tactic: rw [Set.Sum.elim_range, Submodule.span_union,
      show Set.range (fun i ↦ (bW i : V)) = W.subtype '' (Set.range (fun i ↦ bW i)) by aesop,
      ← Submodule.map_span, bW.span_eq, Submodule.map_top, Submodule.range_subtype, top_le_iff,
      ← Submodule.map_mkQ_eq_top, Submodule.map_span, ← Set.range_comp, ← bQ.span_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : 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)
i : m
⊢ Eq (α := m ⊕ n →₀ R) (((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) (↑((bW : (a : m) → ↥W) i) : V))
    (Finsupp.single (Sum.inl i) 1)
have rw : Eq.{u_3 + 1} (α := V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inl i) : V) ((↑((bW : (a : m) → ↥W) i) : V) : V)
Tactic: rw [← Module.Basis.apply_eq_iff, sumQuot_inl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : 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)
i : m
rw : Eq.{u_3 + 1} (α := V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inl i) : V) ((↑((bW : (a : m) → ↥W) i) : V) : V)
⊢ Eq (α := m ⊕ n →₀ R) (((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) (↑((bW : (a : m) → ↥W) i) : V))
    (Finsupp.single (Sum.inl i) 1)
have rw₁ : Eq.{u_3 + 1} (α := V) (↑((bW : (a : m) → ↥W) i) : V) (↑((bW : (a : m) → ↥W) i) : V)
Tactic: rw [← Module.Basis.apply_eq_iff, sumQuot_inl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : 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)
w : ↥W
i : m
⊢ Eq.{u_2 + 1} (α := R)
    (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) (↑w : V) : m ⊕ n →₀ R) : (a : m ⊕ n) → R) (Sum.inl i) : R)
    ((((bW.repr : (a : ↥W) → m →₀ R) w : m →₀ R) : (a : m) → R) i : R)
have refine_1 : ∀ (x y : ↥W),
  (fun (w : ↥W) (i : m) ↦
        (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) : (a : m ⊕ n) → R)
            (Sum.inl i) :
          R))
      (x + y) =
    HAdd.hAdd (α := m → R)
      ((fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        x)
      ((fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        y)
Tactic: refine Eq.symm <| (bW.repr_apply_eq
      (fun w i => (sumQuot bW bQ).repr (W.subtype w) (Sum.inl i)) ?_ ?_ ?_ w i)