awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ 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)
have rw₃ : finrank K V ≤ finrank K V
Tactic: rw [Set.card_image_of_injective _ Subtype.coe_injective, ← finrank_eq_card_basis bS, ←
            finrank_eq_card_basis b, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
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))
⊢ S = ⊤
have this₁ : 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) sorry
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])
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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) ⋯
⊢ S = ⊤
have rw : S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))
Tactic: rw [← b.span_eq, b_eq, Basis.coe_extend, Subtype.range_coe, ← this, ← Submodule.coe_subtype,
    span_image]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
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) ⋯
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))
have 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)))
  ⊤
Tactic: have := bS.span_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
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)))
    ⊤
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))
have this₁ : Eq.{v + 1} (α := Submodule K ↥S) (span K (Basis.ofVectorSpaceIndex K ↥S)) ⊤
Tactic: rw [bS_eq, Basis.coe_ofVectorSpace, Subtype.range_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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)) ⊤
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))
have rw : S = Submodule.map S.subtype ⊤
Tactic: rw [this, Submodule.map_top (Submodule.subtype S), range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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 ⊤
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))
have rw₁ : S = S.subtype.range
Tactic: rw [this, Submodule.map_top (Submodule.subtype S), range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))
have rw₂ : S = S
Tactic: rw [this, Submodule.map_top (Submodule.subtype S), range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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'
⊢ ∃ (g : V ≃ₗ[K] V), ∀ (x : ↥W), Eq (α := V) ((↑((f : (a : ↥W) → ↥W') x) : V) : V) ((g : (a : V) → V) (↑x : V) : V)
have 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)
Tactic: obtain ⟨Q, hQ⟩ := Submodule.exists_isCompl W
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ ∃ (g : V ≃ₗ[K] V), ∀ (x : ↥W), Eq (α := V) ((↑((f : (a : ↥W) → ↥W') x) : V) : V) ((g : (a : V) → V) (↑x : V) : V)
have 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)
Tactic: obtain ⟨Q', hQ'⟩ := Submodule.exists_isCompl W'
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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'
⊢ ∃ (g : V ≃ₗ[K] V), ∀ (x : ↥W), Eq (α := V) ((↑((f : (a : ↥W) → ↥W') x) : V) : V) ((g : (a : V) → V) (↑x : V) : V)
have suffices : Nonempty.{v + 1} (↥Q ≃ₗ[K] ↥Q')
Tactic: suffices Nonempty (Q ≃ₗ[K] Q') from
    ⟨eQ.symm ≪≫ₗ (LinearEquiv.prodCongr f this.some) ≪≫ₗ eQ', by aesop⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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')
have refine : Module.rank K ↥Q = Module.rank K ↥Q'
Tactic: refine LinearEquiv.nonempty_equiv_iff_rank_eq.mpr ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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 ↥Q = Module.rank K ↥Q'
have rw : Module.rank K ↥W < ℵ₀
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'⟩]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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), Eq (α := W) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := L) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, 0 < f x
have 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
Tactic: obtain ⟨f, sum, total, nonzero⟩ :=
    Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ (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
have 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)
Tactic: apply_fun b.repr using b.repr.toEquiv.injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ 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)
have apply_fun : Eq.{u + 1} (α := K)
  ((Finsupp.uniqueEquiv default : (a : ι →₀ K) → 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)
  ((Finsupp.uniqueEquiv default : (a : ι →₀ K) → K) ((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : K)
Tactic: apply_fun Finsupp.uniqueEquiv default
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ Eq.{u + 1} (α := K)
    ((Finsupp.uniqueEquiv default : (a : ι →₀ K) → 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)
    ((Finsupp.uniqueEquiv default : (a : ι →₀ K) → K) ((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : K)
have simp : HMul.hMul (α := K) (β := K)
    ((RingHom.id K : (a : K) → K)
        (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)
    ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) =
  (((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default
Tactic: simp only [map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same,
          smul_eq_mul, Pi.smul_apply, Finsupp.uniqueEquiv_apply]