awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
simp_rw :
  Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
    (Ideal.span
      (Set.range (ι := σ)
        (Function.comp (β := MvPowerSeries σ R)
          (⇑(AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) :
            (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
          X)))
    (Ideal.span
      (Set.range (ι := σ)
        (Function.comp (β := MvPolynomial σ R)
          (⇑(algebraMap (MvPolynomial σ R)
                (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) :
            (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
          MvPolynomial.X)))
⊢ Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
    (Ideal.map (R := MvPowerSeries σ R) (F :=
      MvPowerSeries σ R ≃+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) (Ideal.span (Set.range X)))
    (Ideal.map (R := MvPolynomial σ R) (F :=
      MvPolynomial σ R →+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (algebraMap (MvPolynomial σ R)
        (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R))

Tactic:
simp_rw [Ideal.map_span, ← Set.range_comp]

Premises used: Set.range_comp, Ideal.map_span
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
e_s :
  Eq (α := σ → AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    (Function.comp (β := MvPowerSeries σ R)
      (⇑(AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) :
        (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      X)
    (Function.comp (β := MvPolynomial σ R)
      (⇑(algebraMap (MvPolynomial σ R)
            (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) :
        (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      MvPolynomial.X)
⊢ Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
    (Ideal.span
      (Set.range (ι := σ)
        (Function.comp (β := MvPowerSeries σ R)
          (⇑(AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) :
            (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
          X)))
    (Ideal.span
      (Set.range (ι := σ)
        (Function.comp (β := MvPolynomial σ R)
          (⇑(algebraMap (MvPolynomial σ R)
                (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) :
            (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
          MvPolynomial.X)))

Tactic:
congr 2
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
e_s :
  ∀ (x : σ),
    Eq (α := AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (Function.comp (β := MvPowerSeries σ R)
        (⇑(AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) :
          (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        X x)
      (Function.comp (β := MvPolynomial σ R)
        (⇑(algebraMap (MvPolynomial σ R)
              (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) :
          (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        MvPolynomial.X x)
⊢ Eq (α := σ → AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    (Function.comp (β := MvPowerSeries σ R)
      (⇑(AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) :
        (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      X)
    (Function.comp (β := MvPolynomial σ R)
      (⇑(algebraMap (MvPolynomial σ R)
            (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) :
        (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      MvPolynomial.X)

Tactic:
ext1
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
x : σ
⊢ Eq (α := AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    (Function.comp (β := MvPowerSeries σ R)
      (⇑(AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) :
        (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      X x)
    (Function.comp (β := MvPolynomial σ R)
      (⇑(algebraMap (MvPolynomial σ R)
            (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) :
        (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      MvPolynomial.X x)

Tactic:
simp [AdicCompletion.algebraMap_apply, ← MvPolynomial.coe_X, toAdicCompletion_coe]

Premises used: AdicCompletion.algebraMap_apply, MvPowerSeries.toAdicCompletion_coe, MvPolynomial.coe_X
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
⊢ Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
    (Ideal.map (R := MvPowerSeries σ R) (F :=
      MvPowerSeries σ R ≃+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) (Ideal.span (Set.range X)))
    (Ideal.map (R := MvPolynomial σ R) (F :=
      MvPolynomial σ R →+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (algebraMap (MvPolynomial σ R)
        (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R))

Tactic:
have : Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    (MvPolynomial.idealOfVars σ R).map (algebraMap ..):= by
    simp_rw [Ideal.map_span, ← Set.range_comp]
    congr 2; ext1
    simp [AdicCompletion.algebraMap_apply, ← MvPolynomial.coe_X, toAdicCompletion_coe]
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
this :
  Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
    (Ideal.map (R := MvPowerSeries σ R) (F :=
      MvPowerSeries σ R ≃+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) (Ideal.span (Set.range X)))
    (Ideal.map (R := MvPolynomial σ R) (F :=
      MvPolynomial σ R →+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (algebraMap (MvPolynomial σ R)
        (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R))
rw :
  IsAdicComplete (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R)
    (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
⊢ IsAdicComplete (R := MvPowerSeries σ R) (Ideal.span (Set.range X)) (MvPowerSeries σ R)

Tactic:
rw [← IsAdicComplete.congr_ringEquiv _ (toAdicCompletionAlgEquiv σ R).toRingEquiv, this,
    IsAdicComplete.map_algebraMap_iff]

Premises used: MvPowerSeries.toAdicCompletionAlgEquiv, IsAdicComplete.map_algebraMap_iff, IsAdicComplete.congr_ringEquiv, AlgEquiv.toRingEquiv
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
this :
  Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
    (Ideal.map (R := MvPowerSeries σ R) (F :=
      MvPowerSeries σ R ≃+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) (Ideal.span (Set.range X)))
    (Ideal.map (R := MvPolynomial σ R) (F :=
      MvPolynomial σ R →+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (algebraMap (MvPolynomial σ R)
        (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R))
⊢ IsAdicComplete (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R)
    (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))

Tactic:
AdicCompletion.isAdicComplete (MvPolynomial.idealOfVars_fg σ R)

Premises used: Set.Mem, AdicCompletion.isAdicComplete, MvPolynomial.idealOfVars_fg
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
this :
  Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
    (Ideal.map (R := MvPowerSeries σ R) (F :=
      MvPowerSeries σ R ≃+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) (Ideal.span (Set.range X)))
    (Ideal.map (R := MvPolynomial σ R) (F :=
      MvPolynomial σ R →+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (algebraMap (MvPolynomial σ R)
        (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R))
⊢ IsAdicComplete (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R)
    (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))

Tactic:
exact AdicCompletion.isAdicComplete (MvPolynomial.idealOfVars_fg σ R)

Premises used: AdicCompletion.isAdicComplete, MvPolynomial.idealOfVars_fg
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
⊢ IsAdicComplete.{u_1, u_1} (R := MvPowerSeries Unit R) (Ideal.span (Set.range MvPowerSeries.X)) (MvPowerSeries Unit R)

Tactic:
have : IsAdicComplete (.span (.range MvPowerSeries.X) : Ideal (MvPowerSeries Unit R))
    (MvPowerSeries Unit R) := inferInstance
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
this :
  IsAdicComplete.{u_1, u_1} (R := MvPowerSeries Unit R) (Ideal.span (Set.range MvPowerSeries.X)) (MvPowerSeries Unit R)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : IsAdicComplete (R := MvPowerSeries Unit R) (Ideal.span {MvPowerSeries.X default}) (MvPowerSeries Unit R)),
    IsAdicComplete (R := R⟦X⟧) (Ideal.span {X}) R⟦X⟧
⊢ IsAdicComplete (R := R⟦X⟧) (Ideal.span {X}) R⟦X⟧

Tactic:
rwa [Set.range_unique] at this

Premises used: Set.range_unique
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : AdicCauchySequence I N
n : ℕ
y yₙ : M
hy : (f : (a : M) → N) y = (↑x : ℕ → N) (n + 1)
hyₙ : (f : (a : M) → N) yₙ = (↑x : ℕ → N) n
rw : (↑x : ℕ → N) (n + 1) ≡ (↑x : ℕ → N) n [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
⊢ Membership.mem (α := N) (Submodule.map f (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
    ((f : (a : M) → N) (yₙ - y) : N)

Tactic:
rw [Submodule.map_smul'', Submodule.map_top, LinearMap.range_eq_top.2 hf,
      map_sub, hyₙ, hy, ← Submodule.neg_mem_iff, neg_sub, ← SModEq.sub_mem]

Premises used: Iff.mpr, neg_sub, map_sub, Submodule.map_smul'', Submodule.map_top, SModEq.sub_mem, Submodule.neg_mem_iff, LinearMap.range_eq_top
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : AdicCauchySequence I N
n : ℕ
y yₙ : M
hy : (f : (a : M) → N) y = (↑x : ℕ → N) (n + 1)
hyₙ : (f : (a : M) → N) yₙ = (↑x : ℕ → N) n
⊢ (↑x : ℕ → N) (n + 1) ≡ (↑x : ℕ → N) n [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]

Tactic:
AdicCauchySequence.mk_eq_mk (Nat.le_succ n) x

Premises used: AdicCompletion.AdicCauchySequence.mk_eq_mk, Nat.le_succ, SModEq
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : AdicCauchySequence I N
n : ℕ
y yₙ : M
hy : (f : (a : M) → N) y = (↑x : ℕ → N) (n + 1)
hyₙ : (f : (a : M) → N) yₙ = (↑x : ℕ → N) n
⊢ (↑x : ℕ → N) (n + 1) ≡ (↑x : ℕ → N) n [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]

Tactic:
exact AdicCauchySequence.mk_eq_mk (Nat.le_succ n) x

Premises used: AdicCompletion.AdicCauchySequence.mk_eq_mk, Nat.le_succ
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : AdicCauchySequence I N
n : ℕ
y : M := Exists.choose (p := fun (a : M) ↦ (f : (a : M) → N) a = (↑x : ℕ → N) (n + 1)) ⋯
hy :
  (f : (a : M) → N) (Exists.choose (p := fun (a : M) ↦ (f : (a : M) → N) a = (↑x : ℕ → N) (n + 1)) ⋯) =
    (↑x : ℕ → N) (n + 1)
yₙ : M
hyₙ : (f : (a : M) → N) yₙ = (↑x : ℕ → N) n
d : M
property : d ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
p : Eq.{w + 1} (α := N) ((f : (a : M) → N) d : N) ((f : (a : M) → N) (yₙ - y) : N)
⊢ Membership.mem (γ := Set M) (Set.preimage (β := N) (⇑f : (a : M) → N) {(↑x : ℕ → N) n.succ}) (yₙ - d)

Tactic:
simpa [p]
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : AdicCompletion I N
apply :
  ∀ (b : AdicCauchySequence I N),
    ∃ (a : AdicCompletion I M),
      Eq.{w + 1} (α := AdicCompletion I N)
        ((map I f : (a : AdicCompletion I M) → AdicCompletion I N) a : AdicCompletion I N)
        ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)
⊢ ∃ (a : AdicCompletion I M), (map I f : (a : AdicCompletion I M) → AdicCompletion I N) a = y

Tactic:
apply AdicCompletion.induction_on I N y (fun b ↦ ?_)

Premises used: AdicCompletion.induction_on
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → (↑(Set.preimage (β := N) (⇑f : (a : M) → N) {(↑b : ℕ → N) n}) : Type v) := mapPreimage hf b
⊢ ∃ (a : AdicCompletion I M),
    Eq.{w + 1} (α := AdicCompletion I N)
      ((map I f : (a : AdicCompletion I M) → AdicCompletion I N) a : AdicCompletion I N)
      ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)

Tactic:
⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩

Premises used: AdicCompletion.mk, Exists.intro, Subtype.val, AdicCompletion.AdicCauchySequence.mk, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → (↑(Set.preimage (β := N) (⇑f : (a : M) → N) {(↑b : ℕ → N) n}) : Type v) := mapPreimage hf b
refine_1 :
  ∀ (n : ℕ),
    (fun (n : ℕ) ↦ (↑(a n) : M)) n ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) (n + 1) [SMOD
      HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
refine_2 :
  Eq.{w + 1} (α := AdicCompletion I N)
    ((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
        ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
          (AdicCauchySequence.mk I M (fun (n : ℕ) ↦ (↑(a n) : M)) ⋯)) :
      AdicCompletion I N)
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)
⊢ ∃ (a : AdicCompletion I M),
    Eq.{w + 1} (α := AdicCompletion I N)
      ((map I f : (a : AdicCompletion I M) → AdicCompletion I N) a : AdicCompletion I N)
      ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)

Tactic:
refine ⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → (↑(Set.preimage (β := N) (⇑f : (a : M) → N) {(↑b : ℕ → N) n}) : Type v) := mapPreimage hf b
⊢ ∀ (n : ℕ),
    (fun (n : ℕ) ↦ (↑(a n) : M)) n ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) (n + 1) [SMOD
      HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
fun n ↦ SModEq.symm ?_

Premises used: SModEq.symm
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → (↑(Set.preimage (β := N) (⇑f : (a : M) → N) {(↑b : ℕ → N) n}) : Type v) := mapPreimage hf b
refine_1 :
  ∀ (n : ℕ),
    (fun (n : ℕ) ↦ (↑(a n) : M)) (n + 1) ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) n [SMOD
      HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ ∀ (n : ℕ),
    (fun (n : ℕ) ↦ (↑(a n) : M)) n ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) (n + 1) [SMOD
      HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
refine fun n ↦ SModEq.symm ?_

Premises used: SModEq.symm
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → (↑(Set.preimage (β := N) (⇑f : (a : M) → N) {(↑b : ℕ → N) n}) : Type v) := mapPreimage hf b
n : ℕ
⊢ (fun (n : ℕ) ↦ (↑(a n) : M)) (n + 1) ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) n [SMOD
    HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
simp only [SModEq, mapPreimage, Submodule.Quotient.mk_sub,
      sub_eq_self, Submodule.Quotient.mk_eq_zero, SetLike.coe_mem, a]

Premises used: SetLike.coe_mem, Submodule.Quotient.mk_sub, _private.0.AdicCompletion.mapPreimage, sub_eq_self, SModEq, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → (↑(Set.preimage (β := N) (⇑f : (a : M) → N) {(↑b : ℕ → N) n}) : Type v) := mapPreimage hf b
⊢ Eq.{w + 1} (α := AdicCompletion I N)
    ((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
        ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
          (AdicCauchySequence.mk I M (fun (n : ℕ) ↦ (↑(a n) : M)) ⋯)) :
      AdicCompletion I N)
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)

Tactic:
_root_.AdicCompletion.ext fun n ↦ congrArg _ ((a n).property)

Premises used: congrArg, AdicCompletion.ext, Setoid.r, Subtype.property, Quot.mk
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
obtain :
  ∀ (k : ℕ)
    (hk :
      ∀ n ≥ k,
        HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤ ⊓ f.range =
          I ^ (n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range)),
    Function.Injective (α := AdicCompletion I M) (β := AdicCompletion I N)
      (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I N)
⊢ Function.Injective (α := AdicCompletion I M) (β := AdicCompletion I N)
    (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I N)

Tactic:
obtain ⟨k, hk⟩ := Ideal.exists_pow_inf_eq_pow_smul I (range f)

Premises used: LinearMap.range, Ideal.exists_pow_inf_eq_pow_smul
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
k : ℕ
hk :
  ∀ n ≥ k,
    HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤ ⊓ f.range =
      I ^ (n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range)
rw :
  ∀ (m : AdicCompletion I M),
    Eq (α := AdicCompletion I N) ((map I f : (a : AdicCompletion I M) → AdicCompletion I N) m : AdicCompletion I N)
        (0 : AdicCompletion I N) →
      m = 0
⊢ Function.Injective (α := AdicCompletion I M) (β := AdicCompletion I N)
    (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I N)

Tactic:
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']

Premises used: LinearMap.ker_eq_bot, LinearMap.ker_eq_bot'