awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
h : ¬T = ⊥
right : ∀ (h : ∃ x ∈ T, x ≠ 0), v ∈ T
⊢ K ∙ v ≤ T

Tactic:
simp_rw [span_singleton_le_iff_mem, ← Ne.eq_def, Submodule.ne_bot_iff] at *

Premises used: Ne.eq_def, Submodule.ne_bot_iff, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
h : ∃ x ∈ T, x ≠ 0
right : ∀ (s : V) (hs : s ∈ T) (hz : s ≠ 0), v ∈ T
⊢ v ∈ T

Tactic:
rcases h with ⟨s, ⟨hs, hz⟩⟩
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
s : V
hs : s ∈ T
hz : s ≠ 0
right : ∀ (a : K) (hs : a • v ∈ T) (hz : a • v ≠ 0), v ∈ T
⊢ v ∈ T

Tactic:
rcases mem_span_singleton.1 (hT.1 hs) with ⟨a, rfl⟩

Premises used: Submodule.mem_span_singleton, And.left, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
right : ∀ (hs : HSMul.hSMul.{u_3, u_4, u_4} (α := K) 0 v ∈ T) (hz : HSMul.hSMul.{u_3, u_4, u_4} (α := K) 0 v ≠ 0), v ∈ T
right₁ : ∀ (h : a ≠ 0), v ∈ T
⊢ v ∈ T

Tactic:
rcases eq_or_ne a 0 with rfl | h

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
hs : HSMul.hSMul.{u_3, u_4, u_4} (α := K) 0 v ∈ T
hz : HSMul.hSMul.{u_3, u_4, u_4} (α := K) 0 v ≠ 0
⊢ v ∈ T

Tactic:
simp only [zero_smul, ne_eq, not_true] at hz

Premises used: ne_eq, zero_smul, not_true
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
h : a ≠ 0
right right₁ right₂ right₃ : ∀ (hs : v ∈ T) (hz : a • v ≠ 0) (h : a ≠ 0), v ∈ T
⊢ v ∈ T

Tactic:
rwa [T.smul_mem_iff h] at hs

Premises used: Submodule.smul_mem_iff
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
⊢ IsAtom W ↔ ∃ (v : V), v ≠ 0 ∧ W = K ∙ v

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
refine_1 : ∀ (h : IsAtom W), ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
refine_2 : ∀ (h : ∃ (v : V), v ≠ 0 ∧ W = K ∙ v), IsAtom W
⊢ IsAtom W ↔ ∃ (v : V), v ≠ 0 ∧ W = K ∙ v

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
h : IsAtom W
⊢ W ≠ ⊥

Tactic:
obtain ⟨hbot, h⟩ := h
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
h : IsAtom W
hbot : W ≠ ⊥
⊢ ∀ b < W, b = ⊥

Tactic:
obtain ⟨hbot, h⟩ := h
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
refine_1 : ∀ (v : V) (hW : v ∈ W) (hv : v ≠ 0), ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
⊢ ∃ (v : V), v ≠ 0 ∧ W = K ∙ v

Tactic:
rcases (Submodule.ne_bot_iff W).1 hbot with ⟨v, ⟨hW, hv⟩⟩

Premises used: Submodule.ne_bot_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ ∃ (v : V), v ≠ 0 ∧ W = K ∙ v

Tactic:
⟨v, ⟨hv, ?_⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
refine_1 : W = K ∙ v
⊢ ∃ (v : V), v ≠ 0 ∧ W = K ∙ v

Tactic:
refine ⟨v, ⟨hv, ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
refine_1 : ∀ (heq : ¬W = K ∙ v), False
⊢ W = K ∙ v

Tactic:
by_contra heq
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
⊢ K ∙ v < W → Eq (α := Submodule K V) (K ∙ v) ⊥

Tactic:
specialize h (span K {v})

Premises used: Submodule.span, Singleton.singleton
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
h : K ∙ v < W → Eq (α := Submodule K V) (K ∙ v) ⊥
⊢ K ∙ v ≤ W ∧ K ∙ v ≠ W → v = 0

Tactic:
rw [span_singleton_eq_bot, lt_iff_le_and_ne] at h

Premises used: lt_iff_le_and_ne, Submodule.span_singleton_eq_bot
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
h : K ∙ v ≤ W ∧ K ∙ v ≠ W → v = 0
⊢ False

Tactic:
hv (h ⟨(span_singleton_le_iff_mem v W).2 hW, Ne.symm heq⟩)

Premises used: Iff.mpr, Ne.symm, And.intro, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
h : K ∙ v ≤ W ∧ K ∙ v ≠ W → v = 0
⊢ False

Tactic:
exact hv (h ⟨(span_singleton_le_iff_mem v W).2 hW, Ne.symm heq⟩)

Premises used: Iff.mpr, Ne.symm, And.intro, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
h : ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
refine_2 : ∀ (v : V) (hv : v ≠ 0), IsAtom (α := Submodule K V) (K ∙ v)
⊢ IsAtom W

Tactic:
rcases h with ⟨v, ⟨hv, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ IsAtom (α := Submodule K V) (K ∙ v)

Tactic:
nonzero_span_atom v hv

Premises used: nonzero_span_atom
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ IsAtom (α := Submodule K V) (K ∙ v)

Tactic:
exact nonzero_span_atom v hv

Premises used: nonzero_span_atom
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
⊢ ∃ (s : Set (Submodule K V)), W = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
⟨_, submodule_eq_sSup_le_nonzero_spans W, ?_⟩

Premises used: Submodule.submodule_eq_sSup_le_nonzero_spans, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
refine :
  ∀ (a : Submodule K V),
    Membership.mem (γ := Set (Submodule K V)) {T : Submodule K V | ∃ m ∈ W, m ≠ 0 ∧ T = K ∙ m} a → IsAtom a
⊢ ∃ (s : Set (Submodule K V)), W = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
refine ⟨_, submodule_eq_sSup_le_nonzero_spans W, ?_⟩
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
w : V
left : w ∈ W
hw : w ≠ 0
⊢ IsAtom (α := Submodule K V) (K ∙ w)

Tactic:
nonzero_span_atom w hw

Premises used: nonzero_span_atom
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
w : V
left : w ∈ W
hw : w ≠ 0
⊢ IsAtom (α := Submodule K V) (K ∙ w)

Tactic:
exact nonzero_span_atom w hw

Premises used: nonzero_span_atom
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
⊢ LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))

Tactic:
have hB₀ : _ := hB.linearIndependent.linearIndepOn_id
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
⊢ Disjoint
    (span K
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
        (⇑(Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V)))
    f.ker

Tactic:
simp [hf_inj]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
⊢ LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id
    (image.{u_4, u_5} (α := V) (⇑f : (a : V) → V')
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
        (⇑(Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V)))

Tactic:
have h₁ : LinearIndepOn K _root_.id (f '' Set.range (Basis.ofVectorSpace K V)) :=
      LinearIndepOn.image (f := f) hB₀ (show Disjoint _ _ by simp [hf_inj])
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
h₁ :
  LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id
    (image.{u_4, u_5} (α := V) (⇑f : (a : V) → V')
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
        (⇑(Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V)))
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h₁ : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' Basis.ofVectorSpaceIndex K V)),
    LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
⊢ LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)

Tactic:
rwa [Basis.range_ofVectorSpace K V] at h₁

Premises used: Module.Basis.range_ofVectorSpace
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
⊢ LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)

Tactic:
have : LinearIndepOn K _root_.id (f '' B) := by
    have h₁ : LinearIndepOn K _root_.id (f '' Set.range (Basis.ofVectorSpace K V)) :=
      LinearIndepOn.image (f := f) hB₀ (show Disjoint _ _ by simp [hf_inj])
    rwa [Basis.range_ofVectorSpace K V] at h₁
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
this : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
C : Set V' := this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
⊢ (⇑f : (a : V) → V') '' B ⊆ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯

Tactic:
have BC := this.subset_extend (subset_univ _)
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
this : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
C : Set V' := this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
BC : (⇑f : (a : V) → V') '' B ⊆ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
hC : Basis (↑(this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯) : Type u_5) K V' :=
  Basis.extend (s := (⇑f : (a : V) → V') '' B) this
haveI : ∀ (Vinh : Inhabited V), ∃ (g : V' →ₗ[K] V), g ∘ₗ f = id
⊢ ∃ (g : V' →ₗ[K] V), g ∘ₗ f = id

Tactic:
haveI Vinh : Inhabited V := ⟨0⟩
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
this : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
C : Set V' := this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
BC : (⇑f : (a : V) → V') '' B ⊆ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
hC : Basis (↑(this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯) : Type u_5) K V' :=
  Basis.extend (s := (⇑f : (a : V) → V') '' B) this
Vinh : Inhabited V
⊢ ∃ (g : V' →ₗ[K] V), g ∘ₗ f = id

Tactic:
⟨(hC.constr ℕ : _ → _) (C.restrict (invFun f)), hB.ext fun b => ?_⟩

Premises used: Function.invFun, Nat, Exists.intro, Set.restrict, DFunLike.coe, Module.Basis.ext, Module.Basis.constr
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
this : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
C : Set V' := this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
BC : (⇑f : (a : V) → V') '' B ⊆ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
hC : Basis (↑(this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯) : Type u_5) K V' :=
  Basis.extend (s := (⇑f : (a : V) → V') '' B) this
Vinh : Inhabited V
refine :
  ∀ (b : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)),
    Eq (α := V)
      (((hC.constr ℕ : (a : (↑(this.extend ⋯) : Type u_5) → V) → V' →ₗ[K] V)
                (C.restrict (π := fun (a : V') ↦ V) (invFun (⇑f : (a : V) → V'))) ∘ₗ
              f :
            (a : V) → V)
          ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V) :
        V)
      ((id : (a : V) → V) ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V) : V)
⊢ ∃ (g : V' →ₗ[K] V), g ∘ₗ f = id

Tactic:
refine ⟨(hC.constr ℕ : _ → _) (C.restrict (invFun f)), hB.ext fun b => ?_⟩
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
this : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
C : Set V' := this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
BC : (⇑f : (a : V) → V') '' B ⊆ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
hC : Basis (↑(this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯) : Type u_5) K V' :=
  Basis.extend (s := (⇑f : (a : V) → V') '' B) this
Vinh : Inhabited V
b : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)
rw :
  ∀ (BC : B ⊆ (⇑f : (a : V) → V') ⁻¹' this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯),
    let hC := Basis.extend (s := (⇑f : (a : V) → V') '' B) this;
    ∀ (Vinh : Inhabited V) (b : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)),
      Eq (α := V)
        (((hC.constr ℕ : (a : (↑(this.extend ⋯) : Type u_5) → V) → V' →ₗ[K] V)
                  (C.restrict (π := fun (a : V') ↦ V) (invFun (⇑f : (a : V) → V'))) ∘ₗ
                f :
              (a : V) → V)
            ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V) :
          V)
        ((id : (a : V) → V) ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V) : V)
⊢ Eq (α := V)
    (((hC.constr ℕ : (a : (↑(this.extend ⋯) : Type u_5) → V) → V' →ₗ[K] V)
              (C.restrict (π := fun (a : V') ↦ V) (invFun (⇑f : (a : V) → V'))) ∘ₗ
            f :
          (a : V) → V)
        ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V) :
      V)
    ((id : (a : V) → V) ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V) : V)

Tactic:
rw [image_subset_iff] at BC

Premises used: Set.image_subset_iff
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
this : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
C : Set V' := this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
BC : B ⊆ (⇑f : (a : V) → V') ⁻¹' this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
hC : Basis (↑(this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯) : Type u_5) K V' :=
  Basis.extend (s := (⇑f : (a : V) → V') '' B) this
Vinh : Inhabited V
b : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)
change :
  Eq.{u_5 + 1} (α := V') ((f : (a : V) → V') (↑b : V) : V')
    ((Basis.extend (s := (⇑f : (a : V) → V') '' B) this : (a : (↑(this.extend ⋯) : Type u_5)) → V')
        (Subtype.mk (p := fun (x : V') ↦ x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯)
            ((f : (a : V) → V') (↑b : V)) ⋯ :
          { x : V' // x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯ }) :
      V')
⊢ Eq.{u_5 + 1} (α := V') ((f : (a : V) → V') (↑b : V) : V')
    ((hC : (a : (↑(this.extend ⋯) : Type u_5)) → V')
        (Subtype.mk (p := fun (x : V') ↦ x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯)
            ((f : (a : V) → V') (↑b : V)) ⋯ :
          { x : V' // x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯ }) :
      V')

Tactic:
change f b = Basis.extend this _

Premises used: Module.Basis.extend, Subtype.val, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
this : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
C : Set V' := this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
BC : B ⊆ (⇑f : (a : V) → V') ⁻¹' this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
hC : Basis (↑(this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯) : Type u_5) K V' :=
  Basis.extend (s := (⇑f : (a : V) → V') '' B) this
Vinh : Inhabited V
b : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)
⊢ Eq.{u_5 + 1} (α := V') ((f : (a : V) → V') (↑b : V) : V')
    ((Basis.extend (s := (⇑f : (a : V) → V') '' B) this : (a : (↑(this.extend ⋯) : Type u_5)) → V')
        (Subtype.mk (p := fun (x : V') ↦ x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯)
            ((f : (a : V) → V') (↑b : V)) ⋯ :
          { x : V' // x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯ }) :
      V')

Tactic:
simp_rw [Basis.extend_apply_self]

Premises used: Module.Basis.extend_apply_self