awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L

Tactic:
exact finrank_quotient_map p K L

Premises used: Ideal.finrank_quotient_map
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 ≠ ⊥
⊢ 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₂⟩
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
rw :
  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

Tactic:
rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]

Premises used: Ideal.sum_ramification_inertia, Finset.add_sum_erase
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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

Tactic:
le_trans (Nat.le_mul_of_pos_left _ ?_) (Nat.le_add_right _ _)

Premises used: Nat.le_add_right, Nat.le_mul_of_pos_left, le_trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
refine : 0 < p.ramificationIdx 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:
refine le_trans (Nat.le_mul_of_pos_left _ ?_) (Nat.le_add_right _ _)

Premises used: Nat.le_add_right, Nat.le_mul_of_pos_left, le_trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
⊢ 0 < p.ramificationIdx P

Tactic:
Nat.pos_iff_ne_zero.mpr <| IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver _ hp0

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
⊢ 0 < p.ramificationIdx P

Tactic:
exact Nat.pos_iff_ne_zero.mpr <| IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver _ hp0

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
have₄ :
  ∀ (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P), 0 < p.ramificationIdx 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

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver, Nat.le_add_right, Ideal.sum_ramification_inertia, Nat.le_mul_of_pos_left, le_trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
neg : ∀ (hp0 : ¬p = ⊥), p.ramificationIdx P ≤ finrank K L
⊢ p.ramificationIdx P ≤ finrank K L

Tactic:
by_cases hp0 : p = ⊥
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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

Tactic:
simp [hp0]
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 = ⊥
⊢ 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₂⟩
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
neg :
  p.ramificationIdx P ≤
    p.ramificationIdx P * p.inertiaDeg P +
      ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x
⊢ p.ramificationIdx P ≤ finrank K L

Tactic:
rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]

Premises used: Ideal.sum_ramification_inertia, Finset.add_sum_erase
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 ≤
    p.ramificationIdx P * p.inertiaDeg P +
      ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x

Tactic:
le_trans (Nat.le_mul_of_pos_right _ ?_) (Nat.le_add_right _ _)

Premises used: Nat.le_mul_of_pos_right, Nat.le_add_right, le_trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
neg : 0 < p.inertiaDeg P
⊢ p.ramificationIdx P ≤
    p.ramificationIdx P * p.inertiaDeg P +
      ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x

Tactic:
refine le_trans (Nat.le_mul_of_pos_right _ ?_) (Nat.le_add_right _ _)

Premises used: Nat.le_mul_of_pos_right, Nat.le_add_right, le_trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
⊢ 0 < p.inertiaDeg P

Tactic:
Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Ideal.inertiaDeg_ne_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
⊢ 0 < p.inertiaDeg P

Tactic:
exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Ideal.inertiaDeg_ne_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
neg neg₁ : ∀ (hp0 : ¬p = ⊥), p.ramificationIdx P ≤ finrank K L
neg₂ :
  ∀ (hp0 : ¬p = ⊥) (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
    p.ramificationIdx P ≤ finrank K L
neg₃ :
  ∀ (hp0 : ¬p = ⊥) (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
    p.ramificationIdx P ≤
      p.ramificationIdx P * p.inertiaDeg P +
        ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x
neg₄ :
  ∀ (hp0 : ¬p = ⊥) (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
    0 < p.inertiaDeg P
⊢ p.ramificationIdx P ≤ finrank K L

Tactic:
classical
  by_cases hp0 : p = ⊥
  · simp [hp0]
  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_right _ ?_) (Nat.le_add_right _ _)
  exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P

Premises used: Iff.mpr, Nat.le_mul_of_pos_right, Nat.pos_iff_ne_zero, Nat.le_add_right, Ideal.inertiaDeg_ne_zero, le_trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hp0 : p ≠ ⊥
rw :
  LE.le (α := ℕ) (∑ x ∈ IsDedekindDomain.primesOverFinset p S, 1)
    (∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx P * p.inertiaDeg P)
⊢ Finset.card (α := Ideal S) (IsDedekindDomain.primesOverFinset p S) ≤ finrank K L

Tactic:
rw [← sum_ramification_inertia S K L hp0, Finset.card_eq_sum_ones]

Premises used: Finset.card_eq_sum_ones, Ideal.sum_ramification_inertia
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hp0 : p ≠ ⊥
⊢ LE.le (α := ℕ) (∑ x ∈ IsDedekindDomain.primesOverFinset p S, 1)
    (∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx P * p.inertiaDeg P)

Tactic:
Finset.sum_le_sum fun P hP ↦ ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hp0 : p ≠ ⊥
refine :
  ∀ (P : Ideal S) (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
    1 ≤ p.ramificationIdx P * p.inertiaDeg P
⊢ LE.le (α := ℕ) (∑ x ∈ IsDedekindDomain.primesOverFinset p S, 1)
    (∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx P * p.inertiaDeg P)

Tactic:
refine Finset.sum_le_sum fun P hP ↦ ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hp0 : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
⊢ P.IsPrime

Tactic:
have : P.IsPrime := ((IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mp hP).1
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hp0 : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
this : P.IsPrime
⊢ P.LiesOver p

Tactic:
have : P.LiesOver p := ((IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mp hP).2
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hp0 : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
this_1 : P.IsPrime
this : P.LiesOver p
⊢ 1 ≤ p.ramificationIdx P * p.inertiaDeg P

Tactic:
Right.one_le_mul ?_ ?_

Premises used: Right.one_le_mul
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hp0 : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
this_1 : P.IsPrime
this : P.LiesOver p
refine_1 : 1 ≤ p.ramificationIdx P
refine_2 : 1 ≤ p.inertiaDeg P
⊢ 1 ≤ p.ramificationIdx P * p.inertiaDeg P

Tactic:
refine Right.one_le_mul ?_ ?_

Premises used: Right.one_le_mul
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hp0 : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
this_1 : P.IsPrime
this : P.LiesOver p
⊢ 1 ≤ p.ramificationIdx P

Tactic:
Nat.pos_iff_ne_zero.mpr <| IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver _ hp0

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver, Nat.lt