awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
p : Ideal R
inst_16 : p.IsMaximal
hp0 : p ≠ ⊥
e : (P : Ideal S) → ℕ := p.ramificationIdx
⊢ ∑ P ∈ IsDedekindDomain.primesOverFinset p S, e P * p.inertiaDeg P = finrank K L
have calc_1 : Eq (α := ℕ) (∑ P ∈ Multiset.toFinset (factors (map (F := R →+* S) f p)), e P * p.inertiaDeg P)
  (∑ P ∈ Finset.attach (Multiset.toFinset (factors (map (F := R →+* S) f p))),
    finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S)))
Tactic: calc
    ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * inertiaDeg p P =
        ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset.attach,
          finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ e P) := ?_
    _ = finrank (R ⧸ p)
          (∀ P : (factors (map (algebraMap R S) p)).toFinset, S ⧸ (P : Ideal S) ^ e P) :=
      (finrank_pi_fintype (R ⧸ p)).symm
    _ = finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) := ?_
    _ = finrank K L := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
p : Ideal R
inst_16 : p.IsMaximal
hp0 : p ≠ ⊥
e : (P : Ideal S) → ℕ := p.ramificationIdx
calc_1 :
  Eq (α := ℕ) (∑ P ∈ Multiset.toFinset (factors (map (F := R →+* S) f p)), e P * p.inertiaDeg P)
    (∑ P ∈ Finset.attach (Multiset.toFinset (factors (map (F := R →+* S) f p))),
      finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S)))
⊢ ∑ P ∈ IsDedekindDomain.primesOverFinset p S, e P * p.inertiaDeg P = finrank K L
have calc_2 : finrank.{u, v} (R ⧸ p)
    ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) → S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S)) =
  finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
Tactic: calc
    ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * inertiaDeg p P =
        ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset.attach,
          finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ e P) := ?_
    _ = finrank (R ⧸ p)
          (∀ P : (factors (map (algebraMap R S) p)).toFinset, S ⧸ (P : Ideal S) ^ e P) :=
      (finrank_pi_fintype (R ⧸ p)).symm
    _ = finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) := ?_
    _ = finrank K L := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
p : Ideal R
inst_16 : p.IsMaximal
hp0 : p ≠ ⊥
e : (P : Ideal S) → ℕ := p.ramificationIdx
calc_1 :
  Eq (α := ℕ) (∑ P ∈ Multiset.toFinset (factors (map (F := R →+* S) f p)), e P * p.inertiaDeg P)
    (∑ P ∈ Finset.attach (Multiset.toFinset (factors (map (F := R →+* S) f p))),
      finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S)))
calc_2 :
  finrank.{u, v} (R ⧸ p)
      ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) → S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S)) =
    finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
⊢ ∑ P ∈ IsDedekindDomain.primesOverFinset p S, e P * p.inertiaDeg P = finrank K L
have calc_3 : finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
Tactic: calc
    ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * inertiaDeg p P =
        ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset.attach,
          finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ e P) := ?_
    _ = finrank (R ⧸ p)
          (∀ P : (factors (map (algebraMap R S) p)).toFinset, S ⧸ (P : Ideal S) ^ e P) :=
      (finrank_pi_fintype (R ⧸ p)).symm
    _ = finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) := ?_
    _ = finrank K L := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
p : Ideal R
inst_16 : p.IsMaximal
hp0 : p ≠ ⊥
e : (P : Ideal S) → ℕ := p.ramificationIdx
⊢ Eq (α := ℕ) (∑ P ∈ Multiset.toFinset (factors (map (F := R →+* S) f p)), e P * p.inertiaDeg P)
    (∑ P ∈ Finset.attach (Multiset.toFinset (factors (map (F := R →+* S) f p))),
      finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S)))
have calc_1 : Eq (α := ℕ)
  (∑ x ∈ Finset.attach (Multiset.toFinset (factors (map (F := R →+* S) f p))),
    e (↑x : Ideal S) * p.inertiaDeg (↑x : Ideal S))
  (∑ P ∈ Finset.attach (Multiset.toFinset (factors (map (F := R →+* S) f p))),
    finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S)))
Tactic: rw [← Finset.sum_attach]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
p : Ideal R
inst_16 : p.IsMaximal
hp0 : p ≠ ⊥
e : (P : Ideal S) → ℕ := p.ramificationIdx
⊢ Eq (α := ℕ)
    (∑ x ∈ Finset.attach (Multiset.toFinset (factors (map (F := R →+* S) f p))),
      e (↑x : Ideal S) * p.inertiaDeg (↑x : Ideal S))
    (∑ P ∈ Finset.attach (Multiset.toFinset (factors (map (F := R →+* S) f p))),
      finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S)))
have calc_1 : ∀ (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))),
  Membership.mem (γ := Finset ↥(Multiset.toFinset (factors (map (F := R →+* S) f p))))
      (Finset.attach (Multiset.toFinset (factors (map (F := R →+* S) f p)))) P →
    e (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S) = finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S))
Tactic: refine Finset.sum_congr rfl fun P _ => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
p : Ideal R
inst_16 : p.IsMaximal
hp0 : p ≠ ⊥
e : (P : Ideal S) → ℕ := p.ramificationIdx
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
h :
  Membership.mem (γ := Finset ↥(Multiset.toFinset (factors (map (F := R →+* S) f p))))
    (Finset.attach (Multiset.toFinset (factors (map (F := R →+* S) f p)))) P
⊢ e (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S) = finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S))
have calc_1 : e (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S) = p.ramificationIdx (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S)
Tactic: rw [Factors.finrank_pow_ramificationIdx]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
p : Ideal R
inst_16 : p.IsMaximal
hp0 : p ≠ ⊥
e : (P : Ideal S) → ℕ := p.ramificationIdx
⊢ finrank.{u, v} (R ⧸ p)
      ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) → S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S)) =
    finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
have calc_2 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
Tactic: refine LinearEquiv.finrank_eq (Factors.piQuotientLinearEquiv S p ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
p : Ideal R
inst_16 : p.IsMaximal
hp0 : p ≠ ⊥
e : (P : Ideal S) → ℕ := p.ramificationIdx
⊢ Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have calc_2 : ¬Eq.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
Tactic: rwa [Ne, Ideal.map_eq_bot_iff_le_ker, (RingHom.injective_iff_ker_eq_bot _).mp <|
      algebraMap_injective_of_field_isFractionRing R S K L, le_bot_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
p : Ideal R
inst_16 : p.IsMaximal
hp0 : p ≠ ⊥
e : (P : Ideal S) → ℕ := p.ramificationIdx
calc_2 : ¬Eq.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
⊢ Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have calc_2₁ : ¬p ≤ RingHom.ker (F := R →+* S) f
Tactic: rwa [Ne, Ideal.map_eq_bot_iff_le_ker, (RingHom.injective_iff_ker_eq_bot _).mp <|
      algebraMap_injective_of_field_isFractionRing R S K L, le_bot_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
p : Ideal R
inst_16 : p.IsMaximal
hp0 : p ≠ ⊥
e : (P : Ideal S) → ℕ := p.ramificationIdx
calc_2 : ¬Eq.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
calc_2₁ : ¬p ≤ RingHom.ker (F := R →+* S) f
⊢ Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have calc_2₂ : ¬p ≤ ⊥
Tactic: rwa [Ne, Ideal.map_eq_bot_iff_le_ker, (RingHom.injective_iff_ker_eq_bot _).mp <|
      algebraMap_injective_of_field_isFractionRing R S K L, le_bot_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
p : Ideal R
inst_16 : p.IsMaximal
hp0 : p ≠ ⊥
e : (P : Ideal S) → ℕ := p.ramificationIdx
calc_2 : ¬Eq.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
calc_2₁ : ¬p ≤ RingHom.ker (F := R →+* S) f
calc_2₂ : ¬p ≤ ⊥
⊢ Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have calc_2₃ : ¬p = ⊥
Tactic: rwa [Ne, Ideal.map_eq_bot_iff_le_ker, (RingHom.injective_iff_ker_eq_bot _).mp <|
      algebraMap_injective_of_field_isFractionRing R S K L, le_bot_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : p ≠ ⊥
⊢ p.inertiaDeg P ≤ finrank K L
have hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
Tactic: have hP : P ∈ IsDedekindDomain.primesOverFinset p S :=
    (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : p ≠ ⊥
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
⊢ p.inertiaDeg P ≤ finrank K L
have rw : p.inertiaDeg P ≤
  p.ramificationIdx P * p.inertiaDeg P +
    ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x
Tactic: rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : p ≠ ⊥
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
⊢ p.inertiaDeg P ≤
    p.ramificationIdx P * p.inertiaDeg P +
      ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x
have refine : 0 < p.ramificationIdx P
Tactic: refine le_trans (Nat.le_mul_of_pos_left _ ?_) (Nat.le_add_right _ _)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : p ≠ ⊥
⊢ p.inertiaDeg P ≤ finrank K L
have have : ∀ (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P), p.inertiaDeg P ≤ finrank K L
Tactic: classical
  have hP : P ∈ IsDedekindDomain.primesOverFinset p S :=
    (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
  rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]
  refine le_trans (Nat.le_mul_of_pos_left _ ?_) (Nat.le_add_right _ _)
  exact Nat.pos_iff_ne_zero.mpr <| IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver _ hp0
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : p ≠ ⊥
have have₁ have₂ :
  ∀ (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
    p.inertiaDeg P ≤ finrank K L
⊢ p.inertiaDeg P ≤ finrank K L
have have₃ : ∀ (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
  p.inertiaDeg P ≤
    p.ramificationIdx P * p.inertiaDeg P +
      ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x
Tactic: classical
  have hP : P ∈ IsDedekindDomain.primesOverFinset p S :=
    (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
  rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]
  refine le_trans (Nat.le_mul_of_pos_left _ ?_) (Nat.le_add_right _ _)
  exact Nat.pos_iff_ne_zero.mpr <| IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver _ hp0
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : p ≠ ⊥
have have₁ have₂ :
  ∀ (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
    p.inertiaDeg P ≤ finrank K L
have₃ :
  ∀ (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
    p.inertiaDeg P ≤
      p.ramificationIdx P * p.inertiaDeg P +
        ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x
⊢ p.inertiaDeg P ≤ finrank K L
have have₄ : ∀ (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P), 0 < p.ramificationIdx P
Tactic: classical
  have hP : P ∈ IsDedekindDomain.primesOverFinset p S :=
    (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
  rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]
  refine le_trans (Nat.le_mul_of_pos_left _ ?_) (Nat.le_add_right _ _)
  exact Nat.pos_iff_ne_zero.mpr <| IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver _ hp0
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
⊢ p.ramificationIdx P ≤ finrank K L
have pos : ∀ (hp0 : p = ⊥), p.ramificationIdx P ≤ finrank K L
Tactic: by_cases hp0 : p = ⊥
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
pos : ∀ (hp0 : p = ⊥), p.ramificationIdx P ≤ finrank K L
⊢ p.ramificationIdx P ≤ finrank K L
have neg : ∀ (hp0 : ¬p = ⊥), p.ramificationIdx P ≤ finrank K L
Tactic: by_cases hp0 : p = ⊥
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : ¬p = ⊥
⊢ p.ramificationIdx P ≤ finrank K L
have hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
Tactic: have hP : P ∈ IsDedekindDomain.primesOverFinset p S :=
    (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : ¬p = ⊥
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
⊢ p.ramificationIdx P ≤ finrank K L
have neg : p.ramificationIdx P ≤
  p.ramificationIdx P * p.inertiaDeg P +
    ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x
Tactic: rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]