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
inst_5 : SMul S R
inst_6 : SMul T R
inst_7 : SMul S M
inst_8 : SMul T M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower T R M
inst_11 : SMulCommClass S T M
s : S
t : T
f : AdicCompletion I M
h : ∀ (n : ℕ), (↑(s • t • f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(t • s • f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ s • t • f = t • s • f

Tactic:
ext
-- 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 : SMul S R
inst_6 : SMul T R
inst_7 : SMul S M
inst_8 : SMul T M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower T R M
inst_11 : SMulCommClass S T M
s : S
t : T
f : AdicCompletion I M
n : ℕ
⊢ (↑(s • t • f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(t • s • f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
simp [val_smul, smul_comm]

Premises used: AdicCompletion.val_smul, SMulCommClass.smul_comm
-- 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 : SMul S R
inst_6 : SMul.{u_2, u_1} Sᵐᵒᵖ R
inst_7 : SMul S M
inst_8 : SMul.{u_2, u_4} Sᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_2, u_1, u_4} Sᵐᵒᵖ R M
inst_11 : IsCentralScalar S M
s : S
f : AdicCompletion I M
h : ∀ (n : ℕ), (↑(MulOpposite.op s • f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(s • f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ MulOpposite.op s • f = s • f

Tactic:
ext
-- 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 : SMul S R
inst_6 : SMul.{u_2, u_1} Sᵐᵒᵖ R
inst_7 : SMul S M
inst_8 : SMul.{u_2, u_4} Sᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_2, u_1, u_4} Sᵐᵒᵖ R M
inst_11 : IsCentralScalar S M
s : S
f : AdicCompletion I M
n : ℕ
⊢ (↑(MulOpposite.op s • f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(s • f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
simp [val_smul, op_smul_eq_smul]

Premises used: AdicCompletion.val_smul, IsCentralScalar.op_smul_eq_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
ι : Type u_6
s : Finset ι
f : ι → AdicCompletion I M
simp_rw :
  Eq (α := (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((incl I M : (a : AdicCompletion I M) → (n : ℕ) → M ⧸ I ^ n • ⊤) (∑ i ∈ s, f i) :
      (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (∑ x ∈ s, (incl I M : (a : AdicCompletion I M) → (n : ℕ) → M ⧸ I ^ n • ⊤) (f x) :
      (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
⊢ Eq.{u_4 + 1} (α := (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (↑(∑ i ∈ s, f i) : (n : ℕ) → M ⧸ I ^ n • ⊤) (∑ i ∈ s, (↑(f i) : (n : ℕ) → M ⧸ I ^ n • ⊤))

Tactic:
simp_rw [← funext (incl_apply _ _ _), map_sum]

Premises used: AdicCompletion.incl_apply, map_sum, funext
-- 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
ι : Type u_6
s : Finset ι
f : ι → AdicCompletion I M
n : ℕ
⊢ Eq.{u_4 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ((↑(∑ i ∈ s, f i) : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
    (∑ i ∈ s, (↑(f i) : (n : ℕ) → M ⧸ I ^ n • ⊤) n)

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
x : M
n : ℕ
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((↑((of I M : (a : M) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).mkQ : (a : M) → M ⧸ I ^ n • ⊤) x :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)

Tactic:
rfl

Premises used: Set.Mem, 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 : ℕ
⊢ Eq (α := (a : AdicCompletion I M) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (⇑(eval I M n) : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤) fun (f : AdicCompletion I M) ↦
    (↑f : (n : ℕ) → M ⧸ I ^ n • ⊤) 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 : ℕ
f : AdicCompletion I M
⊢ (eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤) f = (↑f : (n : ℕ) → M ⧸ I ^ n • ⊤) 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 : ℕ
x : M
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤) ((of I M : (a : M) → AdicCompletion I M) x) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).mkQ : (a : M) → M ⧸ I ^ n • ⊤) x :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)

Tactic:
rfl

Premises used: Set.Mem, Submodule.Quotient.mk, 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 : ℕ
⊢ eval I M n ∘ₗ of I M = (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).mkQ

Tactic:
rfl

Premises used: Set.Mem, Submodule.Quotient.mk, Submodule.mkQ, 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 : ℕ
⊢ Function.Surjective (α := AdicCompletion I M) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (⇑(eval I M n) : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤)

Tactic:
fun x ↦
  Quotient.inductionOn' x fun x ↦ ⟨of I M x, rfl⟩

Premises used: Quotient.inductionOn', Function.Surjective
-- 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 : ℕ
⊢ Eq (α := Submodule R (M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) (LinearMap.range (eval I M n)) ⊤

Tactic:
LinearMap.range_eq_top.2 (eval_surjective I M n)

Premises used: Iff.mpr, LinearMap.range_eq_top, AdicCompletion.eval_surjective
-- 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 : AdicCompletion I M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤]
n : ℕ
⊢ (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
smul_induction_on (SModEq.zero.1 <| h n) (fun r hr x _ ↦ ?_) (fun x y hx hy ↦ ?_)

Premises used: SModEq.zero, Submodule.smul_induction_on, Iff.mp
-- 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 : AdicCompletion I M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤]
n : ℕ
refine_1 :
  ∀ (r : R) (hr : r ∈ I ^ n) (x : AdicCompletion I M),
    Membership.mem (γ := Submodule R (AdicCompletion I M)) ⊤ x →
      (↑(r • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n
refine_2 :
  ∀ (x y : AdicCompletion I M) (hx : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n)
    (hy : (↑y : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n),
    (↑(x + y) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
refine smul_induction_on (SModEq.zero.1 <| h n) (fun r hr x _ ↦ ?_) (fun x y hx hy ↦ ?_)
-- 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 : AdicCompletion I M
h : ∀ (n : ℕ), x_1 ≡ 0 [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤]
n : ℕ
r : R
hr : r ∈ I ^ n
x : AdicCompletion I M
h_1 : Membership.mem (γ := Submodule R (AdicCompletion I M)) ⊤ x
refine_1 : ∀ (a : M), HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) r (Quotient.mk'' a) = 0 n
⊢ r • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0 n

Tactic:
induction x.val n using Quotient.inductionOn' with | _ a

Premises used: Subtype.val
-- 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 : AdicCompletion I M
h : ∀ (n : ℕ), x_1 ≡ 0 [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤]
n : ℕ
r : R
hr : r ∈ I ^ n
x : AdicCompletion I M
h_1 : Membership.mem (γ := Submodule R (AdicCompletion I M)) ⊤ x
a : M
⊢ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) r (Quotient.mk'' a) = 0 n

Tactic:
SModEq.zero.2 <| smul_mem_smul hr mem_top

Premises used: Iff.mpr, SModEq.zero, Submodule.Quotient.mk, Quot.map, Quotient.map', Submodule.smul_mem_smul, Submodule.mem_top, SModEq
-- 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 : AdicCompletion I M
h : ∀ (n : ℕ), x_1 ≡ 0 [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤]
n : ℕ
r : R
hr : r ∈ I ^ n
x : AdicCompletion I M
h_1 : Membership.mem (γ := Submodule R (AdicCompletion I M)) ⊤ x
a : M
⊢ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) r (Quotient.mk'' a) = 0 n

Tactic:
exact SModEq.zero.2 <| smul_mem_smul hr mem_top

Premises used: Iff.mpr, SModEq.zero, Submodule.smul_mem_smul, Submodule.mem_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
x_1 : AdicCompletion I M
h : ∀ (n : ℕ), x_1 ≡ 0 [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤]
n : ℕ
x y : AdicCompletion I M
hx : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n
hy : (↑y : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ (↑(x + y) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
simp only [val_add_apply, hx, val_zero_apply, hy, add_zero]

Premises used: AdicCompletion.val_add_apply, add_zero, AdicCompletion.val_zero_apply
-- 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 : ℕ
hmn : m ≤ n
x : AdicCompletion I M
⊢ (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) m

Tactic:
x.property hmn

Premises used: Set.Mem, 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
m n : ℕ
hmn : m ≤ n
h :
  ∀ (x : AdicCompletion I M),
    Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((transitionMap I M hmn ∘ₗ eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ m • ⊤) x :
        M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((eval I M m : (a : AdicCompletion I M) → M ⧸ I ^ m • ⊤) x : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
⊢ Eq (α := AdicCompletion I M →ₗ[R] M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    (transitionMap I M hmn ∘ₗ eval I M n) (eval I M m)

Tactic:
ext x
-- 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 : ℕ
hmn : m ≤ n
x : AdicCompletion I M
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn ∘ₗ eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ m • ⊤) x :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((eval I M m : (a : AdicCompletion I M) → M ⧸ I ^ m • ⊤) x : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)

Tactic:
simp
-- 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 g : ℕ → M
hf : Membership.mem (γ := Set (ℕ → M)) {f : ℕ → M | IsAdicCauchy I M f} f
hg : Membership.mem (γ := Set (ℕ → M)) {f : ℕ → M | IsAdicCauchy I M f} g
m n : ℕ
hmn : m ≤ n
⊢ (f + g) m ≡ (f + g) n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
SModEq.add (hf hmn) (hg hmn)

Premises used: SModEq.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 g : ℕ → M
hf : Membership.mem (γ := Set (ℕ → M)) {f : ℕ → M | IsAdicCauchy I M f} f
hg : Membership.mem (γ := Set (ℕ → M)) {f : ℕ → M | IsAdicCauchy I M f} g
m n : ℕ
hmn : m ≤ n
⊢ (f + g) m ≡ (f + g) n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
exact SModEq.add (hf hmn) (hg hmn)

Premises used: SModEq.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
m : ℕ
_ : ∀ {n : ℕ}, m ≤ n → 0 m ≡ 0 n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
⊢ ∀ {n : ℕ}, m ≤ n → 0 m ≡ 0 n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
_
-- 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
m n : ℕ
_ : m ≤ n → 0 m ≡ 0 n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
⊢ m ≤ n → 0 m ≡ 0 n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
_
-- 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
m n : ℕ
h : m ≤ n
⊢ 0 m ≡ 0 n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

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
r : R
f : ℕ → M
hf : Membership.mem (γ := Set (ℕ → M)) {f : ℕ → M | IsAdicCauchy I M f} f
m n : ℕ
hmn : m ≤ n
⊢ (r • f) m ≡ (r • f) n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
SModEq.smul (hf hmn) r

Premises used: SModEq.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
r : R
f : ℕ → M
hf : Membership.mem (γ := Set (ℕ → M)) {f : ℕ → M | IsAdicCauchy I M f} f
m n : ℕ
hmn : m ≤ n
⊢ (r • f) m ≡ (r • f) n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
exact SModEq.smul (hf hmn) r

Premises used: SModEq.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 : AdicCauchySequence I M → ℕ → M := Subtype.val (p := fun (f : ℕ → M) ↦ IsAdicCauchy I M f)
⊢ AddCommGroup (AdicCauchySequence I M)

Tactic:
apply Subtype.val_injective.addCommGroup f rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Premises used: Subtype.val_injective, Function.Injective.addCommGroup, 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 : ℕ
⊢ Eq.{u_4 + 1} (α := M) ((↑0 : ℕ → M) n) 0

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 : ℕ
f g : AdicCauchySequence I M
⊢ (↑(f + g) : ℕ → M) n = (↑f : ℕ → M) n + (↑g : ℕ → M) 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 : ℕ
f g : AdicCauchySequence I M
⊢ (↑(f - g) : ℕ → M) n = (↑f : ℕ → M) n - (↑g : ℕ → M) 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 : ℕ
r : R
f : AdicCauchySequence I M
⊢ (↑(r • f) : ℕ → M) n = r • (↑f : ℕ → M) 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
x y : AdicCauchySequence I M
h : ∀ (n : ℕ), (↑x : ℕ → M) n = (↑y : ℕ → M) n
⊢ x = y

Tactic:
Subtype.ext <| funext h

Premises used: funext, AdicCompletion.AdicCauchySequence, Subtype.ext
-- 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 : ℕ
hmn : m ≤ n
f : AdicCauchySequence I M
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R 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: Set.Mem, SModEq.symm, 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
f : ℕ → M
mp : IsAdicCauchy I M f → ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
mpr : (∀ (n : ℕ), f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]) → IsAdicCauchy I M f
⊢ IsAdicCauchy I M f ↔ ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

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
f : ℕ → M
h : IsAdicCauchy I M f
n : ℕ
⊢ f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
h (Nat.le_succ n)

Premises used: Set.Mem, Nat.le_succ
-- 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 : ℕ → M
h : IsAdicCauchy I M f
n : ℕ
⊢ f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
exact h (Nat.le_succ n)

Premises used: Nat.le_succ
-- 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 : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
m n : ℕ
⊢ f m ≡ f m [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

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
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
m n_1 n : ℕ
hmn : m ≤ n
ih trans : f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
trans₁ : f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
trans₂ : M
⊢ f m ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
trans
-- 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 : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
m n_1 n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
⊢ f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
ih
-- 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 : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
m n_1 n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
⊢ f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
exact ih
-- 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 : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
m n_1 n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
⊢ LE.le.{u_4} (α := Submodule R M) ⊤ ⊤

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
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
m n_1 n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
⊢ f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
refine SModEq.mono (smul_mono (Ideal.pow_le_pow_right hmn) (by rfl)) (h n)

Premises used: SModEq.mono, Submodule.smul_mono, Ideal.pow_le_pow_right
-- 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 : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
m n : ℕ
hmn : m ≤ n
mpr : f m ≡ f m [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
mpr₁ :
  ∀ (n : ℕ) (hmn : m ≤ n) (ih : f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]),
    f m ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
⊢ f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]

Tactic:
induction n, hmn using Nat.le_induction with
    | base => rfl
    | succ n hmn ih =>
        trans
        · exact ih
        · refine SModEq.mono (smul_mono (Ideal.pow_le_pow_right hmn) (by rfl)) (h n)

Premises used: SModEq.mono, Submodule.smul_mono, Ideal.pow_le_pow_right
-- 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 : ℕ → M
h rwa rwa₁ rwa₂ rwa₃ : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ IsAdicCauchy I M f

Tactic:
rwa [isAdicCauchy_iff]

Premises used: AdicCompletion.isAdicCauchy_iff