awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this :
  LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
b : Basis
  (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
        (t := Set.univ) ⋯) :
    Type v)
  K V :=
  Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) this
b_eq :
  b =
    Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      this
i2 : Fintype
  (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v) :=
  ⋯.fintype (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
rw :
  Fintype.card.{v}
      (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
            (t := Set.univ) ⋯) :
        Type v) ≤
    Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v)
rw₁ :
  Fintype.card.{v}
      (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
            (t := Set.univ) ⋯) :
        Type v) ≤
    finrank.{u, v} K ↥S
rw₂ : finrank K V ≤ finrank.{u, v} K ↥S
rw₃ rw₄ : finrank K V ≤ finrank K V
⊢ Fintype.card.{v}
      (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
            (t := Set.univ) ⋯) :
        Type v) ≤
    Fintype.card.{v}
      (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v)

Tactic:
rw [Set.card_image_of_injective _ Subtype.coe_injective, ← finrank_eq_card_basis bS, ←
            finrank_eq_card_basis b, h]

Premises used: Module.finrank_eq_card_basis, Subtype.coe_injective, Set.card_image_of_injective
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this :
  LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
b : Basis
  (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
        (t := Set.univ) ⋯) :
    Type v)
  K V :=
  Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) this
b_eq :
  b =
    Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      this
i2 : Fintype
  (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v) :=
  ⋯.fintype (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
⊢ Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S) =
    this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      (t := Set.univ) ⋯

Tactic:
have : (↑) '' Basis.ofVectorSpaceIndex K S = this.extend (Set.subset_univ _) :=
    Set.eq_of_subset_of_card_le (this.subset_extend _)
      (by
        rw [Set.card_image_of_injective _ Subtype.coe_injective, ← finrank_eq_card_basis bS, ←
            finrank_eq_card_basis b, h])
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this_1 :
  LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
b : Basis
  (↑(this_1.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
        (t := Set.univ) ⋯) :
    Type v)
  K V :=
  Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
    this_1
b_eq :
  b =
    Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      this_1
i2 : Fintype
  (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v) :=
  ⋯.fintype (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
this :
  Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S) =
    this_1.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      (t := Set.univ) ⋯
rw : S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))
⊢ S = ⊤

Tactic:
rw [← b.span_eq, b_eq, Basis.coe_extend, Subtype.range_coe, ← this, ← Submodule.coe_subtype,
    span_image]

Premises used: Subtype.range_coe, Submodule.coe_subtype, Submodule.span_image, Module.Basis.span_eq, Module.Basis.coe_extend
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this_1 :
  LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
b : Basis
  (↑(this_1.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
        (t := Set.univ) ⋯) :
    Type v)
  K V :=
  Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
    this_1
b_eq :
  b =
    Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      this_1
i2 : Fintype
  (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v) :=
  ⋯.fintype (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
this :
  Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S) =
    this_1.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      (t := Set.univ) ⋯
⊢ Eq.{v + 1} (α := Submodule K ↥S)
    (span K
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v))
        (⇑bS : (a : (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v)) → ↥S)))
    ⊤

Tactic:
have := bS.span_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this_1 :
  LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
b : Basis
  (↑(this_1.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
        (t := Set.univ) ⋯) :
    Type v)
  K V :=
  Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
    this_1
b_eq :
  b =
    Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      this_1
i2 : Fintype
  (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v) :=
  ⋯.fintype (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
this_2 :
  Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S) =
    this_1.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      (t := Set.univ) ⋯
this :
  Eq.{v + 1} (α := Submodule K ↥S)
    (span K
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v))
        (⇑bS : (a : (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v)) → ↥S)))
    ⊤
⊢ Eq.{v + 1} (α := Submodule K ↥S) (span K (Basis.ofVectorSpaceIndex K ↥S)) ⊤

Tactic:
rw [bS_eq, Basis.coe_ofVectorSpace, Subtype.range_coe] at this

Premises used: Subtype.range_coe, Module.Basis.coe_ofVectorSpace
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this_1 :
  LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
b : Basis
  (↑(this_1.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
        (t := Set.univ) ⋯) :
    Type v)
  K V :=
  Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
    this_1
b_eq :
  b =
    Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      this_1
i2 : Fintype
  (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v) :=
  ⋯.fintype (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
this_2 :
  Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S) =
    this_1.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      (t := Set.univ) ⋯
this : Eq.{v + 1} (α := Submodule K ↥S) (span K (Basis.ofVectorSpaceIndex K ↥S)) ⊤
rw : S = Submodule.map S.subtype ⊤
rw₁ : S = S.subtype.range
rw₂ rw₃ : S = S
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))

Tactic:
rw [this, Submodule.map_top (Submodule.subtype S), range_subtype]

Premises used: Submodule.map_top, Submodule.subtype, Submodule.range_subtype
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W W' : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥W
f : ↥W ≃ₗ[K] ↥W'
obtain :
  ∀ (Q : Submodule K V) (hQ : IsCompl W Q),
    ∃ (g : V ≃ₗ[K] V), ∀ (x : ↥W), Eq (α := V) ((↑((f : (a : ↥W) → ↥W') x) : V) : V) ((g : (a : V) → V) (↑x : V) : V)
⊢ ∃ (g : V ≃ₗ[K] V), ∀ (x : ↥W), Eq (α := V) ((↑((f : (a : ↥W) → ↥W') x) : V) : V) ((g : (a : V) → V) (↑x : V) : V)

Tactic:
obtain ⟨Q, hQ⟩ := Submodule.exists_isCompl W

Premises used: Submodule.exists_isCompl
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W W' : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
obtain :
  ∀ (Q' : Submodule K V) (hQ' : IsCompl W' Q'),
    ∃ (g : V ≃ₗ[K] V), ∀ (x : ↥W), Eq (α := V) ((↑((f : (a : ↥W) → ↥W') x) : V) : V) ((g : (a : V) → V) (↑x : V) : V)
⊢ ∃ (g : V ≃ₗ[K] V), ∀ (x : ↥W), Eq (α := V) ((↑((f : (a : ↥W) → ↥W') x) : V) : V) ((g : (a : V) → V) (↑x : V) : V)

Tactic:
obtain ⟨Q', hQ'⟩ := Submodule.exists_isCompl W'

Premises used: Submodule.exists_isCompl
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W W' : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
this : Nonempty.{v + 1} (↥Q ≃ₗ[K] ↥Q')
⊢ ∀ (x : ↥W),
    Eq (α := V) ((↑((f : (a : ↥W) → ↥W') x) : V) : V)
      ((eQ.symm ≪≫ₗ f.prodCongr this.some ≪≫ₗ eQ' : (a : V) → V) (↑x : V) : V)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W W' : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
suffices : Nonempty.{v + 1} (↥Q ≃ₗ[K] ↥Q')
⊢ ∃ (g : V ≃ₗ[K] V), ∀ (x : ↥W), Eq (α := V) ((↑((f : (a : ↥W) → ↥W') x) : V) : V) ((g : (a : V) → V) (↑x : V) : V)

Tactic:
suffices Nonempty (Q ≃ₗ[K] Q') from
    ⟨eQ.symm ≪≫ₗ (LinearEquiv.prodCongr f this.some) ≪≫ₗ eQ', by aesop⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W W' : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Nonempty.{v + 1} (↥Q ≃ₗ[K] ↥Q')

Tactic:
LinearEquiv.nonempty_equiv_iff_rank_eq.mpr ?_

Premises used: Iff.mpr, LinearEquiv.nonempty_equiv_iff_rank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W W' : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
refine : Module.rank K ↥Q = Module.rank K ↥Q'
⊢ Nonempty.{v + 1} (↥Q ≃ₗ[K] ↥Q')

Tactic:
refine LinearEquiv.nonempty_equiv_iff_rank_eq.mpr ?_

Premises used: Iff.mpr, LinearEquiv.nonempty_equiv_iff_rank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W W' : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
rw : Module.rank K ↥W < ℵ₀
⊢ Module.rank K ↥Q = Module.rank K ↥Q'

Tactic:
rw [← Cardinal.add_right_inj_of_lt_aleph0 (γ := Module.rank K W),
    add_comm, ← rank_prod', LinearEquiv.nonempty_equiv_iff_rank_eq.mp ⟨eQ⟩,
    add_comm, LinearEquiv.nonempty_equiv_iff_rank_eq.mp ⟨f⟩,
    ← rank_prod', LinearEquiv.nonempty_equiv_iff_rank_eq.mp ⟨eQ'⟩]

Premises used: Cardinal.add_right_inj_of_lt_aleph0, Nonempty.intro, add_comm, Iff.mp, rank_prod', LinearEquiv.nonempty_equiv_iff_rank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W W' : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥W < ℵ₀

Tactic:
Module.rank_lt_aleph0 K ↥W

Premises used: Membership.mem, Subtype, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W W' : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥W < ℵ₀

Tactic:
exact Module.rank_lt_aleph0 K ↥W

Premises used: Membership.mem, Subtype, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
L : Type u_1
inst : Field L
inst_1 : LinearOrder L
inst_2 : IsStrictOrderedRing L
W : Type v
inst_3 : AddCommGroup W
inst_4 : Module L W
inst_5 : FiniteDimensional L W
t : Finset W
h : finrank L W + 1 < #t
obtain :
  ∀ (f : W → L) (sum : Eq (α := W) (∑ e ∈ t, f e • e) 0) (total : Eq.{u_1 + 1} (α := L) (∑ e ∈ t, f e) 0)
    (nonzero : ∃ x ∈ t, f x ≠ 0),
    ∃ (f : W → L), Eq (α := W) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := L) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, 0 < f x
⊢ ∃ (f : W → L), Eq (α := W) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := L) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, 0 < f x

Tactic:
obtain ⟨f, sum, total, nonzero⟩ :=
    Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card h

Premises used: Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card, Cardinal.sum
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
L : Type u_1
inst : Field L
inst_1 : LinearOrder L
inst_2 : IsStrictOrderedRing L
W : Type v
inst_3 : AddCommGroup W
inst_4 : Module L W
inst_5 : FiniteDimensional L W
t : Finset W
h : finrank L W + 1 < #t
f : W → L
sum : Eq (α := W) (∑ e ∈ t, f e • e) 0
total : Eq.{u_1 + 1} (α := L) (∑ e ∈ t, f e) 0
nonzero : ∃ x ∈ t, f x ≠ 0
⊢ ∃ (f : W → L), Eq (α := W) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := L) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, 0 < f x

Tactic:
⟨f, sum, total, exists_pos_of_sum_zero_of_exists_nonzero f total nonzero⟩

Premises used: And.intro, Exists.intro, Finset.exists_pos_of_sum_zero_of_exists_nonzero
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
L : Type u_1
inst : Field L
inst_1 : LinearOrder L
inst_2 : IsStrictOrderedRing L
W : Type v
inst_3 : AddCommGroup W
inst_4 : Module L W
inst_5 : FiniteDimensional L W
t : Finset W
h : finrank L W + 1 < #t
f : W → L
sum : Eq (α := W) (∑ e ∈ t, f e • e) 0
total : Eq.{u_1 + 1} (α := L) (∑ e ∈ t, f e) 0
nonzero : ∃ x ∈ t, f x ≠ 0
⊢ ∃ (f : W → L), Eq (α := W) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := L) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, 0 < f x

Tactic:
exact ⟨f, sum, total, exists_pos_of_sum_zero_of_exists_nonzero f total nonzero⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
ι : Type u_1
inst_5 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
⊢ ∀ (x y : V),
    Finsupp.single default
        (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) default : K)
          ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) =
      HAdd.hAdd (α := ι →₀ K)
        (Finsupp.single default
          (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) default : K)
            ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)))
        (Finsupp.single default
          (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) default : K)
            ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)))

Tactic:
simp [add_div]

Premises used: add_div
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
ι : Type u_1
inst_5 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
⊢ ∀ (m : K) (x : V),
    Finsupp.single default
        (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) (m • x) : ι →₀ K) : (a : ι) → K) default : K)
          ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) =
      HSMul.hSMul (α := K) (β := ι →₀ K) ((RingHom.id K : (a : K) → K) m : K)
        (Finsupp.single default
          (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) default : K)
            ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)))

Tactic:
simp [mul_div]

Premises used: mul_div
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
ι : Type u_1
inst_5 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
w : V
⊢ Injective (α := V) (β := ι →₀ K) (⇑b.repr : (a : V) → ι →₀ K)

Tactic:
b.repr.toEquiv.injective

Premises used: Finsupp.equivMapDomain, Module.Basis.repr, LinearEquiv.toEquiv, Equiv.injective
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
ι : Type u_1
inst_5 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
w : V
apply_fun :
  Eq (α := ι →₀ K)
    ((b.repr : (a : V) → ι →₀ K)
        ((fun (f : ι →₀ K) ↦ HSMul.hSMul.{u, v, v} (α := K) ((f : (a : ι) → K) default : K) v)
          ((fun (w : V) ↦
              (Finsupp.single default
                  (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
                    ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
                ι →₀ K))
            w)) :
      ι →₀ K)
    ((b.repr : (a : V) → ι →₀ K) w : ι →₀ K)
⊢ (fun (f : ι →₀ K) ↦ HSMul.hSMul.{u, v, v} (α := K) ((f : (a : ι) → K) default : K) v)
      ((fun (w : V) ↦
          (Finsupp.single default
              (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
                ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
            ι →₀ K))
        w) =
    w

Tactic:
apply_fun b.repr using b.repr.toEquiv.injective

Premises used: Module.Basis.repr, LinearEquiv.toEquiv, Equiv.injective