awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
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
f : AdicCauchySequence I M
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 ((↑f : ℕ → M) n)) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    (Submodule.Quotient.mk ((↑f : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)

Tactic:
(f.property hmn).symm

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.Quotient.mk, SModEq.symm, SModEq, Subtype.property
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
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
f : AdicCauchySequence I M
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 ((↑f : ℕ → M) n)) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    (Submodule.Quotient.mk ((↑f : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)

Tactic:
exact (f.property hmn).symm

Premises used: SModEq.symm, 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
f : AdicCauchySequence I M
h : ∃ (k : ℕ), ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
obtain :
  ∀ (k : ℕ) (h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤),
    Eq (α := AdicCompletion I M) ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f : AdicCompletion I M)
      (0 : AdicCompletion I M)
⊢ Eq (α := AdicCompletion I M) ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f : AdicCompletion I M)
    (0 : AdicCompletion I M)

Tactic:
obtain ⟨k, h⟩ := 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
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
h₁ :
  ∀ (n : ℕ),
    Eq.{u_4 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
      ((↑((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
      ((↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
⊢ Eq (α := AdicCompletion I M) ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f : AdicCompletion I M)
    (0 : AdicCompletion I M)

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
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
n : ℕ
⊢ n + k ≥ k

Tactic:
lia
-- 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
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
n : ℕ
h₁ :
  ∀ (m : ℕ) (hnm : m ≥ n + k) (l : ℕ) (hnl : l ≥ n + k)
    (hl : (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤),
    Eq.{u_4 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
      ((↑((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
      ((↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
⊢ Eq.{u_4 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((↑((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
    ((↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n)

Tactic:
obtain ⟨m, hnm, l, hnl, hl⟩ := h (n + k) (by lia)

Premises used: HAdd.hAdd
-- 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
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
n m : ℕ
hnm : m ≥ n + k
l : ℕ
hnl : l ≥ n + k
hl : (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
⊢ n ≤ m

Tactic:
lia
-- 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
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
n m : ℕ
hnm : m ≥ n + k
l : ℕ
hnl : l ≥ n + k
hl : (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
h₁ :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((↑f : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (0 n : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
⊢ Eq.{u_4 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((↑((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
    ((↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n)

Tactic:
rw [mk_apply_coe, Submodule.mkQ_apply, val_zero,
    ← AdicCauchySequence.mk_eq_mk (show n ≤ m by lia)]

Premises used: AdicCompletion.AdicCauchySequence.mk_eq_mk, Submodule.mkQ_apply, AdicCompletion.val_zero, AdicCompletion.mk_apply_coe
-- 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
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
n m : ℕ
hnm : m ≥ n + k
l : ℕ
hnl : l ≥ n + k
hl : (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
⊢ n ≤ l

Tactic:
lia
-- 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
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
n m : ℕ
hnm : m ≥ n + k
l : ℕ
hnl : l ≥ n + k
hl : (↑f : ℕ → M) m ∈ HSMul.hSMul (β := Submodule R M) (I ^ l) ⊤
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((↑f : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (0 n : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)

Tactic:
simpa using (Submodule.smul_mono_left (Ideal.pow_le_pow_right (by lia))) hl

Premises used: Ideal.pow_le_pow_right, Submodule.smul_mono_left
-- 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
x : AdicCompletion I M
choose :
  ∀ (a : (n : ℕ) → M) (ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n),
    ∃ (a : AdicCauchySequence I M), (mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a = x
⊢ ∃ (a : AdicCauchySequence I M), (mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a = x

Tactic:
choose a ha using fun n ↦ Submodule.Quotient.mk_surjective _ (x.val 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
x : AdicCompletion I M
a : (n : ℕ) → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ ∃ (a : AdicCauchySequence I M), (mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a = x

Tactic:
⟨⟨a, ?_⟩, ?_⟩

Premises used: Subtype.mk, 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
x : AdicCompletion I M
a : (n : ℕ) → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n
refine_1 : IsAdicCauchy I M a
refine_2 :
  (mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
      (Subtype.mk (p := fun (f : ℕ → M) ↦ IsAdicCauchy I M f) a ⋯) =
    x
⊢ ∃ (a : AdicCauchySequence I M), (mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a = x

Tactic:
refine ⟨⟨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
x : AdicCompletion I M
a : (n : ℕ) → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n
m n : ℕ
hmn : m ≤ n
refine_1 :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) (Submodule.Quotient.mk (a m)) (Submodule.Quotient.mk (a n))
refine_1₁ : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m = Submodule.Quotient.mk (a n)
refine_1₂ :
  (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m = ((HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤).mkQ : (a : M) → M ⧸ I ^ m • ⊤) (a n)
refine_1₃ :
  (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m =
    (Submodule.factor ⋯ : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤)
      (((HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).mkQ : (a : M) → M ⧸ I ^ n • ⊤) (a n))
refine_1₄ :
  (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m =
    (Submodule.factor ⋯ : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (Submodule.Quotient.mk (a n))
refine_1₅ :
  (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m =
    (Submodule.factor ⋯ : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
refine_1₆ refine_1₇ : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m
⊢ a m ≡ a n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
rw [SModEq.def, ha m, ← mkQ_apply,
      ← factor_mk (Submodule.smul_mono_left (Ideal.pow_le_pow_right hmn)) (a n),
      mkQ_apply, ha n, x.property hmn]

Premises used: Submodule.factor_mk, SModEq.def, Submodule.mkQ_apply, Ideal.pow_le_pow_right, Subtype.property, Submodule.smul_mono_left
-- 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
x : AdicCompletion I M
a : (n : ℕ) → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n
refine_2 :
  ∀ (n : ℕ),
    (↑((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
              (Subtype.mk (p := fun (f : ℕ → M) ↦ IsAdicCauchy I M f) a ⋯)) :
          (n : ℕ) → M ⧸ I ^ n • ⊤)
        n =
      (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ (mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
      (Subtype.mk (p := fun (f : ℕ → M) ↦ IsAdicCauchy I M f) a ⋯) =
    x

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
x : AdicCompletion I M
a : (n : ℕ) → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n
n : ℕ
⊢ (↑((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
            (Subtype.mk (p := fun (f : ℕ → M) ↦ IsAdicCauchy I M f) a ⋯)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      n =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
simp [ha 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
p : AdicCompletion I M → Prop
x : AdicCompletion I M
h obtain : ∀ (f : AdicCauchySequence I M), p ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f)
⊢ p x

Tactic:
obtain ⟨f, rfl⟩ := mk_surjective I M x

Premises used: AdicCompletion.mk_surjective, rfl
-- 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
p : AdicCompletion I M → Prop
h : ∀ (f : AdicCauchySequence I M), p ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f)
f : AdicCauchySequence I M
⊢ p ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f)

Tactic:
h f
-- 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
p : AdicCompletion I M → Prop
h : ∀ (f : AdicCauchySequence I M), p ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f)
f : AdicCauchySequence I M
⊢ p ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) f)

Tactic:
exact h f
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
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
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), transitionMap I N hle ∘ₗ f n = f m
x y : M
simp :
  Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦
        HAdd.hAdd (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) (β :=
          N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          ((f n : (a : M) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤))
      ⋯ =
    HAdd.hAdd (α := AdicCompletion I N)
      (Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (f n : (a : M) → N ⧸ I ^ n • ⊤) x) ⋯)
      (Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (f n : (a : M) → N ⧸ I ^ n • ⊤) y) ⋯)
⊢ Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (f n : (a : M) → N ⧸ I ^ n • ⊤) (x + y)) ⋯ =
    HAdd.hAdd (α := AdicCompletion I N)
      (Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (f n : (a : M) → N ⧸ I ^ n • ⊤) x) ⋯)
      (Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (f n : (a : M) → N ⧸ I ^ n • ⊤) y) ⋯)

Tactic:
simp only [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
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
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), transitionMap I N hle ∘ₗ f n = f m
x y : M
⊢ Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦
        HAdd.hAdd (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) (β :=
          N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          ((f n : (a : M) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤))
      ⋯ =
    HAdd.hAdd (α := AdicCompletion I N)
      (Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (f n : (a : M) → N ⧸ I ^ n • ⊤) x) ⋯)
      (Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (f n : (a : M) → N ⧸ I ^ n • ⊤) y) ⋯)

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
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
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), transitionMap I N hle ∘ₗ f n = f m
r : R
x : M
simp :
  Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦
        HSMul.hSMul (β := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) r
          ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤))
      ⋯ =
    HSMul.hSMul (β := AdicCompletion I N) r
      (Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (f n : (a : M) → N ⧸ I ^ n • ⊤) x) ⋯)
⊢ Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (f n : (a : M) → N ⧸ I ^ n • ⊤) (r • x)) ⋯ =
    HSMul.hSMul (α := R) (β := AdicCompletion I N) ((RingHom.id R : (a : R) → R) r : R)
      (Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (f n : (a : M) → N ⧸ I ^ n • ⊤) x) ⋯)

Tactic:
simp only [LinearMapClass.map_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, LinearMapClass.map_smul
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
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
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), transitionMap I N hle ∘ₗ f n = f m
r : R
x : M
⊢ Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦
        HSMul.hSMul (β := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) r
          ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤))
      ⋯ =
    HSMul.hSMul (β := AdicCompletion I N) r
      (Subtype.mk (p := fun (f : (n : ℕ) → N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I N hmn : (a : N ⧸ I ^ n • ⊤) → N ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (f n : (a : M) → N ⧸ I ^ n • ⊤) x) ⋯)

Tactic:
rfl
-- 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
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), transitionMap I N hle ∘ₗ f n = f m
n : ℕ
⊢ eval I N n ∘ₗ lift I f ⋯ = f n

Tactic:
rfl

Premises used: rfl
-- 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
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), transitionMap I N hle ∘ₗ f n = f m
n : ℕ
x : M
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((↑((lift I f ⋯ : (a : M) → AdicCompletion I N) x) : (n : ℕ) → N ⧸ I ^ n • ⊤) n :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)

Tactic:
rfl

Premises used: rfl
-- 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.Injective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M) → IsHausdorff I M
mpr : IsHausdorff I M → Function.Injective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)
⊢ Function.Injective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M) ↔ IsHausdorff 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.Injective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M) → IsHausdorff I M

Tactic:
fun h ↦ ⟨fun x hx ↦ h ?_⟩

Premises used: IsHausdorff.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.Injective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)) (x : M)
    (hx : ∀ (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)
      ((of I M : (a : M) → AdicCompletion I M) 0 : AdicCompletion I M)
⊢ Function.Injective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M) → IsHausdorff I M

Tactic:
refine fun h ↦ ⟨fun x hx ↦ 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
h : Function.Injective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
mp :
  ∀ (n : ℕ),
    Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
      ((↑((of I M : (a : M) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
      ((↑((of I M : (a : M) → AdicCompletion I M) 0) : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
⊢ Eq (α := AdicCompletion I M) ((of I M : (a : M) → AdicCompletion I M) x : AdicCompletion I M)
    ((of I M : (a : M) → AdicCompletion I M) 0 : AdicCompletion I M)

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 : Function.Injective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((↑((of I M : (a : M) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
    ((↑((of I M : (a : M) → AdicCompletion I M) 0) : (n : ℕ) → M ⧸ I ^ n • ⊤) n)

Tactic:
simpa [of, SModEq.zero] using hx n

Premises used: SModEq.zero, AdicCompletion.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 : IsHausdorff I M
mpr : Eq (α := Submodule R M) (LinearMap.ker (of I M)) ⊥
⊢ Function.Injective (α := M) (β := AdicCompletion I M) (⇑(of I M) : (a : M) → AdicCompletion I M)

Tactic:
rw [← LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot
-- 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
mpr :
  ∀ (x : M), Membership.mem (γ := Submodule R M) (LinearMap.ker (of I M)) x ↔ Membership.mem (γ := Submodule R M) ⊥ x
⊢ Eq (α := Submodule R M) (LinearMap.ker (of I M)) ⊥

Tactic:
ext x