awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (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)))
e_φ₃ 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)))
⊢ 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]

Premises used: AlgHom.comp_assoc
-- Module: Mathlib.RingTheory.Unramified.Basic
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
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))
⊢ 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
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
C : Type u_3
_ :
  ∀ [inst_9 : CommRing C] [inst_10 : 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_9 : CommRing C] [inst_10 : 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
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
C : Type u_3
inst_9 : CommRing C
_ :
  ∀ [inst_10 : 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_10 : 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
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
C : Type u_3
inst_9 : CommRing C
inst_10 : 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 :
  Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I))
    (AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (IsScalarTower.toAlgHom R A B))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (IsScalarTower.toAlgHom R A B)))
rw₁ :
  Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I))
    (AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂) (IsScalarTower.toAlgHom R A B))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (IsScalarTower.toAlgHom R A B)))
rw₂ rw₃ :
  Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (IsScalarTower.toAlgHom R A B)))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (IsScalarTower.toAlgHom R A B)))
⊢ Eq (α := AlgHom.{u_1, u_2, u_3} R A (C ⧸ I))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₁.comp (IsScalarTower.toAlgHom R A B)))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp (IsScalarTower.toAlgHom R A B)))

Tactic:
rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc]

Premises used: AlgHom.comp_assoc
-- Module: Mathlib.RingTheory.Unramified.Basic
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
C : Type u_3
inst_9 : CommRing C
inst_10 : 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 (α := A →ₐ[R] C) (f₁.comp (IsScalarTower.toAlgHom R A B)) (f₂.comp (IsScalarTower.toAlgHom R A B))

Tactic:
have e' :=
    FormallyUnramified.lift_unique I ⟨2, hI⟩ (f₁.comp <| IsScalarTower.toAlgHom R A B)
      (f₂.comp <| IsScalarTower.toAlgHom R A B) (by rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc])
-- Module: Mathlib.RingTheory.Unramified.Basic
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
C : Type u_3
inst_9 : CommRing C
inst_10 : 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 (α := A →ₐ[R] C) (f₁.comp (IsScalarTower.toAlgHom R A B)) (f₂.comp (IsScalarTower.toAlgHom R A B))
this : Algebra A C := RingHom.toAlgebra (AlgHom.toRingHom (AlgHom.restrictDomain A f₁))
F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }
F₂ : B →ₐ[A] C := { toRingHom := f₂.toRingHom, commutes' := ⋯ }
H : ∀ (x : B), Eq (α := C) ((f₁ : (a : B) → C) x : C) ((f₂ : (a : B) → C) x : C)
⊢ f₁ = f₂

Tactic:
ext1 x
-- Module: Mathlib.RingTheory.Unramified.Basic
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
C : Type u_3
inst_9 : CommRing C
inst_10 : 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 (α := A →ₐ[R] C) (f₁.comp (IsScalarTower.toAlgHom R A B)) (f₂.comp (IsScalarTower.toAlgHom R A B))
this : Algebra A C := RingHom.toAlgebra (AlgHom.toRingHom (AlgHom.restrictDomain A f₁))
F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }
F₂ : B →ₐ[A] C := { toRingHom := f₂.toRingHom, commutes' := ⋯ }
x : B
H : Eq (α := C) ((F₁ : (a : B) → C) x : C) ((F₂ : (a : B) → C) x : C)
⊢ Eq (α := C) ((f₁ : (a : B) → C) x : C) ((f₂ : (a : B) → C) x : C)

Tactic:
change F₁ x = F₂ x

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.Unramified.Basic
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
C : Type u_3
inst_9 : CommRing C
inst_10 : 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 (α := A →ₐ[R] C) (f₁.comp (IsScalarTower.toAlgHom R A B)) (f₂.comp (IsScalarTower.toAlgHom R A B))
this : Algebra A C := RingHom.toAlgebra (AlgHom.toRingHom (AlgHom.restrictDomain A f₁))
F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }
F₂ : B →ₐ[A] C := { toRingHom := f₂.toRingHom, commutes' := ⋯ }
x : B
H : F₁ = F₂
⊢ Eq (α := C) ((F₁ : (a : B) → C) x : C) ((F₂ : (a : B) → C) x : C)

Tactic:
congr
-- Module: Mathlib.RingTheory.Unramified.Basic
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
C : Type u_3
inst_9 : CommRing C
inst_10 : 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 (α := A →ₐ[R] C) (f₁.comp (IsScalarTower.toAlgHom R A B)) (f₂.comp (IsScalarTower.toAlgHom R A B))
this : Algebra A C := RingHom.toAlgebra (AlgHom.toRingHom (AlgHom.restrictDomain A f₁))
F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }
F₂ : B →ₐ[A] C := { toRingHom := f₂.toRingHom, commutes' := ⋯ }
x : B
⊢ F₁ = F₂

Tactic:
FormallyUnramified.ext I ⟨2, hI⟩ (AlgHom.congr_fun e)

Premises used: Algebra.FormallyUnramified.ext, Exists.intro, AlgHom.congr_fun, OfNat.ofNat
-- Module: Mathlib.RingTheory.Unramified.Basic
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
C : Type u_3
inst_9 : CommRing C
inst_10 : 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 (α := A →ₐ[R] C) (f₁.comp (IsScalarTower.toAlgHom R A B)) (f₂.comp (IsScalarTower.toAlgHom R A B))
this : Algebra A C := RingHom.toAlgebra (AlgHom.toRingHom (AlgHom.restrictDomain A f₁))
F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }
F₂ : B →ₐ[A] C := { toRingHom := f₂.toRingHom, commutes' := ⋯ }
x : B
⊢ F₁ = F₂

Tactic:
exact FormallyUnramified.ext I ⟨2, hI⟩ (AlgHom.congr_fun e)
-- Module: Mathlib.RingTheory.Unramified.Basic
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 B
rw :
  ∀ ⦃B_1 : Type u_3⦄ [inst : CommRing B_1] [inst_8 : Algebra A B_1] (I : Ideal B_1),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B →ₐ[A] B_1) (β := B →ₐ[A] B_1 ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ A I))
⊢ FormallyUnramified A 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
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 B
Q : Type u_3
_ :
  ∀ [inst : CommRing Q] [inst_8 : Algebra A Q] (I : Ideal Q),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B →ₐ[A] Q) (β := B →ₐ[A] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ A I))
⊢ ∀ [inst : CommRing Q] [inst_8 : Algebra A Q] (I : Ideal Q),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B →ₐ[A] Q) (β := B →ₐ[A] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ A I))

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

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
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 B
Q : Type u_3
inst_8 : CommRing Q
inst_9 : Algebra A Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : Eq (α := B →ₐ[A] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂)
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A Q) (algebraMap R A))
this : IsScalarTower R A Q := ⋯
⊢ f₁ = f₂

Tactic:
AlgHom.restrictScalars_injective R ?_

Premises used: AlgHom.restrictScalars_injective
-- Module: Mathlib.RingTheory.Unramified.Basic
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 B
Q : Type u_3
inst_8 : CommRing Q
inst_9 : Algebra A Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : Eq (α := B →ₐ[A] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂)
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A Q) (algebraMap R A))
this : IsScalarTower R A Q := ⋯
refine : Eq (α := B →ₐ[R] Q) (AlgHom.restrictScalars R f₁) (AlgHom.restrictScalars R f₂)
⊢ f₁ = f₂

Tactic:
refine AlgHom.restrictScalars_injective R ?_

Premises used: AlgHom.restrictScalars_injective
-- Module: Mathlib.RingTheory.Unramified.Basic
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 B
Q : Type u_3
inst_8 : CommRing Q
inst_9 : Algebra A Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : Eq (α := B →ₐ[A] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂)
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A Q) (algebraMap R A))
this : IsScalarTower R A Q := ⋯
⊢ Eq (α := B →ₐ[R] Q) (AlgHom.restrictScalars R f₁) (AlgHom.restrictScalars R f₂)

Tactic:
FormallyUnramified.ext I ⟨2, e⟩ ?_

Premises used: Algebra.FormallyUnramified.ext, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Unramified.Basic
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 B
Q : Type u_3
inst_8 : CommRing Q
inst_9 : Algebra A Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : Eq (α := B →ₐ[A] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂)
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A Q) (algebraMap R A))
this : IsScalarTower R A Q := ⋯
refine :
  ∀ (x : B),
    Eq (α := Q ⧸ I) ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((AlgHom.restrictScalars R f₁ : (a : B) → Q) x) : Q ⧸ I)
      ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((AlgHom.restrictScalars R f₂ : (a : B) → Q) x) : Q ⧸ I)
⊢ Eq (α := B →ₐ[R] Q) (AlgHom.restrictScalars R f₁) (AlgHom.restrictScalars R f₂)

Tactic:
refine FormallyUnramified.ext I ⟨2, e⟩ ?_

Premises used: Algebra.FormallyUnramified.ext, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Unramified.Basic
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 B
Q : Type u_3
inst_8 : CommRing Q
inst_9 : Algebra A Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : Eq (α := B →ₐ[A] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂)
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A Q) (algebraMap R A))
this : IsScalarTower R A Q := ⋯
x : B
⊢ Eq (α := Q ⧸ I) ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((AlgHom.restrictScalars R f₁ : (a : B) → Q) x) : Q ⧸ I)
    ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((AlgHom.restrictScalars R f₂ : (a : B) → Q) x) : Q ⧸ I)

Tactic:
AlgHom.congr_fun e' x

Premises used: Submodule.Quotient.mk, AlgHom.congr_fun
-- Module: Mathlib.RingTheory.Unramified.Basic
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 B
Q : Type u_3
inst_8 : CommRing Q
inst_9 : Algebra A Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : Eq (α := B →ₐ[A] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂)
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A Q) (algebraMap R A))
this : IsScalarTower R A Q := ⋯
x : B
⊢ Eq (α := Q ⧸ I) ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((AlgHom.restrictScalars R f₁ : (a : B) → Q) x) : Q ⧸ I)
    ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((AlgHom.restrictScalars R f₂ : (a : B) → Q) x) : Q ⧸ I)

Tactic:
exact AlgHom.congr_fun e' x

Premises used: AlgHom.congr_fun
-- 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
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → 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
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
Q : Type u_3
_ :
  ∀ [inst_6 : CommRing Q] [inst_7 : Algebra R Q] (I : Ideal Q),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B →ₐ[R] Q) (β := B →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ ∀ [inst_6 : CommRing Q] [inst_7 : Algebra R Q] (I : Ideal Q),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B →ₐ[R] Q) (β := B →ₐ[R] Q ⧸ 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
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
Q : Type u_3
inst_6 : CommRing Q
_ :
  ∀ [inst_7 : Algebra R Q] (I : Ideal Q),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B →ₐ[R] Q) (β := B →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ ∀ [inst_7 : Algebra R Q] (I : Ideal Q),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B →ₐ[R] Q) (β := B →ₐ[R] Q ⧸ 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
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
Q : Type u_3
inst_6 : CommRing Q
inst_7 : Algebra R Q
I : Ideal Q
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : Eq (α := B →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
H₁ : ∀ (x : B), Eq (α := Q) ((f₁ : (a : B) → Q) x : Q) ((f₂ : (a : B) → Q) x : Q)
⊢ f₁ = f₂

Tactic:
ext x
-- 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
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
Q : Type u_3
inst_6 : CommRing Q
inst_7 : Algebra R Q
I : Ideal Q
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : Eq (α := B →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
x : B
H₁ :
  ∀ (x : A),
    Eq (α := Q) ((f₁ : (a : B) → Q) ((f : (a : A) → B) x : B) : Q) ((f₂ : (a : B) → Q) ((f : (a : A) → B) x : B) : Q)
⊢ Eq (α := Q) ((f₁ : (a : B) → Q) x : Q) ((f₂ : (a : B) → Q) x : Q)

Tactic:
obtain ⟨x, rfl⟩ := H x

Premises used: rfl
-- 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
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
Q : Type u_3
inst_6 : CommRing Q
inst_7 : Algebra R Q
I : Ideal Q
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : Eq (α := B →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
x : A
H₁ : Eq.{u_3 + 1} (α := Q) ((f₁.comp f : (a : A) → Q) x : Q) ((f₂.comp f : (a : A) → Q) x : Q)
⊢ Eq (α := Q) ((f₁ : (a : B) → Q) ((f : (a : A) → B) x : B) : Q) ((f₂ : (a : B) → Q) ((f : (a : A) → B) x : B) : Q)

Tactic:
rw [← AlgHom.comp_apply, ← AlgHom.comp_apply]

Premises used: AlgHom.comp_apply
-- 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
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
Q : Type u_3
inst_6 : CommRing Q
inst_7 : Algebra R Q
I : Ideal Q
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : Eq (α := B →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
x : A
H₁ : f₁.comp f = f₂.comp f
⊢ Eq.{u_3 + 1} (α := Q) ((f₁.comp f : (a : A) → Q) x : Q) ((f₂.comp f : (a : A) → Q) x : Q)

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
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
Q : Type u_3
inst_6 : CommRing Q
inst_7 : Algebra R Q
I : Ideal Q
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : Eq (α := B →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
x : A
H₁ :
  Eq (α := AlgHom.{u_1, u_2, u_3} R A (Q ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₁.comp f))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp f))
⊢ f₁.comp f = f₂.comp f

Tactic:
apply FormallyUnramified.comp_injective I hI

Premises used: Algebra.FormallyUnramified.comp_injective