awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
h₁ :
  HSMul.hSMul (β := AddSubmonoid M) (I ^ n).toAddSubmonoid ⊤ ≤
    HSMul.hSMul (β := AddSubmonoid M) (J ^ n).toAddSubmonoid ⊤
⊢ (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).toAddSubgroup.toAddSubmonoid ≤
    (HSMul.hSMul (β := Submodule S M) (J ^ n) ⊤).toAddSubgroup.toAddSubmonoid

Tactic:
simp only [Submodule.smul_toAddSubmonoid, Submodule.top_toAddSubmonoid]

Premises used: Submodule.top_toAddSubmonoid, Submodule.smul_toAddSubmonoid
-- 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
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
h₁ :
  ∀ m ∈ (I ^ n).toAddSubmonoid,
    ∀ (n_1 : M),
      Membership.mem (γ := AddSubmonoid M) ⊤ n_1 → m • n_1 ∈ HSMul.hSMul (β := AddSubmonoid M) (J ^ n).toAddSubmonoid ⊤
⊢ HSMul.hSMul (β := AddSubmonoid M) (I ^ n).toAddSubmonoid ⊤ ≤
    HSMul.hSMul (β := AddSubmonoid M) (J ^ n).toAddSubmonoid ⊤

Tactic:
rw [AddSubmonoid.smul_le]

Premises used: AddSubmonoid.smul_le
-- 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
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
r : R
hr : r ∈ (I ^ n).toAddSubmonoid
m : M
hm : Membership.mem (γ := AddSubmonoid M) ⊤ m
h₁ :
  HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) r : S) m ∈
    HSMul.hSMul (β := AddSubmonoid M) (J ^ n).toAddSubmonoid ⊤
⊢ r • m ∈ HSMul.hSMul (β := AddSubmonoid M) (J ^ n).toAddSubmonoid ⊤

Tactic:
rw [← algebraMap_smul S r m]

Premises used: algebraMap_smul
-- 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
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
r : R
hr : r ∈ (I ^ n).toAddSubmonoid
m : M
hm : Membership.mem (γ := AddSubmonoid M) ⊤ m
apply : Membership.mem (α := S) (J ^ n).toAddSubmonoid ((algebraMap R S : (a : R) → S) r : S)
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) r : S) m ∈
    HSMul.hSMul (β := AddSubmonoid M) (J ^ n).toAddSubmonoid ⊤

Tactic:
apply AddSubmonoid.smul_mem_smul ?_ hm

Premises used: AddSubmonoid.smul_mem_smul
-- 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
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
r : R
hr : r ∈ (I ^ n).toAddSubmonoid
m : M
hm : Membership.mem (γ := AddSubmonoid M) ⊤ m
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (I ^ n))
    ((algebraMap R S : (a : R) → S) r : S)

Tactic:
have := Ideal.mem_map_of_mem (algebraMap R S) hr
-- 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
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
r : R
hr : r ∈ (I ^ n).toAddSubmonoid
m : M
hm : Membership.mem (γ := AddSubmonoid M) ⊤ m
this :
  Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (I ^ n))
    ((algebraMap R S : (a : R) → S) r : S)
⊢ Membership.mem (α := S) (HPow.hPow (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) n)
    ((algebraMap R S : (a : R) → S) r : S)

Tactic:
simp only [Ideal.map_pow] at this

Premises used: Ideal.map_pow
-- 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
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
r : R
hr : r ∈ (I ^ n).toAddSubmonoid
m : M
hm : Membership.mem (γ := AddSubmonoid M) ⊤ m
this :
  Membership.mem (α := S) (HPow.hPow (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) n)
    ((algebraMap R S : (a : R) → S) r : S)
⊢ Membership.mem (α := S) (J ^ n).toAddSubmonoid ((algebraMap R S : (a : R) → S) r : S)

Tactic:
Ideal.pow_right_mono hIJ n this

Premises used: Set.Mem, Ideal.pow_right_mono
-- 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
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
r : R
hr : r ∈ (I ^ n).toAddSubmonoid
m : M
hm : Membership.mem (γ := AddSubmonoid M) ⊤ m
this :
  Membership.mem (α := S) (HPow.hPow (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) n)
    ((algebraMap R S : (a : R) → S) r : S)
⊢ Membership.mem (α := S) (J ^ n).toAddSubmonoid ((algebraMap R S : (a : R) → S) r : S)

Tactic:
exact Ideal.pow_right_mono hIJ n this

Premises used: Ideal.pow_right_mono
-- 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
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
⊢ x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
h n
-- 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
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
⊢ x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
exact h n
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
N : Type u_5
inst_1 : AddCommGroup N
inst_2 : Module R N
M : Type u_6
inst_3 : IsHausdorff I N
f g : M → N
h :
  ∀ (n : ℕ) (m : M),
    Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) (Submodule.Quotient.mk (f m)) (Submodule.Quotient.mk (g m))
h₁ : ∀ (m : M), f m = g m
⊢ f = g

Tactic:
ext m
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
N : Type u_5
inst_1 : AddCommGroup N
inst_2 : Module R N
M : Type u_6
inst_3 : IsHausdorff I N
f g : M → N
h :
  ∀ (n : ℕ) (m : M),
    Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) (Submodule.Quotient.mk (f m)) (Submodule.Quotient.mk (g m))
m : M
h₁ : ∀ (n : ℕ), f m ≡ g m [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
⊢ f m = g m

Tactic:
rw [IsHausdorff.eq_iff_smodEq (I := I)]

Premises used: IsHausdorff.eq_iff_smodEq
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
N : Type u_5
inst_1 : AddCommGroup N
inst_2 : Module R N
M : Type u_6
inst_3 : IsHausdorff I N
f g : M → N
h :
  ∀ (n : ℕ) (m : M),
    Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) (Submodule.Quotient.mk (f m)) (Submodule.Quotient.mk (g m))
m : M
n : ℕ
⊢ f m ≡ g m [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]

Tactic:
h n m

Premises used: SModEq
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
N : Type u_5
inst_1 : AddCommGroup N
inst_2 : Module R N
M : Type u_6
inst_3 : IsHausdorff I N
f g : M → N
h :
  ∀ (n : ℕ) (m : M),
    Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) (Submodule.Quotient.mk (f m)) (Submodule.Quotient.mk (g m))
m : M
n : ℕ
⊢ f m ≡ g m [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]

Tactic:
exact h n m
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
N : Type u_5
inst_1 : AddCommGroup N
inst_2 : Module R N
M : Type u_6
inst_3 : IsHausdorff I N
f g : M → N
a : ℕ → ℕ
ha : StrictMono a
h :
  ∀ (n : ℕ) (m : M),
    Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤) (Submodule.Quotient.mk (f m))
      (Submodule.Quotient.mk (g m))
h₁ : ∀ (m : M), f m = g m
⊢ f = g

Tactic:
ext m
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
N : Type u_5
inst_1 : AddCommGroup N
inst_2 : Module R N
M : Type u_6
inst_3 : IsHausdorff I N
f g : M → N
a : ℕ → ℕ
ha : StrictMono a
h :
  ∀ (n : ℕ) (m : M),
    Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤) (Submodule.Quotient.mk (f m))
      (Submodule.Quotient.mk (g m))
m : M
h₁ : ∀ (n : ℕ), f m ≡ g m [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
⊢ f m = g m

Tactic:
rw [IsHausdorff.eq_iff_smodEq (I := I)]

Premises used: IsHausdorff.eq_iff_smodEq
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
N : Type u_5
inst_1 : AddCommGroup N
inst_2 : Module R N
M : Type u_6
inst_3 : IsHausdorff I N
f g : M → N
a : ℕ → ℕ
ha : StrictMono a
h :
  ∀ (n : ℕ) (m : M),
    Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤) (Submodule.Quotient.mk (f m))
      (Submodule.Quotient.mk (g m))
m : M
n : ℕ
h₁ : f m ≡ g m [SMOD HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤]
⊢ f m ≡ g m [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]

Tactic:
apply SModEq.mono (Submodule.pow_smul_top_le I N ha.le_apply)

Premises used: StrictMono.le_apply, SModEq.mono, Submodule.pow_smul_top_le
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
N : Type u_5
inst_1 : AddCommGroup N
inst_2 : Module R N
M : Type u_6
inst_3 : IsHausdorff I N
f g : M → N
a : ℕ → ℕ
ha : StrictMono a
h :
  ∀ (n : ℕ) (m : M),
    Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤) (Submodule.Quotient.mk (f m))
      (Submodule.Quotient.mk (g m))
m : M
n : ℕ
⊢ f m ≡ g m [SMOD HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤]

Tactic:
h n m

Premises used: Set.Mem, SModEq
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
N : Type u_5
inst_1 : AddCommGroup N
inst_2 : Module R N
M : Type u_6
inst_3 : IsHausdorff I N
f g : M → N
a : ℕ → ℕ
ha : StrictMono a
h :
  ∀ (n : ℕ) (m : M),
    Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤) (Submodule.Quotient.mk (f m))
      (Submodule.Quotient.mk (g m))
m : M
n : ℕ
⊢ f m ≡ g m [SMOD HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤]

Tactic:
exact h n m
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_6
S : Type u_7
inst : CommRing S
I : Ideal S
inst_1 : IsHausdorff I S
f g : R → S
h :
  ∀ (n : ℕ) (r : R),
    Eq (α := S ⧸ I ^ n) ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (f r) : S ⧸ I ^ n)
      ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (g r) : S ⧸ I ^ n)
h₁ : ∀ (r : R), f r = g r
⊢ f = g

Tactic:
ext r
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_6
S : Type u_7
inst : CommRing S
I : Ideal S
inst_1 : IsHausdorff I S
f g : R → S
h :
  ∀ (n : ℕ) (r : R),
    Eq (α := S ⧸ I ^ n) ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (f r) : S ⧸ I ^ n)
      ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (g r) : S ⧸ I ^ n)
r : R
h₁ : ∀ (n : ℕ), SModEq (R := S) (HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (f r) (g r)
⊢ f r = g r

Tactic:
rw [IsHausdorff.eq_iff_smodEq (I := I)]

Premises used: IsHausdorff.eq_iff_smodEq
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_6
S : Type u_7
inst : CommRing S
I : Ideal S
inst_1 : IsHausdorff I S
f g : R → S
h :
  ∀ (n : ℕ) (r : R),
    Eq (α := S ⧸ I ^ n) ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (f r) : S ⧸ I ^ n)
      ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (g r) : S ⧸ I ^ n)
r : R
n : ℕ
⊢ SModEq (R := S) (HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (f r) (g r)

Tactic:
simpa using h n r
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_6
S : Type u_7
inst : CommRing S
I : Ideal S
inst_1 : IsHausdorff I S
f g : R → S
a : ℕ → ℕ
ha : StrictMono a
h :
  ∀ (n : ℕ) (r : R),
    Eq (α := S ⧸ I ^ a n) ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n) (f r) : S ⧸ I ^ a n)
      ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n) (g r) : S ⧸ I ^ a n)
h₁ : ∀ (m : R), f m = g m
⊢ f = g

Tactic:
ext m
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_6
S : Type u_7
inst : CommRing S
I : Ideal S
inst_1 : IsHausdorff I S
f g : R → S
a : ℕ → ℕ
ha : StrictMono a
h :
  ∀ (n : ℕ) (r : R),
    Eq (α := S ⧸ I ^ a n) ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n) (f r) : S ⧸ I ^ a n)
      ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n) (g r) : S ⧸ I ^ a n)
m : R
h₁ : ∀ (n : ℕ), SModEq (R := S) (HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (f m) (g m)
⊢ f m = g m

Tactic:
rw [IsHausdorff.eq_iff_smodEq (I := I)]

Premises used: IsHausdorff.eq_iff_smodEq
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_6
S : Type u_7
inst : CommRing S
I : Ideal S
inst_1 : IsHausdorff I S
f g : R → S
a : ℕ → ℕ
ha : StrictMono a
h :
  ∀ (n : ℕ) (r : R),
    Eq (α := S ⧸ I ^ a n) ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n) (f r) : S ⧸ I ^ a n)
      ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n) (g r) : S ⧸ I ^ a n)
m : R
n : ℕ
h₁ : SModEq (R := S) (HSMul.hSMul (β := Submodule S S) (I ^ a n) ⊤) (f m) (g m)
⊢ SModEq (R := S) (HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (f m) (g m)

Tactic:
apply SModEq.mono (Submodule.pow_smul_top_le I S ha.le_apply)

Premises used: StrictMono.le_apply, SModEq.mono, Submodule.pow_smul_top_le
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_6
S : Type u_7
inst : CommRing S
I : Ideal S
inst_1 : IsHausdorff I S
f g : R → S
a : ℕ → ℕ
ha : StrictMono a
h :
  ∀ (n : ℕ) (r : R),
    Eq (α := S ⧸ I ^ a n) ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n) (f r) : S ⧸ I ^ a n)
      ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n) (g r) : S ⧸ I ^ a n)
m : R
n : ℕ
⊢ SModEq (R := S) (HSMul.hSMul (β := Submodule S S) (I ^ a n) ⊤) (f m) (g m)

Tactic:
simpa using h n m
-- 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
f : ℕ → M
⊢ (∀ {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) ⊤]

Tactic:
IsPrecomplete.prec' _

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
⊢ IsPrecomplete I M ↔
    ∀ (f : ℕ → M),
      (∀ {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) ⊤]

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: Iff.intro, IsPrecomplete.prec', IsPrecomplete.mk
-- 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
⊢ IsPrecomplete.{u_2, u_4} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I) M ↔ IsPrecomplete I M

Tactic:
simp [isPrecomplete_iff, ← Ideal.map_pow, ← SModEq.restrictScalars R,
    restrictScalars_map_smul_eq]

Premises used: Submodule.restrictScalars_map_smul_eq, SModEq.restrictScalars, isPrecomplete_iff, Ideal.map_pow
-- 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
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ n) ⊤]
⊢ x = 0

Tactic:
simpa only [pow_one ⊥, bot_smul, SModEq.bot] using hx 1

Premises used: SModEq.bot, Submodule.bot_smul, Bot.bot, pow_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsHausdorff.{u_1, u_4} (R := R) ⊤ M
x y : M
n : ℕ
rw : SModEq.{u_1, u_4} (R := R) ⊤ (x - y) 0
⊢ x - y ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊤ n) ⊤]

Tactic:
rw [Ideal.top_pow, top_smul]

Premises used: Submodule.top_smul, Ideal.top_pow
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsHausdorff.{u_1, u_4} (R := R) ⊤ M
x y : M
n : ℕ
⊢ SModEq.{u_1, u_4} (R := R) ⊤ (x - y) 0

Tactic:
SModEq.top

Premises used: SModEq.top
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsHausdorff.{u_1, u_4} (R := R) ⊤ M
x y : M
n : ℕ
⊢ SModEq.{u_1, u_4} (R := R) ⊤ (x - y) 0

Tactic:
exact SModEq.top

Premises used: SModEq.top
-- 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
inst_5 : Subsingleton M
⊢ IsHausdorff I M

Tactic:
⟨fun _ _ => Subsingleton.elim _ _⟩

Premises used: IsHausdorff.mk, Subsingleton.elim, OfNat.ofNat
-- 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
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ⊥

Tactic:
eq_bot_iff.2 fun x hx =>
    (mem_bot _).2 <| h.haus x fun n => SModEq.zero.2 <| (mem_iInf fun n : ℕ => I ^ n • ⊤).1 hx n

Premises used: Iff.mpr, Submodule.mem_iInf, Submodule.mem_bot, SModEq.zero, IsHausdorff.haus, HPow.hPow, Iff.mp, HSMul.hSMul, eq_bot_iff, Top.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
C : Hausdorffification I M → Prop
x : Hausdorffification I M
ih : ∀ (x : M), C ((of I M : (a : M) → Hausdorffification I M) x)
⊢ C x

Tactic:
Quotient.inductionOn' x ih

Premises used: Quotient.inductionOn'
-- 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
x_1 : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R (Hausdorffification I M)) (I ^ n) ⊤]
n : ℕ
⊢ Submodule.comap (M₂ :=
      HasQuotient.Quotient M (B := Submodule R M) (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      (mkQ (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      (Submodule.map (mkQ (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
        (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) =
    (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ⊔ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤

Tactic:
have := comap_map_mkQ (⨅ n : ℕ, I ^ n • ⊤ : Submodule R M) (I ^ n • ⊤)
-- 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
x_1 : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R (Hausdorffification I M)) (I ^ n) ⊤]
n : ℕ
this :
  Submodule.comap (M₂ :=
      HasQuotient.Quotient M (B := Submodule R M) (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      (mkQ (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      (Submodule.map (mkQ (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
        (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) =
    (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ⊔ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
⊢ Submodule.comap (M₂ :=
      HasQuotient.Quotient M (B := Submodule R M) (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      (mkQ (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      (Submodule.map (mkQ (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
        (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) =
    HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤

Tactic:
simp only [sup_of_le_right (iInf_le (fun n => (I ^ n • ⊤ : Submodule R M)) n)] at this

Premises used: sup_of_le_right, HPow.hPow, HSMul.hSMul, Top.top, iInf_le
-- 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
x_1 : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R (Hausdorffification I M)) (I ^ n) ⊤]
n : ℕ
this :
  Submodule.comap (M₂ :=
      HasQuotient.Quotient M (B := Submodule R M) (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      (mkQ (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
      (Submodule.map (mkQ (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
        (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) =
    HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
rw :
  (mkQ (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) : (a : M) → M ⧸ ⨅ (n : ℕ), I ^ n • ⊤) x ≡ 0 [SMOD
    HSMul.hSMul (β :=
      Submodule R (HasQuotient.Quotient M (B := Submodule R M) (⨅ (n : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)))
      (I ^ n) ⊤]
⊢ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤

Tactic:
rw [← this, map_smul'', Submodule.mem_comap, Submodule.map_top, range_mkQ, ← SModEq.zero]

Premises used: Submodule.map_smul'', SModEq.zero, Submodule.map_top, Submodule.range_mkQ, Submodule.mem_comap