ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
⊢ Function.RightInverse
    ↑(piQuotientLift p (pi Set.univ p) single (_ : ∀ (x : ι), p x ≤ comap (single x) (pi Set.univ p)))
    ↑(quotientPiLift p (fun i => mkQ (p i)) (_ : ∀ (i : ι), p i ≤ ker (mkQ (p i))))
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
⊢ Function.RightInverse (invFun p) (toFun p)
dsimp only [toFun, invFun]
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
⊢ ↑(comp (quotientPiLift p (fun i => mkQ (p i)) (_ : ∀ (i : ι), p i ≤ ker (mkQ (p i))))
        (piQuotientLift p (pi Set.univ p) single (_ : ∀ (x : ι), p x ≤ comap (single x) (pi Set.univ p)))) =
    ↑LinearMap.id
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
⊢ Function.RightInverse
    ↑(piQuotientLift p (pi Set.univ p) single (_ : ∀ (x : ι), p x ≤ comap (single x) (pi Set.univ p)))
    ↑(quotientPiLift p (fun i => mkQ (p i)) (_ : ∀ (i : ι), p i ≤ ker (mkQ (p i))))
rw [Function.rightInverse_iff_comp, ← coe_comp, ← @id_coe R]
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
⊢ ↑(comp (quotientPiLift p (fun i => mkQ (p i)) (_ : ∀ (i : ι), p i ≤ ker (mkQ (p i))))
          (piQuotientLift p (pi Set.univ p) single (_ : ∀ (x : ι), p x ≤ comap (single x) (pi Set.univ p))))
      (Pi.single i (Quotient.mk'' x')) j =
    ↑LinearMap.id (Pi.single i (Quotient.mk'' x')) j
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
⊢ ↑(comp (quotientPiLift p (fun i => mkQ (p i)) (_ : ∀ (i : ι), p i ≤ ker (mkQ (p i))))
        (piQuotientLift p (pi Set.univ p) single (_ : ∀ (x : ι), p x ≤ comap (single x) (pi Set.univ p)))) =
    ↑LinearMap.id
refine' congr_arg _ (pi_ext fun i x => Quotient.inductionOn' x fun x' => funext fun j => _)
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
⊢ (fun i_1 => ↑(mkQ (p i_1)) (↑(single i) x' i_1)) j = Pi.single i (Quotient.mk x') j
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
⊢ ↑(comp (quotientPiLift p (fun i => mkQ (p i)) (_ : ∀ (i : ι), p i ≤ ker (mkQ (p i))))
          (piQuotientLift p (pi Set.univ p) single (_ : ∀ (x : ι), p x ≤ comap (single x) (pi Set.univ p))))
      (Pi.single i (Quotient.mk'' x')) j =
    ↑LinearMap.id (Pi.single i (Quotient.mk'' x')) j
rw [comp_apply, piQuotientLift_single, Quotient.mk''_eq_mk, mapQ_apply,
  quotientPiLift_mk, id_apply]
case pos
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
hij : i = j
⊢ Quotient.mk (Pi.single i x' j) = Pi.single i (Quotient.mk x') j

case neg
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
hij : ¬i = j
⊢ Quotient.mk (Pi.single i x' j) = Pi.single i (Quotient.mk x') j
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
⊢ (fun i_1 => ↑(mkQ (p i_1)) (↑(single i) x' i_1)) j = Pi.single i (Quotient.mk x') j
by_cases hij : i = j <;> simp only [mkQ_apply, coe_single]
case pos
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
⊢ Quotient.mk (Pi.single i x' i) = Pi.single i (Quotient.mk x') i
case pos
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
hij : i = j
⊢ Quotient.mk (Pi.single i x' j) = Pi.single i (Quotient.mk x') j
subst hij
no goals
case pos
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
⊢ Quotient.mk (Pi.single i x' i) = Pi.single i (Quotient.mk x') i
rw [Pi.single_eq_same, Pi.single_eq_same]
no goals
case neg
ι : Type u_1
R : Type u_3
inst✝⁸ : CommRing R
Ms : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type ?u.135340
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.135847
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
hij : ¬i = j
⊢ Quotient.mk (Pi.single i x' j) = Pi.single i (Quotient.mk x') j
rw [Pi.single_eq_of_ne (Ne.symm hij), Pi.single_eq_of_ne (Ne.symm hij), Quotient.mk_zero]