awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑p : (a : Fin n → R) → M)
f : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : LinearMap.{u_1, u_1, u_1, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
  (AdicCompletion I R ⊗[R] (Fin n → R)) (AdicCompletion I M) :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I M)
    (⇑(ofTensorProduct I M) : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M)
have hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdicCompletion I R ⊗[R] (Fin n → R)) (β := AdicCompletion I M)
  (⇑f : (a : AdicCompletion I R ⊗[R] (Fin n → R)) → AdicCompletion I M)
Tactic: have hf : Function.Surjective f := by
    simp only [hfg, LinearMap.coe_comp, g]
    apply Function.Surjective.comp
    · exact AdicCompletion.map_surjective I hp
    · exact (ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).surjective
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
⊢ Function.Bijective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I M)
    (⇑(ofTensorProduct I M) : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M)
have obtain : ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M) (hf : Function.Surjective (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)),
  Function.Bijective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I M)
    (⇑(ofTensorProduct I M) : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M)
Tactic: obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
⊢ Eq (α := AdicCompletion I R ⊗[R] M)
    ((LinearEquiv.symm (ofTensorProductEquivOfFiniteNoetherian I M) :
          (a : AdicCompletion I M) → AdicCompletion I R ⊗[R] M)
        ((of I M : (a : M) → AdicCompletion I M) x) :
      AdicCompletion I R ⊗[R] M)
    (1 ⊗ₜ[R] x : AdicCompletion I R ⊗[R] M)
have h : Eq (α := AdicCompletion I M) ((of I M : (a : M) → AdicCompletion I M) x : AdicCompletion I M)
  ((ofTensorProductEquivOfFiniteNoetherian I M : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M) (1 ⊗ₜ[R] x) :
    AdicCompletion I M)
Tactic: have h : (of I M) x = ofTensorProductEquivOfFiniteNoetherian I M (1 ⊗ₜ x) := by
    simp
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
h :
  Eq (α := AdicCompletion I M) ((of I M : (a : M) → AdicCompletion I M) x : AdicCompletion I M)
    ((ofTensorProductEquivOfFiniteNoetherian I M : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M) (1 ⊗ₜ[R] x) :
      AdicCompletion I M)
⊢ Eq (α := AdicCompletion I R ⊗[R] M)
    ((LinearEquiv.symm (ofTensorProductEquivOfFiniteNoetherian I M) :
          (a : AdicCompletion I M) → AdicCompletion I R ⊗[R] M)
        ((of I M : (a : M) → AdicCompletion I M) x) :
      AdicCompletion I R ⊗[R] M)
    (1 ⊗ₜ[R] x : AdicCompletion I R ⊗[R] M)
have rw : Eq (α := AdicCompletion I R ⊗[R] M)
  ((LinearEquiv.symm (ofTensorProductEquivOfFiniteNoetherian I M) :
        (a : AdicCompletion I M) → AdicCompletion I R ⊗[R] M)
      ((ofTensorProductEquivOfFiniteNoetherian I M : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M)
        (1 ⊗ₜ[R] x)) :
    AdicCompletion I R ⊗[R] M)
  (1 ⊗ₜ[R] x : AdicCompletion I R ⊗[R] M)
Tactic: rw [h, LinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
h :
  Eq (α := AdicCompletion I M) ((of I M : (a : M) → AdicCompletion I M) x : AdicCompletion I M)
    ((ofTensorProductEquivOfFiniteNoetherian I M : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M) (1 ⊗ₜ[R] x) :
      AdicCompletion I M)
rw :
  Eq (α := AdicCompletion I R ⊗[R] M)
    ((LinearEquiv.symm (ofTensorProductEquivOfFiniteNoetherian I M) :
          (a : AdicCompletion I M) → AdicCompletion I R ⊗[R] M)
        ((ofTensorProductEquivOfFiniteNoetherian I M : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M)
          (1 ⊗ₜ[R] x)) :
      AdicCompletion I R ⊗[R] M)
    (1 ⊗ₜ[R] x : AdicCompletion I R ⊗[R] M)
⊢ Eq (α := AdicCompletion I R ⊗[R] M)
    ((LinearEquiv.symm (ofTensorProductEquivOfFiniteNoetherian I M) :
          (a : AdicCompletion I M) → AdicCompletion I R ⊗[R] M)
        ((of I M : (a : M) → AdicCompletion I M) x) :
      AdicCompletion I R ⊗[R] M)
    (1 ⊗ₜ[R] x : AdicCompletion I R ⊗[R] M)
have rw₁ : Eq (α := AdicCompletion I R ⊗[R] M) (1 ⊗ₜ[R] x) (1 ⊗ₜ[R] x)
Tactic: rw [h, LinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
M : Type u
inst_2 : AddCommGroup M
inst_3 : Module R M
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module R N
f : M →ₗ[R] N
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
⊢ AlgebraTensorModule.map LinearMap.id f =
    (↑(LinearEquiv.symm (ofTensorProductEquivOfFiniteNoetherian I N)) :
        AdicCompletion I N →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] N) ∘ₗ
      map I f ∘ₗ
        (↑(ofTensorProductEquivOfFiniteNoetherian I M) :
          AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M)
have rw : Eq (α :=
  LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] M)
    (AdicCompletion I R ⊗[R] N))
  (AlgebraTensorModule.map LinearMap.id f :
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] M)
      (AdicCompletion I R ⊗[R] N))
  ((↑(LinearEquiv.symm (ofTensorProductEquivOfFiniteNoetherian I N)) :
        AdicCompletion I N →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] N) ∘ₗ
      ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f :
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] M)
      (AdicCompletion I R ⊗[R] N))
Tactic: rw [coe_ofTensorProductEquivOfFiniteNoetherian, ofTensorProduct_naturality I f]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
M : Type u
inst_2 : AddCommGroup M
inst_3 : Module R M
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module R N
f : M →ₗ[R] N
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] M)
      (AdicCompletion I R ⊗[R] N))
    (AlgebraTensorModule.map LinearMap.id f :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] M)
        (AdicCompletion I R ⊗[R] N))
    ((↑(LinearEquiv.symm (ofTensorProductEquivOfFiniteNoetherian I N)) :
          AdicCompletion I N →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] N) ∘ₗ
        ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f :
      LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] M)
        (AdicCompletion I R ⊗[R] N))
have a : ∀ (x : M),
  Eq (α := AdicCompletion I R ⊗[R] N)
    ((((AlgebraTensorModule.curry (AlgebraTensorModule.map LinearMap.id f) :
                LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                  (M →ₗ[R] AdicCompletion I R ⊗[R] N)) :
              (a : AdicCompletion I R) → M →ₗ[R] AdicCompletion I R ⊗[R] N)
            1 :
          (a : M) → AdicCompletion I R ⊗[R] N)
        x :
      AdicCompletion I R ⊗[R] N)
    ((((AlgebraTensorModule.curry
                  ((↑(LinearEquiv.symm (ofTensorProductEquivOfFiniteNoetherian I N)) :
                      AdicCompletion I N →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] N) ∘ₗ
                    ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f) :
                LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R)
                  (M →ₗ[R] AdicCompletion I R ⊗[R] N)) :
              (a : AdicCompletion I R) → M →ₗ[R] AdicCompletion I R ⊗[R] N)
            1 :
          (a : M) → AdicCompletion I R ⊗[R] N)
        x :
      AdicCompletion I R ⊗[R] N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
M : Type u
inst_2 : AddCommGroup M
inst_3 : Module R M
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module R N
f : M →ₗ[R] N
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Function.Injective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I R ⊗[R] N)
    (⇑(AlgebraTensorModule.map LinearMap.id f :
          LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] M)
            (AdicCompletion I R ⊗[R] N)) :
      (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I R ⊗[R] N)
have rw : Function.Injective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I R ⊗[R] N)
  (⇑((↑(LinearEquiv.symm (ofTensorProductEquivOfFiniteNoetherian I N)) :
          AdicCompletion I N →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] N) ∘ₗ
        map I f ∘ₗ
          (↑(ofTensorProductEquivOfFiniteNoetherian I M) :
            AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M)) :
    (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I R ⊗[R] N)
Tactic: rw [tensor_map_id_left_eq_map I f]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.AsTensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
M : Type u
inst_2 : AddCommGroup M
inst_3 : Module R M
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module R N
f : M →ₗ[R] N
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Function.Injective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I R ⊗[R] N)
    (⇑((↑(LinearEquiv.symm (ofTensorProductEquivOfFiniteNoetherian I N)) :
            AdicCompletion I N →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] N) ∘ₗ
          map I f ∘ₗ
            (↑(ofTensorProductEquivOfFiniteNoetherian I M) :
              AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M)) :
      (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I R ⊗[R] N)
have simp : Function.Injective (α := AdicCompletion I M) (β := AdicCompletion I N)
  (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I N)
Tactic: simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective,
    EquivLike.injective_comp]
-- 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
inst_3 : IsHausdorff I M
x y : M
⊢ x = y ↔ ∀ (n : ℕ), x ≡ y [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
have refine : ∀ (h : ∀ (n : ℕ), x ≡ y [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]), x = y
Tactic: refine ⟨fun h _ ↦ h ▸ rfl, fun h ↦ ?_⟩
-- 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
inst_3 : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ x = y
have rw : x - y = 0
Tactic: rw [← sub_eq_zero]
-- 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
inst_3 : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ x - y = 0
have apply : ∀ (n : ℕ), x - y ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
Tactic: apply IsHausdorff.haus' (I := I) (x - y)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ IsHausdorff I M
have refine : ∀ (x : M) (h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]) (n : ℕ),
  x ≡ 0 [SMOD HSMul.hSMul (β := Submodule S M) (J ^ n) ⊤]
Tactic: refine ⟨fun x h ↦ IsHausdorff.haus ‹_› x fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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 S M) (J ^ n) ⊤]
have h₁ : (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).toAddSubgroup ≤ (HSMul.hSMul (β := Submodule S M) (J ^ n) ⊤).toAddSubgroup
Tactic: apply SModEq.of_toAddSubgroup_le
      (U := (I ^ n • ⊤ : Submodule R M)) (V := (J ^ n • ⊤ : Submodule S M))
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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 (β := Submodule R M) (I ^ n) ⊤).toAddSubgroup ≤
    (HSMul.hSMul (β := Submodule S M) (J ^ n) ⊤).toAddSubgroup
⊢ x ≡ 0 [SMOD HSMul.hSMul (β := Submodule S M) (J ^ n) ⊤]
have hxy : x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
Tactic: apply SModEq.of_toAddSubgroup_le
      (U := (I ^ n • ⊤ : Submodule R M)) (V := (J ^ n • ⊤ : Submodule S M))
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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 : ℕ
⊢ (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).toAddSubgroup.toAddSubmonoid ≤
    (HSMul.hSMul (β := Submodule S M) (J ^ n) ⊤).toAddSubgroup.toAddSubmonoid
have h₁ : HSMul.hSMul (β := AddSubmonoid M) (I ^ n).toAddSubmonoid ⊤ ≤ HSMul.hSMul (β := AddSubmonoid M) (J ^ n).toAddSubmonoid ⊤
Tactic: simp only [Submodule.smul_toAddSubmonoid, Submodule.top_toAddSubmonoid]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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 : ℕ
⊢ HSMul.hSMul (β := AddSubmonoid M) (I ^ n).toAddSubmonoid ⊤ ≤
    HSMul.hSMul (β := AddSubmonoid M) (J ^ n).toAddSubmonoid ⊤
have h₁ : ∀ m ∈ (I ^ n).toAddSubmonoid,
  ∀ (n_1 : M),
    Membership.mem (γ := AddSubmonoid M) ⊤ n_1 → m • n_1 ∈ HSMul.hSMul (β := AddSubmonoid M) (J ^ n).toAddSubmonoid ⊤
Tactic: rw [AddSubmonoid.smul_le]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ r • m ∈ HSMul.hSMul (β := AddSubmonoid M) (J ^ n).toAddSubmonoid ⊤
have 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 ⊤
Tactic: rw [← algebraMap_smul S r m]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ 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 ⊤
have apply : Membership.mem (α := S) (J ^ n).toAddSubmonoid ((algebraMap R S : (a : R) → S) r : S)
Tactic: apply AddSubmonoid.smul_mem_smul ?_ hm
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (hypothesis)
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 (α := S) (J ^ n).toAddSubmonoid ((algebraMap R S : (a : R) → S) r : S)
have 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)
Tactic: have := Ideal.mem_map_of_mem (algebraMap R S) hr
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (hypothesis)
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) (J ^ n).toAddSubmonoid ((algebraMap R S : (a : R) → S) r : S)
have 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)
Tactic: simp only [Ideal.map_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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))
⊢ f = g
have h₁ : ∀ (m : M), f m = g m
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ f m = g m
have h₁ : ∀ (n : ℕ), f m ≡ g m [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
Tactic: rw [IsHausdorff.eq_iff_smodEq (I := I)]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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))
⊢ f = g
have h₁ : ∀ (m : M), f m = g m
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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
⊢ f m = g m
have h₁ : ∀ (n : ℕ), f m ≡ g m [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
Tactic: rw [IsHausdorff.eq_iff_smodEq (I := I)]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
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 ^ n) ⊤]
have h₁ : f m ≡ g m [SMOD HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤]
Tactic: apply SModEq.mono (Submodule.pow_smul_top_le I N ha.le_apply)
-- 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
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)
⊢ f = g
have h₁ : ∀ (r : R), f r = g r
Tactic: ext r
-- 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
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
⊢ f r = g r
have h₁ : ∀ (n : ℕ), SModEq (R := S) (HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (f r) (g r)
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)
⊢ f = g
have h₁ : ∀ (m : R), f m = g m
Tactic: ext m