internlm/Lean-Github huggingface dataset:
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Tactic:
rw [← hs, ← ht, ← t.card_image_of_injective hf.injective,
  ← s.card_image_of_injective Subtype.val_injective, ← Finset.card_union_of_disjoint]
Proof state after:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ (Finset.image Subtype.val s ∪ Finset.image f t).card ≤ finrank R M

case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ Disjoint (Finset.image Subtype.val s) (Finset.image f t)
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ (Finset.image Subtype.val s ∪ Finset.image f t).card ≤ finrank R M

case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ Disjoint (Finset.image Subtype.val s) (Finset.image f t)
Tactic:
apply LinearIndependent.finset_card_le_finrank
Proof state after:
case intro.intro.intro.intro.intro.h
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent R fun x => ↑x

case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ Disjoint (Finset.image Subtype.val s) (Finset.image f t)
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
⊢ Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
Tactic:
apply Disjoint.mono_left (Submodule.span_le.mpr Set.image_val_subset)
Proof state after:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
⊢ Disjoint N (Submodule.span R (f '' ↑t))
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
⊢ Disjoint N (Submodule.span R (f '' ↑t))
Tactic:
rw [disjoint_iff, eq_bot_iff, ← @Subtype.range_val (M ⧸ N) t, ← Set.range_comp,
  ← Finsupp.range_total]
Proof state after:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
⊢ N ⊓ LinearMap.range (Finsupp.total { x // x ∈ ↑t } M R (f ∘ Subtype.val)) ≤ ⊥
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
⊢ N ⊓ LinearMap.range (Finsupp.total { x // x ∈ ↑t } M R (f ∘ Subtype.val)) ≤ ⊥
Tactic:
rintro _ ⟨h, l, rfl⟩
Proof state after:
case intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
l : { x // x ∈ ↑t } →₀ R
h : (Finsupp.total { x // x ∈ ↑t } M R (f ∘ Subtype.val)) l ∈ ↑N
⊢ (Finsupp.total { x // x ∈ ↑t } M R (f ∘ Subtype.val)) l ∈ ⊥
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
l : { x // x ∈ ↑t } →₀ R
h : (Finsupp.total { x // x ∈ ↑t } M R (f ∘ Subtype.val)) l ∈ ↑N
⊢ (Finsupp.total { x // x ∈ ↑t } M R (f ∘ Subtype.val)) l ∈ ⊥
Tactic:
rw [SetLike.mem_coe, ← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply,
  Finsupp.apply_total, ← Function.comp.assoc, show N.mkQ ∘ f = id from funext hf] at h
Proof state after:
case intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
l : { x // x ∈ ↑t } →₀ R
h : (Finsupp.total { x // x ∈ ↑t } (M ⧸ N) R (id ∘ Subtype.val)) l = 0
⊢ (Finsupp.total { x // x ∈ ↑t } M R (f ∘ Subtype.val)) l ∈ ⊥
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
l : { x // x ∈ ↑t } →₀ R
h : (Finsupp.total { x // x ∈ ↑t } (M ⧸ N) R (id ∘ Subtype.val)) l = 0
⊢ (Finsupp.total { x // x ∈ ↑t } M R (f ∘ Subtype.val)) l ∈ ⊥
Tactic:
rw [linearIndependent_iff.mp ht' l h, map_zero]
Proof state after:
case intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
l : { x // x ∈ ↑t } →₀ R
h : (Finsupp.total { x // x ∈ ↑t } (M ⧸ N) R (id ∘ Subtype.val)) l = 0
⊢ 0 ∈ ⊥
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
l : { x // x ∈ ↑t } →₀ R
h : (Finsupp.total { x // x ∈ ↑t } (M ⧸ N) R (id ∘ Subtype.val)) l = 0
⊢ 0 ∈ ⊥
Tactic:
exact zero_mem _
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro.h
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent R fun x => ↑x
Tactic:
rw [← LinearIndependent.finset_toSet, Finset.coe_union, Finset.coe_image, Finset.coe_image]
Proof state after:
case intro.intro.intro.intro.intro.h
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent (ι := { x // x ∈ Subtype.val '' ↑s ∪ f '' ↑t }) R Subtype.val
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro.h
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent (ι := { x // x ∈ Subtype.val '' ↑s ∪ f '' ↑t }) R Subtype.val
Tactic:
refine LinearIndependent.union ?_ ?_ H
Proof state after:
case intro.intro.intro.intro.intro.h.refine_1
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent R fun (x : ↑(Subtype.val '' ↑s)) => ↑x

case intro.intro.intro.intro.intro.h.refine_2
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent R fun (x : ↑(f '' ↑t)) => ↑x
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro.h.refine_1
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent R fun (x : ↑(Subtype.val '' ↑s)) => ↑x
Tactic:
rw [← linearIndependent_image Subtype.val_injective.injOn]
Proof state after:
case intro.intro.intro.intro.intro.h.refine_1
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent R fun (x : ↑↑s) => ↑↑x
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro.h.refine_1
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent R fun (x : ↑↑s) => ↑↑x
Tactic:
exact hs'.map' N.subtype N.ker_subtype
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro.h.refine_2
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent R fun (x : ↑(f '' ↑t)) => ↑x
Tactic:
rw [← linearIndependent_image hf.injective.injOn]
Proof state after:
case intro.intro.intro.intro.intro.h.refine_2
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent R fun (x : ↑↑t) => f ↑x
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro.h.refine_2
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent R fun (x : ↑↑t) => f ↑x
Tactic:
apply LinearIndependent.of_comp N.mkQ
Proof state after:
case intro.intro.intro.intro.intro.h.refine_2
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent (ι := ↑↑t) R (⇑N.mkQ ∘ fun x => f ↑x)
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro.h.refine_2
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ LinearIndependent (ι := ↑↑t) R (⇑N.mkQ ∘ fun x => f ↑x)
Tactic:
convert ht'
Proof state after:
case h.e'_4.h
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
e_1✝ : ↑↑t = { x // x ∈ t }
⊢ (⇑N.mkQ ∘ fun x => f ↑x) = Subtype.val
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case h.e'_4.h
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
e_1✝ : ↑↑t = { x // x ∈ t }
⊢ (⇑N.mkQ ∘ fun x => f ↑x) = Subtype.val
Tactic:
exact funext fun x => hf _
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ Disjoint (Finset.image Subtype.val s) (Finset.image f t)
Tactic:
rw [← Finset.disjoint_coe, Finset.coe_image, Finset.coe_image, Set.disjoint_iff]
Proof state after:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ Subtype.val '' ↑s ∩ f '' ↑t ⊆ ∅
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ Subtype.val '' ↑s ∩ f '' ↑t ⊆ ∅
Tactic:
intro x ⟨h₁, h₂⟩
Proof state after:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
x : M
h₁ : x ∈ Subtype.val '' ↑s
h₂ : x ∈ f '' ↑t
⊢ x ∈ ∅