-- Mathlib/LinearAlgebra/Quotient/Pi.lean
theorem right_inv : Function.RightInverse (invFun p) (toFun p)

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
⊢ (quotientPiLift p (fun i => (p i).mkQ) ⋯ ∘ₗ piQuotientLift p (pi Set.univ p) (single R Ms) ⋯)
      (Pi.single i (Quotient.mk x')) j =
    LinearMap.id (Pi.single i (Quotient.mk x')) j

Tactic:
rw [comp_apply, piQuotientLift_single, mapQ_apply,
  quotientPiLift_mk, id_apply]

Result:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
⊢ (fun i_1 => (p i_1).mkQ ((single R Ms i) x' i_1)) j = Pi.single i (Quotient.mk x') j

Proof state:
case neg
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
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

Tactic:
rw [Pi.single_eq_of_ne (Ne.symm hij), Pi.single_eq_of_ne (Ne.symm hij), Quotient.mk_zero]

Result:
no goals

Proof state:
case pos
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
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

Tactic:
subst hij

Result:
case pos
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : Ms i ⧸ p i
x' : Ms i
⊢ Quotient.mk (Pi.single i x' i) = Pi.single i (Quotient.mk x') i

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Function.RightInverse (invFun p) (toFun p)

Tactic:
dsimp only [toFun, invFun]

Result:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Function.RightInverse ⇑(piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) ⇑(quotientPiLift p (fun i => (p i).mkQ) ⋯)

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
⊢ (fun i_1 => (p i_1).mkQ ((single R Ms i) x' i_1)) j = Pi.single i (Quotient.mk x') j

Tactic:
by_cases hij : i = j <;> simp only [mkQ_apply, coe_single]

Result:
case pos
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
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_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
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

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ⇑(quotientPiLift p (fun i => (p i).mkQ) ⋯ ∘ₗ piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) = ⇑LinearMap.id

Tactic:
refine congr_arg _ (pi_ext fun i x => Submodule.Quotient.induction_on _ x fun x' =>
  funext fun j => ?_)

Result:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
⊢ (quotientPiLift p (fun i => (p i).mkQ) ⋯ ∘ₗ piQuotientLift p (pi Set.univ p) (single R Ms) ⋯)
      (Pi.single i (Quotient.mk x')) j =
    LinearMap.id (Pi.single i (Quotient.mk x')) j

Proof state:
case pos
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : Ms i ⧸ p i
x' : Ms i
⊢ Quotient.mk (Pi.single i x' i) = Pi.single i (Quotient.mk x') i

Tactic:
rw [Pi.single_eq_same, Pi.single_eq_same]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Function.RightInverse ⇑(piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) ⇑(quotientPiLift p (fun i => (p i).mkQ) ⋯)

Tactic:
rw [Function.rightInverse_iff_comp, ← coe_comp, ← @id_coe R]

Result:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ⇑(quotientPiLift p (fun i => (p i).mkQ) ⋯ ∘ₗ piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) = ⇑LinearMap.id