awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
h : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p
⊢ p.ramificationIdxIn B = p.ramificationIdx P
have left : h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).IsPrime
Tactic: obtain ⟨_, _⟩ := h.choose_spec
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
h : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p
left : h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).IsPrime
⊢ p.ramificationIdxIn B = p.ramificationIdx P
have right : h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).LiesOver p
Tactic: obtain ⟨_, _⟩ := h.choose_spec
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
h : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p
left : h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).IsPrime
right : h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).LiesOver p
⊢ p.ramificationIdxIn B = p.ramificationIdx P
have rw : p.ramificationIdx (h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p)) = p.ramificationIdx P
Tactic: rw [ramificationIdxIn, dif_pos h]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
inst_7 : IsDedekindDomain B
p : Ideal A
inst_8 : p.IsPrime
hp : p ≠ ⊥
inst_9 : IsDomain A
inst_10 : IsTorsionFree A B
⊢ p.ramificationIdxIn B ≠ 0
have this : Algebra.IsIntegral A B
Tactic: have : Algebra.IsIntegral A B := IsGaloisGroup.isInvariant.isIntegral A B G
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
inst_7 : IsDedekindDomain B
p : Ideal A
inst_8 : p.IsPrime
hp : p ≠ ⊥
inst_9 : IsDomain A
inst_10 : IsTorsionFree A B
this : Algebra.IsIntegral A B
⊢ p.ramificationIdxIn B ≠ 0
have obtain : ∀ (P : (↑(p.primesOver B) : Type u_2)), p.ramificationIdxIn B ≠ 0
Tactic: obtain ⟨P⟩ := (inferInstance : Nonempty (primesOver p B))
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
inst_7 : IsDedekindDomain B
p : Ideal A
inst_8 : p.IsPrime
hp : p ≠ ⊥
inst_9 : IsDomain A
inst_10 : IsTorsionFree A B
this : Algebra.IsIntegral A B
P : (↑(p.primesOver B) : Type u_2)
⊢ p.ramificationIdxIn B ≠ 0
have rw : p.ramificationIdx (↑P : Ideal B) ≠ 0
Tactic: rw [ramificationIdxIn_eq_ramificationIdx p P G]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
⊢ p.inertiaDegIn B = p.inertiaDeg P
have h : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p
Tactic: have h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p := ⟨P, hPp, hp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
h : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p
⊢ p.inertiaDegIn B = p.inertiaDeg P
have left : h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).IsPrime
Tactic: obtain ⟨_, _⟩ := h.choose_spec
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
h : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p
left : h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).IsPrime
⊢ p.inertiaDegIn B = p.inertiaDeg P
have right : h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).LiesOver p
Tactic: obtain ⟨_, _⟩ := h.choose_spec
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
h : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p
left : h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).IsPrime
right : h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).LiesOver p
⊢ p.inertiaDegIn B = p.inertiaDeg P
have rw : p.inertiaDeg (h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p)) = p.inertiaDeg P
Tactic: rw [inertiaDegIn, dif_pos h]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
p : Ideal A
inst_7 : p.IsMaximal
inst_8 : IsDomain A
inst_9 : IsTorsionFree A B
inst_10 : Module.Finite A B
inst_11 : Nontrivial B
⊢ p.inertiaDegIn B ≠ 0
have obtain : ∀ (P : (↑(p.primesOver B) : Type u_2)), p.inertiaDegIn B ≠ 0
Tactic: obtain ⟨P⟩ := (inferInstance : Nonempty (primesOver p B))
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
p : Ideal A
inst_7 : p.IsMaximal
inst_8 : IsDomain A
inst_9 : IsTorsionFree A B
inst_10 : Module.Finite A B
inst_11 : Nontrivial B
P : (↑(p.primesOver B) : Type u_2)
⊢ p.inertiaDegIn B ≠ 0
have rw : p.inertiaDeg (↑P : Ideal B) ≠ 0
Tactic: rw [inertiaDegIn_eq_inertiaDeg p P G]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : p.IsMaximal
inst_24 : P.IsMaximal
⊢ p.inertiaDegIn B * P.inertiaDegIn C = p.inertiaDegIn C
have obtain : ∀ (Q : Ideal C), Q.IsPrime → Q.LiesOver P → p.inertiaDegIn B * P.inertiaDegIn C = p.inertiaDegIn C
Tactic: obtain ⟨⟨Q, _, _⟩⟩ := P.nonempty_primesOver (S := C)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : p.IsMaximal
inst_24 : P.IsMaximal
Q : Ideal C
left : Q.IsPrime
right : Q.LiesOver P
⊢ p.inertiaDegIn B * P.inertiaDegIn C = p.inertiaDegIn C
have this : Q.LiesOver p
Tactic: have : Q.LiesOver p := LiesOver.trans Q P p
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : p.IsMaximal
inst_24 : P.IsMaximal
Q : Ideal C
left : Q.IsPrime
right : Q.LiesOver P
this : Q.LiesOver p
⊢ p.inertiaDegIn B * P.inertiaDegIn C = p.inertiaDegIn C
have rw : p.inertiaDeg P * P.inertiaDegIn C = p.inertiaDegIn C
Tactic: rw [inertiaDegIn_eq_inertiaDeg p P G, inertiaDegIn_eq_inertiaDeg p Q GAC,
    inertiaDegIn_eq_inertiaDeg P Q GBC, inertiaDeg_algebra_tower p P Q]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : p.IsMaximal
inst_24 : P.IsMaximal
Q : Ideal C
left : Q.IsPrime
right : Q.LiesOver P
this : Q.LiesOver p
rw : p.inertiaDeg P * P.inertiaDegIn C = p.inertiaDegIn C
⊢ p.inertiaDegIn B * P.inertiaDegIn C = p.inertiaDegIn C
have rw₁ : p.inertiaDeg P * P.inertiaDegIn C = p.inertiaDeg Q
Tactic: rw [inertiaDegIn_eq_inertiaDeg p P G, inertiaDegIn_eq_inertiaDeg p Q GAC,
    inertiaDegIn_eq_inertiaDeg P Q GBC, inertiaDeg_algebra_tower p P Q]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : p.IsMaximal
inst_24 : P.IsMaximal
Q : Ideal C
left : Q.IsPrime
right : Q.LiesOver P
this : Q.LiesOver p
rw : p.inertiaDeg P * P.inertiaDegIn C = p.inertiaDegIn C
rw₁ : p.inertiaDeg P * P.inertiaDegIn C = p.inertiaDeg Q
⊢ p.inertiaDegIn B * P.inertiaDegIn C = p.inertiaDegIn C
have rw₂ : p.inertiaDeg P * P.inertiaDeg Q = p.inertiaDeg Q
Tactic: rw [inertiaDegIn_eq_inertiaDeg p P G, inertiaDegIn_eq_inertiaDeg p Q GAC,
    inertiaDegIn_eq_inertiaDeg P Q GBC, inertiaDeg_algebra_tower p P Q]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : p.IsMaximal
inst_24 : P.IsMaximal
Q : Ideal C
left : Q.IsPrime
right : Q.LiesOver P
this : Q.LiesOver p
rw : p.inertiaDeg P * P.inertiaDegIn C = p.inertiaDegIn C
rw₁ : p.inertiaDeg P * P.inertiaDegIn C = p.inertiaDeg Q
rw₂ : p.inertiaDeg P * P.inertiaDeg Q = p.inertiaDeg Q
⊢ p.inertiaDegIn B * P.inertiaDegIn C = p.inertiaDegIn C
have rw₃ : p.inertiaDeg P * P.inertiaDeg Q = p.inertiaDeg P * P.inertiaDeg Q
Tactic: rw [inertiaDegIn_eq_inertiaDeg p P G, inertiaDegIn_eq_inertiaDeg p Q GAC,
    inertiaDegIn_eq_inertiaDeg P Q GBC, inertiaDeg_algebra_tower p P Q]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp_1 : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : IsDedekindDomain B
inst_24 : IsDedekindDomain C
hp : Ne.{u_4 + 1} (α := Ideal C) (map (F := A →+* C) (algebraMap A C) p) ⊥
hP : Ne.{u_4 + 1} (α := Ideal C) (map (F := B →+* C) (algebraMap B C) P) ⊥
⊢ p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
have obtain : ∀ (Q : Ideal C),
  Q.IsPrime → ∀ (hQ : Q.LiesOver P), p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
Tactic: obtain ⟨⟨Q, _, hQ⟩⟩ := P.nonempty_primesOver (S := C)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp_1 : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : IsDedekindDomain B
inst_24 : IsDedekindDomain C
hp : Ne.{u_4 + 1} (α := Ideal C) (map (F := A →+* C) (algebraMap A C) p) ⊥
hP : Ne.{u_4 + 1} (α := Ideal C) (map (F := B →+* C) (algebraMap B C) P) ⊥
Q : Ideal C
left : Q.IsPrime
hQ : Q.LiesOver P
⊢ p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
have this : Q.LiesOver p
Tactic: have : Q.LiesOver p := LiesOver.trans Q P p
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp_1 : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : IsDedekindDomain B
inst_24 : IsDedekindDomain C
hp : Ne.{u_4 + 1} (α := Ideal C) (map (F := A →+* C) (algebraMap A C) p) ⊥
hP : Ne.{u_4 + 1} (α := Ideal C) (map (F := B →+* C) (algebraMap B C) P) ⊥
Q : Ideal C
left : Q.IsPrime
hQ : Q.LiesOver P
this : Q.LiesOver p
⊢ p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
have rw : map (F := B →+* C) (algebraMap B C) P ≤ Q
Tactic: rw [ramificationIdxIn_eq_ramificationIdx p P G, ramificationIdxIn_eq_ramificationIdx p Q GAC,
    ramificationIdxIn_eq_ramificationIdx P Q GBC, ramificationIdx_algebra_tower hP hp]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : IsDomain A
inst_24 : IsTorsionFree A B
inst_25 : IsDedekindDomain B
inst_26 : IsDedekindDomain C
inst_27 : P.LiesOver p
⊢ p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
have obtain : ∀ (Q : Ideal C),
  Q.IsPrime → ∀ (hQ : Q.LiesOver P), p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
Tactic: obtain ⟨⟨Q, _, hQ⟩⟩ := P.nonempty_primesOver (S := C)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : IsDomain A
inst_24 : IsTorsionFree A B
inst_25 : IsDedekindDomain B
inst_26 : IsDedekindDomain C
inst_27 : P.LiesOver p
Q : Ideal C
left : Q.IsPrime
hQ : Q.LiesOver P
⊢ p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
have this : Q.LiesOver p
Tactic: have : Q.LiesOver p := LiesOver.trans Q P p
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : IsDomain A
inst_24 : IsTorsionFree A B
inst_25 : IsDedekindDomain B
inst_26 : IsDedekindDomain C
inst_27 : P.LiesOver p
Q : Ideal C
left : Q.IsPrime
hQ : Q.LiesOver P
this : Q.LiesOver p
⊢ p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
have rw : p.ramificationIdx P * P.ramificationIdxIn C = p.ramificationIdxIn C
Tactic: rw [ramificationIdxIn_eq_ramificationIdx p P G, ramificationIdxIn_eq_ramificationIdx p Q GAC,
    ramificationIdxIn_eq_ramificationIdx P Q GBC, ramificationIdx_algebra_tower' p P Q]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : IsDomain A
inst_24 : IsTorsionFree A B
inst_25 : IsDedekindDomain B
inst_26 : IsDedekindDomain C
inst_27 : P.LiesOver p
Q : Ideal C
left : Q.IsPrime
hQ : Q.LiesOver P
this : Q.LiesOver p
rw : p.ramificationIdx P * P.ramificationIdxIn C = p.ramificationIdxIn C
⊢ p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
have rw₁ : p.ramificationIdx P * P.ramificationIdxIn C = p.ramificationIdx Q
Tactic: rw [ramificationIdxIn_eq_ramificationIdx p P G, ramificationIdxIn_eq_ramificationIdx p Q GAC,
    ramificationIdxIn_eq_ramificationIdx P Q GBC, ramificationIdx_algebra_tower' p P Q]