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

Proof state:
case h.isTrue
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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
h✝ : j = i
⊢ Submodule.Quotient.mk (Eq.recOn h✝ (↑x n)) = ↑(Eq.recOn h✝ ((mk I (M j)) x)) n

Tactic:
next h => subst h; simp

Result:
no goals

Proof state:
case h.isFalse
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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
h✝ : ¬j = i
⊢ Submodule.Quotient.mk 0 = ↑0 n

Tactic:
simp

Result:
no goals

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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
h : j = i
⊢ Submodule.Quotient.mk (Eq.recOn h (↑x n)) = ↑(Eq.recOn h ((mk I (M j)) x)) n

Tactic:
subst h

Result:
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 ι
j : ι
x : AdicCauchySequence I (M j)
n : ℕ
⊢ Submodule.Quotient.mk (Eq.recOn ⋯ (↑x n)) = ↑(Eq.recOn ⋯ ((mk I (M j)) x)) 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 ι
⊢ sumInv I M ∘ₗ sum I M = LinearMap.id

Tactic:
ext j x : 2

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 ι
j : ι
x : AdicCauchySequence I (M j)
⊢ ((sumInv I M ∘ₗ sum I M) ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x) =
    (LinearMap.id ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x)

Proof state:
case 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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
⊢ Submodule.Quotient.mk ((component R ι M i) ((lof R ι M j) (↑x n))) =
    ↑((component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i)
          ((lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x)))
      n

Tactic:
rw [DirectSum.component.of, DirectSum.component.of]

Result:
case 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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
⊢ Submodule.Quotient.mk (if h : j = i then Eq.recOn h (↑x n) else 0) =
    ↑(if h : j = i then Eq.recOn h ((mk I (M j)) x) else 0) 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 ι
j : ι
x : AdicCauchySequence I (M j)
n : ℕ
⊢ Submodule.Quotient.mk (Eq.recOn ⋯ (↑x n)) = ↑(Eq.recOn ⋯ ((mk I (M j)) x)) n

Tactic:
simp

Result:
no goals

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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
⊢ (component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i)
      (((sumInv I M ∘ₗ sum I M) ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x)) =
    (component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i)
      ((LinearMap.id ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x))

Tactic:
ext n

Result:
case 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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
⊢ ↑((component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i)
          (((sumInv I M ∘ₗ sum I M) ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j)
            ((mk I (M j)) x)))
      n =
    ↑((component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i)
          ((LinearMap.id ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x)))
      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 ι
j : ι
x : AdicCauchySequence I (M j)
⊢ ((sumInv I M ∘ₗ sum I M) ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x) =
    (LinearMap.id ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x)

Tactic:
apply DirectSum.ext_component (AdicCompletion I R) (fun i ↦ ?_)

Result:
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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
⊢ (component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i)
      (((sumInv I M ∘ₗ sum I M) ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x)) =
    (component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i)
      ((LinearMap.id ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x))

Proof state:
case 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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
⊢ ↑((component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i)
          (((sumInv I M ∘ₗ sum I M) ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j)
            ((mk I (M j)) x)))
      n =
    ↑((component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i)
          ((LinearMap.id ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x)))
      n

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, sum_lof, map_mk, component_sumInv,
  mk_apply_coe, AdicCauchySequence.map_apply_coe, Submodule.mkQ_apply, LinearMap.id_comp]

Result:
case 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 ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
⊢ Submodule.Quotient.mk ((component R ι M i) ((lof R ι M j) (↑x n))) =
    ↑((component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i)
          ((lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x)))
      n