awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsHausdorff I M
x : M
hx : x = 0
⊢ Eq (α := AdicCompletion I M) ((of I M : (a : M) → AdicCompletion I M) x : AdicCompletion I M) (0 : AdicCompletion I M)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsHausdorff I M
x : M
mpr :
  ∀
    (hx :
      Eq (α := AdicCompletion I M) ((of I M : (a : M) → AdicCompletion I M) x : AdicCompletion I M)
        (0 : AdicCompletion I M))
    (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ Eq (α := AdicCompletion I M) ((of I M : (a : M) → AdicCompletion I M) x : AdicCompletion I M)
      (0 : AdicCompletion I M) ↔
    x = 0

Tactic:
refine ⟨fun hx ↦ h.haus x fun n ↦ ?_, fun hx ↦ by simp [hx]⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsHausdorff I M
x : M
hx :
  Eq (α := AdicCompletion I M) ((of I M : (a : M) → AdicCompletion I M) x : AdicCompletion I M) (0 : AdicCompletion I M)
n : ℕ
mpr :
  ∀
    (hx :
      Eq.{u_4 + 1} (α := (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
        (↑((of I M : (a : M) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤) (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤))
    (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
rw [Subtype.ext_iff] at hx

Premises used: Subtype.ext_iff
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsHausdorff I M
x : M
hx :
  Eq.{u_4 + 1} (α := (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (↑((of I M : (a : M) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤) (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤)
n : ℕ
⊢ x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
simpa [SModEq.zero] using congrFun hx n

Premises used: SModEq.zero, congrFun
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsHausdorff I M
⊢ Function.Injective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)

Tactic:
of_injective_iff.mpr ‹_›

Premises used: Iff.mpr, AdicCompletion.of_injective_iff
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsHausdorff I M
a b : M
⊢ Eq (α := AdicCompletion I M) ((of I M : (a : M) → AdicCompletion I M) a : AdicCompletion I M)
      ((of I M : (a : M) → AdicCompletion I M) b : AdicCompletion I M) ↔
    a = b

Tactic:
(of_injective I M).eq_iff

Premises used: Function.Injective.eq_iff, AdicCompletion.of_injective
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
mp :
  Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M) → IsPrecomplete I M
mpr :
  IsPrecomplete I M → Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)
⊢ Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M) ↔ IsPrecomplete I M

Tactic:
constructor
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M) → IsPrecomplete I M

Tactic:
fun h ↦ ⟨fun f hmn ↦ ?_⟩

Premises used: IsPrecomplete.mk
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
mp :
  ∀ (h : Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)) (f : ℕ → M)
    (hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]),
    ∃ (L : M), ∀ (n : ℕ), f n ≡ L [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M) → IsPrecomplete I M

Tactic:
refine fun h ↦ ⟨fun f hmn ↦ ?_⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
u : AdicCompletion I M :=
  Subtype.mk (p := fun (f : (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (n : ℕ) ↦ Submodule.Quotient.mk (f n)) ⋯
mp :
  ∀ (x : M) (hx : (of I M : (a : M) → AdicCompletion I M) x = u),
    ∃ (L : M), ∀ (n : ℕ), f n ≡ L [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ ∃ (L : M), ∀ (n : ℕ), f n ≡ L [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
obtain ⟨x, hx⟩ := h u
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
u : AdicCompletion I M :=
  Subtype.mk (p := fun (f : (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (n : ℕ) ↦ Submodule.Quotient.mk (f n)) ⋯
x : M
hx : (of I M : (a : M) → AdicCompletion I M) x = u
⊢ ∃ (L : M), ∀ (n : ℕ), f n ≡ L [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
⟨x, fun n ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
u : AdicCompletion I M :=
  Subtype.mk (p := fun (f : (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (n : ℕ) ↦ Submodule.Quotient.mk (f n)) ⋯
x : M
hx : (of I M : (a : M) → AdicCompletion I M) x = u
mp : ∀ (n : ℕ), f n ≡ x [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ ∃ (L : M), ∀ (n : ℕ), f n ≡ L [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
refine ⟨x, fun n ↦ ?_⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
u : AdicCompletion I M :=
  Subtype.mk (p := fun (f : (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (n : ℕ) ↦ Submodule.Quotient.mk (f n)) ⋯
x : M
hx : (of I M : (a : M) → AdicCompletion I M) x = u
n : ℕ
mp :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) (Submodule.Quotient.mk (f n))
    ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤) u)
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) (Submodule.Quotient.mk (f n)) (Submodule.Quotient.mk x)

Tactic:
rw [← mkQ_apply _ x, ← eval_of, hx]

Premises used: Submodule.mkQ_apply, AdicCompletion.eval_of
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
u : AdicCompletion I M :=
  Subtype.mk (p := fun (f : (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (n : ℕ) ↦ Submodule.Quotient.mk (f n)) ⋯
x : M
hx : (of I M : (a : M) → AdicCompletion I M) x = u
n : ℕ
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) (Submodule.Quotient.mk (f n))
    ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤) u)

Tactic:
simp [u]
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
mpr :
  ∀ (x : (n : ℕ) → M) (hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = (↑u : (n : ℕ) → M ⧸ I ^ n • ⊤) n),
    ∃ (a : M), (of I M : (a : M) → AdicCompletion I M) a = u
⊢ ∃ (a : M), (of I M : (a : M) → AdicCompletion I M) a = u

Tactic:
choose x hx using (fun n ↦ Submodule.Quotient.mk_surjective (I ^ n • ⊤ : Submodule R M) (u.1 n))

Premises used: HPow.hPow, Submodule.Quotient.mk_surjective, HSMul.hSMul, Top.top, Subtype.val
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : (n : ℕ) → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = (↑u : (n : ℕ) → M ⧸ I ^ n • ⊤) n
m n : ℕ
hmn : m ≤ n
rw :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (Submodule.Quotient.mk (x n)) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    (Submodule.Quotient.mk (x n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
⊢ x m ≡ x n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
rw [SModEq, hx, ← u.2 hmn, ← hx]

Premises used: SModEq, Subtype.property
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : (n : ℕ) → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = (↑u : (n : ℕ) → M ⧸ I ^ n • ⊤) n
m n : ℕ
hmn : m ≤ n
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (Submodule.Quotient.mk (x n)) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    (Submodule.Quotient.mk (x n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : (n : ℕ) → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = (↑u : (n : ℕ) → M ⧸ I ^ n • ⊤) n
mpr :
  ∀ (a : M) (ha : ∀ (n : ℕ), x n ≡ a [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]),
    ∃ (a : M), (of I M : (a : M) → AdicCompletion I M) a = u
⊢ ∃ (a : M), (of I M : (a : M) → AdicCompletion I M) a = u

Tactic:
obtain ⟨a, ha⟩ := h.prec (f := x) (fun hmn ↦ by rw [SModEq, hx, ← u.2 hmn, ← hx]; simp)

Premises used: IsPrecomplete.prec
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : (n : ℕ) → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = (↑u : (n : ℕ) → M ⧸ I ^ n • ⊤) n
a : M
ha : ∀ (n : ℕ), x n ≡ a [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
h₁ : (of I M : (a : M) → AdicCompletion I M) a = u
⊢ ∃ (a : M), (of I M : (a : M) → AdicCompletion I M) a = u

Tactic:
use a
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : (n : ℕ) → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = (↑u : (n : ℕ) → M ⧸ I ^ n • ⊤) n
a : M
ha : ∀ (n : ℕ), x n ≡ a [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
h₁ :
  ∀ (n : ℕ),
    (↑((of I M : (a : M) → AdicCompletion I M) a) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑u : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ (of I M : (a : M) → AdicCompletion I M) a = u

Tactic:
ext n
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : (n : ℕ) → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = (↑u : (n : ℕ) → M ⧸ I ^ n • ⊤) n
a : M
ha : ∀ (n : ℕ), x n ≡ a [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
⊢ (↑((of I M : (a : M) → AdicCompletion I M) a) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑u : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
simpa [SModEq, ← eval_of, ha, ← hx] using (ha n).symm

Premises used: SModEq.symm, AdicCompletion.eval_of, SModEq
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrecomplete I M
⊢ Function.Surjective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)

Tactic:
of_surjective_iff.mpr ‹_›

Premises used: AdicCompletion.of_surjective_iff, Iff.mpr
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Function.Bijective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M) ↔ IsAdicComplete I M

Tactic:
⟨fun h ↦
    { toIsHausdorff := of_injective_iff.mp h.1,
      toIsPrecomplete := of_surjective_iff.mp h.2 },
   fun h ↦ ⟨of_injective_iff.mpr h.1, of_surjective_iff.mpr h.2⟩⟩

Premises used: AdicCompletion.of_surjective_iff, Iff.mpr, IsAdicComplete.toIsHausdorff, IsAdicComplete.mk, IsAdicComplete.toIsPrecomplete, And.right, And.left, And.intro, Iff.intro, Iff.mp, AdicCompletion.of_injective_iff
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsAdicComplete I M
⊢ Function.Bijective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)

Tactic:
of_bijective_iff.mpr ‹_›

Premises used: Iff.mpr, AdicCompletion.of_bijective_iff
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsAdicComplete I M
x : M
⊢ (LinearEquiv.symm (ofLinearEquiv I M) : (a : AdicCompletion I M) → M)
      ((of I M : (a : M) → AdicCompletion I M) x : AdicCompletion I M) =
    x

Tactic:
simp [ofLinearEquiv]

Premises used: AdicCompletion.ofLinearEquiv
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsAdicComplete I M
x : AdicCompletion I M
⊢ (of I M : (a : M) → AdicCompletion I M) ((LinearEquiv.symm (ofLinearEquiv I M) : (a : AdicCompletion I M) → M) x) = x

Tactic:
simp [ofLinearEquiv]

Premises used: AdicCompletion.ofLinearEquiv
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
simp : ∀ r ∈ I ^ n, ∀ (n_1 : AdicCompletion I M), r • (↑n_1 : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
⊢ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤ ≤ LinearMap.ker (eval I M n)

Tactic:
simp only [smul_le, mem_top, LinearMap.mem_ker, map_smul, coe_eval, forall_const]

Premises used: AdicCompletion.coe_eval, LinearMap.mem_ker, Submodule.smul_le, forall_const, Submodule.mem_top, map_smul
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
r : R
r_in : r ∈ I ^ n
x : AdicCompletion I M
rw : r • out ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
⊢ r • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0

Tactic:
rw [← Submodule.Quotient.mk_out (x.val n), ← Quotient.mk_smul, Quotient.mk_eq_zero]

Premises used: Submodule.Quotient.mk_smul, Submodule.Quotient.mk_out, Subtype.val, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
r : R
r_in : r ∈ I ^ n
x : AdicCompletion I M
⊢ r • out ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤

Tactic:
smul_mem_smul r_in mem_top

Premises used: Set.Mem, Submodule.smul_mem_smul, Submodule.mem_top
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
r : R
r_in : r ∈ I ^ n
x : AdicCompletion I M
⊢ r • out ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤

Tactic:
exact smul_mem_smul r_in mem_top

Premises used: Submodule.smul_mem_smul, Submodule.mem_top
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
⊢ (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m ∈
      HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)) (I ^ n) ⊤ ↔
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
refine_1 :
  ∀
    (h :
      (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m ∈
        HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)) (I ^ n) ⊤),
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
refine_2 :
  ∀ (h : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0),
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m ∈
      HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)) (I ^ n) ⊤
⊢ (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m ∈
      HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)) (I ^ n) ⊤ ↔
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
h :
  (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m ∈
    HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)) (I ^ n) ⊤
refine_1 :
  (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m ∈
    ((HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤).liftQ
        ((HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).mkQ ∘ₗ LinearMap.id) ⋯).ker
⊢ (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0

Tactic:
rw [← x.prop m_ge, transitionMap, Submodule.factorPow, Submodule.factor, mapQ,
      ← LinearMap.mem_ker]

Premises used: Submodule.factorPow, LinearMap.mem_ker, AdicCompletion.transitionMap, Submodule.mapQ, Subtype.prop, Submodule.factor
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
h :
  (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m ∈
    HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)) (I ^ n) ⊤
⊢ (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m ∈
    ((HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤).liftQ
        ((HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).mkQ ∘ₗ LinearMap.id) ⋯).ker

Tactic:
simpa [ker_liftQ]

Premises used: Submodule.ker_liftQ
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
h : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
⊢ (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m ∈
    HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)) (I ^ n) ⊤

Tactic:
simpa [mapQ, h, ← LinearMap.mem_ker, ker_liftQ] using x.prop m_ge

Premises used: LinearMap.mem_ker, Submodule.mapQ, Subtype.prop, Submodule.ker_liftQ
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing S
inst_4 : Module S M
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
⊢ IsAdicComplete.{u_2, u_4} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I) M ↔ IsAdicComplete I M

Tactic:
simp [isAdicComplete_iff, IsPrecomplete.map_algebraMap_iff, IsHausdorff.map_algebraMap_iff]

Premises used: IsHausdorff.map_algebraMap_iff, IsPrecomplete.map_algebraMap_iff, isAdicComplete_iff
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsAdicComplete I N
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
x : M
⊢ Eq (α := AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) ((lift I f ⋯ : (a : M) → N) x) : AdicCompletion I N)
    ((AdicCompletion.lift I f ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N)

Tactic:
simp [lift]

Premises used: IsAdicComplete.lift
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsAdicComplete I N
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
h₁ :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := AdicCompletion I N)
      ((of I N ∘ₗ lift I f ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N)
      ((AdicCompletion.lift I f ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N)
⊢ of I N ∘ₗ lift I f ⋯ = AdicCompletion.lift I f ⋯

Tactic:
ext1
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsAdicComplete I N
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
x : M
⊢ Eq.{u_5 + 1} (α := AdicCompletion I N) ((of I N ∘ₗ lift I f ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N)
    ((AdicCompletion.lift I f ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N)

Tactic:
simp