awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
i : ℕ
hi : i = 0
⊢ Eq (α := AlgHom.{v, u, w} R A (B ⧸ I ^ i)) (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₂)
have pos : ∀ (x : A),
  Eq.{w + 1} (α := B ⧸ I ^ i)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₁ : AlgHom.{v, u, w} R A (B ⧸ I ^ i)) : (a : A) → B ⧸ I ^ i) x :
      B ⧸ I ^ i)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₂ : AlgHom.{v, u, w} R A (B ⧸ I ^ i)) : (a : A) → B ⧸ I ^ i) x :
      B ⧸ I ^ i)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
i : ℕ
hi : i = 0
x : A
⊢ Subsingleton.{w + 1} (B ⧸ I ^ i)
have rw : Subsingleton.{w + 1} (HasQuotient.Quotient B (B := Ideal B) ⊤)
Tactic: rw [hi, pow_zero, Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (hypothesis)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
i : ℕ
hi : i = 0
x : A
⊢ Eq.{w + 1} (α := B ⧸ I ^ i)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₁ : AlgHom.{v, u, w} R A (B ⧸ I ^ i)) : (a : A) → B ⧸ I ^ i) x :
      B ⧸ I ^ i)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₂ : AlgHom.{v, u, w} R A (B ⧸ I ^ i)) : (a : A) → B ⧸ I ^ i) x :
      B ⧸ I ^ i)
have this : Subsingleton.{w + 1} (B ⧸ I ^ i)
Tactic: have : Subsingleton (B ⧸ I ^ i) := by
        rw [hi, pow_zero, Ideal.one_eq_top]
        infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
i : ℕ
hi : ¬i = 0
⊢ Eq (α := AlgHom.{v, u, w} R A (B ⧸ I ^ i)) (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₂)
have neg : ∀ (x : A),
  Eq (α :=
    HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
      (Ideal.map (F := B →+* B ⧸ I ^ i) (algebraMap B (B ⧸ I ^ i)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (algebraMap B (B ⧸ I ^ i)) I) :
          (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (algebraMap B (B ⧸ I ^ i)) I)
        (((AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₁ : AlgHom.{v, u, w} R A (B ⧸ I ^ i)) : (a : A) → B ⧸ I ^ i) x) :
      HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
        (Ideal.map (F := B →+* B ⧸ I ^ i) (algebraMap B (B ⧸ I ^ i)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (algebraMap B (B ⧸ I ^ i)) I) :
          (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (algebraMap B (B ⧸ I ^ i)) I)
        (((AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₂ : AlgHom.{v, u, w} R A (B ⧸ I ^ i)) : (a : A) → B ⧸ I ^ i) x) :
      HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
        (Ideal.map (F := B →+* B ⧸ I ^ i) (algebraMap B (B ⧸ I ^ i)) I))
Tactic: apply ext (I.map (algebraMap _ _)) ⟨i, by simp [← Ideal.map_pow]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
i : ℕ
hi : ¬i = 0
x : A
⊢ Eq (α :=
    HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
      (Ideal.map (F := B →+* B ⧸ I ^ i) (algebraMap B (B ⧸ I ^ i)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (algebraMap B (B ⧸ I ^ i)) I) :
          (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (algebraMap B (B ⧸ I ^ i)) I)
        (((AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₁ : AlgHom.{v, u, w} R A (B ⧸ I ^ i)) : (a : A) → B ⧸ I ^ i) x) :
      HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
        (Ideal.map (F := B →+* B ⧸ I ^ i) (algebraMap B (B ⧸ I ^ i)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (algebraMap B (B ⧸ I ^ i)) I) :
          (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (algebraMap B (B ⧸ I ^ i)) I)
        (((AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₂ : AlgHom.{v, u, w} R A (B ⧸ I ^ i)) : (a : A) → B ⧸ I ^ i) x) :
      HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
        (Ideal.map (F := B →+* B ⧸ I ^ i) (algebraMap B (B ⧸ I ^ i)) I))
have neg : Eq (α :=
  HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
    (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
  ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I) :
        (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (Ideal.Quotient.mk (I ^ i)) I)
      ((Ideal.Quotient.mk (I ^ i) : (a : B) → B ⧸ I ^ i) ((g₁ : (a : A) → B) x)) :
    HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
      (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
  ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I) :
        (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (Ideal.Quotient.mk (I ^ i)) I)
      ((Ideal.Quotient.mk (I ^ i) : (a : B) → B ⧸ I ^ i) ((g₂ : (a : A) → B) x)) :
    HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
      (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
i : ℕ
hi : ¬i = 0
x : A
⊢ Eq (α :=
    HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
      (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I) :
          (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (Ideal.Quotient.mk (I ^ i)) I)
        ((Ideal.Quotient.mk (I ^ i) : (a : B) → B ⧸ I ^ i) ((g₁ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
        (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I) :
          (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (Ideal.Quotient.mk (I ^ i)) I)
        ((Ideal.Quotient.mk (I ^ i) : (a : B) → B ⧸ I ^ i) ((g₂ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
        (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
have neg : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
  ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
Tactic: rw [Ideal.Quotient.eq, ← map_sub, ← Ideal.mem_comap, Ideal.comap_map_of_surjective',
      sup_eq_left.mpr, ← Ideal.Quotient.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
i : ℕ
hi : ¬i = 0
x : A
neg :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
⊢ Eq (α :=
    HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
      (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I) :
          (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (Ideal.Quotient.mk (I ^ i)) I)
        ((Ideal.Quotient.mk (I ^ i) : (a : B) → B ⧸ I ^ i) ((g₁ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
        (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I) :
          (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (Ideal.Quotient.mk (I ^ i)) I)
        ((Ideal.Quotient.mk (I ^ i) : (a : B) → B ⧸ I ^ i) ((g₂ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
        (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
have neg₁ : RingHom.ker (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) ≤ I
Tactic: rw [Ideal.Quotient.eq, ← map_sub, ← Ideal.mem_comap, Ideal.comap_map_of_surjective',
      sup_eq_left.mpr, ← Ideal.Quotient.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
i : ℕ
hi : ¬i = 0
x : A
neg :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
neg₁ : RingHom.ker (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) ≤ I
⊢ Eq (α :=
    HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
      (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I) :
          (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (Ideal.Quotient.mk (I ^ i)) I)
        ((Ideal.Quotient.mk (I ^ i) : (a : B) → B ⧸ I ^ i) ((g₁ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
        (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I) :
          (a : B ⧸ I ^ i) → (B ⧸ I ^ i) ⧸ Ideal.map (Ideal.Quotient.mk (I ^ i)) I)
        ((Ideal.Quotient.mk (I ^ i) : (a : B) → B ⧸ I ^ i) ((g₂ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I ^ i) (B := Ideal (B ⧸ I ^ i))
        (Ideal.map (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) I))
have neg₂ : Function.Surjective (α := B) (β := B ⧸ I ^ i) (⇑(Ideal.Quotient.mk (I ^ i)) : (a : B) → B ⧸ I ^ i)
Tactic: rw [Ideal.Quotient.eq, ← map_sub, ← Ideal.mem_comap, Ideal.comap_map_of_surjective',
      sup_eq_left.mpr, ← Ideal.Quotient.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (hypothesis)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
⊢ g₁ = g₂
have this : ∀ (i : ℕ),
  Eq (α := AlgHom.{v, u, w} R A (B ⧸ I ^ i)) (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₂)
Tactic: have (i : ℕ) :
      (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂ := by
    by_cases hi : i = 0
    · ext x
      have : Subsingleton (B ⧸ I ^ i) := by
        rw [hi, pow_zero, Ideal.one_eq_top]
        infer_instance
      exact Subsingleton.elim _ _
    apply ext (I.map (algebraMap _ _)) ⟨i, by simp [← Ideal.map_pow]⟩
    intro x
    dsimp
    rw [Ideal.Quotient.eq, ← map_sub, ← Ideal.mem_comap, Ideal.comap_map_of_surjective',
      sup_eq_left.mpr, ← Ideal.Quotient.eq]
    · exact H _
    · simpa using Ideal.pow_le_self hi
    · exact Ideal.Quotient.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
this :
  ∀ (i : ℕ),
    Eq (α := AlgHom.{v, u, w} R A (B ⧸ I ^ i)) (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₁)
      (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₂)
⊢ g₁ = g₂
have H₁ : ∀ (x : A), Eq.{w + 1} (α := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
this :
  ∀ (i : ℕ),
    Eq (α := AlgHom.{v, u, w} R A (B ⧸ I ^ i)) (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₁)
      (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₂)
x : A
⊢ Eq.{w + 1} (α := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B)
have H₁ : ∀ (i : ℕ), HSub.hSub (α := B) (β := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B) ∈ I ^ i
Tactic: rw [← sub_eq_zero, ← Ideal.mem_bot, ← hI, Ideal.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : Eq.{w + 1} (α := Ideal B) (⨅ (i : ℕ), I ^ i) ⊥
g₁ g₂ : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x) : B ⧸ I)
this :
  ∀ (i : ℕ),
    Eq (α := AlgHom.{v, u, w} R A (B ⧸ I ^ i)) (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₁)
      (AlgHom.comp (Ideal.Quotient.mkₐ R (I ^ i)) g₂)
x : A
i : ℕ
⊢ HSub.hSub (α := B) (β := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B) ∈ I ^ i
have H₁ : Eq (α := B ⧸ I ^ i) ((Ideal.Quotient.mk (I ^ i) : (a : B) → B ⧸ I ^ i) ((g₁ : (a : A) → B) x) : B ⧸ I ^ i)
  ((Ideal.Quotient.mk (I ^ i) : (a : B) → B ⧸ I ^ i) ((g₂ : (a : A) → B) x) : B ⧸ I ^ i)
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
⊢ FormallyUnramified R R
have rw : ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_2 : Algebra R B] (I : Ideal B),
  HPow.hPow (β := ℕ) I 2 = ⊥ →
    Function.Injective (α := R →ₐ[R] B) (β := R →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Tactic: rw [iff_comp_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
e : A ≃ₐ[R] B
⊢ FormallyUnramified R B
have rw : ∀ ⦃B_1 : Type u_3⦄ [inst_6 : CommRing B_1] [inst_7 : Algebra R B_1] (I : Ideal B_1),
  HPow.hPow (β := ℕ) I 2 = ⊥ →
    Function.Injective (α := B →ₐ[R] B_1) (β := B →ₐ[R] B_1 ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Tactic: rw [iff_comp_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst_6 : CommRing C
inst_7 : Algebra R C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : Eq (α := B →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
⊢ f₁ = f₂
have rw : (f₁.comp (↑e : A →ₐ[R] B)).comp (↑e.symm : B →ₐ[R] A) = (f₂.comp (↑e : A →ₐ[R] B)).comp (↑e.symm : B →ₐ[R] A)
Tactic: rw [← f₁.comp_id, ← f₂.comp_id, ← e.comp_symm, ← AlgHom.comp_assoc, ← AlgHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst_6 : CommRing C
inst_7 : Algebra R C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : Eq (α := B →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
⊢ (f₁.comp (↑e : A →ₐ[R] B)).comp (↑e.symm : B →ₐ[R] A) = (f₂.comp (↑e : A →ₐ[R] B)).comp (↑e.symm : B →ₐ[R] A)
have e_φ₁ : f₁.comp (↑e : A →ₐ[R] B) = f₂.comp (↑e : A →ₐ[R] B)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst_6 : CommRing C
inst_7 : Algebra R C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : Eq (α := B →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
⊢ f₁.comp (↑e : A →ₐ[R] B) = f₂.comp (↑e : A →ₐ[R] B)
have e_φ₁ : Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₁.comp (↑e : A →ₐ[R] B)))
  (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
Tactic: refine FormallyUnramified.comp_injective I hI ?_
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst_6 : CommRing C
inst_7 : Algebra R C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : Eq (α := B →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
⊢ Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₁.comp (↑e : A →ₐ[R] B)))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
have e_φ₁ : Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I)) (AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (↑e : A →ₐ[R] B))
  (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
Tactic: rw [← AlgHom.comp_assoc, e', AlgHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst_6 : CommRing C
inst_7 : Algebra R C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : Eq (α := B →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
e_φ₁ :
  Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I)) (AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (↑e : A →ₐ[R] B))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
⊢ Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₁.comp (↑e : A →ₐ[R] B)))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
have e_φ₂ : Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I)) (AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂) (↑e : A →ₐ[R] B))
  (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
Tactic: rw [← AlgHom.comp_assoc, e', AlgHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst_6 : CommRing C
inst_7 : Algebra R C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : Eq (α := B →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
e_φ₁ :
  Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I)) (AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (↑e : A →ₐ[R] B))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
e_φ₂ :
  Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I)) (AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂) (↑e : A →ₐ[R] B))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
⊢ Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₁.comp (↑e : A →ₐ[R] B)))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
have e_φ₃ : Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
  (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
Tactic: rw [← AlgHom.comp_assoc, e', AlgHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallyUnramified A B
⊢ FormallyUnramified R B
have rw : ∀ ⦃B_1 : Type u_3⦄ [inst_9 : CommRing B_1] [inst_10 : Algebra R B_1] (I : Ideal B_1),
  HPow.hPow (β := ℕ) I 2 = ⊥ →
    Function.Injective (α := B →ₐ[R] B_1) (β := B →ₐ[R] B_1 ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Tactic: rw [iff_comp_injective]