awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsPrecomplete I M
inst_6 : IsHausdorff I N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
⊢ ∃ (a : M), (f : (a : M) → N) a = y
have obtain : ∀ (x' : AdicCompletion I M)
  (hx' :
    Eq.{u_3 + 1} (α := AdicCompletion I N)
      ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N) x' : AdicCompletion I N)
      ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)),
  ∃ (a : M), (f : (a : M) → N) a = y
Tactic: obtain ⟨x', hx'⟩ := AdicCompletion.map_surjective_of_mkQ_comp_surjective h (of I N y)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsPrecomplete I M
inst_6 : IsHausdorff I N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
x' : AdicCompletion I M
hx' :
  Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N) x' : AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
⊢ ∃ (a : M), (f : (a : M) → N) a = y
have obtain : ∀ (x : M) (hx : (of I M : (a : M) → AdicCompletion I M) x = x'), ∃ (a : M), (f : (a : M) → N) a = y
Tactic: obtain ⟨x, hx⟩ := of_surjective I M x'
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsPrecomplete I M
inst_6 : IsHausdorff I N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
x' : AdicCompletion I M
hx' :
  Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N) x' : AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
x : M
hx : (of I M : (a : M) → AdicCompletion I M) x = x'
⊢ ∃ (a : M), (f : (a : M) → N) a = y
have h₁ : (f : (a : M) → N) x = y
Tactic: use x
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsPrecomplete I M
inst_6 : IsHausdorff I N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
x' : AdicCompletion I M
hx' :
  Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N) x' : AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
x : M
hx : (of I M : (a : M) → AdicCompletion I M) x = x'
⊢ (f : (a : M) → N) x = y
have h₁ : Eq (α := AdicCompletion I N) ((of I N : (a : N) → AdicCompletion I N) ((f : (a : M) → N) x) : AdicCompletion I N)
  ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
Tactic: rwa [← of_inj (I := I), ← map_of, hx]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsPrecomplete I M
inst_6 : IsHausdorff I N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : N
x' : AdicCompletion I M
hx' :
  Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N) x' : AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
x : M
hx : (of I M : (a : M) → AdicCompletion I M) x = x'
h₁ :
  Eq (α := AdicCompletion I N) ((of I N : (a : N) → AdicCompletion I N) ((f : (a : M) → N) x) : AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
⊢ (f : (a : M) → N) x = y
have h₂ : Eq.{u_3 + 1} (α := AdicCompletion I N)
  ((AdicCompletion.map I f : (a : AdicCompletion I M) → AdicCompletion I N)
      ((of I M : (a : M) → AdicCompletion I M) x) :
    AdicCompletion I N)
  ((of I N : (a : N) → AdicCompletion I N) y : AdicCompletion I N)
Tactic: rwa [← of_inj (I := I), ← map_of, hx]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (hypothesis)
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
h :
  Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β := HasQuotient.Quotient S (B := Ideal S) (Ideal.map f I))
    (⇑(RingHom.comp (Ideal.Quotient.mk (Ideal.map f I)) f) : (a : R) → S ⧸ Ideal.map f I)
x : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := AlgHom.toLinearMap (Algebra.ofId R S)
⊢ Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have 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))
Tactic: change Function.Surjective ((restrictScalars R (I.map f)).mkQ ∘ₗ fₗ) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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)
have simp : Eq.{u_6 + 1} (α := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I) (Ideal.map f I)
Tactic: simp only [Ideal.smul_top_eq_map, restrictScalars_inj]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (hypothesis)
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))
⊢ Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (hypothesis)
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)
⊢ Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have x : IsHausdorff I S
Tactic: have _ := IsHausdorff.map_algebraMap_iff.mp haus
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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
⊢ Function.Surjective.{u_1 + 1, u_6 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have 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 • ⊤)
Tactic: apply surjective_of_mkQ_comp_surjective (I := I) (f := fₗ)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (goal)
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
⊢ 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 • ⊤)
have 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))
Tactic: rwa [Ideal.smul_top_eq_map]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Noetherian (goal)
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)
⊢ ∃ (L : A),
    ∀ (n : ℕ),
      SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) n) ⊤) (f n) L
have 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
Tactic: obtain ⟨n, hn⟩ := (isArtinianRing_iff_isNilpotent_maximalIdeal A).mp ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Noetherian (goal)
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
⊢ ∃ (L : A),
    ∀ (n : ℕ),
      SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) n) ⊤) (f n) L
have h : ∀ (n_1 : ℕ),
  SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) n_1) ⊤) (f n_1) (f n)
Tactic: use f n
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Noetherian (goal)
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 : ℕ
⊢ SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
have pos : ∀ (h : m ≤ 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
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Noetherian (goal)
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)
⊢ SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
have neg : ∀ (h : ¬m ≤ 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
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Noetherian (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 : 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)
have hf₁ : 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)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Noetherian (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 : 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)
⊢ SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
have hf₁ : f n = f m
Tactic: rw [hn, zero_smul, Ideal.zero_eq_bot, SModEq.bot] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Noetherian (goal)
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
⊢ SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f n)
have neg : SModEq (R := A) (HSMul.hSMul (β := Submodule A A) (HPow.hPow (α := Ideal A) (maximalIdeal A) m) ⊤) (f m) (f m)
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.RingHom (goal)
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
⊢ RingHom.comp (↑(ofAlgEquiv I) : S →+* AdicCompletion I S) (liftRingHom I f ⋯) = AdicCompletion.liftRingHom I f ⋯
have 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 sorry) :
                RingHom.{u_1, u_2} R (AdicCompletion I S)) :
              (a : R) → AdicCompletion I S)
            x) :
        (n : ℕ) → S ⧸ I ^ n • ⊤)
      n)
    ((↑((AdicCompletion.liftRingHom I f sorry : (a : R) → AdicCompletion I S) x) : (n : ℕ) → S ⧸ I ^ n • ⊤) n)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.RingHom (goal)
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)
    ((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)
have 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 sorry : (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 only [liftRingHom, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.RingHom (goal)
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)
    ((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)
have 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 sorry : (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]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.RingHom (goal)
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 : ℕ
⊢ RingHom.comp (Ideal.Quotient.mk (I ^ n)) (liftRingHom I f ⋯) = f n
have a : ∀ (x : R),
  Eq.{u_2 + 1} (α := S ⧸ I ^ n)
    (((RingHom.comp (Ideal.Quotient.mk (I ^ n)) (liftRingHom I f sorry) : 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: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.RingHom (goal)
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
⊢ F = liftRingHom I f ⋯
have 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 sorry))
Tactic: apply DFunLike.coe_injective
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.RingHom (goal)
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
⊢ 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 ⋯))
have 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 sorry) r))
Tactic: apply IsHausdorff.funext' I
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.RingHom (goal)
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)
⊢ f = g
have 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)
Tactic: rw [← AlgHom.cancel_left (f := ((ofAlgEquiv I).restrictScalars R).toAlgHom)
    (ofAlgEquiv I).injective]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.RingHom (goal)
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)
⊢ 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)
have H₁ : ∀ (x : A),
  Eq.{u_4 + 1} (α := AdicCompletion I S)
    (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) f :
            AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
          (a : A) → AdicCompletion I S)
        x :
      AdicCompletion I S)
    (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) g :
            AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
          (a : A) → AdicCompletion I S)
        x :
      AdicCompletion I S)
Tactic: ext1 x