awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k
pos :
  ∀ (k : ℕ) (hk : map (F := R →+* S) f p ≤ P ^ k) (h2k : 2 < k),
    p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2

Tactic:
obtain ⟨k, hk, h2k⟩ := H 2

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k
k : ℕ
hk : map (F := R →+* S) f p ≤ P ^ k
h2k : 2 < k
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2

Tactic:
simp [Ideal.ramificationIdx_eq_zero H, hk.trans (Ideal.pow_le_pow_right h2k.le)]

Premises used: LT.lt.le, Ideal.pow_le_pow_right, Ideal.ramificationIdx_eq_zero, LE.le.trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
neg :
  Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1 ↔
    map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2

Tactic:
rw [Ideal.ramificationIdx_eq_find H]

Premises used: Ideal.ramificationIdx_eq_find
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
neg :
  Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1 →
    map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
neg₁ :
  map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2 →
    Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
⊢ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1 ↔
    map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2

Tactic:
constructor
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
⊢ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 1

Tactic:
simpa
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
⊢ 1 ≤ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H

Tactic:
have : 1 ≤ Nat.find H := Nat.find_spec H 1 (by simpa)
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
this : 1 ≤ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H
⊢ 1 < Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H

Tactic:
lia
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
this : 1 ≤ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H
⊢ ¬∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ 1

Tactic:
have := Nat.find_min H (m := 1) (by lia)
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
this_1 : 1 ≤ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H
this : ¬∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ 1
⊢ ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ 1 < k

Tactic:
push Not at this

Premises used: Not
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
this_1 : 1 ≤ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H
this : ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ 1 < k
neg : ∀ (k : ℕ) (hk : map (F := R →+* S) f p ≤ P ^ k) (h1k : 1 < k), map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
⊢ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2

Tactic:
obtain ⟨k, hk, h1k⟩ := this
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
this : 1 ≤ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H
k : ℕ
hk : map (F := R →+* S) f p ≤ P ^ k
h1k : 1 < k
⊢ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2

Tactic:
hk.trans (Ideal.pow_le_pow_right (Nat.succ_le_iff.mpr h1k))

Premises used: Iff.mpr, Ideal.pow_le_pow_right, LE.le.trans, Nat.succ_le_iff
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
this : 1 ≤ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H
k : ℕ
hk : map (F := R →+* S) f p ≤ P ^ k
h1k : 1 < k
⊢ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2

Tactic:
exact hk.trans (Ideal.pow_le_pow_right (Nat.succ_le_iff.mpr h1k))

Premises used: Iff.mpr, Ideal.pow_le_pow_right, LE.le.trans, Nat.succ_le_iff
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
⊢ 2 ≤ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H

Tactic:
have := Nat.find_spec H 2 he
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
this : 2 ≤ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H
⊢ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : map (F := R →+* S) f p ≤ P
pos :
  ∀ (H : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k),
    p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
neg :
  ∀ (H : ¬∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k),
    p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
pos₁ :
  ∀ (H : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k),
    p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
neg₁ :
  ∀ (H : ¬∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k),
    p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
pos₂ :
  ∀ (H : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k),
    p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
neg₂ neg₃ :
  ∀ (H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n),
    p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
neg₄ :
  ∀ (H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n),
    Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1 ↔
      map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
neg₅ :
  ∀ (H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n),
    Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1 →
      map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
neg₆ neg₇ :
  ∀ (H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n),
    map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2 →
      Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2

Tactic:
classical
  by_cases! H : ∀ n : ℕ, ∃ k, p.map f ≤ P ^ k ∧ n < k
  · obtain ⟨k, hk, h2k⟩ := H 2
    simp [Ideal.ramificationIdx_eq_zero H, hk.trans (Ideal.pow_le_pow_right h2k.le)]
  rw [Ideal.ramificationIdx_eq_find H]
  constructor
  · intro he
    have : 1 ≤ Nat.find H := Nat.find_spec H 1 (by simpa)
    have := Nat.find_min H (m := 1) (by lia)
    push Not at this
    obtain ⟨k, hk, h1k⟩ := this
    exact hk.trans (Ideal.pow_le_pow_right (Nat.succ_le_iff.mpr h1k))
  · intro he
    have := Nat.find_spec H 2 he
    lia

Premises used: Not
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : IsNoetherianRing S
hpP : map (F := R →+* S) f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H :
  Eq.{v + 1} (α := Ideal (Localization.AtPrime P))
    (map (F := RingHom.{u, v} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p)
    (maximalIdeal (Localization.AtPrime P))
rw : ¬map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
⊢ p.ramificationIdx P = 1

Tactic:
rw [← not_ne_iff (b := 1), Ideal.ramificationIdx_ne_one_iff hpP]

Premises used: Ideal.ramificationIdx_ne_one_iff, not_ne_iff
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : IsNoetherianRing S
hpP : map (F := R →+* S) f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H :
  Eq.{v + 1} (α := Ideal (Localization.AtPrime P))
    (map (F := RingHom.{u, v} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p)
    (maximalIdeal (Localization.AtPrime P))
h₂ : map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
⊢ LE.le (α := Ideal (Localization.AtPrime P))
    (map (R := S) (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) (map (F := R →+* S) f p))
    (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) (HPow.hPow (β := ℕ) P 2))

Tactic:
replace h₂ := Ideal.map_mono («f» := algebraMap S (Localization.AtPrime P)) h₂
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : IsNoetherianRing S
hpP : map (F := R →+* S) f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H :
  Eq.{v + 1} (α := Ideal (Localization.AtPrime P))
    (map (F := RingHom.{u, v} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p)
    (maximalIdeal (Localization.AtPrime P))
h₂ :
  LE.le (α := Ideal (Localization.AtPrime P))
    (map (R := S) (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) (map (F := R →+* S) f p))
    (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) (HPow.hPow (β := ℕ) P 2))
⊢ maximalIdeal (Localization.AtPrime P) ≤
    HMul.hMul (α := Ideal (Localization.AtPrime P)) (maximalIdeal (Localization (M := S) P.primeCompl))
      (maximalIdeal (Localization (M := S) P.primeCompl))

Tactic:
rw [Ideal.map_pow, Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_map,
    ← IsScalarTower.algebraMap_eq, H, pow_two] at h₂

Premises used: pow_two, Ideal.map_map, IsScalarTower.algebraMap_eq, Ideal.map_pow, Localization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : IsNoetherianRing S
hpP : map (F := R →+* S) f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H :
  Eq.{v + 1} (α := Ideal (Localization.AtPrime P))
    (map (F := RingHom.{u, v} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p)
    (maximalIdeal (Localization.AtPrime P))
h₂ :
  maximalIdeal (Localization.AtPrime P) ≤
    HMul.hMul (α := Ideal (Localization.AtPrime P)) (maximalIdeal (Localization (M := S) P.primeCompl))
      (maximalIdeal (Localization (M := S) P.primeCompl))
⊢ Eq.{v + 1} (α := Submodule (Localization.AtPrime P) (Localization.AtPrime P)) (maximalIdeal (Localization.AtPrime P))
    ⊥

Tactic:
have := Submodule.eq_bot_of_le_smul_of_le_jacobson_bot _ _ (IsNoetherian.noetherian _) h₂
    (maximalIdeal_le_jacobson _)
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : IsNoetherianRing S
hpP : map (F := R →+* S) f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H :
  Eq.{v + 1} (α := Ideal (Localization.AtPrime P))
    (map (F := RingHom.{u, v} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p)
    (maximalIdeal (Localization.AtPrime P))
h₂ :
  maximalIdeal (Localization.AtPrime P) ≤
    HMul.hMul (α := Ideal (Localization.AtPrime P)) (maximalIdeal (Localization (M := S) P.primeCompl))
      (maximalIdeal (Localization (M := S) P.primeCompl))
this :
  Eq.{v + 1} (α := Submodule (Localization.AtPrime P) (Localization.AtPrime P)) (maximalIdeal (Localization.AtPrime P))
    ⊥
rw : ∀ (this : P = ⊥), False
rw₁ :
  ∀
    (this :
      Eq (α := Submodule (Localization.AtPrime P) (Localization.AtPrime P))
        (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) P) ⊥),
    Function.Injective (α := S) (β := Localization.AtPrime P)
      (⇑(algebraMap S (Localization.AtPrime P)) : (a : S) → Localization.AtPrime P)
⊢ False

Tactic:
rw [← Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_eq_bot_iff_of_injective] at this

Premises used: Ideal.map_eq_bot_iff_of_injective, Localization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : IsNoetherianRing S
hpP : map (F := R →+* S) f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H :
  Eq.{v + 1} (α := Ideal (Localization.AtPrime P))
    (map (F := RingHom.{u, v} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p)
    (maximalIdeal (Localization.AtPrime P))
h₂ :
  maximalIdeal (Localization.AtPrime P) ≤
    HMul.hMul (α := Ideal (Localization.AtPrime P)) (maximalIdeal (Localization (M := S) P.primeCompl))
      (maximalIdeal (Localization (M := S) P.primeCompl))
this : P = ⊥
⊢ False

Tactic:
hp this
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : IsNoetherianRing S
hpP : map (F := R →+* S) f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H :
  Eq.{v + 1} (α := Ideal (Localization.AtPrime P))
    (map (F := RingHom.{u, v} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p)
    (maximalIdeal (Localization.AtPrime P))
h₂ :
  maximalIdeal (Localization.AtPrime P) ≤
    HMul.hMul (α := Ideal (Localization.AtPrime P)) (maximalIdeal (Localization (M := S) P.primeCompl))
      (maximalIdeal (Localization (M := S) P.primeCompl))
this : P = ⊥
⊢ False

Tactic:
exact hp this
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : IsNoetherianRing S
hpP : map (F := R →+* S) f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H :
  Eq.{v + 1} (α := Ideal (Localization.AtPrime P))
    (map (F := RingHom.{u, v} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p)
    (maximalIdeal (Localization.AtPrime P))
h₂ :
  maximalIdeal (Localization.AtPrime P) ≤
    HMul.hMul (α := Ideal (Localization.AtPrime P)) (maximalIdeal (Localization (M := S) P.primeCompl))
      (maximalIdeal (Localization (M := S) P.primeCompl))
this :
  Eq (α := Submodule (Localization.AtPrime P) (Localization.AtPrime P))
    (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) P) ⊥
⊢ Function.Injective (α := S) (β := Localization.AtPrime P)
    (⇑(algebraMap S (Localization.AtPrime P)) : (a : S) → Localization.AtPrime P)

Tactic:
IsLocalization.injective _ hp'

Premises used: IsLocalization.injective
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : IsNoetherianRing S
hpP : map (F := R →+* S) f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H :
  Eq.{v + 1} (α := Ideal (Localization.AtPrime P))
    (map (F := RingHom.{u, v} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p)
    (maximalIdeal (Localization.AtPrime P))
h₂ :
  maximalIdeal (Localization.AtPrime P) ≤
    HMul.hMul (α := Ideal (Localization.AtPrime P)) (maximalIdeal (Localization (M := S) P.primeCompl))
      (maximalIdeal (Localization (M := S) P.primeCompl))
this :
  Eq (α := Submodule (Localization.AtPrime P) (Localization.AtPrime P))
    (map (F := S →+* Localization.AtPrime P) (algebraMap S (Localization.AtPrime P)) P) ⊥
⊢ Function.Injective (α := S) (β := Localization.AtPrime P)
    (⇑(algebraMap S (Localization.AtPrime P)) : (a : S) → Localization.AtPrime P)

Tactic:
exact IsLocalization.injective _ hp'

Premises used: IsLocalization.injective
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
h₁ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊤
h₂ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
⊢ map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
h₁ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊤
h₂ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
refine :
  ∀ (h : map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (map (F := R →+* S) f p) (HAdd.hAdd (α := ℕ) 1 1)), False
⊢ ramificationIdx.{u, v} (S := S) p (map (F := R →+* S) f p) = 1

Tactic:
refine ramificationIdx_spec (by simp) fun h ↦ ?_

Premises used: Ideal.ramificationIdx_spec
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
h₁ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊤
h₂ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
h : map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (map (F := R →+* S) f p) (HAdd.hAdd (α := ℕ) 1 1)
rw : map (F := R →+* S) f p = HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 2
⊢ HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 1 =
    HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 2

Tactic:
rw [pow_one]

Premises used: pow_one
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
h₁ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊤
h₂ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
h : map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (map (F := R →+* S) f p) (HAdd.hAdd (α := ℕ) 1 1)
⊢ map (F := R →+* S) f p = HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 2

Tactic:
le_antisymm h <| pow_le_self two_ne_zero

Premises used: Ideal.pow_le_self, two_ne_zero, le_antisymm
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
h₁ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊤
h₂ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
h : map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (map (F := R →+* S) f p) (HAdd.hAdd (α := ℕ) 1 1)
⊢ map (F := R →+* S) f p = HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 2

Tactic:
exact le_antisymm h <| pow_le_self two_ne_zero

Premises used: Ideal.pow_le_self, two_ne_zero, le_antisymm
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
h₁ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊤
h₂ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
h : map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (map (F := R →+* S) f p) (HAdd.hAdd (α := ℕ) 1 1)
⊢ HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 1 =
    HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 2

Tactic:
have : map f p ^ 1 = (map f p) ^ 2 := by
    rw [pow_one]
    exact le_antisymm h <| pow_le_self two_ne_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
h₁ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊤
h₂ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
h : map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (map (F := R →+* S) f p) (HAdd.hAdd (α := ℕ) 1 1)
this :
  HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 1 =
    HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 2
rwa rwa₁ rwa₂ rwa₃ : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊤
⊢ Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) 1

Tactic:
rwa [one_eq_top]

Premises used: Ideal.one_eq_top