awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hfg₁ : Ne.{u_3 + 1} (α := Ideal T) (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p)) ⊥
⊢ map (F := S →+* T) (algebraMap S T) P ≤ Q

Tactic:
rw [IsScalarTower.algebraMap_eq R S T, ← map_map] at hfg

Premises used: Ideal.map_map, IsScalarTower.algebraMap_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p)) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
⊢ Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥

Tactic:
ne_bot_of_map_ne_bot hfg

Premises used: Ideal.ne_bot_of_map_ne_bot
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p)) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
⊢ Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥

Tactic:
exact ne_bot_of_map_ne_bot hfg

Premises used: Ideal.ne_bot_of_map_ne_bot
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
⊢ Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥

Tactic:
have hf0 : map (algebraMap R S) p ≠ ⊥ := by
    rw [IsScalarTower.algebraMap_eq R S T, ← map_map] at hfg
    exact ne_bot_of_map_ne_bot hfg
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
⊢ P ≠ ⊥

Tactic:
have hp0 : P ≠ ⊥ := ne_bot_of_map_ne_bot hg0
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
⊢ Q ≠ ⊥

Tactic:
have hq0 : Q ≠ ⊥ := ne_bot_of_le_ne_bot hg0 hg
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
rw :
  Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q

Tactic:
rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hf0 hpm hp0,
    IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hg0 hqm hq0,
    IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hfg hqm hq0,
    IsScalarTower.algebraMap_eq R S T, ← map_map]

Premises used: Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count, Ideal.map_map, IsScalarTower.algebraMap_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
rcases :
  ∀ (I : Ideal S) (hcp : P ⊔ I = ⊤)
    (heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I),
    Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
      Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
        Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
⊢ Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))

Tactic:
rcases eq_prime_pow_mul_coprime hf0 P with ⟨I, hcp, heq⟩

Premises used: Ideal.eq_prime_pow_mul_coprime
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
rw : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) (P ⊔ I))
rw₁ : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (R := S) (F := S →+* T) (algebraMap S T) ⊤)
rw₂ rw₃ : Eq.{u_3 + 1} (α := Ideal T) ⊤ ⊤
⊢ Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)

Tactic:
rw [← map_sup, hcp, map_top]

Premises used: Ideal.map_sup, Ideal.map_top
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
⊢ Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)

Tactic:
have hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I := by rw [← map_sup, hcp, map_top]
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp_1 : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
hcp : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
⊢ ¬⊤ ≤ Q

Tactic:
have hntq : ¬ ⊤ ≤ Q := fun ht ↦ IsPrime.ne_top hqm (Iff.mpr (eq_top_iff_one Q) (ht trivial))
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp_1 : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
hcp : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
hntq : ¬⊤ ≤ Q
by_contra : ∀ (h : Eq.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) I) 0), False
⊢ Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) I) 0

Tactic:
by_contra h
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp_1 : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
hcp : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
hntq : ¬⊤ ≤ Q
h : Eq.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) I) 0
⊢ Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P)

Tactic:
simp only [h, Submodule.zero_eq_bot, bot_le, sup_of_le_left] at hcp

Premises used: Submodule.zero_eq_bot, sup_of_le_left, bot_le
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp_1 : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
hntq : ¬⊤ ≤ Q
h : Eq.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) I) 0
hcp : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P)
⊢ False

Tactic:
hntq (hcp.trans_le hg)

Premises used: Eq.trans_le
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp_1 : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
hntq : ¬⊤ ≤ Q
h : Eq.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) I) 0
hcp : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P)
⊢ False

Tactic:
exact hntq (hcp.trans_le hg)

Premises used: Eq.trans_le
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp_1 : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
hcp : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
hntq : ¬⊤ ≤ Q
nth_rw :
  Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
        Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P)) +
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) I)) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
⊢ Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))

Tactic:
nth_rw 1 [heq, Ideal.map_mul, Ideal.map_pow, normalizedFactors_mul (pow_ne_zero _ hg0) <| by
    by_contra h
    simp only [h, Submodule.zero_eq_bot, bot_le, sup_of_le_left] at hcp
    exact hntq (hcp.trans_le hg), Multiset.count_add, normalizedFactors_pow, Multiset.count_nsmul]

Premises used: Ideal.map_mul, UniqueFactorizationMonoid.normalizedFactors_mul, pow_ne_zero, Multiset.count_nsmul, Multiset.count_add, UniqueFactorizationMonoid.normalizedFactors_pow, Ideal.map_pow
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp_1 : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
hcp : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
hntq : ¬⊤ ≤ Q
⊢ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
        Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P)) +
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) I)) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))

Tactic:
add_eq_left.mpr <| Decidable.byContradiction fun h ↦ hntq <| hcp.trans_le <|
    sup_le hg <| le_of_dvd <| dvd_of_mem_normalizedFactors <| Multiset.count_ne_zero.mp h

Premises used: Iff.mpr, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Ideal.le_of_dvd, Eq.trans_le, Multiset.count_ne_zero, add_eq_left, Iff.mp, Decidable.byContradiction, sup_le
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := ⋯
I : Ideal S
hcp_1 : P ⊔ I = ⊤
heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I
hcp : Eq.{u_3 + 1} (α := Ideal T) ⊤ (map (F := S →+* T) (algebraMap S T) P ⊔ map (F := S →+* T) (algebraMap S T) I)
hntq : ¬⊤ ≤ Q
⊢ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
        Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P)) +
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) I)) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))

Tactic:
exact add_eq_left.mpr <| Decidable.byContradiction fun h ↦ hntq <| hcp.trans_le <|
    sup_le hg <| le_of_dvd <| dvd_of_mem_normalizedFactors <| Multiset.count_ne_zero.mp h

Premises used: Iff.mpr, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Ideal.le_of_dvd, Eq.trans_le, Multiset.count_ne_zero, add_eq_left, Iff.mp, Decidable.byContradiction, sup_le
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
inst_9 : IsDomain R
inst_10 : IsTorsionFree R S
inst_11 : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst_12 : Q.IsPrime
inst_13 : Q.LiesOver P
inst_14 : P.LiesOver p
inl :
  ∀ [LiesOver.{u_1, u_2} (A := R) P ⊥],
    ramificationIdx.{u_1, u_3} (R := R) ⊥ Q = ramificationIdx.{u_1, u_2} (R := R) ⊥ P * P.ramificationIdx Q
inr : ∀ (hp : p ≠ ⊥), p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q

Tactic:
obtain rfl | hp := eq_or_ne p ⊥

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
inst_9 : IsDomain R
inst_10 : IsTorsionFree R S
inst_11 : IsTorsionFree S T
P : Ideal S
Q : Ideal T
inst_12 : Q.IsPrime
inst_13 : Q.LiesOver P
inst_14 : LiesOver.{u_1, u_2} (A := R) P ⊥
⊢ ramificationIdx.{u_1, u_3} (R := R) ⊥ Q = ramificationIdx.{u_1, u_2} (R := R) ⊥ P * P.ramificationIdx Q

Tactic:
simp
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
inst_9 : IsDomain R
inst_10 : IsTorsionFree R S
inst_11 : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst_12 : Q.IsPrime
inst_13 : Q.LiesOver P
inst_14 : P.LiesOver p
hp : p ≠ ⊥
⊢ P.IsPrime

Tactic:
have : P.IsPrime := isPrime_of_liesOver Q P
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
inst_9 : IsDomain R
inst_10 : IsTorsionFree R S
inst_11 : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst_12 : Q.IsPrime
inst_13 : Q.LiesOver P
inst_14 : P.LiesOver p
hp : p ≠ ⊥
this : P.IsPrime
⊢ IsTorsionFree R T

Tactic:
Module.IsTorsionFree.of_smul_eq_zero fun r m h ↦ ?_

Premises used: Module.IsTorsionFree.of_smul_eq_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
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
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
inst_9 : IsDomain R
inst_10 : IsTorsionFree R S
inst_11 : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst_12 : Q.IsPrime
inst_13 : Q.LiesOver P
inst_14 : P.LiesOver p
hp : p ≠ ⊥
this : P.IsPrime
refine : ∀ (r : R) (m : T) (h : r • m = 0), r = 0 ∨ m = 0
⊢ IsTorsionFree R T

Tactic:
refine Module.IsTorsionFree.of_smul_eq_zero fun r m h ↦ ?_

Premises used: Module.IsTorsionFree.of_smul_eq_zero