awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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) ⊥
⊢ p.ramificationIdx q = q.ramificationIdx' R
have 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
Tactic: obtain ⟨I, hqI, h⟩ := Ideal.eq_prime_pow_mul_coprime hpS q
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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
have contrapose! : ∀ (hqI : I ≤ q), q ⊔ I ≠ ⊤
Tactic: contrapose! hqI
Cleared hypotheses: hqI
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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 ⊔ I ≠ ⊤
have rw : q ≠ ⊤
Tactic: rw [sup_of_le_left hqI]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (hypothesis)
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
⊢ p.ramificationIdx q = q.ramificationIdx' R
have hqI₁ : ¬I ≤ q
Tactic: replace hqI : ¬ I ≤ q := by
    contrapose! hqI
    rw [sup_of_le_left hqI]
    exact hq.ne_top
Cleared hypotheses: hqI
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (hypothesis)
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
⊢ p.ramificationIdx q = q.ramificationIdx' R
have h₁ : 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
Cleared hypotheses: h, hqI
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (hypothesis)
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
⊢ p.ramificationIdx q = q.ramificationIdx' R
have 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))
Tactic: apply_fun (map (algebraMap S (Localization.AtPrime q))) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (hypothesis)
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))
⊢ p.ramificationIdx q = q.ramificationIdx' R
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (hypothesis)
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)
⊢ p.ramificationIdx q = q.ramificationIdx' R
have hSq : IsDiscreteValuationRing.{u_2} (Localization.AtPrime q)
Tactic: have hSq := isDiscreteValuationRing_of_dedekind_domain S hq' (Localization.AtPrime q)
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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)
⊢ p.ramificationIdx q = q.ramificationIdx' R
have 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
Tactic: rw [ramificationIdx'_eq p q, h, hSq.length_quotient_pow_maximalIdeal, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx q = q.ramificationIdx' R
have 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
Tactic: rw [ramificationIdx'_eq p q, h, hSq.length_quotient_pow_maximalIdeal, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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
⊢ p.ramificationIdx q = q.ramificationIdx' R
have rw₂ : p.ramificationIdx q = ENat.toNat (↑(p.ramificationIdx q) : ℕ∞)
Tactic: rw [ramificationIdx'_eq p q, h, hSq.length_quotient_pow_maximalIdeal, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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) : ℕ∞)
⊢ p.ramificationIdx q = q.ramificationIdx' R
have rw₃ : p.ramificationIdx q = p.ramificationIdx q
Tactic: rw [ramificationIdx'_eq p q, h, hSq.length_quotient_pow_maximalIdeal, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (hypothesis)
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)
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
have this : q.LiesOver (under R r)
Tactic: have : q.LiesOver (r.under R) := LiesOver.tower_bot r q (r.under R)
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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)
⊢ 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)))
have 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))
Tactic: rw [map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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))
⊢ 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)))
have 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))
Tactic: rw [map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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)
f : HasQuotient.Quotient (Localization.AtPrime r) (B := Ideal (Localization.AtPrime r))
    (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r))
      (under R r)) ≃ₐ[Localization.AtPrime r]
  TensorProduct.{u_2, u_3, u_2} (Localization.AtPrime q) (Localization.AtPrime r)
    (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 r))) :=
  AlgEquiv.trans (quotientEquivAlgOfEq (Localization.AtPrime r) ⋯)
    (Algebra.TensorProduct.quotIdealMapEquivTensorQuot (Localization.AtPrime r)
      (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) (under R r)))
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
have rw : (Module.length.{u_3, u_3} (Localization.AtPrime r)
      (HasQuotient.Quotient (Localization.AtPrime r) (B := Ideal (Localization.AtPrime r))
        (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r))
          (under R r)))).toNat =
  q.ramificationIdx' R * r.ramificationIdx' S
Tactic: rw [ramificationIdx'_def, ramificationIdx'_eq (r.under R), ramificationIdx'_eq q,
    f.toLinearEquiv.length_eq, IsLocalRing.length_baseChange, ENat.toNat_mul,
    ← Localization.AtPrime.map_eq_maximalIdeal, map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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)
f : HasQuotient.Quotient (Localization.AtPrime r) (B := Ideal (Localization.AtPrime r))
    (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r))
      (under R r)) ≃ₐ[Localization.AtPrime r]
  TensorProduct.{u_2, u_3, u_2} (Localization.AtPrime q) (Localization.AtPrime r)
    (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 r))) :=
  AlgEquiv.trans (quotientEquivAlgOfEq (Localization.AtPrime r) ⋯)
    (Algebra.TensorProduct.quotIdealMapEquivTensorQuot (Localization.AtPrime r)
      (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) (under R r)))
rw :
  (Module.length.{u_3, u_3} (Localization.AtPrime r)
        (HasQuotient.Quotient (Localization.AtPrime r) (B := Ideal (Localization.AtPrime r))
          (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r))
            (under R r)))).toNat =
    q.ramificationIdx' R * r.ramificationIdx' S
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
have rw₁ : (Module.length.{u_3, u_3} (Localization.AtPrime r)
      (HasQuotient.Quotient (Localization.AtPrime r) (B := Ideal (Localization.AtPrime r))
        (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r))
          (under R r)))).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 r)))).toNat *
    r.ramificationIdx' S
Tactic: rw [ramificationIdx'_def, ramificationIdx'_eq (r.under R), ramificationIdx'_eq q,
    f.toLinearEquiv.length_eq, IsLocalRing.length_baseChange, ENat.toNat_mul,
    ← Localization.AtPrime.map_eq_maximalIdeal, map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
have pos : ∀ (hr : r.IsPrime), r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
Tactic: by_cases hr : r.IsPrime
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
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
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
have neg : ∀ (hr : ¬r.IsPrime), r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
Tactic: by_cases hr : r.IsPrime
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (hypothesis)
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
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
have this : q.IsPrime
Tactic: have : q.IsPrime := isPrime_of_liesOver r q