awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective (α := ι → R) (β := M) (⇑f : (a : ι → R) → M)
inst_3 : IsNoetherianRing R
inst_4 : Finite ι
⊢ Function.Exact (M := AdicCompletion I ↥f.ker) (N := AdicCompletion I (ι → R)) (P := AdicCompletion I M)
    (⇑(map I f.ker.subtype) : (a : AdicCompletion I ↥f.ker) → AdicCompletion I (ι → R))
    (⇑(map I f) : (a : AdicCompletion I (ι → R)) → AdicCompletion I M)

Tactic:
map_exact (Submodule.injective_subtype _) (f.exact_subtype_ker_map) hf

Premises used: Submodule.injective_subtype, AdicCompletion.map_exact, LinearMap.exact_subtype_ker_map
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective (α := ι → R) (β := M) (⇑f : (a : ι → R) → M)
⊢ Function.Surjective (α := AdicCompletion I (ι → R)) (β := AdicCompletion I M)
    (⇑(map I f) : (a : AdicCompletion I (ι → R)) → AdicCompletion I M)

Tactic:
map_surjective I hf

Premises used: AdicCompletion.map_surjective
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective (α := ι → R) (β := M) (⇑f : (a : ι → R) → M)
inst_3 : Finite ι
inst_4 : IsNoetherianRing R
⊢ Function.Bijective (α := AdicCompletion I R ⊗[R] M) (β := AdicCompletion I M)
    (⇑(ofTensorProduct I M) : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M)

Tactic:
LinearMap.bijective_of_surjective_of_bijective_of_bijective_of_injective
    (lTensorKerIncl I M f)
    (lTensorf I M f)
    (0 : AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] Unit)
    (0 : _ →ₗ[AdicCompletion I R] Unit)
    (map I <| (LinearMap.ker f).subtype)
    (map I f)
    (0 : _ →ₗ[AdicCompletion I R] Unit)
    (0 : _ →ₗ[AdicCompletion I R] Unit)
    (ofTensorProduct I (LinearMap.ker f))
    (ofTensorProduct I (ι → R))
    (ofTensorProduct I M)
    0
    0
    (ofTensorProduct_naturality I <| (LinearMap.ker f).subtype)
    (ofTensorProduct_naturality I f)
    rfl
    rfl
    (tens_exact I M f hf)
    ((LinearMap.exact_zero_iff_surjective _ _).mpr <| tens_surj I M f hf)
    ((LinearMap.exact_zero_iff_surjective _ _).mpr <| Function.surjective_to_subsingleton _)
    (adic_exact I M f hf)
    ((LinearMap.exact_zero_iff_surjective _ _).mpr <| adic_surj I M f hf)
    ((LinearMap.exact_zero_iff_surjective _ _).mpr <| Function.surjective_to_subsingleton _)
    (ofTensorProduct_surjective_of_finite I (LinearMap.ker f))
    (ofTensorProduct_bijective_of_pi_of_fintype I ι)
    (Function.bijective_of_subsingleton _)
    (Function.injective_of_subsingleton _)

Premises used: Iff.mpr, LinearMap.exact_zero_iff_surjective, AdicCompletion.ofTensorProduct_surjective_of_finite, Function.bijective_of_subsingleton, _private.0.AdicCompletion.lTensorf, _private.0.AdicCompletion.lTensorKerIncl, LinearMap.ker, AdicCompletion.map, _private.0.AdicCompletion.tens_surj, Membership.mem, Function.injective_of_subsingleton, Subtype, AdicCompletion.ofTensorProduct_bijective_of_pi_of_fintype, Function.surjective_to_subsingleton, _private.0.AdicCompletion.tens_exact, Submodule.subtype, _private.0.AdicCompletion.adic_surj, AdicCompletion.ofTensorProduct_naturality, OfNat.ofNat, _private.0.AdicCompletion.adic_exact, rfl, AdicCompletion.ofTensorProduct, LinearMap.bijective_of_surjective_of_bijective_of_bijective_of_injective
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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
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)
⊢ 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

Premises used: Module.Finite.exists_fin'
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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
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:
ofTensorProduct_bijective_of_map_from_fin I M f hf

Premises used: _private.0.AdicCompletion.ofTensorProduct_bijective_of_map_from_fin
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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
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:
exact ofTensorProduct_bijective_of_map_from_fin I M f hf

Premises used: _private.0.AdicCompletion.ofTensorProduct_bijective_of_map_from_fin
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I R ⊗[R] M)
      (AdicCompletion I M))
    (↑(ofTensorProductEquivOfFiniteNoetherian I M) :
      AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M)
    (ofTensorProduct I M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl, AdicCompletion.ofTensorProduct, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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 : AdicCompletion I R ⊗[R] M
⊢ Eq (α := AdicCompletion I M)
    ((ofTensorProductEquivOfFiniteNoetherian I M : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M) x :
      AdicCompletion I M)
    ((ofTensorProduct I M : (a : AdicCompletion I R ⊗[R] M) → AdicCompletion I M) x : AdicCompletion I M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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 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:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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 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
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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)
rw₁ rw₂ : Eq (α := AdicCompletion I R ⊗[R] M) (1 ⊗ₜ[R] x) (1 ⊗ₜ[R] x)
⊢ 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)

Tactic:
rw [h, LinearEquiv.symm_apply_apply]

Premises used: LinearEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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
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))
⊢ 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)

Tactic:
rw [coe_ofTensorProductEquivOfFiniteNoetherian, ofTensorProduct_naturality I f]

Premises used: AdicCompletion.coe_ofTensorProductEquivOfFiniteNoetherian, AdicCompletion.ofTensorProduct_naturality
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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
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)
⊢ 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:
ext x
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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
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:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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)
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)
⊢ 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)

Tactic:
rw [tensor_map_id_left_eq_map I f]

Premises used: AdicCompletion.tensor_map_id_left_eq_map
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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)
simp :
  Function.Injective (α := AdicCompletion I M) (β := AdicCompletion I N)
    (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I 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)

Tactic:
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective,
    EquivLike.injective_comp]

Premises used: EquivLike.injective_comp, EmbeddingLike.comp_injective, LinearMap.coe_comp, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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 M) (β := AdicCompletion I N)
    (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I N)

Tactic:
map_injective I hf

Premises used: AdicCompletion.map_injective
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
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 M) (β := AdicCompletion I N)
    (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I N)

Tactic:
exact map_injective I hf

Premises used: AdicCompletion.map_injective
-- Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Goal:
R_1 : Type u_1
inst : CommRing R_1
I_1 : Ideal R_1
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R_1 N
R : Type u
inst_5 : CommRing R
I : Ideal R
M : Type u
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : IsNoetherianRing R
⊢ Module.Flat R (AdicCompletion I R)

Tactic:
Module.Flat.iff_lTensor_injective'.mpr fun J ↦
    tensor_map_id_left_injective_of_injective I (Submodule.injective_subtype J)

Premises used: Iff.mpr, Submodule.injective_subtype, AdicCompletion.tensor_map_id_left_injective_of_injective, Module.Flat.iff_lTensor_injective'
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsHausdorff I M
⊢ ∀ (x : M), (∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]) → x = 0

Tactic:
IsHausdorff.haus'

Premises used: IsHausdorff.haus'
-- 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
⊢ IsHausdorff I M ↔ ∀ (x : M), (∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]) → x = 0

Tactic:
⟨IsHausdorff.haus, fun h => ⟨h⟩⟩

Premises used: IsHausdorff.haus, IsHausdorff.mk, Iff.intro
-- 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
inst_3 : IsHausdorff I M
x y : M
⊢ x = y ↔ ∀ (n : ℕ), x ≡ y [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
⟨fun h _ ↦ h ▸ rfl, fun h ↦ ?_⟩

Premises used: Eq.rec, Iff.intro, 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
inst_3 : IsHausdorff I M
x y : M
refine : ∀ (h : ∀ (n : ℕ), x ≡ y [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]), x = y
⊢ x = y ↔ ∀ (n : ℕ), x ≡ y [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
refine ⟨fun h _ ↦ h ▸ rfl, fun h ↦ ?_⟩
-- 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
inst_3 : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
rw : x - y = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- 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
inst_3 : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
apply : ∀ (n : ℕ), x - y ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ x - y = 0

Tactic:
apply IsHausdorff.haus' (I := I) (x - y)

Premises used: HSub.hSub, IsHausdorff.haus'
-- 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
inst_3 : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ ∀ (n : ℕ), x - y ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
simpa [SModEq.sub_mem] using h

Premises used: SModEq.sub_mem
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing S
inst_4 : Module S M
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
⊢ IsHausdorff.{u_2, u_4} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I) M ↔ IsHausdorff I M

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

Premises used: isHausdorff_iff, Submodule.restrictScalars_map_smul_eq, SModEq.restrictScalars, Ideal.map_pow
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing S
inst_4 : Module S M
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
⊢ IsHausdorff I M

Tactic:
⟨fun x h ↦ IsHausdorff.haus ‹_› x fun n ↦ ?_⟩

Premises used: IsHausdorff.haus, IsHausdorff.mk
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing S
inst_4 : Module S M
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
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) ⊤]
⊢ IsHausdorff I M

Tactic:
refine ⟨fun x h ↦ IsHausdorff.haus ‹_› x fun n ↦ ?_⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing S
inst_4 : Module S M
J : Ideal S
inst_5 : Algebra R S
inst_6 : IsScalarTower R S M
hIJ : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ J
inst_7 : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
n : ℕ
h₁ :
  (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).toAddSubgroup ≤
    (HSMul.hSMul (β := Submodule S M) (J ^ n) ⊤).toAddSubgroup
hxy : x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ x ≡ 0 [SMOD HSMul.hSMul (β := Submodule S M) (J ^ n) ⊤]

Tactic:
apply SModEq.of_toAddSubgroup_le
      (U := (I ^ n • ⊤ : Submodule R M)) (V := (J ^ n • ⊤ : Submodule S M))

Premises used: SModEq.of_toAddSubgroup_le