-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem ramificationIdx_lt {n : ℕ} (hgt : ¬map f p ≤ P ^ n) : ramificationIdx f p P < n

Proof state:
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 ^ (n + 1)
this : ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ ramificationIdx f p P ≤ n

Tactic:
rw [ramificationIdx_eq_find ⟨n, this⟩]

Result:
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 ^ (n + 1)
this : ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ Nat.find ⋯ ≤ n

Proof state:
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 + 1)
⊢ ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n

Tactic:
refine fun k hk => le_of_not_lt fun hnk => ?_

Result:
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 + 1)
k : ℕ
hk : map f p ≤ P ^ k
hnk : n < k
⊢ False

Proof state:
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 ^ 0
⊢ ramificationIdx f p P < 0

Tactic:
simp at hgt

Result:
no goals

Proof state:
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

Tactic:
rcases n with - | n

Result:
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 ^ 0
⊢ ramificationIdx f p P < 0

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 ^ (n + 1)
⊢ ramificationIdx f p P < n + 1

Proof state:
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 ^ (n + 1)
⊢ ramificationIdx f p P ≤ n

Tactic:
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_right hnk))

Result:
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 ^ (n + 1)
this : ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ ramificationIdx f p P ≤ n

Proof state:
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 + 1)
k : ℕ
hk : map f p ≤ P ^ k
hnk : n < k
⊢ False

Tactic:
exact hgt (hk.trans (Ideal.pow_le_pow_right hnk))

Result:
no goals

Proof state:
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 ^ (n + 1)
⊢ ramificationIdx f p P < n + 1

Tactic:
rw [Nat.lt_succ_iff]

Result:
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 ^ (n + 1)
⊢ ramificationIdx f p P ≤ n

Proof state:
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 ^ (n + 1)
this : ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ Nat.find ⋯ ≤ n

Tactic:
exact Nat.find_min' ⟨n, this⟩ this

Result:
no goals