awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.Basic
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₂)
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₂)
⊢ g₁ = g₂

Tactic:
apply h₁
-- Module: Mathlib.RingTheory.Unramified.Basic
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₂)
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₂))
⊢ 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₂
-- Module: Mathlib.RingTheory.Unramified.Basic
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₂)
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))
⊢ 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:
ext x
-- Module: Mathlib.RingTheory.Unramified.Basic
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} (α := 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
-- Module: Mathlib.RingTheory.Unramified.Basic
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)
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))
⊢ 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:
dsimp only [AlgHom.comp_apply, Ideal.Quotient.mkₐ_eq_mk] at e ⊢

Premises used: AlgHom.comp_apply, Ideal.Quotient.mkₐ_eq_mk
-- Module: Mathlib.RingTheory.Unramified.Basic
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)
h₅ : HSub.hSub (α := B) (β := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B) ∈ J
h₆ h₇ h₈ h₉ :
  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))

Tactic:
rwa [Ideal.Quotient.eq, ← map_sub, Ideal.mem_quotient_iff_mem hIJ, ← Ideal.Quotient.eq]

Premises used: map_sub, Ideal.mem_quotient_iff_mem, Ideal.Quotient.eq
-- Module: Mathlib.RingTheory.Unramified.Basic
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 : IsNilpotent 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₂

Tactic:
FormallyUnramified.lift_unique I hI g₁ g₂ (AlgHom.ext H)

Premises used: AlgHom.ext, Algebra.FormallyUnramified.lift_unique
-- Module: Mathlib.RingTheory.Unramified.Basic
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))
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))
⊢ 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₂)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Unramified.Basic
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.{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
-- Module: Mathlib.RingTheory.Unramified.Basic
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
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)
⊢ 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:
simpa only [Ideal.Quotient.eq, Function.comp_apply, AlgHom.coe_comp, Ideal.Quotient.mkₐ_eq_mk,
        RingHom.mem_ker, map_sub, sub_eq_zero]

Premises used: map_sub, sub_eq_zero, RingHom.mem_ker, Ideal.Quotient.eq, AlgHom.coe_comp, Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply
-- Module: Mathlib.RingTheory.Unramified.Basic
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 :
  ∀ (x : A),
    Eq.{u_1 + 1} (α := C) ((f : (a : B) → C) ((g₁ : (a : A) → B) x : B) : C)
      ((f : (a : B) → C) ((g₂ : (a : A) → B) x : B) : C)
⊢ g₁ = g₂

Tactic:
FormallyUnramified.lift_unique_of_ringHom f hf g₁ g₂ (RingHom.ext h)

Premises used: RingHom.ext, Algebra.FormallyUnramified.lift_unique_of_ringHom
-- Module: Mathlib.RingTheory.Unramified.Basic
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
inst_7 : Algebra R C
f : B →ₐ[R] C
hf : IsNilpotent (R := Ideal B) (RingHom.ker (F := B →+* C) (↑f : B →+* C))
g₁ g₂ : A →ₐ[R] B
h : f.comp g₁ = f.comp g₂
⊢ g₁ = g₂

Tactic:
FormallyUnramified.ext' _ hf g₁ g₂ (AlgHom.congr_fun h)

Premises used: Algebra.FormallyUnramified.ext', AlgHom.congr_fun
-- Module: Mathlib.RingTheory.Unramified.Basic
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₂)
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₂)
⊢ 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
-- Module: Mathlib.RingTheory.Unramified.Basic
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
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)
⊢ 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:
ext x
-- Module: Mathlib.RingTheory.Unramified.Basic
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
rw : Subsingleton.{w + 1} (HasQuotient.Quotient B (B := Ideal B) ⊤)
⊢ Subsingleton.{w + 1} (B ⧸ I ^ i)

Tactic:
rw [hi, pow_zero, Ideal.one_eq_top]

Premises used: Ideal.one_eq_top, pow_zero
-- Module: Mathlib.RingTheory.Unramified.Basic
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} (HasQuotient.Quotient B (B := Ideal B) ⊤)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Unramified.Basic
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)

Tactic:
have : Subsingleton (B ⧸ I ^ i) := by
        rw [hi, pow_zero, Ideal.one_eq_top]
        infer_instance
-- Module: Mathlib.RingTheory.Unramified.Basic
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
this : Subsingleton.{w + 1} (B ⧸ I ^ i)
⊢ 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:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Unramified.Basic
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
this : Subsingleton.{w + 1} (B ⧸ I ^ i)
⊢ 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:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Unramified.Basic
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
⊢ HPow.hPow (α := Ideal (B ⧸ I ^ i)) (Ideal.map (F := B →+* B ⧸ I ^ i) (algebraMap B (B ⧸ I ^ i)) I) i = 0

Tactic:
simp [← Ideal.map_pow]

Premises used: Ideal.map_pow