awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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

Tactic:
have : p₀.map (algebraMap R S) = p := by
      subst hp
      exact le_bot_iff.mp (Ideal.map_comap_le)
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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))
pos₃ pos₄ :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization (M := S) p.primeCompl))
    (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))

Tactic:
rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, this,
      Localization.AtPrime.map_eq_maximalIdeal]

Premises used: Ideal.map_map, IsScalarTower.algebraMap_eq, Localization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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 = ⊥
neg :
  ¬Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤ HPow.hPow (β := ℕ) p 2
⊢ 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:
rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hp Ideal.map_comap_le,
    ← not_ne_iff, Ideal.ramificationIdx_ne_one_iff Ideal.map_comap_le]

Premises used: Ideal.ramificationIdx_ne_one_iff, not_ne_iff, Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff, Ideal.map_comap_le
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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
⊢ p₀.ramificationIdx P = 1

Tactic:
have := Ideal.ramificationIdx_eq_one_of_map_localization
    (hp₀ ▸ Ideal.map_comap_le) (hP₂ hp) hP₁ h₂
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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
⊢ ¬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

Premises used: Ideal.ramificationIdx_ne_one_iff, not_ne_iff
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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 : ¬Ideal.map (F := R →+* T) (algebraMap R T) p₀ ≤ HPow.hPow (β := ℕ) P 2
⊢ LE.le.{u_3} (α := Ideal T)
    (Ideal.map (R := S) (F := S →+* T) (algebraMap S T)
      (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) p)))
    (Ideal.map (F := S →+* T) (algebraMap S T) (HPow.hPow (β := ℕ) p 2))

Tactic:
replace H := Ideal.map_mono (f := algebraMap S T) H
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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 →+* T) (algebraMap R T) p₀ ≤ HPow.hPow (β := ℕ) P 2
H :
  LE.le.{u_3} (α := Ideal T)
    (Ideal.map (R := S) (F := S →+* T) (algebraMap S T)
      (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) p)))
    (Ideal.map (F := S →+* T) (algebraMap S T) (HPow.hPow (β := ℕ) p 2))
⊢ Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤
    HPow.hPow (α := Ideal T) (β := ℕ) (Ideal.map (F := S →+* T) (algebraMap S T) p) 2

Tactic:
rw [Ideal.map_map, ← IsScalarTower.algebraMap_eq, Ideal.map_pow] at H

Premises used: Ideal.map_map, IsScalarTower.algebraMap_eq, Ideal.map_pow
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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 →+* T) (algebraMap R T) p₀ ≤ HPow.hPow (β := ℕ) P 2
H :
  Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤
    HPow.hPow (α := Ideal T) (β := ℕ) (Ideal.map (F := S →+* T) (algebraMap S T) p) 2
⊢ False

Tactic:
this (H.trans (Ideal.pow_right_mono ?_ _))

Premises used: Ideal.pow_right_mono, LE.le.trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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 →+* T) (algebraMap R T) p₀ ≤ HPow.hPow (β := ℕ) P 2
H :
  Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤
    HPow.hPow (α := Ideal T) (β := ℕ) (Ideal.map (F := S →+* T) (algebraMap S T) p) 2
neg : Ideal.map (F := S →+* T) (algebraMap S T) p ≤ P
⊢ False

Tactic:
refine this (H.trans (Ideal.pow_right_mono ?_ _))

Premises used: Ideal.pow_right_mono, LE.le.trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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 →+* T) (algebraMap R T) p₀ ≤ HPow.hPow (β := ℕ) P 2
H :
  Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤
    HPow.hPow (α := Ideal T) (β := ℕ) (Ideal.map (F := S →+* T) (algebraMap S T) p) 2
⊢ Ideal.map (F := S →+* T) (algebraMap S T) p ≤ P

Tactic:
Ideal.map_le_iff_le_comap.mpr Ideal.LiesOver.over.le

Premises used: Iff.mpr, Eq.le, Ideal.map_le_iff_le_comap, Ideal.LiesOver.over
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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 →+* T) (algebraMap R T) p₀ ≤ HPow.hPow (β := ℕ) P 2
H :
  Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤
    HPow.hPow (α := Ideal T) (β := ℕ) (Ideal.map (F := S →+* T) (algebraMap S T) p) 2
⊢ Ideal.map (F := S →+* T) (algebraMap S T) p ≤ P

Tactic:
exact Ideal.map_le_iff_le_comap.mpr Ideal.LiesOver.over.le

Premises used: Iff.mpr, Eq.le, Ideal.map_le_iff_le_comap, Ideal.LiesOver.over
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
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
inst_14 : IsDomain T
inst_15 : Module.IsTorsionFree S T
⊢ IsUnramifiedAt R p

Tactic:
IsUnramifiedAt.of_liesOver_of_ne_bot R p P P.primeCompl_le_nonZeroDivisors
    (Ideal.ne_bot_of_liesOver_of_ne_bot · P)

Premises used: Ideal.ne_bot_of_liesOver_of_ne_bot, IsUnramifiedAt.of_liesOver_of_ne_bot, Ideal.primeCompl_le_nonZeroDivisors
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsDedekindDomain S
inst_5 : EssFiniteType R S
inst_6 : IsDomain R
inst_7 : Module.Finite ℤ R
inst_8 : CharZero R
inst_9 : Algebra.IsIntegral R S
hp : p ≠ ⊥
this : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R p) p
rw : Algebra.IsSeparable.{u_1, u_2} (Ideal.ResidueField (Ideal.under R p)) p.ResidueField
⊢ IsUnramifiedAt R p ↔ e(p|R) = 1

Tactic:
rw [isUnramifiedAt_iff_map_eq R (p.under R) p, and_iff_right,
    Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hp Ideal.map_comap_le]

Premises used: Algebra.isUnramifiedAt_iff_map_eq, and_iff_right, Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff, Ideal.map_comap_le, Ideal.under
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsDedekindDomain S
inst_5 : EssFiniteType R S
inst_6 : IsDomain R
inst_7 : Module.Finite ℤ R
inst_8 : CharZero R
inst_9 : Algebra.IsIntegral R S
hp : p ≠ ⊥
this : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R p) p
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))

Tactic:
have : Finite (R ⧸ p.under R) :=
    Ideal.finiteQuotientOfFreeOfNeBot _ (mt Ideal.eq_bot_of_comap_eq_bot hp)
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsDedekindDomain S
inst_5 : EssFiniteType R S
inst_6 : IsDomain R
inst_7 : Module.Finite ℤ R
inst_8 : CharZero R
inst_9 : Algebra.IsIntegral R S
hp : p ≠ ⊥
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R p) p
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
⊢ Finite.{u_1 + 1} (Ideal.ResidueField (Ideal.under R p))

Tactic:
have : Finite ((p.under R).ResidueField) := IsLocalization.finite _
    (nonZeroDivisors (R ⧸ p.under R))
-- Module: Mathlib.NumberTheory.RamificationInertia.Unramified
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsDedekindDomain S
inst_5 : EssFiniteType R S
inst_6 : IsDomain R
inst_7 : Module.Finite ℤ R
inst_8 : CharZero R
inst_9 : Algebra.IsIntegral R S
hp : p ≠ ⊥
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R p) p
this_2 : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
this : Finite.{u_1 + 1} (Ideal.ResidueField (Ideal.under R p))
⊢ Algebra.IsSeparable.{u_1, u_2} (Ideal.ResidueField (Ideal.under R p)) p.ResidueField

Tactic:
infer_instance