awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
S : Type u_6
inst_1 : CommRing S
f : R →+* S
inst_2 : IsPrecomplete I R
haus : IsHausdorff (R := S) (Ideal.map f I) S
x : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := AlgHom.toLinearMap (Algebra.ofId R S)
h :
  Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β :=
    HasQuotient.Quotient S (B := Submodule R S) (restrictScalars R (Ideal.map f I)))
    (⇑(mkQ (restrictScalars R (Ideal.map f I)) ∘ₗ fₗ) : (a : R) → S ⧸ restrictScalars R (Ideal.map f I))
⊢ Eq.{u_6 + 1} (α := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I) (Ideal.map f I)

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
S : Type u_6
inst_1 : CommRing S
f : R →+* S
inst_2 : IsPrecomplete I R
haus : IsHausdorff (R := S) (Ideal.map f I) S
x : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := AlgHom.toLinearMap (Algebra.ofId R S)
h :
  Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β :=
    HasQuotient.Quotient S (B := Submodule R S) (restrictScalars R (Ideal.map f I)))
    (⇑(mkQ (restrictScalars R (Ideal.map f I)) ∘ₗ fₗ) : (a : R) → S ⧸ restrictScalars R (Ideal.map f I))
⊢ HSMul.hSMul (β := Submodule R S) I ⊤ = restrictScalars R (Ideal.map f I)

Tactic:
have : I • ⊤ = restrictScalars R (Ideal.map f I) := by
    simp only [Ideal.smul_top_eq_map, restrictScalars_inj]
    rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
S : Type u_6
inst_1 : CommRing S
f : R →+* S
inst_2 : IsPrecomplete I R
haus : IsHausdorff (R := S) (Ideal.map f I) S
x : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := AlgHom.toLinearMap (Algebra.ofId R S)
h :
  Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β :=
    HasQuotient.Quotient S (B := Submodule R S) (restrictScalars R (Ideal.map f I)))
    (⇑(mkQ (restrictScalars R (Ideal.map f I)) ∘ₗ fₗ) : (a : R) → S ⧸ restrictScalars R (Ideal.map f I))
this : HSMul.hSMul (β := Submodule R S) I ⊤ = restrictScalars R (Ideal.map f I)
⊢ IsHausdorff I S

Tactic:
have _ := IsHausdorff.map_algebraMap_iff.mp haus
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
S : Type u_6
inst_1 : CommRing S
f : R →+* S
inst_2 : IsPrecomplete I R
haus : IsHausdorff (R := S) (Ideal.map f I) S
x : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := AlgHom.toLinearMap (Algebra.ofId R S)
h :
  Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β :=
    HasQuotient.Quotient S (B := Submodule R S) (restrictScalars R (Ideal.map f I)))
    (⇑(mkQ (restrictScalars R (Ideal.map f I)) ∘ₗ fₗ) : (a : R) → S ⧸ restrictScalars R (Ideal.map f I))
this : HSMul.hSMul (β := Submodule R S) I ⊤ = restrictScalars R (Ideal.map f I)
h_1 : IsHausdorff I S
apply :
  Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β := S ⧸ HSMul.hSMul (β := Submodule R S) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R S) I ⊤).mkQ ∘ₗ fₗ) : (a : R) → S ⧸ I • ⊤)
⊢ Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
apply surjective_of_mkQ_comp_surjective (I := I) (f := fₗ)

Premises used: surjective_of_mkQ_comp_surjective
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
S : Type u_6
inst_1 : CommRing S
f : R →+* S
inst_2 : IsPrecomplete I R
haus : IsHausdorff (R := S) (Ideal.map f I) S
x : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := AlgHom.toLinearMap (Algebra.ofId R S)
h :
  Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β :=
    HasQuotient.Quotient S (B := Submodule R S) (restrictScalars R (Ideal.map f I)))
    (⇑(mkQ (restrictScalars R (Ideal.map f I)) ∘ₗ fₗ) : (a : R) → S ⧸ restrictScalars R (Ideal.map f I))
this : HSMul.hSMul (β := Submodule R S) I ⊤ = restrictScalars R (Ideal.map f I)
h_1 : IsHausdorff I S
rwa rwa₁ rwa₂ rwa₃ :
  Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β :=
    HasQuotient.Quotient S (B := Submodule R S) (restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) I)))
    (⇑(mkQ (restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) I)) ∘ₗ fₗ) :
      (a : R) → S ⧸ restrictScalars R (Ideal.map (algebraMap R S) I))
⊢ Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β := S ⧸ HSMul.hSMul (β := Submodule R S) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R S) I ⊤).mkQ ∘ₗ fₗ) : (a : R) → S ⧸ I • ⊤)

Tactic:
rwa [Ideal.smul_top_eq_map]

Premises used: Ideal.smul_top_eq_map
-- Module: Mathlib.RingTheory.AdicCompletion.LocalRing
Goal:
R : Type u_1
inst : CommRing R
m : Ideal R
inst_1 : m.IsMaximal
inst_2 : IsAdicComplete m R
⊢ IsLocalRing R

Tactic:
IsLocalRing.of_unique_max_ideal ⟨m, ‹m.IsMaximal›, fun _ hJ ↦
    (‹m.IsMaximal›.eq_of_le hJ.ne_top <|
      (IsAdicComplete.le_jacobson_bot m).trans <| sInf_le ⟨bot_le, hJ⟩).symm⟩

Premises used: IsLocalRing.of_unique_max_ideal, IsAdicComplete.le_jacobson_bot, Ideal.IsMaximal.eq_of_le, sInf_le, And.intro, Exists.intro, Ideal.IsMaximal.ne_top, LE.le.trans, Eq.symm, bot_le
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
h : I ≤ Ideal.jacobson ⊥
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x

Tactic:
simpa [SModEq.zero] using hx

Premises used: SModEq.zero
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
inst_5 : IsLocalRing R
h : I ≠ ⊤
⊢ IsHausdorff I M

Tactic:
of_le_jacobson I M ((le_maximalIdeal h).trans (maximalIdeal_le_jacobson _))

Premises used: IsLocalRing.maximalIdeal_le_jacobson, IsHausdorff.of_le_jacobson, IsLocalRing.le_maximalIdeal, LE.le.trans
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
inst_5 : IsLocalRing R
⊢ IsHausdorff (maximalIdeal R) M

Tactic:
.of_le_jacobson _ _ (maximalIdeal_le_jacobson _)

Premises used: IsLocalRing.maximalIdeal_le_jacobson, IsHausdorff.of_le_jacobson
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
h : I ≠ ⊤
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x

Tactic:
simpa [SModEq.zero] using hx

Premises used: SModEq.zero
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsDomain R
h : I ≠ ⊤
⊢ IsHausdorff I R

Tactic:
.of_isTorsionFree I R h

Premises used: IsHausdorff.of_isTorsionFree
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
A : Type u_3
inst_5 : CommRing A
inst_6 : IsArtinianRing A
inst_7 : IsLocalRing A
f : ℕ → A
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
obtain :
  ∀ (n : ℕ) (hn : HPow.hPow (α := Ideal A) (maximalIdeal A) n = 0),
    ∃ (L : A),
      ∀ (n : ℕ),
        SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) n) ⊤) (f n) L
⊢ ∃ (L : A),
    ∀ (n : ℕ),
      SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) n) ⊤) (f n) L

Tactic:
obtain ⟨n, hn⟩ := (isArtinianRing_iff_isNilpotent_maximalIdeal A).mp ‹_›

Premises used: isArtinianRing_iff_isNilpotent_maximalIdeal, Iff.mp
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
A : Type u_3
inst_5 : CommRing A
inst_6 : IsArtinianRing A
inst_7 : IsLocalRing A
f : ℕ → A
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
n : ℕ
hn : HPow.hPow (α := Ideal A) (maximalIdeal A) n = 0
h :
  ∀ (n_1 : ℕ),
    SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) n_1) ⊤) (f n_1) (f n)
⊢ ∃ (L : A),
    ∀ (n : ℕ),
      SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) n) ⊤) (f n) L

Tactic:
use f n
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
A : Type u_3
inst_5 : CommRing A
inst_6 : IsArtinianRing A
inst_7 : IsLocalRing A
f : ℕ → A
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
n : ℕ
hn : HPow.hPow (α := Ideal A) (maximalIdeal A) n = 0
m : ℕ
pos :
  ∀ (h : m ≤ n),
    SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
neg :
  ∀ (h : ¬m ≤ n),
    SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
⊢ SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)

Tactic:
by_cases h : m ≤ n
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
A : Type u_3
inst_5 : CommRing A
inst_6 : IsArtinianRing A
inst_7 : IsLocalRing A
f : ℕ → A
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
n : ℕ
hn : HPow.hPow (α := Ideal A) (maximalIdeal A) n = 0
m : ℕ
h : m ≤ n
⊢ SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)

Tactic:
hf h
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
A : Type u_3
inst_5 : CommRing A
inst_6 : IsArtinianRing A
inst_7 : IsLocalRing A
f : ℕ → A
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
n : ℕ
hn : HPow.hPow (α := Ideal A) (maximalIdeal A) n = 0
m : ℕ
h : m ≤ n
⊢ SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)

Tactic:
exact hf h
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
A : Type u_3
inst_5 : CommRing A
inst_6 : IsArtinianRing A
inst_7 : IsLocalRing A
f : ℕ → A
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
n : ℕ
hn : HPow.hPow (α := Ideal A) (maximalIdeal A) n = 0
m : ℕ
h : ¬m ≤ n
⊢ n ≤ m

Tactic:
lia
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
A : Type u_3
inst_5 : CommRing A
inst_6 : IsArtinianRing A
inst_7 : IsLocalRing A
f : ℕ → A
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
n : ℕ
hn : HPow.hPow (α := Ideal A) (maximalIdeal A) n = 0
m : ℕ
h : ¬m ≤ n
⊢ SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) n) ⊤) (f n) (f m)

Tactic:
specialize hf (show n ≤ m by lia)
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
A : Type u_3
inst_5 : CommRing A
inst_6 : IsArtinianRing A
inst_7 : IsLocalRing A
f : ℕ → A
n : ℕ
hn : HPow.hPow (α := Ideal A) (maximalIdeal A) n = 0
m : ℕ
h : ¬m ≤ n
hf : SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) n) ⊤) (f n) (f m)
⊢ f n = f m

Tactic:
rw [hn, zero_smul, Ideal.zero_eq_bot, SModEq.bot] at hf

Premises used: SModEq.bot, Ideal.zero_eq_bot, zero_smul
-- Module: Mathlib.RingTheory.AdicCompletion.Noetherian
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 : IsNoetherianRing R
inst_4 : Module.Finite R M
A : Type u_3
inst_5 : CommRing A
inst_6 : IsArtinianRing A
inst_7 : IsLocalRing A
f : ℕ → A
n : ℕ
hn : HPow.hPow (α := Ideal A) (maximalIdeal A) n = 0
m : ℕ
h : ¬m ≤ n
hf : f n = f m
neg neg₁ :
  SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f m)
⊢ SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)

Tactic:
rw [hf]
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
inst_2 : IsAdicComplete I S
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (factorPow I hle) (f n) = f m
x : R
⊢ Eq (α := AdicCompletion I S)
    ((of I S : (a : S) → AdicCompletion I S) ((liftRingHom I f ⋯ : (a : R) → S) x) : AdicCompletion I S)
    ((AdicCompletion.liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x : AdicCompletion I S)

Tactic:
simp [liftRingHom]

Premises used: IsAdicComplete.liftRingHom
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
inst_2 : IsAdicComplete I S
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (factorPow I hle) (f n) = f m
a :
  ∀ (x : R) (n : ℕ),
    Eq.{u_2 + 1} (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
      ((↑(((RingHom.comp (↑(ofAlgEquiv I) : S →+* AdicCompletion I S) (liftRingHom I f ⋯) :
                  RingHom.{u_1, u_2} R (AdicCompletion I S)) :
                (a : R) → AdicCompletion I S)
              x) :
          (n : ℕ) → S ⧸ I ^ n • ⊤)
        n)
      ((↑((AdicCompletion.liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x) : (n : ℕ) → S ⧸ I ^ n • ⊤) n)
⊢ RingHom.comp (↑(ofAlgEquiv I) : S →+* AdicCompletion I S) (liftRingHom I f ⋯) = AdicCompletion.liftRingHom I f ⋯

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
inst_2 : IsAdicComplete I S
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (factorPow I hle) (f n) = f m
x : R
n : ℕ
⊢ Eq.{u_2 + 1} (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
    ((↑(((RingHom.comp (↑(ofAlgEquiv I) : S →+* AdicCompletion I S) (liftRingHom I f ⋯) :
                RingHom.{u_1, u_2} R (AdicCompletion I S)) :
              (a : R) → AdicCompletion I S)
            x) :
        (n : ℕ) → S ⧸ I ^ n • ⊤)
      n)
    ((↑((AdicCompletion.liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x) : (n : ℕ) → S ⧸ I ^ n • ⊤) n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
inst_2 : IsAdicComplete I S
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (factorPow I hle) (f n) = f m
n : ℕ
x : R
simp :
  Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n)
        (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S)
          ((AdicCompletion.liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x : AdicCompletion I S)) :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)
⊢ Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) ((liftRingHom I f ⋯ : (a : R) → S) x) : S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
simp only [liftRingHom, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply]

Premises used: RingHom.coe_coe, IsAdicComplete.liftRingHom, RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
inst_2 : IsAdicComplete I S
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (factorPow I hle) (f n) = f m
n : ℕ
x : R
rw :
  Eq (α := S ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n)
        ((of I S : (a : S) → AdicCompletion I S)
          (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S)
            ((AdicCompletion.liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x : AdicCompletion I S))) :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)
⊢ Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n)
        (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S)
          ((AdicCompletion.liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x : AdicCompletion I S)) :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
rw [← evalₐ_of I n]

Premises used: AdicCompletion.evalₐ_of
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
inst_2 : IsAdicComplete I S
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (factorPow I hle) (f n) = f m
n : ℕ
x : R
⊢ Eq (α := S ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n)
        ((of I S : (a : S) → AdicCompletion I S)
          (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S)
            ((AdicCompletion.liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x : AdicCompletion I S))) :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
inst_2 : IsAdicComplete I S
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (factorPow I hle) (f n) = f m
n : ℕ
a :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S ⧸ I ^ n)
      (((RingHom.comp (Ideal.Quotient.mk (I ^ n)) (liftRingHom I f ⋯) : RingHom.{u_1, u_2} R (S ⧸ I ^ n)) :
            (a : R) → S ⧸ I ^ n)
          x :
        S ⧸ I ^ n)
      ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)
⊢ RingHom.comp (Ideal.Quotient.mk (I ^ n)) (liftRingHom I f ⋯) = f n

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
inst_2 : IsAdicComplete I S
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (factorPow I hle) (f n) = f m
n : ℕ
x : R
⊢ Eq.{u_2 + 1} (α := S ⧸ I ^ n)
    (((RingHom.comp (Ideal.Quotient.mk (I ^ n)) (liftRingHom I f ⋯) : RingHom.{u_1, u_2} R (S ⧸ I ^ n)) :
          (a : R) → S ⧸ I ^ n)
        x :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
inst_2 : IsAdicComplete I S
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (factorPow I hle) (f n) = f m
F : R →+* S
hF : ∀ (n : ℕ), RingHom.comp (Ideal.Quotient.mk (I ^ n)) F = f n
a :
  Eq (α := (a : R) → S) ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) F)
    ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) (liftRingHom I f ⋯))
⊢ F = liftRingHom I f ⋯

Tactic:
apply DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
inst_2 : IsAdicComplete I S
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (factorPow I hle) (f n) = f m
F : R →+* S
hF : ∀ (n : ℕ), RingHom.comp (Ideal.Quotient.mk (I ^ n)) F = f n
a :
  ∀ (n : ℕ) (r : R),
    Eq (α := S ⧸ I ^ n)
      ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) F r))
      ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n)
        ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) (liftRingHom I f ⋯) r))
⊢ Eq (α := (a : R) → S) ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) F)
    ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) (liftRingHom I f ⋯))

Tactic:
apply IsHausdorff.funext' I

Premises used: IsHausdorff.funext'
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
inst_2 : IsAdicComplete I S
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (factorPow I hle) (f n) = f m
F : R →+* S
hF : ∀ (n : ℕ), RingHom.comp (Ideal.Quotient.mk (I ^ n)) F = f n
n : ℕ
m : R
⊢ Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) F m))
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n)
      ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) (liftRingHom I f ⋯) m))

Tactic:
simp [← hF n]
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
inst_3 : IsAdicComplete I S
inst_4 : CommRing A
inst_5 : Algebra R A
f : (n : ℕ) → AlgHom.{u_3, u_5, u_4} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (factorₐ R ⋯) (f n) = f m
n : ℕ
x : A
⊢ Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) ((liftAlgHom I f ⋯ : (a : A) → S) x) : S ⧸ I ^ n)
    ((f n : (a : A) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
simp [liftAlgHom]

Premises used: IsAdicComplete.liftAlgHom
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
inst_3 : IsAdicComplete I S
inst_4 : CommRing A
inst_5 : Algebra R A
f : (n : ℕ) → AlgHom.{u_3, u_5, u_4} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (factorₐ R ⋯) (f n) = f m
n : ℕ
⊢ AlgHom.comp (Quotient.mkₐ R (I ^ n)) (liftAlgHom I f ⋯) = f n

Tactic:
AlgHom.ext fun _ ↦ mk_liftAlgHom _ _ hf _ _

Premises used: AlgHom.ext, IsAdicComplete.mk_liftAlgHom
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
inst_3 : IsAdicComplete I S
inst_4 : CommRing A
inst_5 : Algebra R A
f g : A →ₐ[R] S
H :
  ∀ (n : ℕ),
    Eq (α := AlgHom.{u_3, u_5, u_4} R A (S ⧸ I ^ n)) (AlgHom.comp (Quotient.mkₐ R (I ^ n)) f)
      (AlgHom.comp (Quotient.mkₐ R (I ^ n)) g)
rw :
  Eq (α := AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S))
    (AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) f)
    (AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) g)
⊢ f = g

Tactic:
rw [← AlgHom.cancel_left (f := ((ofAlgEquiv I).restrictScalars R).toAlgHom)
    (ofAlgEquiv I).injective]

Premises used: AdicCompletion.ofAlgEquiv, AlgHom.cancel_left, AlgEquiv.injective