-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem sum_comp_sumInv : sum I M ∘ₗ sumInv I M = LinearMap.id

Proof state:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ (I ^ n • ⊤).mkQ (∑ x : ι, (lof R ι M x) ((component R ι M x) (↑f n))) = (I ^ n • ⊤).mkQ (↑f n)

Tactic:
erw [DirectSum.sum_univ_of]

Result:
no goals

Proof state:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ↑((sum I M ∘ₗ sumInv I M) ((mk I (⨁ (j : ι), M j)) f)) n = ↑(LinearMap.id ((mk I (⨁ (j : ι), M j)) f)) n

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq, mk_apply_coe,
  Submodule.mkQ_apply]

Result:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ↑((sum I M) ((sumInv I M) ((mk I (⨁ (j : ι), M j)) f))) n = Submodule.Quotient.mk (↑f n)

Proof state:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ↑((sum I M) ((sumInv I M) ((mk I (⨁ (j : ι), M j)) f))) n = Submodule.Quotient.mk (↑f n)

Tactic:
rw [← DirectSum.sum_univ_of (((sumInv I M) ((AdicCompletion.mk I (⨁ (j : ι), M j)) f)))]

Result:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ↑((sum I M)
          (∑ i : ι, (DirectSum.of (fun i => AdicCompletion I (M i)) i) (((sumInv I M) ((mk I (⨁ (j : ι), M j)) f)) i)))
      n =
    Submodule.Quotient.mk (↑f n)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ sum I M ∘ₗ sumInv I M = LinearMap.id

Tactic:
ext f n

Result:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ↑((sum I M ∘ₗ sumInv I M) ((mk I (⨁ (j : ι), M j)) f)) n = ↑(LinearMap.id ((mk I (⨁ (j : ι), M j)) f)) n

Proof state:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ↑((sum I M)
          (∑ i : ι, (DirectSum.of (fun i => AdicCompletion I (M i)) i) (((sumInv I M) ((mk I (⨁ (j : ι), M j)) f)) i)))
      n =
    Submodule.Quotient.mk (↑f n)

Tactic:
simp only [sumInv_apply, map_mk, map_sum, sum_of, val_sum_apply, mk_apply_coe,
  AdicCauchySequence.map_apply_coe, Submodule.mkQ_apply]

Result:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ∑ x : ι, Submodule.Quotient.mk ((lof R ι M x) ((component R ι M x) (↑f n))) = Submodule.Quotient.mk (↑f n)

Proof state:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ∑ x : ι, Submodule.Quotient.mk ((lof R ι M x) ((component R ι M x) (↑f n))) = Submodule.Quotient.mk (↑f n)

Tactic:
simp only [← Submodule.mkQ_apply, ← map_sum]

Result:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ (I ^ n • ⊤).mkQ (∑ x : ι, (lof R ι M x) ((component R ι M x) (↑f n))) = (I ^ n • ⊤).mkQ (↑f n)