awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
⊢ Algebra.IsSeparable.{u_1, u_2} p₀.ResidueField p.ResidueField ∧
    Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
      (maximalIdeal (Localization.AtPrime p))
have refine : Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
  (maximalIdeal (Localization.AtPrime p))
Tactic: refine ⟨Algebra.isSeparable_tower_bot_of_isSeparable _ _ P.ResidueField, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
⊢ Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
    (maximalIdeal (Localization.AtPrime p))
have pos : ∀ (hp : p = ⊥),
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
    (maximalIdeal (Localization.AtPrime p))
Tactic: by_cases hp : p = ⊥
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
pos :
  ∀ (hp : p = ⊥),
    Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
      (maximalIdeal (Localization.AtPrime p))
⊢ Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
    (maximalIdeal (Localization.AtPrime p))
have neg : ∀ (hp : ¬p = ⊥),
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
    (maximalIdeal (Localization.AtPrime p))
Tactic: by_cases hp : p = ⊥
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : p = ⊥
⊢ Ideal.map (F := R →+* S) (algebraMap R S) p₀ = p
have subst : ∀ [Ideal.LiesOver.{u_2, u_3} (A := S) P ⊥] [inst_15 : Ideal.IsPrime.{u_2} (α := S) ⊥]
  (hP₂ : Ne.{u_2 + 1} (α := Ideal S) ⊥ ⊥ → P ≠ ⊥),
  let p₀ : Ideal R := Ideal.under.{u_1, u_2} R (B := S) ⊥;
  ∀ (this : P.LiesOver p₀),
    let this_6 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
      Localization.AtPrime.algebraOfLiesOver p₀ P;
    ∀ (hp₀ : p₀ = Ideal.under R P) (h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField)
      (h₂ :
        Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
          (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
          (maximalIdeal (Localization.AtPrime P))),
      Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p₀) ⊥
Tactic: subst hp
Cleared hypotheses: p, inst_7, inst_8, hP₂, p₀, this_1, this_2, this_3, this_4, hp₀, h₁, h₂, hp
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : p = ⊥
⊢ Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
    (maximalIdeal (Localization.AtPrime p))
have this₁ : Ideal.map (F := R →+* S) (algebraMap R S) p₀ = p
Tactic: have : p₀.map (algebraMap R S) = p := by
      subst hp
      exact le_bot_iff.mp (Ideal.map_comap_le)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this_6 : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : p = ⊥
this : Ideal.map (F := R →+* S) (algebraMap R S) p₀ = p
⊢ Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
    (maximalIdeal (Localization.AtPrime p))
have pos : Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.AtPrime p)) (algebraMap R S)) p₀)
  (maximalIdeal (Localization.AtPrime p))
Tactic: rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, this,
      Localization.AtPrime.map_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this_6 : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : p = ⊥
this : Ideal.map (F := R →+* S) (algebraMap R S) p₀ = p
pos :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.AtPrime p)) (algebraMap R S)) p₀)
    (maximalIdeal (Localization.AtPrime p))
⊢ Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
    (maximalIdeal (Localization.AtPrime p))
have pos₁ : Eq (α := Ideal (Localization.AtPrime p))
  (Ideal.map (R := S) (F := S →+* Localization.AtPrime p) (algebraMap S (Localization.AtPrime p))
    (Ideal.map (F := R →+* S) (algebraMap R S) p₀))
  (maximalIdeal (Localization.AtPrime p))
Tactic: rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, this,
      Localization.AtPrime.map_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this_6 : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : p = ⊥
this : Ideal.map (F := R →+* S) (algebraMap R S) p₀ = p
pos :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.AtPrime p)) (algebraMap R S)) p₀)
    (maximalIdeal (Localization.AtPrime p))
pos₁ :
  Eq (α := Ideal (Localization.AtPrime p))
    (Ideal.map (R := S) (F := S →+* Localization.AtPrime p) (algebraMap S (Localization.AtPrime p))
      (Ideal.map (F := R →+* S) (algebraMap R S) p₀))
    (maximalIdeal (Localization.AtPrime p))
⊢ Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
    (maximalIdeal (Localization.AtPrime p))
have pos₂ : Eq (α := Ideal (Localization.AtPrime p))
  (Ideal.map (F := S →+* Localization.AtPrime p) (algebraMap S (Localization.AtPrime p)) p)
  (maximalIdeal (Localization.AtPrime p))
Tactic: rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, this,
      Localization.AtPrime.map_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this_6 : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : p = ⊥
this : Ideal.map (F := R →+* S) (algebraMap R S) p₀ = p
pos :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.AtPrime p)) (algebraMap R S)) p₀)
    (maximalIdeal (Localization.AtPrime p))
pos₁ :
  Eq (α := Ideal (Localization.AtPrime p))
    (Ideal.map (R := S) (F := S →+* Localization.AtPrime p) (algebraMap S (Localization.AtPrime p))
      (Ideal.map (F := R →+* S) (algebraMap R S) p₀))
    (maximalIdeal (Localization.AtPrime p))
pos₂ :
  Eq (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := S →+* Localization.AtPrime p) (algebraMap S (Localization.AtPrime p)) p)
    (maximalIdeal (Localization.AtPrime p))
⊢ Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
    (maximalIdeal (Localization.AtPrime p))
have pos₃ : Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization (M := S) p.primeCompl))
  (maximalIdeal (Localization.AtPrime p))
Tactic: rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, this,
      Localization.AtPrime.map_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : ¬p = ⊥
⊢ Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
    (maximalIdeal (Localization.AtPrime p))
have neg : ¬Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤ HPow.hPow (β := ℕ) p 2
Tactic: rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hp Ideal.map_comap_le,
    ← not_ne_iff, Ideal.ramificationIdx_ne_one_iff Ideal.map_comap_le]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : ¬p = ⊥
H : Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤ HPow.hPow (β := ℕ) p 2
⊢ False
have this₁ : p₀.ramificationIdx P = 1
Tactic: have := Ideal.ramificationIdx_eq_one_of_map_localization
    (hp₀ ▸ Ideal.map_comap_le) (hP₂ hp) hP₁ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this_6 : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : ¬p = ⊥
H : Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤ HPow.hPow (β := ℕ) p 2
this : p₀.ramificationIdx P = 1
⊢ False
have this₁ : ¬Ideal.map (F := R →+* T) (algebraMap R T) p₀ ≤ HPow.hPow (β := ℕ) P 2
Tactic: rw [← not_ne_iff, Ideal.ramificationIdx_ne_one_iff (hp₀ ▸ Ideal.map_comap_le)] at this
Cleared hypotheses: this