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
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m
k : ℕ
hk : map (F := R →+* S) f p ≤ P ^ k
refine : ∀ (hnk : n < k), False
⊢ k ≤ n

Tactic:
refine le_of_not_gt fun hnk => ?_

Premises used: le_of_not_gt
-- 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
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m
k : ℕ
hk : map (F := R →+* S) f p ≤ P ^ k
hnk : n < k
⊢ False

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

Premises used: Ideal.pow_le_pow_right, 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
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m
k : ℕ
hk : map (F := R →+* S) f p ≤ P ^ k
hnk : n < k
⊢ False

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

Premises used: Ideal.pow_le_pow_right, 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
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m
⊢ Q n

Tactic:
have : Q n := by
    intro k hk
    refine le_of_not_gt fun hnk => ?_
    exact hgt (hk.trans (Ideal.pow_le_pow_right hnk))
-- 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
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m
this : Q n
rw : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) ⋯ = n
⊢ p.ramificationIdx P = n

Tactic:
rw [ramificationIdx_eq_find ⟨n, this⟩]

Premises used: Ideal.ramificationIdx_eq_find, Exists.intro
-- 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
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m
this : Q n
⊢ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) ⋯ = n

Tactic:
le_antisymm (Nat.find_min' _ this) (le_of_not_gt fun h : Nat.find _ < n => ?_)

Premises used: le_of_not_gt, le_antisymm, Nat.find_min'
-- 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
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m
this : Q n
refine : ∀ (h : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) ⋯ < n), False
⊢ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) ⋯ = n

Tactic:
refine le_antisymm (Nat.find_min' _ this) (le_of_not_gt fun h : Nat.find _ < n => ?_)

Premises used: le_of_not_gt, le_antisymm, Nat.find_min'
-- 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
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m
this : Q n
h : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) ⋯ < n
⊢ Q (Nat.find (p := Q) ⋯)

Tactic:
obtain this' := Nat.find_spec ⟨n, this⟩

Premises used: Exists.intro, Nat.find_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
P : Ideal S
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m
this : Q n
h : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) ⋯ < n
this' : Q (Nat.find (p := Q) ⋯)
⊢ False

Tactic:
h.not_ge (this' _ hle)

Premises used: LT.lt.not_ge
-- 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
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m
this : Q n
h : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) ⋯ < n
this' : Q (Nat.find (p := Q) ⋯)
⊢ False

Tactic:
exact h.not_ge (this' _ hle)

Premises used: LT.lt.not_ge
-- 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
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
let let₁ let₂ : p.ramificationIdx P = n
let₃ :
  let Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m;
  ∀ (this : Q n), p.ramificationIdx P = n
let₄ :
  let Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m;
  ∀ (this : Q n), Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) ⋯ = n
let₅ :
  let Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m;
  ∀ (this : Q n) (h : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) ⋯ < n), False
let₆ :
  let Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m;
  ∀ (this : Q n) (h : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) ⋯ < n)
    (this' : Q (Nat.find (p := Q) ⋯)), False
⊢ p.ramificationIdx P = n

Tactic:
classical
  let Q : ℕ → Prop := fun m => ∀ k : ℕ, map f p ≤ P ^ k → k ≤ m
  have : Q n := by
    intro k hk
    refine le_of_not_gt fun hnk => ?_
    exact hgt (hk.trans (Ideal.pow_le_pow_right hnk))
  rw [ramificationIdx_eq_find ⟨n, this⟩]
  refine le_antisymm (Nat.find_min' _ this) (le_of_not_gt fun h : Nat.find _ < n => ?_)
  obtain this' := Nat.find_spec ⟨n, this⟩
  exact h.not_ge (this' _ hle)
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ n
zero : ∀ (hgt : ¬map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 0), p.ramificationIdx P < 0
succ : ∀ (n : ℕ) (hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)), p.ramificationIdx P < n + 1
⊢ p.ramificationIdx P < n

Tactic:
rcases n with - | n
-- 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
hgt : ¬map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 0
⊢ p.ramificationIdx P < 0

Tactic:
simp at hgt
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
succ : p.ramificationIdx P ≤ n
⊢ p.ramificationIdx P < n + 1

Tactic:
rw [Nat.lt_succ_iff]

Premises used: Nat.lt_succ_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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
⊢ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n

Tactic:
fun k hk => le_of_not_gt fun hnk => ?_

Premises used: le_of_not_gt
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
refine : ∀ (k : ℕ) (hk : map (F := R →+* S) f p ≤ P ^ k) (hnk : n < k), False
⊢ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n

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

Premises used: le_of_not_gt
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
k : ℕ
hk : map (F := R →+* S) f p ≤ P ^ k
hnk : n < k
⊢ False

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

Premises used: Ideal.pow_le_pow_right, 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
k : ℕ
hk : map (F := R →+* S) f p ≤ P ^ k
hnk : n < k
⊢ False

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

Premises used: Ideal.pow_le_pow_right, 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
⊢ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n

Tactic:
have : ∀ k, map f p ≤ P ^ k → k ≤ n := by
      refine fun k hk => le_of_not_gt fun hnk => ?_
      exact hgt (hk.trans (Ideal.pow_le_pow_right hnk))
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
this : ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n
succ : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) ⋯ ≤ n
⊢ p.ramificationIdx P ≤ n

Tactic:
rw [ramificationIdx_eq_find ⟨n, this⟩]

Premises used: Ideal.ramificationIdx_eq_find, Exists.intro
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
this : ∀ (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) ⋯ ≤ n

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

Premises used: Nat.find_min', Exists.intro
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
this : ∀ (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) ⋯ ≤ n

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

Premises used: Nat.find_min', Exists.intro
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ n
zero : ∀ (hgt : ¬map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 0), p.ramificationIdx P < 0
succ succ₁ : ∀ (n : ℕ) (hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)), p.ramificationIdx P < n + 1
⊢ p.ramificationIdx P < n

Tactic:
classical
  rcases n with - | n
  · simp at hgt
  · rw [Nat.lt_succ_iff]
    have : ∀ k, map f p ≤ P ^ k → k ≤ n := by
      refine fun k hk => le_of_not_gt fun hnk => ?_
      exact hgt (hk.trans (Ideal.pow_le_pow_right hnk))
    rw [ramificationIdx_eq_find ⟨n, this⟩]
    exact Nat.find_min' ⟨n, this⟩ this

Premises used: Nat.lt_succ_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 S
n : ℕ
hn : ∀ (a : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | map (R := R) (F := R →+* S) f ⊥ ≤ P ^ n} a → a ≤ n
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | map (R := R) (F := R →+* S) f ⊥ ≤ P ^ n} n.succ

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
P : Ideal S
h : ¬map (F := R →+* S) f p ≤ P
⊢ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 0

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
P : Ideal S
h : ¬map (F := R →+* S) f p ≤ P
⊢ ¬map (F := R →+* S) f p ≤ P ^ HAdd.hAdd (α := ℕ) 0 1

Tactic:
simpa using 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
hp : p ≠ ⊥
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ ramificationIdx.{u, v} (S := S) p ⊥ = 0

Tactic:
ramificationIdx_of_not_le <| le_bot_iff.not.mpr <| (map_eq_bot_iff_of_injective hf).not.mpr hp

Premises used: le_bot_iff, Iff.mpr, Iff.not, Ideal.map_eq_bot_iff_of_injective, Ideal.ramificationIdx_of_not_le
-- 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
e : ℕ
he : e ≠ 0
hle : map (F := R →+* S) f p ≤ P ^ e
hnle : ¬map (F := R →+* S) f p ≤ P ^ (e + 1)
rwa rwa₁ rwa₂ rwa₃ : e ≠ 0
⊢ p.ramificationIdx P ≠ 0

Tactic:
rwa [ramificationIdx_spec hle hnle]

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
P : Ideal S
n : ℕ
hn : n ≤ p.ramificationIdx P
contrapose! : ∀ (hn : ¬map (F := R →+* S) f p ≤ P ^ n), p.ramificationIdx P < n
⊢ map (F := R →+* S) f p ≤ P ^ n

Tactic:
contrapose! hn
-- 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
n : ℕ
hn : ¬map (F := R →+* S) f p ≤ P ^ n
⊢ p.ramificationIdx P < n

Tactic:
ramificationIdx_lt hn

Premises used: Ideal.ramificationIdx_lt
-- 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
n : ℕ
hn : ¬map (F := R →+* S) f p ≤ P ^ n
⊢ p.ramificationIdx P < n

Tactic:
exact ramificationIdx_lt hn

Premises used: Ideal.ramificationIdx_lt
-- 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
⊢ map (F := R →+* S) f p ≤ P ^ p.ramificationIdx P

Tactic:
le_pow_of_le_ramificationIdx (le_refl _)

Premises used: le_refl, Ideal.le_pow_of_le_ramificationIdx
-- 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
⊢ p ≤ comap (F := R →+* S) f (P ^ p.ramificationIdx P)

Tactic:
map_le_iff_le_comap.mp le_pow_ramificationIdx

Premises used: Ideal.le_pow_ramificationIdx, Ideal.map_le_iff_le_comap, Iff.mp
-- 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
h : p.ramificationIdx P ≠ 0
⊢ p ≤ comap (F := R →+* S) f P

Tactic:
Ideal.map_le_iff_le_comap.mp <| le_pow_ramificationIdx.trans <| Ideal.pow_le_self <| h

Premises used: Ideal.le_pow_ramificationIdx, Ideal.pow_le_self, Ideal.map_le_iff_le_comap, Iff.mp, 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
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
e_a :
  Eq (α := Set ℕ) {n : ℕ | map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (comap e P) n}
    {n : ℕ | map (F := R →+* S₁) (algebraMap R S₁) p ≤ P ^ n}
⊢ Eq (α := ℕ) (sSup {n : ℕ | map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (comap e P) n})
    (sSup {n : ℕ | map (F := R →+* S₁) (algebraMap R S₁) p ≤ P ^ n})

Tactic:
congr 1
-- 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
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
e_a :
  ∀ (n : ℕ),
    Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (comap e P) n} n ↔
      Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* S₁) (algebraMap R S₁) p ≤ P ^ n} n
⊢ Eq (α := Set ℕ) {n : ℕ | map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (comap e P) n}
    {n : ℕ | map (F := R →+* S₁) (algebraMap R S₁) p ≤ P ^ n}

Tactic:
ext n
-- 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
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
e_a :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (comap e P) n} n ↔
    Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* S₁) (algebraMap R S₁) p ≤ P ^ n} n

Tactic:
simp only [Set.mem_setOf_eq, Ideal.map_le_iff_le_comap]

Premises used: Set.mem_setOf_eq, Ideal.map_le_iff_le_comap
-- 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
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
e_a :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e.toRingEquiv : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₂ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₃ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv.symm.symm P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₄ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₅ :
  p ≤ comap (F := R →+* S) f (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₆ :
  p ≤ comap (F := R →+* S) f (comap e.toRingEquiv.symm.symm (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₇ :
  p ≤ comap (F := R →+* S) f (comap (F := S →+* S₁) (↑e.toRingEquiv.symm.symm : S →+* S₁) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₈ :
  p ≤
      comap (F := R →+* S₁)
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.toRingEquiv.symm.symm : S →+* S₁) f) (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₉ :
  p ≤
      comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.toRingEquiv : S →+* S₁) f)
        (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁₀ :
  p ≤ comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e : S →+* S₁) f) (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁₁ :
  p ≤
      comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(↑e : S →ₐ[R] S₁) : S →+* S₁) f)
        (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁₂ e_a₁₃ : p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n) ↔ p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)

Tactic:
rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁),
    ← map_comap_of_equiv, ← Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _),
    comap_comap, RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom,
    AlgHom.comp_algebraMap]

Premises used: AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap, AlgEquiv.toRingEquiv_toRingHom, Ideal.map_comap_of_equiv, AlgEquiv.toRingEquiv, RingEquiv.symm_symm, Ideal.comap_coe, Ideal.map_pow, RingEquiv.symm, Ideal.comap_comap
-- 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
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
E : Type u_2
inst_5 : EquivLike E S S₁
inst_6 : AlgEquivClass E R S S₁
P : Ideal S
e : E
rw : p.ramificationIdx (comap (F := S₁ ≃+* S) (RingEquiv.symm (↑e : S ≃+* S₁)) P) = p.ramificationIdx P
⊢ ramificationIdx.{u, u_1} (S := S₁) p (map e P) = p.ramificationIdx P

Tactic:
rw [show P.map e = _ from P.map_comap_of_equiv (RingEquivClass.toRingEquiv e : S ≃+* S₁)]

Premises used: RingEquivClass.toRingEquiv, Ideal.map_comap_of_equiv
-- 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
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
E : Type u_2
inst_5 : EquivLike E S S₁
inst_6 : AlgEquivClass E R S S₁
P : Ideal S
e : E
⊢ p.ramificationIdx (comap (F := S₁ ≃+* S) (RingEquiv.symm (↑e : S ≃+* S₁)) P) = p.ramificationIdx P

Tactic:
p.ramificationIdx_comap_eq (AlgEquivClass.toAlgEquiv e).symm P

Premises used: Ideal.ramificationIdx_comap_eq, AlgEquiv.symm, AlgEquivClass.toAlgEquiv, Ideal.comap, RingEquiv.symm
-- 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
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
E : Type u_2
inst_5 : EquivLike E S S₁
inst_6 : AlgEquivClass E R S S₁
P : Ideal S
e : E
⊢ p.ramificationIdx (comap (F := S₁ ≃+* S) (RingEquiv.symm (↑e : S ≃+* S₁)) P) = p.ramificationIdx P

Tactic:
exact p.ramificationIdx_comap_eq (AlgEquivClass.toAlgEquiv e).symm P

Premises used: Ideal.ramificationIdx_comap_eq, AlgEquiv.symm, AlgEquivClass.toAlgEquiv
-- 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), k ≤ n),
    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:
by_cases! H : ∀ n : ℕ, ∃ k, p.map f ≤ P ^ k ∧ n < k