ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
⊢ ∃ g, comp g f = id
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
⊢ ∃ g, comp g f = id
let B := Basis.ofVectorSpaceIndex K V
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ ∃ g, comp g f = id
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
⊢ ∃ g, comp g f = id
let hB := Basis.ofVectorSpace K V
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
⊢ ∃ g, comp g f = id
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ ∃ g, comp g f = id
have hB₀ : _ := hB.linearIndependent.to_subtype_range
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
⊢ ∃ g, comp g f = id
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
⊢ ∃ g, comp g f = id
have : LinearIndependent K (fun x => x : f '' B → V') := by
  have h₁ : LinearIndependent K ((↑) : ↥(f '' Set.range (Basis.ofVectorSpace K V)) → V') :=
    @LinearIndependent.image_subtype _ _ _ _ _ _ _ _ _ f hB₀ (show Disjoint _ _ by simp [hf_inj])
  rwa [Basis.range_ofVectorSpace K V] at h₁
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
⊢ ∃ g, comp g f = id
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
⊢ ∃ g, comp g f = id
let C := this.extend (subset_univ _)
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
⊢ ∃ g, comp g f = id
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
⊢ ∃ g, comp g f = id
have BC := this.subset_extend (subset_univ _)
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
⊢ ∃ g, comp g f = id
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
⊢ ∃ g, comp g f = id
let hC := Basis.extend this
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
⊢ ∃ g, comp g f = id
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
⊢ ∃ g, comp g f = id
haveI Vinh : Inhabited V := ⟨0⟩
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
⊢ ∃ g, comp g f = id
refine' ⟨(hC.constr ℕ : _ → _) (C.restrict (invFun f)), hB.ext fun b => _⟩
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
rw [image_subset_iff] at BC
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
have fb_eq : f b = hC ⟨f b, BC b.2⟩ := by
  change f b = Basis.extend this _
  simp_rw [Basis.extend_apply_self]
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ ↑(↑(Basis.constr (Basis.extend this) ℕ)
          (Set.restrict (LinearIndependent.extend this (_ : ↑f '' Basis.ofVectorSpaceIndex K V ⊆ univ)) (invFun ↑f)))
      (↑f (↑(Basis.ofVectorSpace K V) b)) =
    ↑(Basis.ofVectorSpace K V) b
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
dsimp []
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ Set.restrict (LinearIndependent.extend this (_ : ↑f '' Basis.ofVectorSpaceIndex K V ⊆ univ)) (invFun ↑f)
      { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) } =
    ↑b
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ ↑(↑(Basis.constr (Basis.extend this) ℕ)
          (Set.restrict (LinearIndependent.extend this (_ : ↑f '' Basis.ofVectorSpaceIndex K V ⊆ univ)) (invFun ↑f)))
      (↑f (↑(Basis.ofVectorSpace K V) b)) =
    ↑(Basis.ofVectorSpace K V) b
rw [Basis.ofVectorSpace_apply_self, fb_eq, hC.constr_basis]
no goals
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ Set.restrict (LinearIndependent.extend this (_ : ↑f '' Basis.ofVectorSpaceIndex K V ⊆ univ)) (invFun ↑f)
      { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) } =
    ↑b
exact leftInverse_invFun (LinearMap.ker_eq_bot.1 hf_inj) _
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
h₁ : LinearIndependent K Subtype.val
⊢ LinearIndependent K fun x => ↑x
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
⊢ LinearIndependent K fun x => ↑x
have h₁ : LinearIndependent K ((↑) : ↥(f '' Set.range (Basis.ofVectorSpace K V)) → V') :=
  @LinearIndependent.image_subtype _ _ _ _ _ _ _ _ _ f hB₀ (show Disjoint _ _ by simp [hf_inj])
no goals
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
h₁ : LinearIndependent K Subtype.val
⊢ LinearIndependent K fun x => ↑x
rwa [Basis.range_ofVectorSpace K V] at h₁
no goals
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
⊢ Disjoint (span K (Set.range ↑(Basis.ofVectorSpace K V))) (ker f)
simp [hf_inj]
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑f ↑b =
    ↑(Basis.extend this)
      { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
change f b = Basis.extend this _
no goals
ι : Type ?u.1179439
ι' : Type ?u.1179442
R : Type ?u.1179445
R₂ : Type ?u.1179448
K : Type u_1
M : Type ?u.1179454
M' : Type ?u.1179457
M'' : Type ?u.1179460
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑f ↑b =
    ↑(Basis.extend this)
      { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
simp_rw [Basis.extend_apply_self]