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
p : Ideal R
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ (↑P : Ideal S) ≠ ⊥

Tactic:
exacts [Factors.ne_bot p P, NeZero.ne _]

Premises used: Ideal.Factors.ne_bot, NeZero.ne
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
inst_4 : Module.Finite R S
inst_5 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))

Tactic:
.of_finrank_pos ?_

Premises used: FiniteDimensional.of_finrank_pos
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
inst_4 : Module.Finite R S
inst_5 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
refine : 0 < finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
⊢ FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))

Tactic:
refine .of_finrank_pos ?_
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
inst_4 : Module.Finite R S
inst_5 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
rw : p.ramificationIdx (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S) ≠ 0
⊢ 0 < finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))

Tactic:
rw [pos_iff_ne_zero, Factors.finrank_pow_ramificationIdx]

Premises used: Ideal.Factors.finrank_pow_ramificationIdx, pos_iff_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
p : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
inst_4 : Module.Finite R S
inst_5 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ p.ramificationIdx (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S) ≠ 0

Tactic:
mul_ne_zero (Factors.ramificationIdx_ne_zero p P) (inertiaDeg_pos p P.1).ne'

Premises used: Ideal.inertiaDeg_pos, LT.lt.ne', mul_ne_zero, Subtype.val, Ideal.Factors.ramificationIdx_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
p : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
inst_4 : Module.Finite R S
inst_5 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ p.ramificationIdx (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S) ≠ 0

Tactic:
exact mul_ne_zero (Factors.ramificationIdx_ne_zero p P) (inertiaDeg_pos p P.1).ne'

Premises used: Ideal.inertiaDeg_pos, LT.lt.ne', mul_ne_zero, Subtype.val, Ideal.Factors.ramificationIdx_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
p_1 : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
p : Ideal R
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
rw rw₁ :
  (↑P : Ideal S) ^ Multiset.count (↑P : Ideal S) (factors (map (F := R →+* S) f p)) =
    (↑P : Ideal S) ^ Multiset.count (↑P : Ideal S) (factors (map (F := R →+* S) f p))
⊢ (↑P : Ideal S) ^ Multiset.count (↑P : Ideal S) (factors (map (F := R →+* S) f p)) =
    (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S)

Tactic:
rw [IsDedekindDomain.ramificationIdx_eq_factors_count hp (Factors.isPrime p P)
            (Factors.ne_bot p P)]

Premises used: Ideal.Factors.ne_bot, Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count, Ideal.Factors.isPrime
-- 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
p : Ideal R
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
x : S
⊢ Eq (α :=
    (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
      S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
    (((piQuotientEquiv p hp :
            HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
              ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
                S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))) :
          (a : S ⧸ map f p) →
            (P : ↥(factors (map f p)).toFinset) → S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
        ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) x :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) :
      (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
        S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
    fun (x_1 : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) ↦
    ((Quotient.mk ((↑x_1 : Ideal S) ^ p.ramificationIdx (↑x_1 : Ideal S)) :
          (a : S) → S ⧸ (↑x_1 : Ideal S) ^ p.ramificationIdx (↑x_1 : Ideal S))
        x :
      S ⧸ (↑x_1 : Ideal S) ^ p.ramificationIdx (↑x_1 : Ideal S))

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, rfl
-- 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
p : Ideal R
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
x : R
⊢ Eq (α :=
    (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
      S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
    (((piQuotientEquiv p hp :
            HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
              ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
                S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))) :
          (a : S ⧸ map f p) →
            (P : ↥(factors (map f p)).toFinset) → S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
        ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) : (a : R) → S ⧸ map f p) x :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) :
      (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
        S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
    fun (x_1 : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) ↦
    ((Quotient.mk ((↑x_1 : Ideal S) ^ p.ramificationIdx (↑x_1 : Ideal S)) :
          (a : S) → S ⧸ (↑x_1 : Ideal S) ^ p.ramificationIdx (↑x_1 : Ideal S))
        ((f : (a : R) → S) x) :
      S ⧸ (↑x_1 : Ideal S) ^ p.ramificationIdx (↑x_1 : Ideal S))

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
p : Ideal R
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
m : R ⧸ p
c : R
x_1 : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)
x : S
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ Equiv.toFun
      (RingEquiv.toEquiv
        (piQuotientEquiv p hp :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
            ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
              S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))))
      (HMul.hMul (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) (β :=
        HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) : (a : R) → S ⧸ map f p) c :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) x :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
      P =
    HMul.hMul (α := S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S)) (β :=
      S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
      ((algebraMap (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S)) :
            (a : R ⧸ p) → S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
          ((Quotient.mk p : (a : R) → R ⧸ p) c) :
        S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
      (Equiv.toFun
          (RingEquiv.toEquiv
            (piQuotientEquiv p hp :
              HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
                ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
                  S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))))
          ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) x) P :
        S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))

Tactic:
congr
-- 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 ≠ ⊥
set :
  let e : (P : Ideal S) → ℕ := p.ramificationIdx;
  ∑ P ∈ IsDedekindDomain.primesOverFinset p S, e P * p.inertiaDeg P = finrank K L
⊢ ∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx P * p.inertiaDeg P = finrank K L

Tactic:
set e := ramificationIdx p (S := S)

Premises used: Ideal.ramificationIdx
-- 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
⊢ 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:
?_
-- 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
⊢ ∑ 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)) =
    finrank.{u, v} (R ⧸ p)
      ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) → S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S))

Tactic:
(finrank_pi_fintype (R ⧸ p)).symm

Premises used: Finset.univ, HasQuotient.Quotient, Module.finrank_pi_fintype, Finset.attach, Eq.symm
-- 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)
      ((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:
?_
-- 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:
?_
-- 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
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))
calc_3 : finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
⊢ ∑ P ∈ IsDedekindDomain.primesOverFinset p S, e P * p.inertiaDeg 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 := ?_

Premises used: Multiset.toFinset, Algebra.algebraMap, Ideal.map, UniqueFactorizationMonoid.factors, HasQuotient.Quotient, Module.finrank_pi_fintype, Finset.attach, Eq.symm, Module.finrank
-- 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
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)))
⊢ 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:
rw [← Finset.sum_attach]

Premises used: Finset.sum_attach
-- 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
⊢ 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:
Finset.sum_congr rfl fun P _ => ?_

Premises used: Finset.sum_congr, rfl
-- 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
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))
⊢ 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:
refine Finset.sum_congr rfl fun P _ => ?_

Premises used: Finset.sum_congr, rfl
-- 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
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
calc_1 calc_1₁ :
  e (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S) = p.ramificationIdx (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S)
⊢ e (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S) = finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ e (↑P : Ideal S))

Tactic:
rw [Factors.finrank_pow_ramificationIdx]

Premises used: Ideal.Factors.finrank_pow_ramificationIdx
-- 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)
      ((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:
LinearEquiv.finrank_eq (Factors.piQuotientLinearEquiv S p ?_).symm

Premises used: LinearEquiv.symm, Ideal.Factors.piQuotientLinearEquiv, LinearEquiv.finrank_eq
-- 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
calc_2 : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
⊢ 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:
refine LinearEquiv.finrank_eq (Factors.piQuotientLinearEquiv S p ?_).symm

Premises used: LinearEquiv.symm, Ideal.Factors.piQuotientLinearEquiv, LinearEquiv.finrank_eq
-- 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
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 ≤ ⊥
calc_2₃ calc_2₄ calc_2₅ calc_2₆ : ¬p = ⊥
⊢ Ne.{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]

Premises used: le_bot_iff, Ne, algebraMap_injective_of_field_isFractionRing, RingHom.injective_iff_ker_eq_bot, Iff.mp, Ideal.map_eq_bot_iff_le_ker
-- 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:
finrank_quotient_map p K L

Premises used: Ideal.finrank_quotient_map