awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallyUnramified A B
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 (α := 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)))
have 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)))
Tactic: rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallyUnramified A B
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)))
⊢ 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)))
have 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)))
Tactic: rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallyUnramified A B
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)))
⊢ 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)))
have 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)))
Tactic: rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (hypothesis)
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₂)
⊢ f₁ = f₂
have e' : 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])
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallyUnramified A B
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' := ⋯ }
⊢ f₁ = f₂
have H : ∀ (x : B), Eq (α := C) ((f₁ : (a : B) → C) x : C) ((f₂ : (a : B) → C) x : C)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallyUnramified A B
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
⊢ Eq (α := C) ((f₁ : (a : B) → C) x : C) ((f₂ : (a : B) → C) x : C)
have H : Eq (α := C) ((F₁ : (a : B) → C) x : C) ((F₂ : (a : B) → C) x : C)
Tactic: change F₁ x = F₂ x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallyUnramified A B
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
⊢ Eq (α := C) ((F₁ : (a : B) → C) x : C) ((F₂ : (a : B) → C) x : C)
have H : F₁ = F₂
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R B
⊢ FormallyUnramified A B
have 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))
Tactic: rw [iff_comp_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
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₂
have refine : Eq (α := B →ₐ[R] Q) (AlgHom.restrictScalars R f₁) (AlgHom.restrictScalars R f₂)
Tactic: refine AlgHom.restrictScalars_injective R ?_
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R 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₂)
have 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)
Tactic: refine FormallyUnramified.ext I ⟨2, e⟩ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ FormallyUnramified R B
have rw : ∀ ⦃B_1 : Type u_3⦄ [inst_6 : CommRing B_1] [inst_7 : Algebra R B_1] (I : Ideal B_1),
  HPow.hPow (β := ℕ) I 2 = ⊥ →
    Function.Injective (α := B →ₐ[R] B_1) (β := B →ₐ[R] B_1 ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Tactic: rw [iff_comp_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
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₂)
⊢ f₁ = f₂
have H₁ : ∀ (x : B), Eq (α := Q) ((f₁ : (a : B) → Q) x : Q) ((f₂ : (a : B) → Q) x : Q)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
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
⊢ Eq (α := Q) ((f₁ : (a : B) → Q) x : Q) ((f₂ : (a : B) → Q) x : Q)
have 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)
Tactic: obtain ⟨x, rfl⟩ := H x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
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
⊢ Eq (α := Q) ((f₁ : (a : B) → Q) ((f : (a : A) → B) x : B) : Q) ((f₂ : (a : B) → Q) ((f : (a : A) → B) x : B) : Q)
have H₁ : Eq.{u_3 + 1} (α := Q) ((f₁.comp f : (a : A) → Q) x : Q) ((f₂.comp f : (a : A) → Q) x : Q)
Tactic: rw [← AlgHom.comp_apply, ← AlgHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
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
⊢ Eq.{u_3 + 1} (α := Q) ((f₁.comp f : (a : A) → Q) x : Q) ((f₂.comp f : (a : A) → Q) x : Q)
have H₁ : f₁.comp f = f₂.comp f
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
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
⊢ f₁.comp f = f₂.comp f
have 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))
Tactic: apply FormallyUnramified.comp_injective I hI
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
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
⊢ 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))
have H₁ : ∀ (x : A),
  Eq.{u_3 + 1} (α := Q ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₁.comp f) : AlgHom.{u_1, u_2, u_3} R A (Q ⧸ I)) : (a : A) → Q ⧸ I) x :
      Q ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp f) : AlgHom.{u_1, u_2, u_3} R A (Q ⧸ I)) : (a : A) → Q ⧸ I) x :
      Q ⧸ I)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
⊢ FormallyUnramified B (B ⊗[R] A)
have rw : ∀ ⦃B_1 : Type (max u_2 u_3)⦄ [inst_6 : CommRing B_1] [inst_7 : Algebra B B_1] (I : Ideal B_1),
  HPow.hPow (β := ℕ) I 2 = ⊥ →
    Function.Injective (α := B ⊗[R] A →ₐ[B] B_1) (β := B ⊗[R] A →ₐ[B] B_1 ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I))
Tactic: rw [iff_comp_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (hypothesis)
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 : FormallyUnramified R A
C : Type (max u_2 u_3)
inst_6 : CommRing C
inst_7 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : Eq (α := B ⊗[R] A →ₐ[B] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₂)
this : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
⊢ f₁ = f₂
have this₁ : IsScalarTower R B C
Tactic: haveI : IsScalarTower R B C := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
C : Type (max u_2 u_3)
inst_6 : CommRing C
inst_7 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : Eq (α := B ⊗[R] A →ₐ[B] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₂)
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ f₁ = f₂
have h : Eq (α := A →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f₁) TensorProduct.includeRight)
  (AlgHom.comp (AlgHom.restrictScalars R f₂) TensorProduct.includeRight)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
⊢ FormallyUnramified R Rₘ
have rw : ∀ ⦃B : Type u_3⦄ [inst_4 : CommRing B] [inst_5 : Algebra R B] (I : Ideal B),
  HPow.hPow (β := ℕ) I 2 = ⊥ →
    Function.Injective (α := Rₘ →ₐ[R] B) (β := Rₘ →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Tactic: rw [iff_comp_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
inst_4 : CommRing Q
inst_5 : Algebra R Q
I : Ideal Q
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
h_1 : Eq (α := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
⊢ f₁ = f₂
have a : Eq (α := Rₘ →+* Q) (↑f₁ : Rₘ →+* Q) (↑f₂ : Rₘ →+* Q)
Tactic: apply AlgHom.coe_ringHom_injective
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
inst_4 : CommRing Q
inst_5 : Algebra R Q
I : Ideal Q
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
h_1 : Eq (α := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
⊢ Eq (α := Rₘ →+* Q) (↑f₁ : Rₘ →+* Q) (↑f₂ : Rₘ →+* Q)
have a : Eq (α := R →+* Q) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₁ : Rₘ →+* Q) (algebraMap R Rₘ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₂ : Rₘ →+* Q) (algebraMap R Rₘ))
Tactic: refine IsLocalization.ringHom_ext M ?_
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
inst_4 : CommRing Q
inst_5 : Algebra R Q
I : Ideal Q
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
h_1 : Eq (α := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
⊢ Eq (α := R →+* Q) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₁ : Rₘ →+* Q) (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₂ : Rₘ →+* Q) (algebraMap R Rₘ))
have a : ∀ (x : R),
  Eq.{u_3 + 1} (α := Q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₁ : Rₘ →+* Q) (algebraMap R Rₘ) : (a : R) → Q) x : Q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₂ : Rₘ →+* Q) (algebraMap R Rₘ) : (a : R) → Q) x : Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_12 : FormallyUnramified R S
⊢ FormallyUnramified Rₘ Sₘ
have this : FormallyUnramified S Sₘ
Tactic: haveI : FormallyUnramified S Sₘ :=
    FormallyUnramified.of_isLocalization (M.map (algebraMap R S))
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_12 : FormallyUnramified R S
this : FormallyUnramified S Sₘ
⊢ FormallyUnramified Rₘ Sₘ
have this₁ : FormallyUnramified R Sₘ
Tactic: haveI : FormallyUnramified R Sₘ := FormallyUnramified.comp R S Sₘ
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
inst_4 : FormallyUnramified R S
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T), Nonempty.{u + 1} (S ⊗[R] S ≃ₐ[S] S × T)
have obtain : ∀ (e : S ⊗[R] S) (he : IsIdempotentElem e)
  (hsp : Eq (α := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (S ⊗[R] S ∙ e)),
  ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T), Nonempty.{u + 1} (S ⊗[R] S ≃ₐ[S] S × T)
Tactic: obtain ⟨e, he, hsp⟩ : ∃ e, IsIdempotentElem e ∧ KaehlerDifferential.ideal R S = S ⊗[R] S ∙ e :=
    (Ideal.isIdempotentElem_iff_of_fg _ (KaehlerDifferential.ideal_fg R S)).mp <|
      (Ideal.cotangent_subsingleton_iff _).mp <| inferInstanceAs <| Subsingleton Ω[S⁄R]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Dedekind (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
⊢ IsDiscreteValuationRing.{u_2} (Localization.AtPrime q)
have suffices : Submodule.IsPrincipal q'
Tactic: suffices q'.IsPrincipal from ((IsDiscreteValuationRing.TFAE (Localization.AtPrime q)
      (IsLocalization.AtPrime.not_isField B hq (Localization.AtPrime q))).out 4 0).mp this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Dedekind (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
⊢ Submodule.IsPrincipal q'
have this₁ : p.IsMaximal
Tactic: have : p.IsMaximal := (hqp.under A).isMaximal (q.under_ne_bot A hq)