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
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) ⊤
⊢ (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) ⊤]

Tactic:
hx n

Premises used: Set.Mem, Submodule.Quotient.mk
-- 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) ⊤
⊢ (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) ⊤]

Tactic:
exact hx 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
h : IsHausdorff I N
f : M →ₗ[R] N
n : ℕ
rw : I ^ n • Submodule.map f ⊤ ≤ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
⊢ Submodule.map f (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ≤ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤

Tactic:
rw [map_smul'']

Premises used: Submodule.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
h : IsHausdorff I N
f : M →ₗ[R] N
n : ℕ
⊢ I ^ n • Submodule.map f ⊤ ≤ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤

Tactic:
smul_mono le_rfl le_top

Premises used: le_rfl, Submodule.smul_mono, Set.Mem, le_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
h : IsHausdorff I N
f : M →ₗ[R] N
n : ℕ
⊢ I ^ n • Submodule.map f ⊤ ≤ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤

Tactic:
exact smul_mono le_rfl le_top

Premises used: le_rfl, Submodule.smul_mono, le_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 : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
h : IsHausdorff I N
f : M →ₗ[R] N
x : M
⊢ Eq.{u_5 + 1} (α := N)
    ((lift I f : (a : Hausdorffification I M) → N)
        ((of I M : (a : M) → Hausdorffification I M) x : Hausdorffification I M) :
      N)
    ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, 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
h : IsHausdorff I N
f : M →ₗ[R] N
⊢ lift I f ∘ₗ of I M = f

Tactic:
LinearMap.ext fun _ => rfl

Premises used: LinearMap.ext, 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
h : IsHausdorff I N
f : M →ₗ[R] N
g : LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (Hausdorffification I M) N
hg : g ∘ₗ of I M = f
x_1 : Hausdorffification I M
x : M
rw :
  Eq.{u_5 + 1} (α := N)
    ((g : (a : Hausdorffification I M) → N) ((of I M : (a : M) → Hausdorffification I M) x : Hausdorffification I M) :
      N)
    ((f : (a : M) → N) x : N)
rw₁ :
  Eq.{u_5 + 1} (α := N)
    ((g : (a : Hausdorffification I M) → N) ((of I M : (a : M) → Hausdorffification I M) x : Hausdorffification I M) :
      N)
    ((g ∘ₗ of I M : (a : M) → N) x : N)
rw₂ rw₃ :
  Eq.{u_5 + 1} (α := N)
    ((g : (a : Hausdorffification I M) → N) ((of I M : (a : M) → Hausdorffification I M) x : Hausdorffification I M) :
      N)
    ((g : (a : Hausdorffification I M) → N) ((of I M : (a : M) → Hausdorffification I M) x : Hausdorffification I M) :
      N)
⊢ Eq.{u_5 + 1} (α := N)
    ((g : (a : Hausdorffification I M) → N) ((of I M : (a : M) → Hausdorffification I M) x : Hausdorffification I M) :
      N)
    ((lift I f : (a : Hausdorffification I M) → N)
        ((of I M : (a : M) → Hausdorffification I M) x : Hausdorffification I M) :
      N)

Tactic:
rw [lift_of, ← hg, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, Hausdorffification.lift_of
-- 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
⊢ IsPrecomplete.{u_1, u_4} (R := R) ⊥ M

Tactic:
⟨fun f hf => ⟨f 1, fun n => ?_⟩⟩

Premises used: Exists.intro, IsPrecomplete.mk, OfNat.ofNat
-- 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
refine :
  ∀ (f : ℕ → M)
    (hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ m) ⊤])
    (n : ℕ), f n ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ n) ⊤]
⊢ IsPrecomplete.{u_1, u_4} (R := R) ⊥ M

Tactic:
refine ⟨fun f hf => ⟨f 1, fun 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
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ m) ⊤]
n : ℕ
zero : f 0 ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 0) ⊤]
succ : ∀ (n : ℕ), f (n + 1) ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ (n + 1)) ⊤]
⊢ f n ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ n) ⊤]

Tactic:
rcases n with - | 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
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ m) ⊤]
zero : SModEq.{u_1, u_4} (R := R) ⊤ (f 0) (f 1)
⊢ f 0 ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 0) ⊤]

Tactic:
rw [pow_zero, Ideal.one_eq_top, top_smul]

Premises used: Ideal.one_eq_top, pow_zero, Submodule.top_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 : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ m) ⊤]
⊢ SModEq.{u_1, u_4} (R := R) ⊤ (f 0) (f 1)

Tactic:
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
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ m) ⊤]
⊢ SModEq.{u_1, u_4} (R := R) ⊤ (f 0) (f 1)

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
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ m) ⊤]
n : ℕ
⊢ f 1 ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 1) ⊤]

Tactic:
specialize hf (Nat.le_add_left 1 n)

Premises used: Nat.le_add_left, OfNat.ofNat
-- 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
n : ℕ
hf : f 1 ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 1) ⊤]
⊢ f 1 = f (n + 1)

Tactic:
rw [pow_one, bot_smul, SModEq.bot] at hf

Premises used: SModEq.bot, Submodule.bot_smul, pow_one
-- 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
n : ℕ
hf : f 1 = f (n + 1)
succ succ₁ : f (n + 1) ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ (n + 1)) ⊤]
⊢ f (n + 1) ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ (n + 1)) ⊤]

Tactic:
rw [hf]
-- 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 : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊤ m) ⊤]
n : ℕ
rw : SModEq.{u_1, u_4} (R := R) ⊤ (f n) 0
⊢ f n ≡ 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
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 : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊤ m) ⊤]
n : ℕ
⊢ SModEq.{u_1, u_4} (R := R) ⊤ (f n) 0

Tactic:
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
f : ℕ → M
h : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊤ m) ⊤]
n : ℕ
⊢ SModEq.{u_1, u_4} (R := R) ⊤ (f n) 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
f : ℕ → M
h : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤]
n : ℕ
rw rw₁ : 0 ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ f n ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
rw [Subsingleton.elim (f n) 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- 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
a b : (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hf :
  Membership.mem (γ := Set ((n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
    {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}
    a
hg :
  Membership.mem (γ := Set ((n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
    {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}
    b
m n : ℕ
hmn : m ≤ n
rw : (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (a n + b n) = (a + b) m
rw₁ : (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (a n + b n) = a m + b m
rw₂ :
  HAdd.hAdd (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (a n) :
        M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (b n) :
        M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    a m + b m
rw₃ :
  HAdd.hAdd (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) (a m)
      ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (b n) :
        M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    a m + b m
rw₄ rw₅ : a m + b m = a m + b m
⊢ (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) ((a + b) n) = (a + b) m

Tactic:
rw [Pi.add_apply, Pi.add_apply, map_add, hf hmn, hg hmn]

Premises used: map_add, Pi.add_apply
-- 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 : ℕ
hmn : m ≤ n
rw :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) 0) (0 m)
rw₁ :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) 0) 0
rw₂ rw₃ : Eq.{u_4 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) 0 0
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (0 n)) (0 m)

Tactic:
rw [Pi.zero_apply, Pi.zero_apply, map_zero]

Premises used: Pi.zero_apply, map_zero
-- 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
c : R
f : (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
hf :
  Membership.mem (γ := Set ((n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
    {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}
    f
m n : ℕ
hmn : m ≤ n
rw : (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (c • f n) = (c • f) m
rw₁ : (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (c • f n) = c • f m
rw₂ :
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) c
      ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (f n) :
        M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    c • f m
rw₃ rw₄ : c • f m = c • f m
⊢ (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) ((c • f) n) = (c • f) m

Tactic:
rw [Pi.smul_apply, Pi.smul_apply, map_smul, hf hmn]

Premises used: map_smul, Pi.smul_apply
-- 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 : ℕ} (hmn : m ≤ n),
    Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (0 n)) (0 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
x y : AdicCompletion I M
⊢ ∀ {m n : ℕ} (hmn : m ≤ n),
    (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤)
        (((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) + (↑y : (n : ℕ) → M ⧸ I ^ n • ⊤)) n) =
      ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) + (↑y : (n : ℕ) → M ⧸ I ^ n • ⊤)) m

Tactic:
simp [x.property, y.property]

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

Tactic:
simp [x.property]

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

Tactic:
simp [x.property, y.property]

Premises used: 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
inst_5 : SMul S R
inst_6 : SMul S M
inst_7 : IsScalarTower S R M
r : S
x : AdicCompletion I M
⊢ ∀ {m n : ℕ} (hmn : m ≤ n),
    (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) ((r • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤)) n) =
      (r • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤)) m

Tactic:
simp [x.property]

Premises used: 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
⊢ Eq.{u_4 + 1} (α := (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) (↑0 : (n : ℕ) → M ⧸ I ^ 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 : ℕ
⊢ Eq.{u_4 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ((↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) 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
f g : AdicCompletion I M
⊢ (↑(f + g) : (n : ℕ) → M ⧸ I ^ n • ⊤) = (↑f : (n : ℕ) → M ⧸ I ^ n • ⊤) + (↑g : (n : ℕ) → M ⧸ 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
f g : AdicCompletion I M
⊢ (↑(f - g) : (n : ℕ) → M ⧸ I ^ n • ⊤) = (↑f : (n : ℕ) → M ⧸ I ^ n • ⊤) - (↑g : (n : ℕ) → M ⧸ 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
f : AdicCompletion I M
⊢ (↑(-f) : (n : ℕ) → M ⧸ I ^ n • ⊤) = -(↑f : (n : ℕ) → M ⧸ 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
f g : AdicCompletion I M
n : ℕ
⊢ (↑(f + g) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑f : (n : ℕ) → M ⧸ I ^ n • ⊤) n + (↑g : (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
f g : AdicCompletion I M
n : ℕ
⊢ (↑(f - g) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑f : (n : ℕ) → M ⧸ I ^ n • ⊤) n - (↑g : (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
f : AdicCompletion I M
n : ℕ
⊢ (↑(-f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = -(↑f : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
rfl

Premises used: rfl
-- 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 : SMul S R
inst_4 : SMul S M
inst_5 : IsScalarTower S R M
s : S
f : AdicCompletion I M
⊢ (↑(s • f) : (n : ℕ) → M ⧸ I ^ n • ⊤) = s • (↑f : (n : ℕ) → M ⧸ I ^ n • ⊤)

Tactic:
rfl

Premises used: rfl
-- 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 : SMul S R
inst_4 : SMul S M
inst_5 : IsScalarTower S R M
s : S
f : AdicCompletion I M
n : ℕ
⊢ (↑(s • f) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = s • (↑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
x y : AdicCompletion I M
h : ∀ (n : ℕ), (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑y : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ x = y

Tactic:
Subtype.ext <| funext h

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

Tactic:
simp [val_smul]

Premises used: AdicCompletion.val_smul