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 : 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
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))
⊢ 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:
apply ext (I.map (algebraMap _ _)) ⟨i, by simp [← Ideal.map_pow]⟩

Premises used: Algebra.algebraMap, Algebra.FormallyUnramified.ext, Ideal.map, Exists.intro
-- 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
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))
⊢ 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:
dsimp
-- 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
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
neg₂ : Function.Surjective (α := B) (β := B ⧸ I ^ i) (⇑(Ideal.Quotient.mk (I ^ i)) : (a : B) → B ⧸ 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))

Tactic:
rw [Ideal.Quotient.eq, ← map_sub, ← Ideal.mem_comap, Ideal.comap_map_of_surjective',
      sup_eq_left.mpr, ← Ideal.Quotient.eq]

Premises used: Iff.mpr, map_sub, sup_eq_left, Ideal.Quotient.eq, Ideal.comap_map_of_surjective', Ideal.mem_comap
-- 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
⊢ 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:
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 : 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 (α := 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:
exact 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 : 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
⊢ RingHom.ker (F := B →+* B ⧸ I ^ i) (Ideal.Quotient.mk (I ^ i)) ≤ I

Tactic:
simpa using Ideal.pow_le_self hi

Premises used: Ideal.pow_le_self
-- 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
⊢ Function.Surjective (α := B) (β := B ⧸ I ^ i) (⇑(Ideal.Quotient.mk (I ^ i)) : (a : B) → B ⧸ I ^ i)

Tactic:
Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective
-- 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
⊢ Function.Surjective (α := B) (β := B ⧸ I ^ i) (⇑(Ideal.Quotient.mk (I ^ i)) : (a : B) → B ⧸ I ^ i)

Tactic:
exact Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective
-- 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 : ℕ),
    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
-- 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)
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₂)
H₁ : ∀ (x : A), Eq.{w + 1} (α := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B)
⊢ g₁ = 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)
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
H₁ : ∀ (i : ℕ), HSub.hSub (α := B) (β := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B) ∈ I ^ i
⊢ Eq.{w + 1} (α := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B)

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← hI, Ideal.mem_iInf]

Premises used: Ideal.mem_bot, sub_eq_zero, Ideal.mem_iInf
-- 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)
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 : ℕ
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)
⊢ HSub.hSub (α := B) (β := B) ((g₁ : (a : A) → B) x : B) ((g₂ : (a : A) → B) x : B) ∈ I ^ i

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero]

Premises used: map_sub, sub_eq_zero, Ideal.Quotient.eq_zero_iff_mem
-- 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)
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 : ℕ
⊢ 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:
DFunLike.congr_fun (this i) x

Premises used: DFunLike.congr_fun, Set.Mem, Submodule.Quotient.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 : 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 : ℕ
⊢ 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:
exact DFunLike.congr_fun (this i) x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u
inst_1 : CommRing R
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))
⊢ FormallyUnramified R R

Tactic:
rw [iff_comp_injective]

Premises used: Algebra.FormallyUnramified.iff_comp_injective
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u
inst_1 : CommRing R
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))
⊢ ∀ [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:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u
inst_1 : CommRing R
B : Type u
inst_2 : CommRing B
_ :
  ∀ [inst : 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))
⊢ ∀ [inst : 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:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u
inst_1 : CommRing R
B : Type u
inst_2 : CommRing B
inst_3 : 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))
⊢ ∀ (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := R →ₐ[R] B) (β := R →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u
inst_1 : CommRing R
B : Type u
inst_2 : CommRing B
inst_3 : 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))
⊢ HPow.hPow (β := ℕ) I 2 = ⊥ →
    Function.Injective (α := R →ₐ[R] B) (β := R →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u
inst_1 : CommRing R
B : Type u
inst_2 : CommRing B
inst_3 : Algebra R B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : R →ₐ[R] B
_ :
  Eq (α := R →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂) → f₁ = f₂
⊢ Eq (α := R →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂) → f₁ = f₂

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u
inst : CommRing R
B : Type u
inst_1 : CommRing B
inst_2 : Algebra R B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : R →ₐ[R] B
h_1 : Eq (α := R →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
⊢ f₁ = f₂

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u
inst_1 : CommRing R
B : Type u
inst_2 : CommRing B
inst_3 : Algebra R B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : R →ₐ[R] B
h_1 : Eq (α := R →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
⊢ f₁ = f₂

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Unramified.Basic
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
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))
⊢ FormallyUnramified R B

Tactic:
rw [iff_comp_injective]

Premises used: Algebra.FormallyUnramified.iff_comp_injective
-- Module: Mathlib.RingTheory.Unramified.Basic
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),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B →ₐ[R] C) (β := B →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ ∀ [inst_6 : CommRing C] [inst_7 : Algebra R C] (I : Ideal C),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B →ₐ[R] C) (β := B →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
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),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B →ₐ[R] C) (β := B →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ ∀ [inst_7 : Algebra R C] (I : Ideal C),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B →ₐ[R] C) (β := B →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
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₂)
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)
⊢ f₁ = f₂

Tactic:
rw [← f₁.comp_id, ← f₂.comp_id, ← e.comp_symm, ← AlgHom.comp_assoc, ← AlgHom.comp_assoc]

Premises used: AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.comp_id
-- Module: Mathlib.RingTheory.Unramified.Basic
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_φ₁ : f₁.comp (↑e : A →ₐ[R] B) = f₂.comp (↑e : A →ₐ[R] B)
⊢ (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:
congr 1
-- Module: Mathlib.RingTheory.Unramified.Basic
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)

Tactic:
FormallyUnramified.comp_injective I hI ?_

Premises used: Algebra.FormallyUnramified.comp_injective
-- Module: Mathlib.RingTheory.Unramified.Basic
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 (Ideal.Quotient.mkₐ R I) (f₁.comp (↑e : A →ₐ[R] B)))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (↑e : A →ₐ[R] B)))
⊢ f₁.comp (↑e : A →ₐ[R] B) = f₂.comp (↑e : A →ₐ[R] B)

Tactic:
refine FormallyUnramified.comp_injective I hI ?_

Premises used: Algebra.FormallyUnramified.comp_injective