awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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
⊢ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have this₁ : ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ 1 < k
Tactic: push Not at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have neg : ∀ (k : ℕ) (hk : map (F := R →+* S) f p ≤ P ^ k) (h1k : 1 < k), map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
Tactic: obtain ⟨k, hk, h1k⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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
⊢ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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))
⊢ p.ramificationIdx P = 1
have rw : ¬map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
Tactic: rw [← not_ne_iff (b := 1), Ideal.ramificationIdx_ne_one_iff hpP]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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
⊢ False
have 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))
Tactic: replace h₂ := Ideal.map_mono («f» := algebraMap S (Localization.AtPrime P)) h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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))
⊢ False
have h₃ : 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₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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))
⊢ False
have this : 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 _)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
⊢ False
have 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)
Tactic: rw [← Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_eq_bot_iff_of_injective] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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) ⊥
⊢ ramificationIdx.{u, v} (S := S) p (map (F := R →+* S) f p) = 1
have refine : ∀ (h : map (F := R →+* S) f p ≤ HPow.hPow (α := Ideal S) (map (F := R →+* S) f p) (HAdd.hAdd (α := ℕ) 1 1)), False
Tactic: refine ramificationIdx_spec (by simp) fun h ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
have rw : map (F := R →+* S) f p = HPow.hPow (α := Ideal S) (β := ℕ) (map (F := R →+* S) f p) 2
Tactic: rw [pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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)
⊢ False
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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
⊢ False
have this₁ : Eq (α := ℕ) 1 2
Tactic: have := IsMulTorsionFree.pow_right_injective₀ (by rwa [one_eq_top]) h₂ this
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Ideal T
hp : p = comap (F := R →+* S) f P
h : ¬Eq (α := ℕ) (sSup {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n}) 0
⊢ LE.le (α := ℕ) (sSup {n : ℕ | map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n})
    (sSup {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n})
have refine : ∀ (n : ℕ) (hn : Membership.mem (γ := Set ℕ) {n : ℕ | map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n} n),
  Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n} n
Tactic: refine csSup_le_csSup' (h.imp_symm Nat.sSup_of_not_bddAbove) fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Ideal T
hp : p = comap (F := R →+* S) f P
h : ¬Eq (α := ℕ) (sSup {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n}) 0
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n} n
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n} n
have simp_rw : Membership.mem (γ := Set ℕ)
  {n : ℕ |
    LE.le (α := Ideal R) (comap (F := R →+* S) f P)
      (comap (F := R →+* S) f (comap (F := S →+* T) (algebraMap S T) (Q ^ n)))}
  n
Tactic: simp_rw [hp, IsScalarTower.algebraMap_eq R S T, ← map_map, map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Ideal T
hp : p = comap (F := R →+* S) f P
h : ¬Eq (α := ℕ) (sSup {n : ℕ | map (F := R →+* T) (algebraMap R T) p ≤ Q ^ n}) 0
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n} n
⊢ P ≤ comap (F := S →+* T) (algebraMap S T) (Q ^ n)
have rwa : map (F := S →+* T) (algebraMap S T) P ≤ Q ^ n
Tactic: rwa [← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (hypothesis)
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 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
⊢ p.ramificationIdx P = Multiset.count P (normalizedFactors (map (F := R →+* S) f p))
have hPirr : Irreducible P
Tactic: have hPirr := (Ideal.prime_of_isPrime hP0 hP).irreducible
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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 : IsDedekindDomain S
hp0 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ p.ramificationIdx P = Multiset.count P (normalizedFactors (map (F := R →+* S) f p))
have refine_1 : P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) ∣ map (F := R →+* S) f p
Tactic: refine ramificationIdx_spec (Ideal.le_of_dvd ?_) (mt Ideal.dvd_iff_le.mpr ?_)