awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y2 : N
hy2 : y2 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
ih1 :
  ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y1 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
ih2 :
  ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have add : ∀ (x1 : M) (hx1 : x1 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
  (hx1' : (f : (a : M) → N) x1 ≡ y1 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]),
  ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
Tactic: obtain ⟨x1, hx1, hx1'⟩ := ih1
Cleared hypotheses: ih1
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y2 : N
hy2 : y2 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
ih2 :
  ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
x1 : M
hx1 : x1 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hx1' : (f : (a : M) → N) x1 ≡ y1 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have add : ∀ (x2 : M) (hx2 : x2 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
  (hx2' : (f : (a : M) → N) x2 ≡ y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]),
  ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
Tactic: obtain ⟨x2, hx2, hx2'⟩ := ih2
Cleared hypotheses: ih2
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y2 : N
hy2 : y2 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
x1 : M
hx1 : x1 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hx1' : (f : (a : M) → N) x1 ≡ y1 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
x2 : M
hx2 : x2 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hx2' : (f : (a : M) → N) x2 ≡ y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have right : (f : (a : M) → N) (x1 + x2) ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
Tactic: use x1 + x2, add_mem hx1 hx2
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y2 : N
hy2 : y2 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
x1 : M
hx1 : x1 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hx1' : (f : (a : M) → N) x1 ≡ y1 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
x2 : M
hx2 : x2 ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hx2' : (f : (a : M) → N) x2 ≡ y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ (f : (a : M) → N) (x1 + x2) ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have right : HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x1 : N) ((f : (a : M) → N) x2 : N) ≡ y1 + y2 [SMOD
  HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
Tactic: simp only [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
n : ℕ
hy : y ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have smul : ∀ (r : R) (hr : r ∈ I ^ n) (y : N),
  Membership.mem (γ := Submodule R N) ⊤ y →
    ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
      (f : (a : M) → N) x ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
Tactic: induction hy using smul_induction_on' with
  | smul r hr y _ =>
    obtain ⟨x, hx⟩ := h (mkQ _ y)
    use r • x, smul_mem_smul hr mem_top
    simp only [coe_comp, Function.comp_apply, mkQ_apply, ← SModEq.def, map_smul] at ⊢ hx
    rw [pow_succ, ← smul_smul]
    exact SModEq.smul' hx hr
  | add y1 hy1 y2 hy2 ih1 ih2 =>
    obtain ⟨x1, hx1, hx1'⟩ := ih1
    obtain ⟨x2, hx2, hx2'⟩ := ih2
    use x1 + x2, add_mem hx1 hx2
    simp only [map_add]
    exact SModEq.add hx1' hx2'
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
n : ℕ
hy : y ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
smul :
  ∀ (r : R) (hr : r ∈ I ^ n) (y : N),
    Membership.mem (γ := Submodule R N) ⊤ y →
      ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
        (f : (a : M) → N) x ≡ r • y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have add : ∀ (y1 : N) (hy1 : y1 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) (y2 : N)
  (hy2 : y2 ∈ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  (ih1 :
    ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
      (f : (a : M) → N) x ≡ y1 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤])
  (ih2 :
    ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
      (f : (a : M) → N) x ≡ y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]),
  ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ y1 + y2 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
Tactic: induction hy using smul_induction_on' with
  | smul r hr y _ =>
    obtain ⟨x, hx⟩ := h (mkQ _ y)
    use r • x, smul_mem_smul hr mem_top
    simp only [coe_comp, Function.comp_apply, mkQ_apply, ← SModEq.def, map_smul] at ⊢ hx
    rw [pow_succ, ← smul_smul]
    exact SModEq.smul' hx hr
  | add y1 hy1 y2 hy2 ih1 ih2 =>
    obtain ⟨x1, hx1, hx1'⟩ := ih1
    obtain ⟨x2, hx2, hx2'⟩ := ih2
    use x1 + x2, add_mem hx1 hx2
    simp only [map_add]
    exact SModEq.add hx1' hx2'
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
y : N
n : ℕ
hxy : (f : (a : M) → N) x ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
⊢ ∃ (x' : M),
    x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      (f : (a : M) → N) x' ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have obtain : ∀ (z : M) (hz : z ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
  (hz' :
    (f : (a : M) → N) z ≡ HSub.hSub (β := N) y ((f : (a : M) → N) x : N) [SMOD
      HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]),
  ∃ (x' : M),
    x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      (f : (a : M) → N) x' ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
Tactic: obtain ⟨z, hz, hz'⟩ :=
    exists_smodEq_pow_add_one_smul h (y := y - f x) (SModEq.sub_mem.mp hxy.symm)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
y : N
n : ℕ
hxy : (f : (a : M) → N) x ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hz' :
  (f : (a : M) → N) z ≡ HSub.hSub (β := N) y ((f : (a : M) → N) x : N) [SMOD
    HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ∃ (x' : M),
    x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      (f : (a : M) → N) x' ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have h₁ : x ≡ x + z [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
  (f : (a : M) → N) (x + z) ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
Tactic: use x + z
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
y : N
n : ℕ
hxy : (f : (a : M) → N) x ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hz' :
  (f : (a : M) → N) z ≡ HSub.hSub (β := N) y ((f : (a : M) → N) x : N) [SMOD
    HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ x ≡ x + z [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
    (f : (a : M) → N) (x + z) ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have h₁ : x ≡ x + z [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
y : N
n : ℕ
hxy : (f : (a : M) → N) x ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hz' :
  (f : (a : M) → N) z ≡ HSub.hSub (β := N) y ((f : (a : M) → N) x : N) [SMOD
    HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
h₁ : x ≡ x + z [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ x ≡ x + z [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
    (f : (a : M) → N) (x + z) ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
have h₂ : (f : (a : M) → N) (x + z) ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
⊢ ∃ (x' : M),
    x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((f : (a : M) → N) x') =
        y'
have obtain : ∀ (y0 : N) (hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'),
  ∃ (x' : M),
    x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((f : (a : M) → N) x') =
        y'
Tactic: obtain ⟨y0, hy0⟩ := mkQ_surjective _ y'
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
y0 : N
hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'
⊢ (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
have rw : Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  (Submodule.Quotient.mk ((f : (a : M) → N) x) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  (Submodule.Quotient.mk y0 : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
Tactic: rw [SModEq, ← mkQ_apply, ← mkQ_apply, ← factor_mk (pow_smul_top_le I N n.le_succ) y0,
        hy0, hyy', hxy]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
y0 : N
hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'
rw :
  Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((f : (a : M) → N) x) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk y0 : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
have rw₁ : Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
    N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  (Submodule.Quotient.mk y0 : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
Tactic: rw [SModEq, ← mkQ_apply, ← mkQ_apply, ← factor_mk (pow_smul_top_le I N n.le_succ) y0,
        hy0, hyy', hxy]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
y0 : N
hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'
rw :
  Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((f : (a : M) → N) x) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk y0 : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₁ :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk y0 : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
have rw₂ : Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
    N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) y0 :
    N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
Tactic: rw [SModEq, ← mkQ_apply, ← mkQ_apply, ← factor_mk (pow_smul_top_le I N n.le_succ) y0,
        hy0, hyy', hxy]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
y0 : N
hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'
rw :
  Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((f : (a : M) → N) x) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk y0 : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₁ :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk y0 : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₂ :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) y0 :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
have rw₃ : Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
    N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  ((factor sorry : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤)
      (((HSMul.hSMul (β := Submodule R N) (I ^ n.succ) ⊤).mkQ : (a : N) → N ⧸ I ^ n.succ • ⊤) y0) :
    N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
Tactic: rw [SModEq, ← mkQ_apply, ← mkQ_apply, ← factor_mk (pow_smul_top_le I N n.le_succ) y0,
        hy0, hyy', hxy]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
y0 : N
hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'
rw :
  Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((f : (a : M) → N) x) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk y0 : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₁ :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk y0 : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₂ :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) y0 :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₃ :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤)
        (((HSMul.hSMul (β := Submodule R N) (I ^ n.succ) ⊤).mkQ : (a : N) → N ⧸ I ^ n.succ • ⊤) y0) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
have rw₄ : Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
    N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  ((factor sorry : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
Tactic: rw [SModEq, ← mkQ_apply, ← mkQ_apply, ← factor_mk (pow_smul_top_le I N n.le_succ) y0,
        hy0, hyy', hxy]