Theorem: FiniteDimensional.finrank_add_finrank_quotient_le (FltRegular/NumberTheory/Finrank.lean)

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
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Tactic:
obtain ⟨s, hs, hs'⟩ := exists_finset_card_eq_finrank_and_linearIndependent R N
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
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M

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
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Tactic:
obtain ⟨t, ht, ht'⟩ := exists_finset_card_eq_finrank_and_linearIndependent R (M ⧸ N)
State after:
case 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
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M

State before:
case 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
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Tactic:
obtain ⟨f, hf⟩ := N.mkQ_surjective.hasRightInverse
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
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M

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
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Tactic:
have H : Disjoint (Submodule.span R (Subtype.val '' (s : Set N))) (Submodule.span R (f '' t)) := by
  apply Disjoint.mono_left (Submodule.span_le.mpr Set.image_val_subset)
  rw [disjoint_iff, eq_bot_iff, ← @Subtype.range_val (M ⧸ N) t, ← Set.range_comp,
    ← Finsupp.range_total]
  rintro _ ⟨h, l, rfl⟩
  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
  rw [linearIndependent_iff.mp ht' l h, map_zero]
  exact zero_mem _
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))
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M

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]
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)

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
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)

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)
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))

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]
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)) ≤ ⊥

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⟩
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 ∈ ⊥

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
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 ∈ ⊥

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]
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 ∈ ⊥

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 _
State after:
no goals

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]
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

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
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

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]
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

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
State after:
no goals

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]
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

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
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)

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'
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

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 _
State after:
no goals

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]
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 ⊆ ∅

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₂⟩
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 ∈ ∅

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))
x : M
h₁ : x ∈ Subtype.val '' ↑s
h₂ : x ∈ f '' ↑t
⊢ x ∈ ∅
Tactic:
obtain rfl : x = 0 :=
  (disjoint_iff.mp H).le ⟨Submodule.subset_span h₁, Submodule.subset_span h₂⟩
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))
h₁ : 0 ∈ Subtype.val '' ↑s
h₂ : 0 ∈ f '' ↑t
⊢ 0 ∈ ∅

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))
h₁ : 0 ∈ Subtype.val '' ↑s
h₂ : 0 ∈ f '' ↑t
⊢ 0 ∈ ∅
Tactic:
simp only [Set.mem_image, Finset.mem_coe, ZeroMemClass.coe_eq_zero, exists_eq_right] at h₁
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))
h₂ : 0 ∈ f '' ↑t
h₁ : 0 ∈ s
⊢ 0 ∈ ∅

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))
h₂ : 0 ∈ f '' ↑t
h₁ : 0 ∈ s
⊢ 0 ∈ ∅
Tactic:
exact hs'.ne_zero ⟨0, h₁⟩ (by simp only)
State after:
no goals

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
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
h₂ : 0 ∈ f '' ↑t
h₁ : 0 ∈ s
⊢ ↑⟨0, h₁⟩ = 0
Tactic:
simp only
State after:
no goals