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 : 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) ⊤)
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

Tactic:
simp [hx n]
-- 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
suffices :
  ∃ (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) ⊤)
⊢ ∃ (a : AdicCompletion I M), (map I f : (a : AdicCompletion I M) → AdicCompletion I N) a = y

Tactic:
suffices h : ∃ x : ℕ → M, ∀ n, x n ≡ x (n + 1) [SMOD (I ^ n • ⊤ : Submodule R M)] ∧
      Submodule.Quotient.mk (f (x n)) = eval I _ n y by
    obtain ⟨x, hx⟩ := h
    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⟩
    ext n
    simp [hx n]
-- 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
property :
  Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
    (Submodule.Quotient.mk ((f : (a : M) → N) 0) : N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
    ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y :
      N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
⊢ { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
      ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y :
        N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) }

Tactic:
use 0
-- 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
⊢ Submodule.map (↑(LinearEquiv.refl R N) : N →ₗ[R] N) (HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) = ⊤

Tactic:
simp
-- 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
property :
  Eq (α := HasQuotient.Quotient N (B := Submodule R N) ⊤)
    (((Quotient.equiv (HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) ⊤ (LinearEquiv.refl R N)
              ⋯).toEquiv :
          (a : N ⧸ I ^ 0 • ⊤) → N ⧸ ⊤)
        (Submodule.Quotient.mk ((f : (a : M) → N) 0)) :
      HasQuotient.Quotient N (B := Submodule R N) ⊤)
    (((Quotient.equiv (HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) ⊤ (LinearEquiv.refl R N)
              ⋯).toEquiv :
          (a : N ⧸ I ^ 0 • ⊤) → N ⧸ ⊤)
        ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y) :
      HasQuotient.Quotient N (B := Submodule R N) ⊤)
⊢ Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
    (Submodule.Quotient.mk ((f : (a : M) → N) 0) : N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
    ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y :
      N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)

Tactic:
apply_fun (Submodule.Quotient.equiv (I ^ 0 • ⊤) ⊤ (.refl R N) (by simp)).toEquiv

Premises used: Submodule.Quotient.equiv, HPow.hPow, LinearEquiv.toEquiv, HSMul.hSMul, LinearEquiv.refl, Top.top, OfNat.ofNat
-- 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
⊢ Eq (α := HasQuotient.Quotient N (B := Submodule R N) ⊤)
    (((Quotient.equiv (HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) ⊤ (LinearEquiv.refl R N)
              ⋯).toEquiv :
          (a : N ⧸ I ^ 0 • ⊤) → N ⧸ ⊤)
        (Submodule.Quotient.mk ((f : (a : M) → N) 0)) :
      HasQuotient.Quotient N (B := Submodule R N) ⊤)
    (((Quotient.equiv (HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) ⊤ (LinearEquiv.refl R N)
              ⋯).toEquiv :
          (a : N ⧸ I ^ 0 • ⊤) → N ⧸ ⊤)
        ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y) :
      HasQuotient.Quotient N (B := Submodule R N) ⊤)

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
⊢ Eq (α := HasQuotient.Quotient N (B := Submodule R N) ⊤)
    (((Quotient.equiv (HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) ⊤ (LinearEquiv.refl R N)
              ⋯).toEquiv :
          (a : N ⧸ I ^ 0 • ⊤) → N ⧸ ⊤)
        (Submodule.Quotient.mk ((f : (a : M) → N) 0)) :
      HasQuotient.Quotient N (B := Submodule R N) ⊤)
    (((Quotient.equiv (HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) ⊤ (LinearEquiv.refl R N)
              ⋯).toEquiv :
          (a : N ⧸ I ^ 0 • ⊤) → N ⧸ ⊤)
        ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y) :
      HasQuotient.Quotient N (B := Submodule R N) ⊤)

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
n : ℕ
xn :
  { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : 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) ⊤) }
⊢ Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤)
        ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y) :
      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) ⊤)

Tactic:
simp
-- 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
n : ℕ
xn :
  { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : 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) ⊤) }
succ :
  (z : M) →
    (hz :
        (↑xn : M) ≡ z [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
          Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
            (((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤)
                ((f : (a : M) → N) z) :
              N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
            ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y :
              N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)) →
      { m : M //
        Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
          (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
          ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y :
            N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤) }
⊢ { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
      ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤) }

Tactic:
choose z hz using exists_smodEq_pow_smul_top_and_mkQ_eq h
          (y' := eval _ _ (n + 1) y) (by simp) xn.2

Premises used: AdicCompletion.exists_smodEq_pow_smul_top_and_mkQ_eq, Subtype.property
-- 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
n : ℕ
xn :
  { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : 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) ⊤) }
z : M
hz :
  (↑xn : M) ≡ z [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
    Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
      (((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((f : (a : M) → N) z) :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
      ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
⊢ { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
      ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤) }

Tactic:
exact ⟨z, hz.2⟩
-- 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
n : ℕ
zero :
  { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
      ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y :
        N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) }
succ :
  (n : ℕ) →
    (xn :
        { m : M //
          Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
            (Submodule.Quotient.mk ((f : (a : M) → N) m) : 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) ⊤) }) →
      { m : M //
        Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
          (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
          ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y :
            N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤) }
⊢ { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : 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) ⊤) }

Tactic:
induction n with
    | zero =>
      use 0
      apply_fun (Submodule.Quotient.equiv (I ^ 0 • ⊤) ⊤ (.refl R N) (by simp)).toEquiv
      exact Subsingleton.elim _ _
    | succ n xn =>
      choose z hz using exists_smodEq_pow_smul_top_and_mkQ_eq h
          (y' := eval _ _ (n + 1) y) (by simp) xn.2
      exact ⟨z, hz.2⟩

Premises used: Submodule.Quotient.equiv, HPow.hPow, LinearEquiv.toEquiv, HSMul.hSMul, Submodule.zero, LinearEquiv.refl, Subsingleton.elim, Top.top, OfNat.ofNat
-- 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 : (n : ℕ) →
  { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : 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) ⊤) } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n : ℕ
⊢ Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤)
        ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y) :
      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) ⊤)

Tactic:
simp
-- 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 : (n : ℕ) →
  { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : 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) ⊤) } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∃ (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) ⊤)

Tactic:
exact ⟨fun n ↦ (x n).val, fun n ↦ ⟨(Classical.choose_spec (exists_smodEq_pow_smul_top_and_mkQ_eq
      h (y' := eval I _ (n + 1) y) (by simp) (x n).2)).1, (x n).property⟩⟩
-- 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
inst_5 : IsPrecomplete I M
inst_6 : IsHausdorff I 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
obtain :
  ∀ (x' : AdicCompletion I M)
    (hx' :
      Eq.{u_3 + 1} (α := AdicCompletion I N)
        ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N) x' : AdicCompletion I N)
        ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)),
    ∃ (a : M), (f : (a : M) → N) a = y
⊢ ∃ (a : M), (f : (a : M) → N) a = y

Tactic:
obtain ⟨x', hx'⟩ := AdicCompletion.map_surjective_of_mkQ_comp_surjective h (of I N y)

Premises used: AdicCompletion.of, DFunLike.coe, AdicCompletion.map_surjective_of_mkQ_comp_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
inst_5 : IsPrecomplete I M
inst_6 : IsHausdorff I 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
x' : AdicCompletion I M
hx' :
  Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N) x' : AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
obtain : ∀ (x : M) (hx : (of I M : (a : M) → AdicCompletion I M) x = x'), ∃ (a : M), (f : (a : M) → N) a = y
⊢ ∃ (a : M), (f : (a : M) → N) a = y

Tactic:
obtain ⟨x, hx⟩ := of_surjective I M x'

Premises used: AdicCompletion.of_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
inst_5 : IsPrecomplete I M
inst_6 : IsHausdorff I 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
x' : AdicCompletion I M
hx' :
  Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N) x' : AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
x : M
hx : (of I M : (a : M) → AdicCompletion I M) x = x'
h₁ : (f : (a : M) → N) x = y
⊢ ∃ (a : M), (f : (a : M) → N) a = y

Tactic:
use x
-- 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
inst_5 : IsPrecomplete I M
inst_6 : IsHausdorff I 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
x' : AdicCompletion I M
hx' :
  Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N) x' : AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
x : M
hx : (of I M : (a : M) → AdicCompletion I M) x = x'
h₁ :
  Eq (α := AdicCompletion I N) ((of I N : (a : N) → AdicCompletion I N) ((f : (a : M) → N) x) : AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
h₂ :
  Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N)
        ((of I M : (a : M) → AdicCompletion I M) x) :
      AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
h₃ h₄ h₅ h₆ :
  Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N) x' : AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
⊢ (f : (a : M) → N) x = y

Tactic:
rwa [← of_inj (I := I), ← map_of, hx]

Premises used: AdicCompletion.of_inj, AdicCompletion.map_of
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
S : Type u_6
inst_1 : CommRing S
f : R →+* S
inst_2 : IsPrecomplete I R
haus : IsHausdorff (R := S) (Ideal.map f I) S
h :
  Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β := HasQuotient.Quotient S (B := Ideal S) (Ideal.map f I))
    (⇑(RingHom.comp (Ideal.Quotient.mk (Ideal.map f I)) f) : (a : R) → S ⧸ Ideal.map f I)
x : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := AlgHom.toLinearMap (Algebra.ofId R S)
⊢ Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β :=
    HasQuotient.Quotient S (B := Submodule R S) (restrictScalars R (Ideal.map f I)))
    (⇑(mkQ (restrictScalars R (Ideal.map f I)) ∘ₗ fₗ) : (a : R) → S ⧸ restrictScalars R (Ideal.map f I))

Tactic:
change Function.Surjective ((restrictScalars R (I.map f)).mkQ ∘ₗ fₗ) at h

Premises used: Submodule.restrictScalars, Ideal.map, LinearMap.comp, Submodule.mkQ, DFunLike.coe, Function.Surjective
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
S : Type u_6
inst_1 : CommRing S
f : R →+* S
inst_2 : IsPrecomplete I R
haus : IsHausdorff (R := S) (Ideal.map f I) S
x : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := AlgHom.toLinearMap (Algebra.ofId R S)
h :
  Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β :=
    HasQuotient.Quotient S (B := Submodule R S) (restrictScalars R (Ideal.map f I)))
    (⇑(mkQ (restrictScalars R (Ideal.map f I)) ∘ₗ fₗ) : (a : R) → S ⧸ restrictScalars R (Ideal.map f I))
simp : Eq.{u_6 + 1} (α := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I) (Ideal.map f I)
⊢ HSMul.hSMul (β := Submodule R S) I ⊤ = restrictScalars R (Ideal.map f I)

Tactic:
simp only [Ideal.smul_top_eq_map, restrictScalars_inj]

Premises used: Ideal.smul_top_eq_map, Submodule.restrictScalars_inj