-- Mathlib/RingTheory/AdicCompletion/Exactness.lean
theorem map_surjective (hf : Function.Surjective f) : Function.Surjective (map I f) := fun y ↦ by
  apply AdicCompletion.induction_on I N y (fun b ↦ ?_)
  let a := mapPreimage hf b
  refine ⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩
  · refine fun n ↦ SModEq.symm ?_
    simp only [SModEq.symm, SModEq, mapPreimage, Submodule.Quotient.mk_sub,
      sub_eq_self, Submodule.Quotient.mk_eq_zero, SetLike.coe_mem, a]
  · exact _root_.AdicCompletion.ext fun n ↦ congrArg _ ((a n).property)

Proof state:
case refine_1
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := AdicCompletion.mapPreimage hf b
⊢ ∀ (n : ℕ), (fun n => ↑(a n)) n ≡ (fun n => ↑(a n)) (n + 1) [SMOD I ^ n • ⊤]

Tactic:
refine fun n ↦ SModEq.symm ?_

Result:
case refine_1
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := AdicCompletion.mapPreimage hf b
n : ℕ
⊢ (fun n => ↑(a n)) (n + 1) ≡ (fun n => ↑(a n)) n [SMOD I ^ n • ⊤]

Proof state:
case refine_2
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := AdicCompletion.mapPreimage hf b
⊢ (map I f) ((mk I M) (AdicCauchySequence.mk I M (fun n => ↑(a n)) ⋯)) = (mk I N) b

Tactic:
exact _root_.AdicCompletion.ext fun n ↦ congrArg _ ((a n).property)

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := AdicCompletion.mapPreimage hf b
⊢ ∃ a, (map I f) a = (mk I N) b

Tactic:
refine ⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩

Result:
case refine_1
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := AdicCompletion.mapPreimage hf b
⊢ ∀ (n : ℕ), (fun n => ↑(a n)) n ≡ (fun n => ↑(a n)) (n + 1) [SMOD I ^ n • ⊤]

case refine_2
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := AdicCompletion.mapPreimage hf b
⊢ (map I f) ((mk I M) (AdicCauchySequence.mk I M (fun n => ↑(a n)) ?refine_1)) = (mk I N) b

Proof state:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
⊢ ∃ a, (map I f) a = (mk I N) b

Tactic:
let a := mapPreimage hf b

Result:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := AdicCompletion.mapPreimage hf b
⊢ ∃ a, (map I f) a = (mk I N) b

Proof state:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
⊢ ∃ a, (map I f) a = y

Tactic:
apply AdicCompletion.induction_on I N y (fun b ↦ ?_)

Result:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
⊢ ∃ a, (map I f) a = (mk I N) b

Proof state:
case refine_1
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := AdicCompletion.mapPreimage hf b
n : ℕ
⊢ (fun n => ↑(a n)) (n + 1) ≡ (fun n => ↑(a n)) n [SMOD I ^ n • ⊤]

Tactic:
simp only [SModEq.symm, SModEq, mapPreimage, Submodule.Quotient.mk_sub,
  sub_eq_self, Submodule.Quotient.mk_eq_zero, SetLike.coe_mem, a]

Result:
no goals