awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.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 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
have : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have₁ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have₂ : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have₃ have₄ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have have₅ : ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥) (hp0 : P ≠ ⊥),
  p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
Tactic: classical
  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
  have hp0 : P ≠ ⊥ := ne_bot_of_map_ne_bot hg0
  have hq0 : Q ≠ ⊥ := ne_bot_of_le_ne_bot hg0 hg
  letI : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
  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]
  rcases eq_prime_pow_mul_coprime hf0 P with ⟨I, hcp, heq⟩
  have hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I := by rw [← map_sup, hcp, map_top]
  have hntq : ¬ ⊤ ≤ Q := fun ht ↦ IsPrime.ne_top hqm (Iff.mpr (eq_top_iff_one Q) (ht trivial))
  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]
  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
-- Lean 4 proof step from Mathlib.NumberTheory.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 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
have : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have₁ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have₂ : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have₃ have₄ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have₅ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥) (hp0 : P ≠ ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have have₆ : ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥) (hp0 : P ≠ ⊥) (hq0 : Q ≠ ⊥),
  p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
Tactic: classical
  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
  have hp0 : P ≠ ⊥ := ne_bot_of_map_ne_bot hg0
  have hq0 : Q ≠ ⊥ := ne_bot_of_le_ne_bot hg0 hg
  letI : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
  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]
  rcases eq_prime_pow_mul_coprime hf0 P with ⟨I, hcp, heq⟩
  have hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I := by rw [← map_sup, hcp, map_top]
  have hntq : ¬ ⊤ ≤ Q := fun ht ↦ IsPrime.ne_top hqm (Iff.mpr (eq_top_iff_one Q) (ht trivial))
  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]
  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
-- Lean 4 proof step from Mathlib.NumberTheory.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 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
have : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have₁ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have₂ : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have₃ have₄ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have₅ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥) (hp0 : P ≠ ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have₆ have₇ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥) (hp0 : P ≠ ⊥) (hq0 : Q ≠ ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have have₈ : ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥) (hp0 : P ≠ ⊥) (hq0 : Q ≠ ⊥),
  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: classical
  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
  have hp0 : P ≠ ⊥ := ne_bot_of_map_ne_bot hg0
  have hq0 : Q ≠ ⊥ := ne_bot_of_le_ne_bot hg0 hg
  letI : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
  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]
  rcases eq_prime_pow_mul_coprime hf0 P with ⟨I, hcp, heq⟩
  have hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I := by rw [← map_sup, hcp, map_top]
  have hntq : ¬ ⊤ ≤ Q := fun ht ↦ IsPrime.ne_top hqm (Iff.mpr (eq_top_iff_one Q) (ht trivial))
  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]
  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
-- Lean 4 proof step from Mathlib.NumberTheory.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 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
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have 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
Tactic: obtain rfl | hp := eq_or_ne p ⊥
Cleared hypotheses: p, inst_14
-- Lean 4 proof step from Mathlib.NumberTheory.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 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
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have inr : ∀ (hp : p ≠ ⊥), p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
Tactic: obtain rfl | hp := eq_or_ne p ⊥
-- Lean 4 proof step from Mathlib.NumberTheory.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 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.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have this : P.IsPrime
Tactic: have : P.IsPrime := isPrime_of_liesOver Q P
-- Lean 4 proof step from Mathlib.NumberTheory.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 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
have refine : ∀ (r : R) (m : T) (h : r • m = 0), r = 0 ∨ m = 0
Tactic: refine Module.IsTorsionFree.of_smul_eq_zero fun r m h ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.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 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
r : R
m : T
h : r • m = 0
⊢ r = 0 ∨ m = 0
have rwa : ∀ (h : HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((f : (a : R) → S) r : S) m = 0), r = 0 ∨ m = 0
Tactic: rwa [algebra_compatible_smul S, smul_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.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 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
r : R
m : T
h : r • m = 0
rwa : ∀ (h : HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((f : (a : R) → S) r : S) m = 0), r = 0 ∨ m = 0
⊢ r = 0 ∨ m = 0
have rwa₁ : ∀ (h : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S) ∨ m = 0), r = 0 ∨ m = 0
Tactic: rwa [algebra_compatible_smul S, smul_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.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 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
r : R
m : T
h : r • m = 0
rwa : ∀ (h : HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((f : (a : R) → S) r : S) m = 0), r = 0 ∨ m = 0
rwa₁ : ∀ (h : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S) ∨ m = 0), r = 0 ∨ m = 0
⊢ r = 0 ∨ m = 0
have rwa₂ : ∀ (h : r = 0 ∨ m = 0), r = 0 ∨ m = 0
Tactic: rwa [algebra_compatible_smul S, smul_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.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 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
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have this₁ : IsTorsionFree R T
Tactic: have : Module.IsTorsionFree R T := by
    refine Module.IsTorsionFree.of_smul_eq_zero fun r m h ↦ ?_
    rwa [algebra_compatible_smul S, smul_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff] at h
-- Lean 4 proof step from Mathlib.NumberTheory.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 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_1 : P.IsPrime
this : IsTorsionFree R T
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have hP : P ≠ ⊥
Tactic: have hP : P ≠ ⊥ := ne_bot_of_liesOver_of_ne_bot hp _
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (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 S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
⊢ IsUnramifiedAt R p
have this : P.LiesOver p₀
Tactic: have : P.LiesOver p₀ := .trans P p p₀
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (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 S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
⊢ IsUnramifiedAt R p
have hp₀ : p₀ = Ideal.under R P
Tactic: have hp₀ : p₀ = P.under R := Ideal.LiesOver.over
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (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 S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
⊢ IsUnramifiedAt R p
have this₁ : EssFiniteType S T
Tactic: have : EssFiniteType S T := .of_comp R S T
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (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 S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this : EssFiniteType S T
⊢ IsUnramifiedAt R p
have this₁ : IsNoetherianRing T
Tactic: have := Algebra.EssFiniteType.isNoetherianRing S T
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (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 S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this : IsNoetherianRing T
⊢ IsUnramifiedAt R p
have rw : Algebra.IsSeparable.{u_1, u_2} p₀.ResidueField p.ResidueField ∧
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
    (maximalIdeal (Localization.AtPrime p))
Tactic: rw [isUnramifiedAt_iff_map_eq R p₀ p]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (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 S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this : IsNoetherianRing T
⊢ Algebra.IsSeparable.{u_1, u_2} p₀.ResidueField p.ResidueField ∧
    Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
      (maximalIdeal (Localization.AtPrime p))
have h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
Tactic: have ⟨h₁, h₂⟩ := (isUnramifiedAt_iff_map_eq R p₀ P).mp ‹_›
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (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 S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
⊢ Algebra.IsSeparable.{u_1, u_2} p₀.ResidueField p.ResidueField ∧
    Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p)) p₀)
      (maximalIdeal (Localization.AtPrime p))
have h₂ : Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
  (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
  (maximalIdeal (Localization.AtPrime P))
Tactic: have ⟨h₁, h₂⟩ := (isUnramifiedAt_iff_map_eq R p₀ P).mp ‹_›