case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
⊢ c ≤ rank f ↔ ∃ s, lift (#↑s) = lift c ∧ LinearIndependent K fun x => ↑f ↑x
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
⊢ c ≤ rank f ↔ ∃ s, lift (#↑s) = lift c ∧ LinearIndependent K fun x => ↑f ↑x
rcases f.rangeRestrict.exists_rightInverse_of_surjective f.range_rangeRestrict with ⟨g, hg⟩
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
⊢ c ≤ rank f ↔ ∃ s, lift (#↑s) = lift c ∧ LinearIndependent K fun x => ↑f ↑x
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
⊢ c ≤ rank f ↔ ∃ s, lift (#↑s) = lift c ∧ LinearIndependent K fun x => ↑f ↑x
have fg : LeftInverse f.rangeRestrict g := LinearMap.congr_fun hg
case intro.refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
h : c ≤ rank f
⊢ ∃ s, lift (#↑s) = lift c ∧ LinearIndependent K fun x => ↑f ↑x

case intro.refine'_2
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
⊢ (∃ s, lift (#↑s) = lift c ∧ LinearIndependent K fun x => ↑f ↑x) → c ≤ rank f
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
⊢ c ≤ rank f ↔ ∃ s, lift (#↑s) = lift c ∧ LinearIndependent K fun x => ↑f ↑x
refine' ⟨fun h => _, _⟩
case intro.refine'_1.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
⊢ ∃ s_1, lift (#↑s_1) = lift (#↑s) ∧ LinearIndependent K fun x => ↑f ↑x
case intro.refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
h : c ≤ rank f
⊢ ∃ s, lift (#↑s) = lift c ∧ LinearIndependent K fun x => ↑f ↑x
rcases _root_.le_rank_iff_exists_linearIndependent.1 h with ⟨s, rfl, si⟩
case intro.refine'_1.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
⊢ LinearIndependent K fun x => ↑f ↑x
case intro.refine'_1.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
⊢ ∃ s_1, lift (#↑s_1) = lift (#↑s) ∧ LinearIndependent K fun x => ↑f ↑x
refine' ⟨g '' s, Cardinal.mk_image_eq_lift _ _ fg.injective, _⟩
case fg
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
⊢ ∀ (x : { x // x ∈ range f }), ↑f (↑g x) = ↑x

case intro.refine'_1.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
fg : ∀ (x : { x // x ∈ range f }), ↑f (↑g x) = ↑x
⊢ LinearIndependent K fun x => ↑f ↑x
case intro.refine'_1.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
⊢ LinearIndependent K fun x => ↑f ↑x
replace fg : ∀ x, f (g x) = x
case si
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
fg : ∀ (x : { x // x ∈ range f }), ↑f (↑g x) = ↑x
⊢ LinearIndependent K fun x => ↑f (↑g ↑x)

case intro.refine'_1.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
s : Set { x // x ∈ range f }
h : (#↑s) ≤ rank f
fg : ∀ (x : { x // x ∈ range f }), ↑f (↑g x) = ↑x
si : LinearIndependent K fun x => ↑f (↑g ↑x)
⊢ LinearIndependent K fun x => ↑f ↑x
case intro.refine'_1.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
fg : ∀ (x : { x // x ∈ range f }), ↑f (↑g x) = ↑x
⊢ LinearIndependent K fun x => ↑f ↑x
replace si : LinearIndependent K fun x : s => f (g x)
no goals
case intro.refine'_1.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
s : Set { x // x ∈ range f }
h : (#↑s) ≤ rank f
fg : ∀ (x : { x // x ∈ range f }), ↑f (↑g x) = ↑x
si : LinearIndependent K fun x => ↑f (↑g ↑x)
⊢ LinearIndependent K fun x => ↑f ↑x
exact si.image_of_comp s g f
case fg
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
x : { x // x ∈ range f }
⊢ ↑f (↑g x) = ↑x
case fg
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
⊢ ∀ (x : { x // x ∈ range f }), ↑f (↑g x) = ↑x
intro x
no goals
case fg
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
x : { x // x ∈ range f }
⊢ ↑f (↑g x) = ↑x
convert congr_arg Subtype.val (fg x)
no goals
case si
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
s : Set { x // x ∈ range f }
si : LinearIndependent K Subtype.val
h : (#↑s) ≤ rank f
fg : ∀ (x : { x // x ∈ range f }), ↑f (↑g x) = ↑x
⊢ LinearIndependent K fun x => ↑f (↑g ↑x)
simpa only [fg] using si.map' _ (ker_subtype _)
case intro.refine'_2.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set V
hsc : lift (#↑s) = lift c
si : LinearIndependent K fun x => ↑f ↑x
⊢ c ≤ rank f
case intro.refine'_2
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
⊢ (∃ s, lift (#↑s) = lift c ∧ LinearIndependent K fun x => ↑f ↑x) → c ≤ rank f
rintro ⟨s, hsc, si⟩
case intro.refine'_2.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set V
hsc : lift (#↑s) = lift c
si : LinearIndependent K fun x => ↑f ↑x
this : LinearIndependent K fun x => ↑(rangeRestrict f) ↑x
⊢ c ≤ rank f
case intro.refine'_2.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set V
hsc : lift (#↑s) = lift c
si : LinearIndependent K fun x => ↑f ↑x
⊢ c ≤ rank f
have : LinearIndependent K fun x : s => f.rangeRestrict x :=
  LinearIndependent.of_comp f.range.subtype (by convert si)
case h.e'_3
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set V
hsc : lift (#↑s) = lift c
si : LinearIndependent K fun x => ↑f ↑x
this : LinearIndependent K fun x => ↑(rangeRestrict f) ↑x
⊢ c = (#↑(↑(rangeRestrict f) '' s))
case intro.refine'_2.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set V
hsc : lift (#↑s) = lift c
si : LinearIndependent K fun x => ↑f ↑x
this : LinearIndependent K fun x => ↑(rangeRestrict f) ↑x
⊢ c ≤ rank f
convert cardinal_le_rank_of_linearIndependent this.image
case h.e'_3.h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set V
hsc : lift (#↑s) = lift c
si : LinearIndependent K fun x => ↑f ↑x
this : LinearIndependent K fun x => ↑(rangeRestrict f) ↑x
⊢ InjOn (↑(rangeRestrict f)) s
case h.e'_3
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set V
hsc : lift (#↑s) = lift c
si : LinearIndependent K fun x => ↑f ↑x
this : LinearIndependent K fun x => ↑(rangeRestrict f) ↑x
⊢ c = (#↑(↑(rangeRestrict f) '' s))
rw [← Cardinal.lift_inj, ← hsc, Cardinal.mk_image_eq_of_injOn_lift]
no goals
case h.e'_3.h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set V
hsc : lift (#↑s) = lift c
si : LinearIndependent K fun x => ↑f ↑x
this : LinearIndependent K fun x => ↑(rangeRestrict f) ↑x
⊢ InjOn (↑(rangeRestrict f)) s
exact injOn_iff_injective.2 this.injective
no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1163616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal
f : V →ₗ[K] V'
g : { x // x ∈ range f } →ₗ[K] V
hg : comp (rangeRestrict f) g = id
fg : LeftInverse ↑(rangeRestrict f) ↑g
s : Set V
hsc : lift (#↑s) = lift c
si : LinearIndependent K fun x => ↑f ↑x
⊢ LinearIndependent K (↑(Submodule.subtype (range f)) ∘ fun x => ↑(rangeRestrict f) ↑x)
convert si