awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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)) ⊤]
⊢ 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:
SModEq.add hx1' hx2'

Premises used: SModEq.add
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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)) ⊤]
⊢ 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:
exact SModEq.add hx1' hx2'

Premises used: SModEq.add
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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)) ⊤]
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)) ⊤]
⊢ ∃ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤,
    (f : (a : M) → N) x ≡ 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'

Premises used: pow_succ, smul_smul, SModEq.def, map_add, Submodule.mkQ_apply, LinearMap.coe_comp, Submodule.mkQ, Function.comp_apply, AdicCompletion.smul, Submodule.add, DFunLike.coe, map_smul
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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) ⊤]
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)) ⊤]
⊢ ∃ (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)

Premises used: SModEq.symm, SModEq.sub_mem, AdicCompletion.exists_smodEq_pow_add_one_smul, Iff.mp
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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) ⊤] ∧
    (f : (a : M) → N) (x + z) ≡ y [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:
use x + z
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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) ⊤]
h₂ : (f : (a : M) → N) (x + z) ≡ y [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)) ⊤]

Tactic:
constructor
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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) ⊤]

Tactic:
simpa [SModEq.sub_mem]

Premises used: SModEq.sub_mem
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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)) ⊤]
⊢ (f : (a : M) → N) (x + z) ≡ y [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]

Tactic:
simpa [SModEq.sub_mem, sub_sub_eq_add_sub, add_comm] using hz'

Premises used: SModEq.sub_mem, sub_sub_eq_add_sub, add_comm
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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
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'
⊢ ∃ (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'

Premises used: Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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) ⊤)
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 • ⊤) y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₅ : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
rw₆ rw₇ : y = y
⊢ (f : (a : M) → N) x ≡ y0 [SMOD 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]

Premises used: Submodule.factor_mk, Submodule.pow_smul_top_le, Submodule.mkQ_apply, Nat.le_succ, SModEq
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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) ⊤]

Tactic:
have : f x ≡ y0 [SMOD (I ^ n • ⊤ : Submodule R N)] := by
    rw [SModEq, ← mkQ_apply, ← mkQ_apply, ← factor_mk (pow_smul_top_le I N n.le_succ) y0,
        hy0, hyy', hxy]
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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'
this : (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
obtain :
  ∀ (x' : M) (hxx' : x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤])
    (hx'y0 : (f : (a : M) → N) x' ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]),
    ∃ (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'
⊢ ∃ (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 ⟨x', hxx', hx'y0⟩ :=
    exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top h this

Premises used: AdicCompletion.exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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'
this : (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
x' : M
hxx' : x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
hx'y0 : (f : (a : M) → N) x' ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
right :
  ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((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'

Tactic:
use x', hxx'
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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'
this : (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
x' : M
hxx' : x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
hx'y0 : (f : (a : M) → N) x' ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
right : Submodule.Quotient.mk ((f : (a : M) → N) x') = y'
right₁ right₂ right₃ right₄ : Submodule.Quotient.mk y0 = y'
⊢ ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((f : (a : M) → N) x') = y'

Tactic:
rwa [mkQ_apply, hx'y0]

Premises used: Submodule.mkQ_apply
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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_1 :
  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 : AdicCompletion I N
h :
  ∃ (x : ℕ → M),
    ∀ (n : ℕ),
      x n ≡ x (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
        Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          (Submodule.Quotient.mk ((f : (a : M) → N) (x n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
obtain :
  ∀ (x : ℕ → M)
    (hx :
      ∀ (n : ℕ),
        x n ≡ x (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
          Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
            (Submodule.Quotient.mk ((f : (a : M) → N) (x n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
            ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y :
              N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)),
    ∃ (a : AdicCompletion I M), (map I f : (a : AdicCompletion I M) → AdicCompletion I N) a = y
⊢ ∃ (a : AdicCompletion I M), (map I f : (a : AdicCompletion I M) → AdicCompletion I N) a = y

Tactic:
obtain ⟨x, hx⟩ := h
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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 : AdicCompletion I N
x : ℕ → M
hx :
  ∀ (n : ℕ),
    x n ≡ x (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
        (Submodule.Quotient.mk ((f : (a : M) → N) (x n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
        ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h₁ :
  (map I f : (a : AdicCompletion I M) → AdicCompletion I N)
      ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
        (Subtype.mk (p := fun (f : ℕ → M) ↦ IsAdicCauchy I M f) x ⋯)) =
    y
⊢ ∃ (a : AdicCompletion I M), (map I f : (a : AdicCompletion I M) → AdicCompletion I N) a = y

Tactic:
use AdicCompletion.mk I M ⟨x, fun h ↦
        eq_factor_of_eq_factor_succ (fun _ _ ↦ pow_smul_top_le I M) _ (fun n ↦ (hx n).1) h⟩

Premises used: Submodule.pow_smul_top_le, Submodule.Quotient.mk, AdicCompletion.mk, Submodule.eq_factor_of_eq_factor_succ, Subtype.mk, And.left, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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 : AdicCompletion I N
x : ℕ → M
hx :
  ∀ (n : ℕ),
    x n ≡ x (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
        (Submodule.Quotient.mk ((f : (a : M) → N) (x n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
        ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h₁ :
  ∀ (n : ℕ),
    (↑((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
              ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
                (Subtype.mk (p := fun (f : ℕ → M) ↦ IsAdicCauchy I M f) x ⋯))) :
          (n : ℕ) → N ⧸ I ^ n • ⊤)
        n =
      (↑y : (n : ℕ) → N ⧸ I ^ n • ⊤) n
⊢ (map I f : (a : AdicCompletion I M) → AdicCompletion I N)
      ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
        (Subtype.mk (p := fun (f : ℕ → M) ↦ IsAdicCauchy I M f) x ⋯)) =
    y

Tactic:
ext n