[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y✝ : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x y : M
⊢ Setoid.r x y ↔ -(x - y) ∈ p
[PROOFSTEP]
rw [leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y✝ : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x y : M
⊢ -x + y ∈ toAddSubgroup p ↔ -x + y ∈ p
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ mk x = 0 ↔ x ∈ p
[PROOFSTEP]
simpa using (Quotient.eq' p : mk x = 0 ↔ _)
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y✝ : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
S : Type u_3
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
P : Submodule R M
a : S
x y : M
h : Setoid.r x y
⊢ -(fun x x_1 => x • x_1) a x + (fun x x_1 => x • x_1) a y ∈ toAddSubgroup P
[PROOFSTEP]
simpa using Submodule.smul_mem P (a • (1 : R)) (leftRel_apply.mp h)
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Function.Surjective mk
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
b✝ : M ⧸ p
x : M
⊢ ∃ a, mk a = Quot.mk Setoid.r x
[PROOFSTEP]
exact ⟨x, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p < ⊤
⊢ Nontrivial (M ⧸ p)
[PROOFSTEP]
obtain ⟨x, _, not_mem_s⟩ := SetLike.exists_of_lt h
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : ¬x ∈ p
⊢ Nontrivial (M ⧸ p)
[PROOFSTEP]
refine' ⟨⟨mk x, 0, _⟩⟩
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : ¬x ∈ p
⊢ mk x ≠ 0
[PROOFSTEP]
simpa using not_mem_s
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Subsingleton (M ⧸ p) ↔ p = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Subsingleton (M ⧸ p) → p = ⊤
[PROOFSTEP]
rintro h
[GOAL]
case mp
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : Subsingleton (M ⧸ p)
⊢ p = ⊤
[PROOFSTEP]
refine' eq_top_iff.mpr fun x _ => _
[GOAL]
case mp
R : Type u_1
M : Type u_2
r : R
x✝¹ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
⊢ x ∈ p
[PROOFSTEP]
have : x - 0 ∈ p := (Submodule.Quotient.eq p).mp (Subsingleton.elim _ _)
[GOAL]
case mp
R : Type u_1
M : Type u_2
r : R
x✝¹ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
this : x - 0 ∈ p
⊢ x ∈ p
[PROOFSTEP]
rwa [sub_zero] at this 
[GOAL]
case mpr
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ p = ⊤ → Subsingleton (M ⧸ p)
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p' : Submodule R M
⊢ Subsingleton (M ⧸ ⊤)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ p = ⊤ → Nonempty (Unique (M ⧸ p))
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p' : Submodule R M
⊢ Nonempty (Unique (M ⧸ ⊤))
[PROOFSTEP]
exact ⟨QuotientTop.unique⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
inst✝¹ : Fintype M
S : Submodule R M
inst✝ : DecidablePred fun x => x ∈ S
⊢ Fintype.card M = Fintype.card { x // x ∈ S } * Fintype.card (M ⧸ S)
[PROOFSTEP]
rw [mul_comm, ← Fintype.card_prod]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
inst✝¹ : Fintype M
S : Submodule R M
inst✝ : DecidablePred fun x => x ∈ S
⊢ Fintype.card M = Fintype.card ((M ⧸ S) × { x // x ∈ S })
[PROOFSTEP]
exact Fintype.card_congr AddSubgroup.addGroupEquivQuotientProdAddSubgroup
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
⊢ ∀ (x y : M), Quotient.mk (x + y) = Quotient.mk x + Quotient.mk y
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
⊢ ∀ (r : R) (x : M),
    AddHom.toFun
        { toFun := Quotient.mk,
          map_add' := (_ : ∀ (a a_1 : M), Quotient.mk a + Quotient.mk a_1 = Quotient.mk a + Quotient.mk a_1) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := Quotient.mk,
            map_add' := (_ : ∀ (a a_1 : M), Quotient.mk a + Quotient.mk a_1 = Quotient.mk a + Quotient.mk a_1) }
          x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
A : Submodule R M
⊢ Function.Surjective ↑(mkQ A)
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
A : Submodule R M
b✝ : M ⧸ A
x : M
⊢ ∃ a, ↑(mkQ A) a = Quot.mk Setoid.r x
[PROOFSTEP]
exact ⟨x, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
src✝ : M ⧸ toAddSubgroup p →+ M₂ := lift (toAddSubgroup p) (toAddMonoidHom f) h
⊢ ∀ (r : R) (x : M ⧸ p),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : M ⧸ toAddSubgroup p),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        (r • x) =
      ↑τ₁₂ r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' :=
              (_ :
                ∀ (x y : M ⧸ toAddSubgroup p),
                  ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
          x
[PROOFSTEP]
rintro a ⟨x⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝¹ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
src✝ : M ⧸ toAddSubgroup p →+ M₂ := lift (toAddSubgroup p) (toAddMonoidHom f) h
a : R
x✝ : M ⧸ p
x : M
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : M ⧸ toAddSubgroup p),
              ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
      (a • Quot.mk Setoid.r x) =
    ↑τ₁₂ a •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : M ⧸ toAddSubgroup p),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        (Quot.mk Setoid.r x)
[PROOFSTEP]
exact f.map_smulₛₗ a x
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ comp (liftQ p f h) (mkQ p) = f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
x✝ : M
⊢ ↑(comp (liftQ p f h) (mkQ p)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x : M
f : M →ₛₗ[τ₁₂] M₂
h : ↑f x = 0
⊢ span R {x} ≤ ker f
[PROOFSTEP]
rw [span_singleton_le_iff_mem, LinearMap.mem_ker, h]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ ∀ (x : M ⧸ p), x ∈ range (mkQ p)
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝¹ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x✝ : M ⧸ p
x : M
⊢ Quot.mk Setoid.r x ∈ range (mkQ p)
[PROOFSTEP]
exact ⟨x, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ ker (mkQ p) = p
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x✝ : M
⊢ x✝ ∈ ker (mkQ p) ↔ x✝ ∈ p
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p'✝ : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p' : Submodule R (M ⧸ p)
⊢ p ≤ comap (mkQ p) p'
[PROOFSTEP]
simpa using (comap_mono bot_le : ker p.mkQ ≤ comap p.mkQ p')
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ map (mkQ p) p = ⊥
[PROOFSTEP]
rw [eq_bot_iff, map_le_iff_le_comap, comap_bot, ker_mkQ]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ comap (mkQ p) (map (mkQ p) p') = p ⊔ p'
[PROOFSTEP]
simp [comap_map_eq, sup_comm]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ map (mkQ p) p' = ⊤ ↔ p ⊔ p' = ⊤
[PROOFSTEP]
simp only [LinearMap.map_eq_top_iff p.range_mkQ, sup_comm, ker_mkQ]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ p ≤ ker (comp (mkQ q) f)
[PROOFSTEP]
simpa [ker_comp] using h
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ comp (mapQ p q f h) (mkQ p) = comp (mkQ q) f
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
x : M
⊢ ↑(comp (mapQ p q f h) (mkQ p)) x = ↑(comp (mkQ q) f) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ p ≤ comap 0 q
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap 0 q) (_ : p ≤ comap 0 q)
⊢ mapQ p q 0 h = 0
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap 0 q) (_ : p ≤ comap 0 q)
x✝ : M
⊢ ↑(comp (mapQ p q 0 h) (mkQ p)) x✝ = ↑(comp 0 (mkQ p)) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
R₃ : Type u_5
M₃ : Type u_6
inst✝³ : Ring R₃
inst✝² : AddCommGroup M₃
inst✝¹ : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : optParam (p ≤ comap f (comap g p₃)) (_ : p ≤ comap f (comap g p₃))
⊢ mapQ p p₃ (comp g f) h = comp (mapQ p₂ p₃ g hg) (mapQ p p₂ f hf)
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
R₃ : Type u_5
M₃ : Type u_6
inst✝³ : Ring R₃
inst✝² : AddCommGroup M₃
inst✝¹ : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : optParam (p ≤ comap f (comap g p₃)) (_ : p ≤ comap f (comap g p₃))
x✝ : M
⊢ ↑(comp (mapQ p p₃ (comp g f) h) (mkQ p)) x✝ = ↑(comp (comp (mapQ p₂ p₃ g hg) (mapQ p p₂ f hf)) (mkQ p)) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ p ≤ comap LinearMap.id p
[PROOFSTEP]
rw [comap_id]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap LinearMap.id p) (_ : p ≤ comap LinearMap.id p)
⊢ mapQ p p LinearMap.id h = LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap LinearMap.id p) (_ : p ≤ comap LinearMap.id p)
x✝ : M
⊢ ↑(comp (mapQ p p LinearMap.id h) (mkQ p)) x✝ = ↑(comp LinearMap.id (mkQ p)) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)
⊢ mapQ p p (f ^ k) h' = mapQ p p f h ^ k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h'✝ : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)
h' : optParam (p ≤ comap (f ^ Nat.zero) p) (_ : p ≤ comap (f ^ Nat.zero) p)
⊢ mapQ p p (f ^ Nat.zero) h' = mapQ p p f h ^ Nat.zero
[PROOFSTEP]
simp [LinearMap.one_eq_id]
[GOAL]
case succ
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p (f ^ Nat.succ k) h' = mapQ p p f h ^ Nat.succ k
[PROOFSTEP]
simp only [LinearMap.iterate_succ]
  -- porting note: why does any of these `optParams` need to be applied? Why didn't `simp` handle
      -- all of this for us?
[GOAL]
case succ
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p (comp (f ^ k) f) (_ : p ≤ comap (comp (f ^ k) f) p) = comp (mapQ p p f h ^ k) (mapQ p p f h)
[PROOFSTEP]
convert
  mapQ_comp p p p f (f ^ k) h (p.le_comap_pow_of_le_comap h k) (h.trans (comap_mono <| p.le_comap_pow_of_le_comap h k))
[GOAL]
case h.e'_3.h.e'_20
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p f h ^ k = mapQ p p (f ^ k) (_ : p ≤ comap (f ^ k) p)
[PROOFSTEP]
exact (ih _).symm
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ comap (liftQ p f h) q ≤ map (mkQ p) (comap f q)
[PROOFSTEP]
rintro ⟨x⟩ hx
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝¹ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
x✝ : M ⧸ p
x : M
hx : Quot.mk Setoid.r x ∈ comap (liftQ p f h) q
⊢ Quot.mk Setoid.r x ∈ map (mkQ p) (comap f q)
[PROOFSTEP]
exact ⟨_, hx, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ map (mkQ p) (comap f q) ≤ comap (liftQ p f h) q
[PROOFSTEP]
rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
q : Submodule R (M ⧸ p)
⊢ map (liftQ p f h) q ≤ map f (comap (mkQ p) q)
[PROOFSTEP]
rintro _ ⟨⟨x⟩, hxq, rfl⟩
[GOAL]
case intro.mk.intro
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
q : Submodule R (M ⧸ p)
w✝ : M ⧸ p
x : M
hxq : Quot.mk Setoid.r x ∈ ↑q
⊢ ↑(liftQ p f h) (Quot.mk Setoid.r x) ∈ map f (comap (mkQ p) q)
[PROOFSTEP]
exact ⟨x, hxq, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
q : Submodule R (M ⧸ p)
⊢ map f (comap (mkQ p) q) ≤ map (liftQ p f h) q
[PROOFSTEP]
rintro _ ⟨x, hxq, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
q : Submodule R (M ⧸ p)
x : M
hxq : x ∈ ↑(comap (mkQ p) q)
⊢ ↑f x ∈ map (liftQ p f h) q
[PROOFSTEP]
exact ⟨Quotient.mk x, hxq, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ range (liftQ p f h) = range f
[PROOFSTEP]
simpa only [range_eq_map] using map_liftQ _ _ _ _
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
h' : ker f ≤ p
⊢ ker (liftQ p f h) = ⊥
[PROOFSTEP]
rw [ker_liftQ, le_antisymm h h', mkQ_map_self]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p'✝ : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
p' : Submodule R (M ⧸ p)
⊢ p' ≤ range (mkQ p)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
x✝ : { p' // p ≤ p' }
q : Submodule R M
hq : p ≤ q
⊢ ↑((fun p' => { val := comap (mkQ p) p', property := (_ : p ≤ comap (mkQ p) p') })
        ((fun q => map (mkQ p) ↑q) { val := q, property := hq })) =
    ↑{ val := q, property := hq }
[PROOFSTEP]
simpa [comap_map_mkQ p]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
⊢ span R (↑f ⁻¹' s) = comap f (span R₂ s)
[PROOFSTEP]
suffices (span R₂ s).comap f ≤ span R (f ⁻¹' s) by exact le_antisymm (span_preimage_le f s) this
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
this : comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
⊢ span R (↑f ⁻¹' s) = comap f (span R₂ s)
[PROOFSTEP]
exact le_antisymm (span_preimage_le f s) this
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
have hk : ker f ≤ span R (f ⁻¹' s) := by
  let y := Classical.choose h₀
  have hy : y ∈ s := Classical.choose_spec h₀
  rw [ker_le_iff]
  use y, h₁ hy
  rw [← Set.singleton_subset_iff] at hy 
  exact Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
⊢ ker f ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
let y := Classical.choose h₀
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
⊢ ker f ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
have hy : y ∈ s := Classical.choose_spec h₀
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ker f ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
rw [ker_le_iff]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ∃ y, y ∈ range f ∧ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
[PROOFSTEP]
use y, h₁ hy
[GOAL]
case right
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
[PROOFSTEP]
rw [← Set.singleton_subset_iff] at hy 
[GOAL]
case right
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : {y} ⊆ s
⊢ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
[PROOFSTEP]
exact Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
hk : ker f ≤ span R (↑f ⁻¹' s)
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
rw [← left_eq_sup] at hk 
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
rw [range_coe f] at h₁ 
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ Set.range ↑f
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
rw [hk, ← LinearMap.map_le_map_iff, map_span, map_comap_eq, Set.image_preimage_eq_of_subset h₁]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ Set.range ↑f
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ range f ⊓ span R₂ s ≤ span R₂ s
[PROOFSTEP]
exact inf_le_right
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map f P = Q
src✝ : M ⧸ P →ₗ[R] N ⧸ Q := mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)
x : N
hx : x ∈ Q
⊢ x ∈ comap (↑(LinearEquiv.symm f)) P
[PROOFSTEP]
rw [← hf, Submodule.mem_map] at hx 
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map f P = Q
src✝ : M ⧸ P →ₗ[R] N ⧸ Q := mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)
x : N
hx : ∃ y, y ∈ P ∧ ↑f y = x
⊢ x ∈ comap (↑(LinearEquiv.symm f)) P
[PROOFSTEP]
obtain ⟨y, hy, rfl⟩ := hx
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map f P = Q
src✝ : M ⧸ P →ₗ[R] N ⧸ Q := mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)
y : M
hy : y ∈ P
⊢ ↑f y ∈ comap (↑(LinearEquiv.symm f)) P
[PROOFSTEP]
simpa
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map f P = Q
src✝ : M ⧸ P →ₗ[R] N ⧸ Q := mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)
x : M ⧸ P
⊢ ∀ (a : M),
    ↑(mapQ Q P ↑(LinearEquiv.symm f) (_ : ∀ (x : N), x ∈ Q → x ∈ comap (↑(LinearEquiv.symm f)) P))
        (AddHom.toFun
          {
              toAddHom :=
                { toFun := ↑(mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)),
                  map_add' :=
                    (_ :
                      ∀ (x y : M ⧸ P),
                        AddHom.toFun src✝.toAddHom (x + y) =
                          AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : M ⧸ P),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          (Quotient.mk'' a)) =
      Quotient.mk'' a
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map f P = Q
src✝ : M ⧸ P →ₗ[R] N ⧸ Q := mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)
x : N ⧸ Q
⊢ ∀ (a : N),
    AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)),
                map_add' :=
                  (_ :
                    ∀ (x y : M ⧸ P),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : M ⧸ P),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        (↑(mapQ Q P ↑(LinearEquiv.symm f) (_ : ∀ (x : N), x ∈ Q → x ∈ comap (↑(LinearEquiv.symm f)) P))
          (Quotient.mk'' a)) =
      Quotient.mk'' a
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
O : Type u_6
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (LinearEquiv.trans e f) P = S
⊢ equiv P S (LinearEquiv.trans e f) hef = LinearEquiv.trans (equiv P Q e he) (equiv Q S f hf)
[PROOFSTEP]
ext
  -- `simp` can deal with `hef` depending on `e` and `f`
[GOAL]
case h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
O : Type u_6
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (LinearEquiv.trans e f) P = S
x✝ : M ⧸ P
⊢ ↑(equiv P S (LinearEquiv.trans e f) hef) x✝ = ↑(LinearEquiv.trans (equiv P Q e he) (equiv Q S f hf)) x✝
[PROOFSTEP]
simp only [Quotient.equiv_apply, LinearEquiv.trans_apply, LinearEquiv.coe_trans]
  -- `rw` can deal with `mapQ_comp` needing extra hypotheses coming from the RHS
[GOAL]
case h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
O : Type u_6
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (LinearEquiv.trans e f) P = S
x✝ : M ⧸ P
⊢ ↑(mapQ P S (comp ↑f ↑e) (_ : P ≤ comap (comp ↑f ↑e) S)) x✝ =
    ↑(mapQ Q S ↑f (_ : ∀ (x : N), x ∈ Q → x ∈ comap (↑f) S))
      (↑(mapQ P Q ↑e (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑e) Q)) x✝)
[PROOFSTEP]
rw [mapQ_comp, LinearMap.comp_apply]
[GOAL]
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
x : M
⊢ ↑(comp (mkQ (range f)) f) x = ↑0 x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ ker g ≤ range f ↔ comp (mkQ (range f)) (Submodule.subtype (ker g)) = 0
[PROOFSTEP]
rw [← range_le_ker_iff, Submodule.ker_mkQ, Submodule.range_subtype]
[GOAL]
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), comp u f = comp v f → u = v
⊢ range f = ⊤
[PROOFSTEP]
have h₁ : (0 : M₂ →ₗ[R₂] M₂ ⧸ (range f)).comp f = 0 := zero_comp _
[GOAL]
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), comp u f = comp v f → u = v
h₁ : comp 0 f = 0
⊢ range f = ⊤
[PROOFSTEP]
rw [← Submodule.ker_mkQ (range f), ← h 0 f.range.mkQ (Eq.trans h₁ (range_mkQ_comp _).symm)]
[GOAL]
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), comp u f = comp v f → u = v
h₁ : comp 0 f = 0
⊢ ker 0 = ⊤
[PROOFSTEP]
exact ker_zero
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p = p'
a b : M
⊢ Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b)
[PROOFSTEP]
subst h
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
a b : M
⊢ Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p = p'
src✝ : Quotient (quotientRel p) ≃ Quotient (quotientRel p') :=
  Quotient.congr (Equiv.refl M) (_ : ∀ (a b : M), Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b))
⊢ ∀ (x y : M ⧸ p), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y
[PROOFSTEP]
rintro ⟨x⟩ ⟨y⟩
[GOAL]
case mk.mk
R : Type u_1
M : Type u_2
r : R
x✝¹ y✝¹ : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p = p'
src✝ : Quotient (quotientRel p) ≃ Quotient (quotientRel p') :=
  Quotient.congr (Equiv.refl M) (_ : ∀ (a b : M), Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b))
x✝ : M ⧸ p
x : M
y✝ : M ⧸ p
y : M
⊢ Equiv.toFun src✝ (Quot.mk Setoid.r x + Quot.mk Setoid.r y) =
    Equiv.toFun src✝ (Quot.mk Setoid.r x) + Equiv.toFun src✝ (Quot.mk Setoid.r y)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p = p'
src✝ : Quotient (quotientRel p) ≃ Quotient (quotientRel p') :=
  Quotient.congr (Equiv.refl M) (_ : ∀ (a b : M), Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b))
⊢ ∀ (r : R) (x : M ⧸ p),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (x y : M ⧸ p), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' := (_ : ∀ (x y : M ⧸ p), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y) }
          x
[PROOFSTEP]
rintro x ⟨y⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝¹ y✝ : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p = p'
src✝ : Quotient (quotientRel p) ≃ Quotient (quotientRel p') :=
  Quotient.congr (Equiv.refl M) (_ : ∀ (a b : M), Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b))
x : R
x✝ : M ⧸ p
y : M
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' := (_ : ∀ (x y : M ⧸ p), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y) }
      (x • Quot.mk Setoid.r y) =
    ↑(RingHom.id R) x •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (x y : M ⧸ p), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y) }
        (Quot.mk Setoid.r y)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' P Q : Submodule R M
hf : map (↑(LinearEquiv.refl R M)) P = Q
⊢ P = Q
[PROOFSTEP]
simpa using hf
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x✝ y✝ : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x y : { x // x ∈ compatibleMaps p q }
⊢ (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y) =
    (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x + (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x✝¹ y✝ : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x y : { x // x ∈ compatibleMaps p q }
x✝ : M
⊢ ↑(LinearMap.comp ((fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y)) (mkQ p)) x✝ =
    ↑(LinearMap.comp
          ((fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x +
            (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y)
          (mkQ p))
      x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x y : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
c : R
f : { x // x ∈ compatibleMaps p q }
⊢ AddHom.toFun
      { toFun := fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q),
        map_add' :=
          (_ :
            ∀ (x y : { x // x ∈ compatibleMaps p q }),
              (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y) =
                (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x +
                  (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y) }
      (c • f) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q),
          map_add' :=
            (_ :
              ∀ (x y : { x // x ∈ compatibleMaps p q }),
                (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y) =
                  (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x +
                    (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y) }
        f
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x y : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
c : R
f : { x // x ∈ compatibleMaps p q }
x✝ : M
⊢ ↑(LinearMap.comp
          (AddHom.toFun
            { toFun := fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q),
              map_add' :=
                (_ :
                  ∀ (x y : { x // x ∈ compatibleMaps p q }),
                    (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y) =
                      (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x +
                        (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y) }
            (c • f))
          (mkQ p))
      x✝ =
    ↑(LinearMap.comp
          (↑(RingHom.id R) c •
            AddHom.toFun
              { toFun := fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q),
                map_add' :=
                  (_ :
                    ∀ (x y : { x // x ∈ compatibleMaps p q }),
                      (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y) =
                        (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x +
                          (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y) }
              f)
          (mkQ p))
      x✝
[PROOFSTEP]
rfl
