awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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 R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
hr : ¬r.IsPrime
neg : 0 = q.inertiaDeg' R * r.inertiaDeg' S
neg₁ : 0 = q.inertiaDeg' R * 0
neg₂ neg₃ : Eq (α := ℕ) 0 0
⊢ r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S

Tactic:
rw [inertiaDeg'_of_not_isPrime r R hr, inertiaDeg'_of_not_isPrime r S hr, mul_zero]

Premises used: MulZeroClass.mul_zero, Ideal.inertiaDeg'_of_not_isPrime
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
S : Type u_1
inst : CommRing S
q : Ideal S
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R S
inst_3 : q.IsPrime
⊢ q.ramificationIdx' R =
    (Module.length.{u_1, u_1} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_2, u_1} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
            (under R q)))).toNat

Tactic:
dif_pos _

Premises used: Ideal.ramificationIdx', dif_pos
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
S : Type u_1
inst : CommRing S
q : Ideal S
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R S
hq : ¬q.IsPrime
⊢ q.ramificationIdx' R = 0

Tactic:
dif_neg hq

Premises used: Ideal.ramificationIdx', dif_neg
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.LiesOver p
inst_4 : q.IsPrime
rw :
  (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
            (under R q)))).toNat =
    (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p))).toNat
rw₁ rw₂ :
  (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
            (under R q)))).toNat =
    (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
            (under R q)))).toNat
⊢ q.ramificationIdx' R =
    (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p))).toNat

Tactic:
rw [ramificationIdx'_def, over_def q p]

Premises used: Ideal.ramificationIdx'_def, Ideal.over_def
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
⊢ p.IsPrime

Tactic:
have : p.IsPrime := isPrime_of_liesOver q p
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this : p.IsPrime
⊢ q ≠ ⊥

Tactic:
have hq' : q ≠ ⊥ := ne_bot_of_liesOver_of_ne_bot hp q
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this : p.IsPrime
hq' : q ≠ ⊥
⊢ q.IsMaximal

Tactic:
have : q.IsMaximal := hq.isMaximal hq'
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
⊢ Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥

Tactic:
have hpS : p.map (algebraMap R S) ≠ ⊥ := map_ne_bot_of_ne_bot hp
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
obtain :
  ∀ (I : Ideal S) (hqI : q ⊔ I = ⊤)
    (h :
      map (F := R →+* S) (algebraMap R S) p =
        q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (F := R →+* S) (algebraMap R S) p)) * I),
    p.ramificationIdx q = q.ramificationIdx' R
⊢ p.ramificationIdx q = q.ramificationIdx' R

Tactic:
obtain ⟨I, hqI, h⟩ := Ideal.eq_prime_pow_mul_coprime hpS q

Premises used: Ideal.eq_prime_pow_mul_coprime
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
I : Ideal S
hqI : q ⊔ I = ⊤
h :
  map (F := R →+* S) (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (F := R →+* S) (algebraMap R S) p)) * I
contrapose! : ∀ (hqI : I ≤ q), q ⊔ I ≠ ⊤
⊢ ¬I ≤ q

Tactic:
contrapose! hqI
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
I : Ideal S
h :
  map (F := R →+* S) (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (F := R →+* S) (algebraMap R S) p)) * I
hqI : I ≤ q
rw : q ≠ ⊤
⊢ q ⊔ I ≠ ⊤

Tactic:
rw [sup_of_le_left hqI]

Premises used: sup_of_le_left
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
I : Ideal S
h :
  map (F := R →+* S) (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (F := R →+* S) (algebraMap R S) p)) * I
hqI : I ≤ q
⊢ q ≠ ⊤

Tactic:
hq.ne_top

Premises used: Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
I : Ideal S
h :
  map (F := R →+* S) (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (F := R →+* S) (algebraMap R S) p)) * I
hqI : I ≤ q
⊢ q ≠ ⊤

Tactic:
exact hq.ne_top

Premises used: Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
I : Ideal S
hqI : q ⊔ I = ⊤
h :
  map (F := R →+* S) (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (F := R →+* S) (algebraMap R S) p)) * I
⊢ ¬I ≤ q

Tactic:
replace hqI : ¬ I ≤ q := by
    contrapose! hqI
    rw [sup_of_le_left hqI]
    exact hq.ne_top
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
I : Ideal S
h :
  map (F := R →+* S) (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (F := R →+* S) (algebraMap R S) p)) * I
hqI : ¬I ≤ q
⊢ map (F := R →+* S) (algebraMap R S) p = q ^ p.ramificationIdx q * I

Tactic:
rw [← IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hpS hq hq'] at h

Premises used: Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
I : Ideal S
h :
  map (F := R →+* S) (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (F := R →+* S) (algebraMap R S) p)) * I
hqI : ¬I ≤ q
h₁ : map (F := R →+* S) (algebraMap R S) p = q ^ p.ramificationIdx q * I
⊢ ¬I ≤ q

Tactic:
rw [← IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hpS hq hq'] at h

Premises used: Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
I : Ideal S
h : map (F := R →+* S) (algebraMap R S) p = q ^ p.ramificationIdx q * I
hqI : ¬I ≤ q
⊢ Eq (α := Ideal (Localization.AtPrime q))
    (map (R := S) (F := S →+* Localization.AtPrime q) (algebraMap S (Localization.AtPrime q))
      (map (F := R →+* S) (algebraMap R S) p))
    (map (F := S →+* Localization.AtPrime q) (algebraMap S (Localization.AtPrime q)) (q ^ p.ramificationIdx q * I))

Tactic:
apply_fun (map (algebraMap S (Localization.AtPrime q))) at h

Premises used: Algebra.algebraMap, Localization.AtPrime, Ideal.map
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
I : Ideal S
hqI : ¬I ≤ q
h :
  Eq (α := Ideal (Localization.AtPrime q))
    (map (R := S) (F := S →+* Localization.AtPrime q) (algebraMap S (Localization.AtPrime q))
      (map (F := R →+* S) (algebraMap R S) p))
    (map (F := S →+* Localization.AtPrime q) (algebraMap S (Localization.AtPrime q)) (q ^ p.ramificationIdx q * I))
⊢ map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p =
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (IsLocalRing.maximalIdeal (Localization (M := S) q.primeCompl))
      (p.ramificationIdx q)

Tactic:
rw [map_map, ← IsScalarTower.algebraMap_eq, Ideal.map_mul, Ideal.map_pow,
    map_eq_top_of_not_le (Localization.AtPrime q) hqI, mul_top, AtPrime.map_eq_maximalIdeal] at h

Premises used: Ideal.map_mul, Localization.AtPrime, Ideal.map_map, IsScalarTower.algebraMap_eq, Ideal.mul_top, Ideal.map_pow, Localization.AtPrime.map_eq_maximalIdeal, IsLocalization.AtPrime.map_eq_top_of_not_le
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
I : Ideal S
hqI : ¬I ≤ q
h :
  map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p =
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (IsLocalRing.maximalIdeal (Localization (M := S) q.primeCompl))
      (p.ramificationIdx q)
⊢ IsDiscreteValuationRing.{u_2} (Localization.AtPrime q)

Tactic:
have hSq := isDiscreteValuationRing_of_dedekind_domain S hq' (Localization.AtPrime q)
-- Module: Mathlib.RingTheory.RamificationInertia.Ramification
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
I : Ideal S
hqI : ¬I ≤ q
h :
  map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p =
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (IsLocalRing.maximalIdeal (Localization (M := S) q.primeCompl))
      (p.ramificationIdx q)
hSq : IsDiscreteValuationRing.{u_2} (Localization.AtPrime q)
rw :
  p.ramificationIdx q =
    (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p))).toNat
rw₁ :
  p.ramificationIdx q =
    (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (Localization.AtPrime q ⧸
          HPow.hPow (α := Ideal (Localization.AtPrime q))
            (IsLocalRing.maximalIdeal (Localization (M := S) q.primeCompl)) (p.ramificationIdx q))).toNat
rw₂ : p.ramificationIdx q = ENat.toNat (↑(p.ramificationIdx q) : ℕ∞)
rw₃ rw₄ : p.ramificationIdx q = p.ramificationIdx q
⊢ p.ramificationIdx q = q.ramificationIdx' R

Tactic:
rw [ramificationIdx'_eq p q, h, hSq.length_quotient_pow_maximalIdeal, ENat.toNat_coe]

Premises used: Ideal.ramificationIdx'_eq, ENat.toNat_coe, IsDiscreteValuationRing.length_quotient_pow_maximalIdeal
-- Module: Mathlib.RingTheory.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 R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : q.IsPrime
inst_8 : r.IsPrime
inst_9 : r.LiesOver q
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime q) (Localization.AtPrime r)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra q r
inst_12 : Module.Flat.{u_2, u_3} (Localization.AtPrime q) (Localization.AtPrime r)
⊢ q.LiesOver (under R r)

Tactic:
have : q.LiesOver (r.under R) := LiesOver.tower_bot r q (r.under R)
-- Module: Mathlib.RingTheory.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 R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : q.IsPrime
inst_8 : r.IsPrime
inst_9 : r.LiesOver q
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime q) (Localization.AtPrime r)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra q r
inst_12 : Module.Flat.{u_2, u_3} (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
rw :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime r))
    (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r)) (under R r))
    (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r))
      (@RingHom.comp.{u_1, u_2, u_3} _ (Localization.AtPrime q) _ _ Semiring.toNonAssocSemiring _
        (algebraMap (Localization.AtPrime q) (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime q)))
      (under R r))
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime r))
    (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r)) (under R r))
    (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r)) (under R r))
⊢ Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime r))
    (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r)) (under R r))
    (map (R := Localization.AtPrime q) (F := RingHom.{u_2, u_3} (Localization.AtPrime q) (Localization.AtPrime r))
      (algebraMap (Localization.AtPrime q) (Localization.AtPrime r))
      (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) (under R r)))

Tactic:
rw [map_map, ← IsScalarTower.algebraMap_eq]

Premises used: Ideal.map_map, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.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 R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
inst_8 : Module.Flat S T
pos : ∀ (hr : r.IsPrime), r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
neg : ∀ (hr : ¬r.IsPrime), r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S

Tactic:
by_cases hr : r.IsPrime

Premises used: Ideal.IsPrime
-- Module: Mathlib.RingTheory.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 R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
inst_8 : Module.Flat S T
hr : r.IsPrime
⊢ q.IsPrime

Tactic:
have : q.IsPrime := isPrime_of_liesOver r q
-- Module: Mathlib.RingTheory.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 R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
inst_8 : Module.Flat S T
hr : r.IsPrime
this_1 : q.IsPrime
this : Algebra.{u_2, u_3} (Localization.AtPrime q) (Localization.AtPrime r) :=
  Localization.AtPrime.algebraOfLiesOver q r
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S

Tactic:
apply ramificationIdx'_tower'

Premises used: Ideal.ramificationIdx'_tower'
-- Module: Mathlib.RingTheory.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 R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
inst_8 : Module.Flat S T
hr : ¬r.IsPrime
neg : 0 = q.ramificationIdx' R * r.ramificationIdx' S
neg₁ : 0 = q.ramificationIdx' R * 0
neg₂ neg₃ : Eq (α := ℕ) 0 0
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S

Tactic:
rw [ramificationIdx'_of_not_isPrime r R hr, ramificationIdx'_of_not_isPrime r S hr, mul_zero]

Premises used: MulZeroClass.mul_zero, Ideal.ramificationIdx'_of_not_isPrime
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
a b : R[X]
hf : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} a
hg : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} b
i : ℕ
rw : ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, a.coeff x.1 * b.coeff x.2 ∈ I ^ i
⊢ (a * b).coeff i ∈ I ^ i

Tactic:
rw [coeff_mul]

Premises used: Polynomial.coeff_mul
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
a_1 b : R[X]
hf : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} a_1
hg : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} b
i : ℕ
a : ∀ c ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, a_1.coeff c.1 * b.coeff c.2 ∈ I ^ i
⊢ ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, a_1.coeff x.1 * b.coeff x.2 ∈ I ^ i

Tactic:
apply Ideal.sum_mem

Premises used: Ideal.sum_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
a_1 b : R[X]
hf : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} a_1
hg : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} b
i j k : ℕ
e : (j, k) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
a : a_1.coeff (j, k).1 * b.coeff (j, k).2 ∈ I ^ (j, k).1 * I ^ (j, k).2
⊢ a_1.coeff (j, k).1 * b.coeff (j, k).2 ∈ I ^ i

Tactic:
rw [← Finset.mem_antidiagonal.mp e, pow_add]

Premises used: pow_add, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
a b : R[X]
hf : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} a
hg : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} b
i j k : ℕ
e : (j, k) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
⊢ a.coeff (j, k).1 * b.coeff (j, k).2 ∈ I ^ (j, k).1 * I ^ (j, k).2

Tactic:
Ideal.mul_mem_mul (hf j) (hg k)

Premises used: Set.Mem, Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
a b : R[X]
hf : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} a
hg : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} b
i j k : ℕ
e : (j, k) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
⊢ a.coeff (j, k).1 * b.coeff (j, k).2 ∈ I ^ (j, k).1 * I ^ (j, k).2

Tactic:
exact Ideal.mul_mem_mul (hf j) (hg k)

Premises used: Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
i : ℕ
rw : (if i = 0 then 1 else 0) ∈ I ^ i
⊢ coeff 1 i ∈ I ^ i

Tactic:
rw [coeff_one]

Premises used: Polynomial.coeff_one
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
i : ℕ
pos : ∀ (h : i = 0), 1 ∈ I ^ i
neg : ∀ (h : ¬i = 0), 0 ∈ I ^ i
⊢ (if i = 0 then 1 else 0) ∈ I ^ i

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
i : ℕ
h : i = 0
pos : 1 ∈ HPow.hPow (β := ℕ) I 0
⊢ 1 ∈ I ^ i

Tactic:
subst h