-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
private lemma secondRow_exact [Fintype ι] [IsNoetherianRing R] : (secondRow I M f).Exact where
  zero
    | 0, _ => ModuleCat.hom_ext (adic_exact I M f hf).linearMap_comp_eq_zero
    | 1, _ => ModuleCat.hom_ext (LinearMap.zero_comp (map I f))
    | 2, _ => ModuleCat.hom_ext (LinearMap.zero_comp 0)
  exact k _

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
k : ℕ
x✝ : autoParam (2 + 2 ≤ 4) _auto✝
⊢ ∀ (x₂ : ↑((AdicCompletion.secondRow I M f).sc ⋯ 2 ⋯).X₂),
    (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 2 ⋯).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 2 ⋯).f) x₁ = x₂

Tactic:
intro _ _

Result:
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
k : ℕ
x✝¹ : autoParam (2 + 2 ≤ 4) _auto✝
x₂✝ : ↑((AdicCompletion.secondRow I M f).sc ⋯ 2 ⋯).X₂
x✝ : (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 2 ⋯).g) x₂✝ = 0
⊢ ∃ x₁, (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 2 ⋯).f) x₁ = x₂✝

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
k : ℕ
x✝ : autoParam (1 + 2 ≤ 4) _auto✝
⊢ ∀ (x₂ : ↑((AdicCompletion.secondRow I M f).sc ⋯ 1 ⋯).X₂),
    (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 1 ⋯).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 1 ⋯).f) x₁ = x₂

Tactic:
intro x _

Result:
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
k : ℕ
x✝¹ : autoParam (1 + 2 ≤ 4) _auto✝
x : ↑((AdicCompletion.secondRow I M f).sc ⋯ 1 ⋯).X₂
x✝ : (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 1 ⋯).g) x = 0
⊢ ∃ x₁, (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 1 ⋯).f) x₁ = x

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
k : ℕ
x✝ : autoParam (k + 2 ≤ 4) _auto✝
⊢ ∀ (x₂ : ↑((AdicCompletion.secondRow I M f).sc ⋯ k ⋯).X₂),
    (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ k ⋯).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ k ⋯).f) x₁ = x₂

Tactic:
match k with
| 0 => intro x hx; exact (adic_exact I M f hf x).mp hx
| 1 => intro x _; exact (adic_surj I M f hf) x
| 2 => intro _ _; exact ⟨0, rfl⟩

Result:
no goals

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
k : ℕ
x✝¹ : autoParam (1 + 2 ≤ 4) _auto✝
x : ↑((AdicCompletion.secondRow I M f).sc ⋯ 1 ⋯).X₂
x✝ : (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 1 ⋯).g) x = 0
⊢ ∃ x₁, (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 1 ⋯).f) x₁ = x

Tactic:
exact (adic_surj I M f hf) x

Result:
no goals

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
k : ℕ
x✝ : autoParam (0 + 2 ≤ 4) _auto✝
x : ↑((AdicCompletion.secondRow I M f).sc ⋯ 0 ⋯).X₂
hx : (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 0 ⋯).g) x = 0
⊢ ∃ x₁, (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 0 ⋯).f) x₁ = x

Tactic:
exact (adic_exact I M f hf x).mp hx

Result:
no goals

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
k : ℕ
x✝ : autoParam (k + 2 ≤ 4) _auto✝
⊢ ((AdicCompletion.secondRow I M f).sc ⋯ k ⋯).Exact

Tactic:
rw [ShortComplex.moduleCat_exact_iff]

Result:
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
k : ℕ
x✝ : autoParam (k + 2 ≤ 4) _auto✝
⊢ ∀ (x₂ : ↑((AdicCompletion.secondRow I M f).sc ⋯ k ⋯).X₂),
    (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ k ⋯).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ k ⋯).f) x₁ = x₂

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
k : ℕ
x✝¹ : autoParam (2 + 2 ≤ 4) _auto✝
x₂✝ : ↑((AdicCompletion.secondRow I M f).sc ⋯ 2 ⋯).X₂
x✝ : (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 2 ⋯).g) x₂✝ = 0
⊢ ∃ x₁, (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 2 ⋯).f) x₁ = x₂✝

Tactic:
exact ⟨0, rfl⟩

Result:
no goals

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
k : ℕ
x✝ : autoParam (0 + 2 ≤ 4) _auto✝
⊢ ∀ (x₂ : ↑((AdicCompletion.secondRow I M f).sc ⋯ 0 ⋯).X₂),
    (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 0 ⋯).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 0 ⋯).f) x₁ = x₂

Tactic:
intro x hx

Result:
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
k : ℕ
x✝ : autoParam (0 + 2 ≤ 4) _auto✝
x : ↑((AdicCompletion.secondRow I M f).sc ⋯ 0 ⋯).X₂
hx : (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 0 ⋯).g) x = 0
⊢ ∃ x₁, (ConcreteCategory.hom ((AdicCompletion.secondRow I M f).sc ⋯ 0 ⋯).f) x₁ = x