awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (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
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Module.Finite R T
Q : Ideal T
inst_8 : P.LiesOver p
inst_9 : Q.LiesOver P
inst_10 : p.IsPrime
this : Q.LiesOver p
⊢ finrank.{v, u_2} (S ⧸ P) (T ⧸ Q) ≤ finrank.{u, u_2} (R ⧸ p) (T ⧸ Q)
have this₁ : IsScalarTower.{u, v, u_2} (R ⧸ p) (S ⧸ P) (T ⧸ Q)
Tactic: have : IsScalarTower (R ⧸ p) (S ⧸ P) (T ⧸ Q) := IsScalarTower.of_algebraMap_eq <| by
    rintro ⟨x⟩
    simp [Submodule.Quotient.quot_mk_eq_mk, IsScalarTower.algebraMap_apply R (S ⧸ P) (T ⧸ Q)]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : IsDedekindDomain R
inst_5 : Free ℤ R
inst_6 : Algebra S R
inst_7 : Module.Finite S R
P : Ideal R
p : Ideal S
inst_8 : P.LiesOver p
hp : p.IsPrime
hp_ne_bot : p ≠ ⊥
⊢ (absNorm : (a : Ideal R) → ℕ) P = HPow.hPow (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) p : ℕ) (p.inertiaDeg P)
have this : p.IsMaximal
Tactic: have : p.IsMaximal := hp.isMaximal hp_ne_bot
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
⊢ p.inertiaDeg I = p.inertiaDeg P * P.inertiaDeg I
have h₁ : p = under R P
Tactic: have h₁ := P.over_def p
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
h₁ : p = under R P
⊢ p.inertiaDeg I = p.inertiaDeg P * P.inertiaDeg I
have h₂ : P = under S I
Tactic: have h₂ := I.over_def P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
⊢ p.inertiaDeg I = p.inertiaDeg P * P.inertiaDeg I
have h₃ : p = under R I
Tactic: have h₃ := (LiesOver.trans I P p).over
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
⊢ p.inertiaDeg I = p.inertiaDeg P * P.inertiaDeg I
have simp : finrank.{u_1, u_3} (R ⧸ p) (T ⧸ I) = finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) * finrank.{u_2, u_3} (S ⧸ P) (T ⧸ I)
Tactic: simp only [inertiaDeg, dif_pos h₁.symm, dif_pos h₂.symm, dif_pos h₃.symm]
-- 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
h : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k
⊢ ¬∃ (n : ℕ), ∀ (a : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* S) f p ≤ P ^ n} a → a ≤ n
have push : ∀ (n : ℕ), ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* S) f p ≤ P ^ n} a ∧ n < a
Tactic: push Not
-- 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
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
⊢ k ≤ n
have refine : ∀ (hnk : n < k), False
Tactic: refine le_of_not_gt fun hnk => ?_
-- 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
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
⊢ p.ramificationIdx P = n
have this : 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))
-- 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
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
⊢ p.ramificationIdx P = n
have rw : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) sorry = n
Tactic: rw [ramificationIdx_eq_find ⟨n, 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
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
have refine : ∀ (h : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) sorry < n), False
Tactic: refine le_antisymm (Nat.find_min' _ this) (le_of_not_gt fun h : Nat.find _ < n => ?_)
-- 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
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
⊢ False
have this' : Q (Nat.find (p := Q) sorry)
Tactic: obtain this' := Nat.find_spec ⟨n, 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
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
⊢ p.ramificationIdx P = n
have let₃ : let Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m;
∀ (this : Q n), 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)
-- 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
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
⊢ p.ramificationIdx P = n
have 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) sorry = 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)
-- 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
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
⊢ p.ramificationIdx P = n
have 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) sorry < n), False
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)
-- 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
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
⊢ p.ramificationIdx P = n
have 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) sorry < n)
  (this' : Q (Nat.find (p := Q) sorry)), False
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)
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ n
⊢ p.ramificationIdx P < n
have zero : ∀ (hgt : ¬map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 0), p.ramificationIdx P < 0
Tactic: rcases n with - | n
Cleared hypotheses: n, hgt
-- 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
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
⊢ p.ramificationIdx P < n
have succ : ∀ (n : ℕ) (hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)), p.ramificationIdx P < n + 1
Tactic: rcases n with - | n
Cleared hypotheses: n, hgt
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
⊢ p.ramificationIdx P < n + 1
have succ : p.ramificationIdx P ≤ n
Tactic: rw [Nat.lt_succ_iff]
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
⊢ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n
have refine : ∀ (k : ℕ) (hk : map (F := R →+* S) f p ≤ P ^ k) (hnk : n < k), False
Tactic: refine fun k hk => le_of_not_gt fun hnk => ?_
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
⊢ p.ramificationIdx P ≤ n
have this : ∀ (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))
-- 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
this : ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n
⊢ p.ramificationIdx P ≤ n
have succ : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) sorry ≤ n
Tactic: rw [ramificationIdx_eq_find ⟨n, 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
n : ℕ
hgt : ¬map (F := R →+* S) f p ≤ P ^ n
⊢ p.ramificationIdx P < n
have zero : ∀ (hgt : ¬map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 0), p.ramificationIdx P < 0
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
Cleared hypotheses: n, hgt
-- 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
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
⊢ p.ramificationIdx P < n
have succ : ∀ (n : ℕ) (hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)), p.ramificationIdx P < n + 1
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
Cleared hypotheses: n, hgt
-- 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
n : ℕ
hn : n ≤ p.ramificationIdx P
⊢ map (F := R →+* S) f p ≤ P ^ n
have contrapose! : ∀ (hn : ¬map (F := R →+* S) f p ≤ P ^ n), p.ramificationIdx P < n
Tactic: contrapose! hn
Cleared hypotheses: 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
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
⊢ 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})
have 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}
Tactic: congr 1
-- 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
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
⊢ 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}
have 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
Tactic: ext n
-- 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
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
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
have 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)
Tactic: simp only [Set.mem_setOf_eq, Ideal.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
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
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)
have 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)
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]
-- 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
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)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have 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)
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]
-- 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
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)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have 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)
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]
-- 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
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)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have 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)
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]
-- 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
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)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have 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)
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]