-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
private lemma ofTensorProduct_iso [Fintype ι] [IsNoetherianRing R] :
    IsIso (ModuleCat.ofHom (ofTensorProduct I M))

Proof state:
case refine_4
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ Mono (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 4 ⋯)

Tactic:
apply ConcreteCategory.mono_of_injective

Result:
case refine_4.i
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ Function.Injective ⇑(ConcreteCategory.hom (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 4 ⋯))

Proof state:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ IsIso (ModuleCat.ofHom (ofTensorProduct I M))

Tactic:
refine Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
  (firstRow_exact I M f hf) (secondRow_exact I M f hf) (firstRowToSecondRow I M f) ?_ ?_ ?_ ?_

Result:
case refine_1
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ Epi (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 0 ⋯)

case refine_2
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ IsIso (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 1 ⋯)

case refine_3
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ IsIso (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 3 ⋯)

case refine_4
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ Mono (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 4 ⋯)

Proof state:
case refine_1
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ Epi (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 0 ⋯)

Tactic:
apply ConcreteCategory.epi_of_surjective

Result:
case refine_1.s
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ Function.Surjective ⇑(ConcreteCategory.hom (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 0 ⋯))

Proof state:
case refine_3
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ IsIso (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 3 ⋯)

Tactic:
show IsIso (ModuleCat.ofHom 0)

Result:
case refine_3
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ IsIso (ModuleCat.ofHom 0)

Proof state:
case refine_2
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ Function.Bijective ⇑(ConcreteCategory.hom (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 1 ⋯))

Tactic:
exact ofTensorProduct_bijective_of_pi_of_fintype I ι

Result:
no goals

Proof state:
case refine_1.s
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ Function.Surjective ⇑(ConcreteCategory.hom (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 0 ⋯))

Tactic:
exact ofTensorProduct_surjective_of_finite I (LinearMap.ker f)

Result:
no goals

Proof state:
case refine_4.i
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
x y : ↑((AdicCompletion.firstRow I M f).obj' 4 ⋯)
a✝ :
  (ConcreteCategory.hom (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 4 ⋯)) x =
    (ConcreteCategory.hom (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 4 ⋯)) y
⊢ x = y

Tactic:
rfl

Result:
no goals

Proof state:
case refine_4.i
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ Function.Injective ⇑(ConcreteCategory.hom (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 4 ⋯))

Tactic:
intro x y _

Result:
case refine_4.i
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
x y : ↑((AdicCompletion.firstRow I M f).obj' 4 ⋯)
a✝ :
  (ConcreteCategory.hom (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 4 ⋯)) x =
    (ConcreteCategory.hom (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 4 ⋯)) y
⊢ x = y

Proof state:
case refine_2
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ IsIso (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 1 ⋯)

Tactic:
apply (ConcreteCategory.isIso_iff_bijective _).mpr

Result:
case refine_2
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ Function.Bijective ⇑(ConcreteCategory.hom (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 1 ⋯))

Proof state:
case refine_3
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ IsIso (ModuleCat.ofHom 0)

Tactic:
apply Limits.isIso_of_isTerminal
  <;> exact Limits.IsZero.isTerminal (ModuleCat.isZero_of_subsingleton _)

Result:
no goals