case zero
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hgt : ¬map f p ≤ P ^ Nat.zero
⊢ ramificationIdx f p P < Nat.zero

case succ
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ Nat.succ n
⊢ ramificationIdx f p P < Nat.succ n
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ n
⊢ ramificationIdx f p P < n
cases' n with n n
no goals
case zero
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hgt : ¬map f p ≤ P ^ Nat.zero
⊢ ramificationIdx f p P < Nat.zero
simp at hgt
case succ
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ Nat.succ n
⊢ ramificationIdx f p P ≤ n
case succ
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ Nat.succ n
⊢ ramificationIdx f p P < Nat.succ n
rw [Nat.lt_succ_iff]
case succ
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ Nat.succ n
this : ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ ramificationIdx f p P ≤ n
case succ
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ Nat.succ n
⊢ ramificationIdx f p P ≤ n
have : ∀ k, map f p ≤ P ^ k → k ≤ n := by
  refine fun k hk => le_of_not_lt fun hnk => ?_
  exact hgt (hk.trans (Ideal.pow_le_pow hnk))
case succ
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ Nat.succ n
this : ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ Nat.find (_ : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n) ≤ n
case succ
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ Nat.succ n
this : ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ ramificationIdx f p P ≤ n
rw [ramificationIdx_eq_find ⟨n, this⟩]
no goals
case succ
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ Nat.succ n
this : ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ Nat.find (_ : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n) ≤ n
exact Nat.find_min' ⟨n, this⟩ this
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ Nat.succ n
k : ℕ
hk : map f p ≤ P ^ k
hnk : n < k
⊢ False
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ Nat.succ n
⊢ ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
refine fun k hk => le_of_not_lt fun hnk => ?_
no goals
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ Nat.succ n
k : ℕ
hk : map f p ≤ P ^ k
hnk : n < k
⊢ False
exact hgt (hk.trans (Ideal.pow_le_pow hnk))