awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ f m = g m
have h₁ : ∀ (n : ℕ), SModEq (R := S) (HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (f m) (g m)
Tactic: rw [IsHausdorff.eq_iff_smodEq (I := I)]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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 ^ n) ⊤) (f m) (g m)
have h₁ : SModEq (R := S) (HSMul.hSMul (β := Submodule S S) (I ^ a n) ⊤) (f m) (g m)
Tactic: apply SModEq.mono (Submodule.pow_smul_top_le I S ha.le_apply)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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 : ℕ
⊢ x - y ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊤ n) ⊤]
have rw : SModEq.{u_1, u_4} (R := R) ⊤ (x - y) 0
Tactic: rw [Ideal.top_pow, top_smul]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (hypothesis)
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 : ℕ
⊢ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
have 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) ⊤
Tactic: have := comap_map_mkQ (⨅ n : ℕ, I ^ n • ⊤ : Submodule R M) (I ^ n • ⊤)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (hypothesis)
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) ⊤
⊢ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
have 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) ⊤
Tactic: simp only [sup_of_le_right (iInf_le (fun n => (I ^ n • ⊤ : Submodule R M)) n)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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) ⊤
⊢ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
have 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) ⊤]
Tactic: rw [← this, map_smul'', Submodule.mem_comap, Submodule.map_top, range_mkQ, ← SModEq.zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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 : ℕ
⊢ Submodule.map f (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ≤ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
have rw : I ^ n • Submodule.map f ⊤ ≤ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
Tactic: rw [map_smul'']
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [lift_of, ← hg, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [lift_of, ← hg, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [lift_of, ← hg, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
have 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) ⊤]
Tactic: refine ⟨fun f hf => ⟨f 1, fun n => ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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 n ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ n) ⊤]
have zero : f 0 ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 0) ⊤]
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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) ⊤]
⊢ f n ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ n) ⊤]
have succ : ∀ (n : ℕ), f (n + 1) ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ (n + 1)) ⊤]
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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) ⊤]
⊢ f 0 ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 0) ⊤]
have zero : SModEq.{u_1, u_4} (R := R) ⊤ (f 0) (f 1)
Tactic: rw [pow_zero, Ideal.one_eq_top, top_smul]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (hypothesis)
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 (n + 1) ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ (n + 1)) ⊤]
have hf₁ : 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)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (hypothesis)
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 (n + 1) ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ (n + 1)) ⊤]
have hf₁ : f 1 = f (n + 1)
Tactic: rw [pow_one, bot_smul, SModEq.bot] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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)
⊢ f (n + 1) ≡ f 1 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ (n + 1)) ⊤]
have succ : f (n + 1) ≡ f (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊥ (n + 1)) ⊤]
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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 : ℕ
⊢ f n ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (HPow.hPow (α := Ideal R) ⊤ n) ⊤]
have rw : SModEq.{u_1, u_4} (R := R) ⊤ (f n) 0
Tactic: rw [Ideal.top_pow, top_smul]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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 : ℕ
⊢ f n ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
have rw : 0 ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
Tactic: rw [Subsingleton.elim (f n) 0]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) ((a + b) n) = (a + b) m
have rw : (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (a n + b n) = (a + b) m
Tactic: rw [Pi.add_apply, Pi.add_apply, map_add, hf hmn, hg hmn]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) ((a + b) n) = (a + b) m
have rw₁ : (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (a n + b n) = a m + b m
Tactic: rw [Pi.add_apply, Pi.add_apply, map_add, hf hmn, hg hmn]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) ((a + b) n) = (a + b) m
have 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
Tactic: rw [Pi.add_apply, Pi.add_apply, map_add, hf hmn, hg hmn]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) ((a + b) n) = (a + b) m
have 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
Tactic: rw [Pi.add_apply, Pi.add_apply, map_add, hf hmn, hg hmn]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) ((a + b) n) = (a + b) m
have rw₄ : a m + b m = a m + b m
Tactic: rw [Pi.add_apply, Pi.add_apply, map_add, hf hmn, hg hmn]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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)
have rw : Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
  ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) 0) (0 m)
Tactic: rw [Pi.zero_apply, Pi.zero_apply, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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)
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (0 n)) (0 m)
have rw₁ : Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
  ((transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) 0) 0
Tactic: rw [Pi.zero_apply, Pi.zero_apply, map_zero]