ι : Type u'
ι' : Type ?u.98368
R : Type u_1
K : Type ?u.98374
M : Type u_2
M' : Type u_3
M'' : Type ?u.98383
V : Type u
V' : Type ?u.98388
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
f : M →ₗ[R] M'
hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) ≤ LinearMap.ker (Finsupp.total ι M R v)
⊢ LinearIndependent R (↑f ∘ v)
ι : Type u'
ι' : Type ?u.98368
R : Type u_1
K : Type ?u.98374
M : Type u_2
M' : Type u_3
M'' : Type ?u.98383
V : Type u
V' : Type ?u.98388
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
f : M →ₗ[R] M'
hf_inj : Disjoint (span R (range v)) (LinearMap.ker f)
⊢ LinearIndependent R (↑f ∘ v)
rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_total,
  map_inf_eq_map_inf_comap, map_le_iff_le_comap, comap_bot, Finsupp.supported_univ, top_inf_eq]
    at hf_inj
ι : Type u'
ι' : Type ?u.98368
R : Type u_1
K : Type ?u.98374
M : Type u_2
M' : Type u_3
M'' : Type ?u.98383
V : Type u
V' : Type ?u.98388
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥
f : M →ₗ[R] M'
hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) ≤ LinearMap.ker (Finsupp.total ι M R v)
⊢ LinearMap.ker (Finsupp.total ι M' R (↑f ∘ v)) = ⊥
ι : Type u'
ι' : Type ?u.98368
R : Type u_1
K : Type ?u.98374
M : Type u_2
M' : Type u_3
M'' : Type ?u.98383
V : Type u
V' : Type ?u.98388
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
f : M →ₗ[R] M'
hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) ≤ LinearMap.ker (Finsupp.total ι M R v)
⊢ LinearIndependent R (↑f ∘ v)
unfold LinearIndependent at hv⊢
ι : Type u'
ι' : Type ?u.98368
R : Type u_1
K : Type ?u.98374
M : Type u_2
M' : Type u_3
M'' : Type ?u.98383
V : Type u
V' : Type ?u.98388
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥
f : M →ₗ[R] M'
hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) = ⊥
⊢ LinearMap.ker (Finsupp.total ι M' R (↑f ∘ v)) = ⊥
ι : Type u'
ι' : Type ?u.98368
R : Type u_1
K : Type ?u.98374
M : Type u_2
M' : Type u_3
M'' : Type ?u.98383
V : Type u
V' : Type ?u.98388
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥
f : M →ₗ[R] M'
hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) ≤ LinearMap.ker (Finsupp.total ι M R v)
⊢ LinearMap.ker (Finsupp.total ι M' R (↑f ∘ v)) = ⊥
rw [hv, le_bot_iff] at hf_inj
ι : Type u'
ι' : Type ?u.98368
R : Type u_1
K : Type ?u.98374
M : Type u_2
M' : Type u_3
M'' : Type ?u.98383
V : Type u
V' : Type ?u.98388
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥
f : M →ₗ[R] M'
hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) = ⊥
this : Inhabited M
⊢ LinearMap.ker (Finsupp.total ι M' R (↑f ∘ v)) = ⊥
ι : Type u'
ι' : Type ?u.98368
R : Type u_1
K : Type ?u.98374
M : Type u_2
M' : Type u_3
M'' : Type ?u.98383
V : Type u
V' : Type ?u.98388
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥
f : M →ₗ[R] M'
hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) = ⊥
⊢ LinearMap.ker (Finsupp.total ι M' R (↑f ∘ v)) = ⊥
haveI : Inhabited M := ⟨0⟩
ι : Type u'
ι' : Type ?u.98368
R : Type u_1
K : Type ?u.98374
M : Type u_2
M' : Type u_3
M'' : Type ?u.98383
V : Type u
V' : Type ?u.98388
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥
f : M →ₗ[R] M'
hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) = ⊥
this : Inhabited M
⊢ ∀ (i : ι), ↑f (v i) = ↑f (v i)
ι : Type u'
ι' : Type ?u.98368
R : Type u_1
K : Type ?u.98374
M : Type u_2
M' : Type u_3
M'' : Type ?u.98383
V : Type u
V' : Type ?u.98388
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥
f : M →ₗ[R] M'
hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) = ⊥
this : Inhabited M
⊢ LinearMap.ker (Finsupp.total ι M' R (↑f ∘ v)) = ⊥
rw [Finsupp.total_comp, @Finsupp.lmapDomain_total _ _ R _ _ _ _ _ _ _ _ _ _ f, LinearMap.ker_comp,
  hf_inj]
no goals
ι : Type u'
ι' : Type ?u.98368
R : Type u_1
K : Type ?u.98374
M : Type u_2
M' : Type u_3
M'' : Type ?u.98383
V : Type u
V' : Type ?u.98388
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥
f : M →ₗ[R] M'
hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) = ⊥
this : Inhabited M
⊢ ∀ (i : ι), ↑f (v i) = ↑f (v i)
exact fun _ => rfl