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 : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
h₁ :
  ∀ ⦃S : Type w⦄ [inst_5 : CommRing S] (I : Ideal S),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      ∀ [inst_6 : Algebra R S],
        Function.Injective (α := A →ₐ[R] S) (β := AlgHom.{v, u, w} R A (S ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ ∀ [inst_5 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
have h₂ : ∀ ⦃S : Type w⦄ [inst_5 : CommRing S] (I J : Ideal S),
  I ≤ J →
    (∀ [inst_6 : Algebra R S],
        Function.Injective (α := A →ₐ[R] S) (β := AlgHom.{v, u, w} R A (S ⧸ I))
          (AlgHom.comp (Ideal.Quotient.mkₐ R I))) →
      (∀ [inst_6 : Algebra.{v, w} R (S ⧸ I)],
          Function.Injective (α := AlgHom.{v, u, w} R A (S ⧸ I)) (β :=
            AlgHom.{v, u, w} R A
              (HasQuotient.Quotient (S ⧸ I) (B := Ideal (S ⧸ I))
                (Ideal.map (F := S →+* S ⧸ I) (Ideal.Quotient.mk I) J)))
            (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := S →+* S ⧸ I) (Ideal.Quotient.mk I) J)))) →
        ∀ [inst_6 : Algebra R S],
          Function.Injective (α := A →ₐ[R] S) (β := AlgHom.{v, u, w} R A (S ⧸ J)) (AlgHom.comp (Ideal.Quotient.mkₐ R J))
Tactic: apply Ideal.IsNilpotent.induction_on (S := B) I hI
-- 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_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{v, w} R (B ⧸ I)],
    Function.Injective (α := AlgHom.{v, u, w} R A (B ⧸ I)) (β :=
      AlgHom.{v, u, w} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g₁ g₂ : A →ₐ[R] B
e :
  Eq (α := AlgHom.{v, u, w} R A (B ⧸ J)) (AlgHom.comp (Ideal.Quotient.mkₐ R J) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R J) g₂)
⊢ g₁ = g₂
have h₃ : Eq (α := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁)
  (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂)
Tactic: apply h₁
-- 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_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{v, w} R (B ⧸ I)],
    Function.Injective (α := AlgHom.{v, u, w} R A (B ⧸ I)) (β :=
      AlgHom.{v, u, w} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g₁ g₂ : A →ₐ[R] B
e :
  Eq (α := AlgHom.{v, u, w} R A (B ⧸ J)) (AlgHom.comp (Ideal.Quotient.mkₐ R J) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R J) g₂)
⊢ Eq (α := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂)
have h₃ : Eq (α :=
  AlgHom.{v, u, w} R A
    (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
  (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁))
  (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂))
Tactic: apply h₂
-- 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_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{v, w} R (B ⧸ I)],
    Function.Injective (α := AlgHom.{v, u, w} R A (B ⧸ I)) (β :=
      AlgHom.{v, u, w} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g₁ g₂ : A →ₐ[R] B
e :
  Eq (α := AlgHom.{v, u, w} R A (B ⧸ J)) (AlgHom.comp (Ideal.Quotient.mkₐ R J) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R J) g₂)
⊢ Eq (α :=
    AlgHom.{v, u, w} R A
      (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
    (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
      (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁))
    (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
      (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂))
have h₃ : ∀ (x : A),
  Eq.{w + 1} (α :=
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
              (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁) :
            AlgHom.{v, u, w} R A
              (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I))
                (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))) :
          (a : A) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        x :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
              (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂) :
            AlgHom.{v, u, w} R A
              (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I))
                (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))) :
          (a : A) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        x :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
Tactic: ext x
-- 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_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{v, w} R (B ⧸ I)],
    Function.Injective (α := AlgHom.{v, u, w} R A (B ⧸ I)) (β :=
      AlgHom.{v, u, w} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g₁ g₂ : A →ₐ[R] B
e :
  Eq (α := AlgHom.{v, u, w} R A (B ⧸ J)) (AlgHom.comp (Ideal.Quotient.mkₐ R J) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R J) g₂)
x : A
⊢ Eq.{w + 1} (α :=
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
              (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁) :
            AlgHom.{v, u, w} R A
              (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I))
                (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))) :
          (a : A) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        x :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
              (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂) :
            AlgHom.{v, u, w} R A
              (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I))
                (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))) :
          (a : A) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        x :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
have e₁ : Eq.{w + 1} (α := B ⧸ J)
  (((AlgHom.comp (Ideal.Quotient.mkₐ R J) g₁ : AlgHom.{v, u, w} R A (B ⧸ J)) : (a : A) → B ⧸ J) x : B ⧸ J)
  (((AlgHom.comp (Ideal.Quotient.mkₐ R J) g₂ : AlgHom.{v, u, w} R A (B ⧸ J)) : (a : A) → B ⧸ J) x : B ⧸ J)
Tactic: replace e := AlgHom.congr_fun e x
Cleared hypotheses: e
-- 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_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{v, w} R (B ⧸ I)],
    Function.Injective (α := AlgHom.{v, u, w} R A (B ⧸ I)) (β :=
      AlgHom.{v, u, w} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g₁ g₂ : A →ₐ[R] B
x : A
e :
  Eq.{w + 1} (α := B ⧸ J)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R J) g₁ : AlgHom.{v, u, w} R A (B ⧸ J)) : (a : A) → B ⧸ J) x : B ⧸ J)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R J) g₂ : AlgHom.{v, u, w} R A (B ⧸ J)) : (a : A) → B ⧸ J) x : B ⧸ J)
⊢ Eq.{w + 1} (α :=
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
              (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁) :
            AlgHom.{v, u, w} R A
              (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I))
                (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))) :
          (a : A) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        x :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
              (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂) :
            AlgHom.{v, u, w} R A
              (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I))
                (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))) :
          (a : A) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        x :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
have h₃ : Eq (α := HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
  ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) :
        (a : B ⧸ I) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x)) :
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
  ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) :
        (a : B ⧸ I) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x)) :
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
Tactic: dsimp only [AlgHom.comp_apply, Ideal.Quotient.mkₐ_eq_mk] at e ⊢
-- 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_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{v, w} R (B ⧸ I)],
    Function.Injective (α := AlgHom.{v, u, w} R A (B ⧸ I)) (β :=
      AlgHom.{v, u, w} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g₁ g₂ : A →ₐ[R] B
x : A
e :
  Eq (α := B ⧸ J) ((Ideal.Quotient.mk J : (a : B) → B ⧸ J) ((g₁ : (a : A) → B) x) : B ⧸ J)
    ((Ideal.Quotient.mk J : (a : B) → B ⧸ J) ((g₂ : (a : A) → B) x) : B ⧸ J)
⊢ Eq (α := HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) :
          (a : B ⧸ I) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) :
          (a : B ⧸ I) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
have h₃ : Membership.mem (γ := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)
  (HSub.hSub (α := B ⧸ I) (β := 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: rwa [Ideal.Quotient.eq, ← map_sub, Ideal.mem_quotient_iff_mem hIJ, ← 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_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{v, w} R (B ⧸ I)],
    Function.Injective (α := AlgHom.{v, u, w} R A (B ⧸ I)) (β :=
      AlgHom.{v, u, w} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g₁ g₂ : A →ₐ[R] B
x : A
e :
  Eq (α := B ⧸ J) ((Ideal.Quotient.mk J : (a : B) → B ⧸ J) ((g₁ : (a : A) → B) x) : B ⧸ J)
    ((Ideal.Quotient.mk J : (a : B) → B ⧸ J) ((g₂ : (a : A) → B) x) : B ⧸ J)
h₃ :
  Membership.mem (γ := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)
    (HSub.hSub (α := B ⧸ I) (β := 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) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) :
          (a : B ⧸ I) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) :
          (a : B ⧸ I) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
have h₄ : Membership.mem (α := B ⧸ I) (γ := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)
  ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
      (HSub.hSub (α := B) (β := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B)) :
    B ⧸ I)
Tactic: rwa [Ideal.Quotient.eq, ← map_sub, Ideal.mem_quotient_iff_mem hIJ, ← 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_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{v, w} R (B ⧸ I)],
    Function.Injective (α := AlgHom.{v, u, w} R A (B ⧸ I)) (β :=
      AlgHom.{v, u, w} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g₁ g₂ : A →ₐ[R] B
x : A
e :
  Eq (α := B ⧸ J) ((Ideal.Quotient.mk J : (a : B) → B ⧸ J) ((g₁ : (a : A) → B) x) : B ⧸ J)
    ((Ideal.Quotient.mk J : (a : B) → B ⧸ J) ((g₂ : (a : A) → B) x) : B ⧸ J)
h₃ :
  Membership.mem (γ := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)
    (HSub.hSub (α := B ⧸ I) (β := 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))
h₄ :
  Membership.mem (α := B ⧸ I) (γ := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        (HSub.hSub (α := B) (β := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B)) :
      B ⧸ I)
⊢ Eq (α := HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) :
          (a : B ⧸ I) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₁ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
    ((Ideal.Quotient.mk (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) :
          (a : B ⧸ I) → (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((g₂ : (a : A) → B) x)) :
      HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
have h₅ : HSub.hSub (α := B) (β := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B) ∈ J
Tactic: rwa [Ideal.Quotient.eq, ← map_sub, Ideal.mem_quotient_iff_mem hIJ, ← 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
inst_5 : FormallyUnramified R A
C : Type u_1
inst_6 : Ring C
f : B →+* C
hf : IsNilpotent (R := Ideal B) (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : Eq (α := A →+* C) (f.comp (↑g₁ : A →+* B)) (f.comp (↑g₂ : A →+* B))
⊢ Eq (α := AlgHom.{v, u, w} R A (HasQuotient.Quotient B (B := Ideal B) (RingHom.ker f)))
    (AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₁) (AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₂)
have H : ∀ (x : A),
  Eq.{w + 1} (α := HasQuotient.Quotient B (B := Ideal B) (RingHom.ker f))
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₁ :
            AlgHom.{v, u, w} R A (HasQuotient.Quotient B (B := Ideal B) (RingHom.ker f))) :
          (a : A) → B ⧸ RingHom.ker f)
        x :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker f))
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₂ :
            AlgHom.{v, u, w} R A (HasQuotient.Quotient B (B := Ideal B) (RingHom.ker f))) :
          (a : A) → B ⧸ RingHom.ker f)
        x :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker f))
Tactic: ext x
-- 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
inst_5 : FormallyUnramified R A
C : Type u_1
inst_6 : Ring C
f : B →+* C
hf : IsNilpotent (R := Ideal B) (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : Eq (α := A →+* C) (f.comp (↑g₁ : A →+* B)) (f.comp (↑g₂ : A →+* B))
x : A
⊢ Eq.{w + 1} (α := HasQuotient.Quotient B (B := Ideal B) (RingHom.ker f))
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₁ :
            AlgHom.{v, u, w} R A (HasQuotient.Quotient B (B := Ideal B) (RingHom.ker f))) :
          (a : A) → B ⧸ RingHom.ker f)
        x :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker f))
    (((AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₂ :
            AlgHom.{v, u, w} R A (HasQuotient.Quotient B (B := Ideal B) (RingHom.ker f))) :
          (a : A) → B ⧸ RingHom.ker f)
        x :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker f))
have this : Eq.{u_1 + 1} (α := C) ((f.comp (↑g₁ : A →+* B) : (a : A) → C) x : C) ((f.comp (↑g₂ : A →+* B) : (a : A) → C) x : C)
Tactic: have := RingHom.congr_fun h 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 : ℕ
⊢ 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 : ∀ (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₂)
Tactic: by_cases hi : i = 0
-- 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 : ℕ
pos :
  ∀ (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₂)
⊢ 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 : ∀ (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₂)
Tactic: by_cases hi : i = 0