ι : 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.124946
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.125453
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ invFun p (toFun p (Quotient.mk x')) = Quotient.mk x'
ι : 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.124946
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.125453
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ invFun p (toFun p (Quotient.mk'' x')) = Quotient.mk'' x'
rw [Quotient.mk''_eq_mk x']
ι : 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.124946
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.125453
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ ↑(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)))) (Quotient.mk x')) =
    Quotient.mk x'
ι : 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.124946
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.125453
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ invFun p (toFun p (Quotient.mk x')) = Quotient.mk x'
dsimp only [toFun, invFun]
no goals
ι : 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.124946
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.125453
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ ↑(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)))) (Quotient.mk x')) =
    Quotient.mk x'
rw [quotientPiLift_mk p, funext fun i => (mkQ_apply (p i) (x' i)), piQuotientLift_mk p,
  lsum_single, id_apply]