[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ comap (Submodule.subtype p) (p ⊓ p') ≤ ker (subToSupQuotient p p')
[PROOFSTEP]
rw [LinearMap.ker_comp, Submodule.ofLe, comap_codRestrict, ker_mkQ, map_comap_subtype]
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ comap (Submodule.subtype p) (p ⊓ p') ≤ comap (Submodule.subtype p) ((p ⊔ p') ⊓ p')
[PROOFSTEP]
exact comap_mono (inf_le_inf_right _ le_sup_left)
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ Function.Injective ↑(quotientInfToSupQuotient p p')
[PROOFSTEP]
rw [← ker_eq_bot, quotientInfToSupQuotient, ker_liftQ_eq_bot]
[GOAL]
case h'
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ ker (subToSupQuotient p p') ≤ comap (Submodule.subtype p) (p ⊓ p')
[PROOFSTEP]
rw [ker_comp, ker_mkQ]
[GOAL]
case h'
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ comap (ofLe (_ : p ≤ p ⊔ p')) (comap (Submodule.subtype (p ⊔ p')) p') ≤ comap (Submodule.subtype p) (p ⊓ p')
[PROOFSTEP]
exact fun ⟨x, hx1⟩ hx2 =>
  ⟨hx1, hx2⟩
    -- Porting note: breaking up original definition of quotientInfEquivSupQuotient to avoid timing out
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ Function.Surjective ↑(quotientInfToSupQuotient p p')
[PROOFSTEP]
rw [← range_eq_top, quotientInfToSupQuotient, range_liftQ, eq_top_iff']
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ ∀ (x : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'), x ∈ range (subToSupQuotient p p')
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mk.mk
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
x : M
hx : x ∈ p ⊔ p'
⊢ Quot.mk Setoid.r { val := x, property := hx } ∈ range (subToSupQuotient p p')
[PROOFSTEP]
rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩
[GOAL]
case mk.mk.intro.intro.intro.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ Quot.mk Setoid.r { val := y + z, property := hx } ∈ range (subToSupQuotient p p')
[PROOFSTEP]
use⟨y, hy⟩
[GOAL]
case h
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ ↑(subToSupQuotient p p') { val := y, property := hy } = Quot.mk Setoid.r { val := y + z, property := hx }
[PROOFSTEP]
apply (Submodule.Quotient.eq _).2
[GOAL]
case h
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ ↑(ofLe (_ : p ≤ p ⊔ p')) { val := y, property := hy } - { val := y + z, property := hx } ∈
    comap (Submodule.subtype (p ⊔ p')) p'
[PROOFSTEP]
simp only [mem_comap, map_sub, coeSubtype, coe_ofLe, sub_add_cancel', neg_mem_iff, hz]
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x : { x // x ∈ p ⊔ p' }
hx : ↑x ∈ p
⊢ Submodule.Quotient.mk x = ↑(quotientInfEquivSupQuotient p p') (Submodule.Quotient.mk { val := ↑x, property := hx })
[PROOFSTEP]
rw [quotientInfEquivSupQuotient_apply_mk, ofLe_apply]
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x : { x // x ∈ p ⊔ p' }
⊢ Submodule.Quotient.mk x = ↑(quotientInfEquivSupQuotient p p') 0 ↔ ↑x ∈ p'
[PROOFSTEP]
rw [_root_.map_zero, Quotient.mk_eq_zero, mem_comap, Submodule.coeSubtype]
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
⊢ map (mkQ S) T ≤ LinearMap.ker (mapQ S T LinearMap.id h)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
x : M
hx : x ∈ ↑T
⊢ ↑(mkQ S) x ∈ LinearMap.ker (mapQ S T LinearMap.id h)
[PROOFSTEP]
rw [LinearMap.mem_ker, mkQ_apply, mapQ_apply]
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
x : M
hx : x ∈ ↑T
⊢ Quotient.mk (↑LinearMap.id x) = 0
[PROOFSTEP]
exact (Quotient.mk_eq_zero _).mpr hx
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
x : M
⊢ ↑(quotientQuotientEquivQuotientAux S T h) (Quotient.mk (Quotient.mk x)) = Quotient.mk x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
src✝ : (M ⧸ S) ⧸ map (mkQ S) T →ₗ[R] M ⧸ T := quotientQuotientEquivQuotientAux S T h
x✝¹ : (M ⧸ S) ⧸ map (mkQ S) T
x✝ : M ⧸ S
x : M
⊢ ↑(mapQ T (map (mkQ S) T) (mkQ S) (_ : T ≤ comap (mkQ S) (map (mkQ S) T)))
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(quotientQuotientEquivQuotientAux S T h),
                map_add' :=
                  (_ :
                    ∀ (x y : (M ⧸ S) ⧸ map (mkQ S) T),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : (M ⧸ S) ⧸ map (mkQ S) T),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        (Quotient.mk'' (Quotient.mk'' x))) =
    Quotient.mk'' (Quotient.mk'' x)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
src✝ : (M ⧸ S) ⧸ map (mkQ S) T →ₗ[R] M ⧸ T := quotientQuotientEquivQuotientAux S T h
x✝ : M ⧸ T
x : M
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(quotientQuotientEquivQuotientAux S T h),
              map_add' :=
                (_ :
                  ∀ (x y : (M ⧸ S) ⧸ map (mkQ S) T),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : (M ⧸ S) ⧸ map (mkQ S) T),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      (↑(mapQ T (map (mkQ S) T) (mkQ S) (_ : T ≤ comap (mkQ S) (map (mkQ S) T))) (Quotient.mk'' x)) =
    Quotient.mk'' x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
f : M →ₗ[R] M₂
S✝ T✝ : Submodule R M
h : S✝ ≤ T✝
S T : Submodule R M
hST : T ≤ S
inst✝² : DecidablePred fun x => x ∈ map (mkQ T) S
inst✝¹ : Fintype (M ⧸ S)
inst✝ : Fintype (M ⧸ T)
⊢ Fintype.card { x // x ∈ map (mkQ T) S } * Fintype.card (M ⧸ S) = Fintype.card (M ⧸ T)
[PROOFSTEP]
rw [Submodule.card_eq_card_quotient_mul_card (map T.mkQ S),
  Fintype.card_eq.mpr ⟨(quotientQuotientEquivQuotient T S hST).toEquiv⟩]
