awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
inst_9 : IsDomain R
inst_10 : IsTorsionFree R S
inst_11 : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst_12 : Q.IsPrime
inst_13 : Q.LiesOver P
inst_14 : P.LiesOver p
hp : p ≠ ⊥
this : P.IsPrime
r : R
m : T
h : r • m = 0
rwa : ∀ (h : HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((f : (a : R) → S) r : S) m = 0), r = 0 ∨ m = 0
rwa₁ : ∀ (h : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S) ∨ m = 0), r = 0 ∨ m = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : r = 0 ∨ m = 0), r = 0 ∨ m = 0
⊢ r = 0 ∨ m = 0

Tactic:
rwa [algebra_compatible_smul S, smul_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff] at h

Premises used: algebra_compatible_smul, smul_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
inst_9 : IsDomain R
inst_10 : IsTorsionFree R S
inst_11 : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst_12 : Q.IsPrime
inst_13 : Q.LiesOver P
inst_14 : P.LiesOver p
hp : p ≠ ⊥
this : P.IsPrime
⊢ IsTorsionFree R T

Tactic:
have : Module.IsTorsionFree R T := by
    refine Module.IsTorsionFree.of_smul_eq_zero fun r m h ↦ ?_
    rwa [algebra_compatible_smul S, smul_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff] at h
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
inst_9 : IsDomain R
inst_10 : IsTorsionFree R S
inst_11 : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst_12 : Q.IsPrime
inst_13 : Q.LiesOver P
inst_14 : P.LiesOver p
hp : p ≠ ⊥
this_1 : P.IsPrime
this : IsTorsionFree R T
⊢ P ≠ ⊥

Tactic:
have hP : P ≠ ⊥ := ne_bot_of_liesOver_of_ne_bot hp _
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
inst_9 : IsDomain R
inst_10 : IsTorsionFree R S
inst_11 : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst_12 : Q.IsPrime
inst_13 : Q.LiesOver P
inst_14 : P.LiesOver p
hp : p ≠ ⊥
this_1 : P.IsPrime
this : IsTorsionFree R T
hP : P ≠ ⊥
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q

Tactic:
ramificationIdx_algebra_tower (map_ne_bot_of_ne_bot hP) (map_ne_bot_of_ne_bot hp)
    <| map_le_iff_le_comap.mpr <| le_of_eq <| over_def Q P

Premises used: Iff.mpr, Ideal.ramificationIdx_algebra_tower, Ideal.map_le_iff_le_comap, Ideal.map_ne_bot_of_ne_bot, Ideal.over_def, le_of_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
inst_9 : IsDomain R
inst_10 : IsTorsionFree R S
inst_11 : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst_12 : Q.IsPrime
inst_13 : Q.LiesOver P
inst_14 : P.LiesOver p
hp : p ≠ ⊥
this_1 : P.IsPrime
this : IsTorsionFree R T
hP : P ≠ ⊥
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q

Tactic:
exact ramificationIdx_algebra_tower (map_ne_bot_of_ne_bot hP) (map_ne_bot_of_ne_bot hp)
    <| map_le_iff_le_comap.mpr <| le_of_eq <| over_def Q P

Premises used: Iff.mpr, Ideal.ramificationIdx_algebra_tower, Ideal.map_le_iff_le_comap, Ideal.map_ne_bot_of_ne_bot, Ideal.over_def, le_of_eq
-- 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 : IsNoetherianRing S
inst_5 : IsUnramifiedAt R p
hp : p ≠ ⊥
inst_6 : IsDomain S
inst_7 : EssFiniteType R S
⊢ e(p|R) = 1

Tactic:
let := Localization.AtPrime.algebraOfLiesOver (p.under R) p
  (Ideal.ramificationIdx_eq_one_of_map_localization Ideal.map_comap_le hp
    p.primeCompl_le_nonZeroDivisors
    ((isUnramifiedAt_iff_map_eq R (p.under R) p).mp ‹_›).2)

Premises used: Localization.AtPrime.algebraOfLiesOver, Ideal.ramificationIdx_eq_one_of_map_localization, Algebra.isUnramifiedAt_iff_map_eq, And.right, Iff.mp, Ideal.primeCompl_le_nonZeroDivisors, Ideal.map_comap_le, Ideal.under
-- 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
⊢ P.LiesOver p₀

Tactic:
have : P.LiesOver p₀ := .trans P p p₀
-- 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 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
⊢ p₀ = Ideal.under R P

Tactic:
have hp₀ : p₀ = P.under R := 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 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
⊢ EssFiniteType S T

Tactic:
have : EssFiniteType S T := .of_comp R S T
-- 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 : EssFiniteType S T
⊢ IsNoetherianRing T

Tactic:
have := Algebra.EssFiniteType.isNoetherianRing S T
-- 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
rw :
  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))
⊢ IsUnramifiedAt R p

Tactic:
rw [isUnramifiedAt_iff_map_eq R p₀ p]

Premises used: Algebra.isUnramifiedAt_iff_map_eq
-- 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
⊢ Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField

Tactic:
have ⟨h₁, h₂⟩ := (isUnramifiedAt_iff_map_eq R p₀ P).mp ‹_›
-- 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
⊢ 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))

Tactic:
have ⟨h₁, h₂⟩ := (isUnramifiedAt_iff_map_eq R p₀ P).mp ‹_›
-- 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))
⊢ 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))

Tactic:
⟨Algebra.isSeparable_tower_bot_of_isSeparable _ _ P.ResidueField, ?_⟩

Premises used: Ideal.ResidueField, Algebra.isSeparable_tower_bot_of_isSeparable, And.intro
-- 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))
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))
⊢ 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))

Tactic:
refine ⟨Algebra.isSeparable_tower_bot_of_isSeparable _ _ P.ResidueField, ?_⟩
-- 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))
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))
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))
⊢ 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 = ⊥
-- 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 = ⊥
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₀) ⊥
⊢ Ideal.map (F := R →+* S) (algebraMap R S) p₀ = p

Tactic:
subst hp
-- 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 T
inst_7 : P.IsPrime
inst_8 : IsUnramifiedAt R P
inst_9 : EssFiniteType R S
inst_10 : EssFiniteType R T
inst_11 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
this_1 : EssFiniteType S T
this_2 : IsNoetherianRing T
inst_12 : Ideal.LiesOver.{u_2, u_3} (A := S) P ⊥
inst_13 : Ideal.IsPrime.{u_2} (α := S) ⊥
hP₂ : Ne.{u_2 + 1} (α := Ideal S) ⊥ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under.{u_1, u_2} R (B := S) ⊥
this_3 : P.LiesOver p₀
this_4 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime (R := S) ⊥) :=
  Localization.AtPrime.algebraOfLiesOver p₀ ⊥
this_5 : Algebra.{u_2, u_3} (Localization.AtPrime (R := S) ⊥) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver ⊥ P
this : 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:
le_bot_iff.mp (Ideal.map_comap_le)

Premises used: le_bot_iff, 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 T
inst_7 : P.IsPrime
inst_8 : IsUnramifiedAt R P
inst_9 : EssFiniteType R S
inst_10 : EssFiniteType R T
inst_11 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
this_1 : EssFiniteType S T
this_2 : IsNoetherianRing T
inst_12 : Ideal.LiesOver.{u_2, u_3} (A := S) P ⊥
inst_13 : Ideal.IsPrime.{u_2} (α := S) ⊥
hP₂ : Ne.{u_2 + 1} (α := Ideal S) ⊥ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under.{u_1, u_2} R (B := S) ⊥
this_3 : P.LiesOver p₀
this_4 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime (R := S) ⊥) :=
  Localization.AtPrime.algebraOfLiesOver p₀ ⊥
this_5 : Algebra.{u_2, u_3} (Localization.AtPrime (R := S) ⊥) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver ⊥ P
this : 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:
exact le_bot_iff.mp (Ideal.map_comap_le)

Premises used: le_bot_iff, Iff.mp, Ideal.map_comap_le