awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
⊢ h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).LiesOver p

Tactic:
obtain ⟨_, _⟩ := h.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
rw : p.ramificationIdx (h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p)) = p.ramificationIdx P
⊢ p.ramificationIdxIn B = p.ramificationIdx P

Tactic:
rw [ramificationIdxIn, dif_pos h]

Premises used: dif_pos, Ideal.ramificationIdxIn
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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.ramificationIdx (h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p)) = p.ramificationIdx P

Tactic:
ramificationIdx_eq_of_isGaloisGroup p h.choose P G

Premises used: Exists.choose, Ideal.ramificationIdx_eq_of_isGaloisGroup
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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.ramificationIdx (h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p)) = p.ramificationIdx P

Tactic:
exact ramificationIdx_eq_of_isGaloisGroup p h.choose P G

Premises used: Exists.choose, Ideal.ramificationIdx_eq_of_isGaloisGroup
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
⊢ Algebra.IsIntegral A B

Tactic:
have : Algebra.IsIntegral A B := IsGaloisGroup.isInvariant.isIntegral A B G
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
obtain : ∀ (P : (↑(p.primesOver B) : Type u_2)), p.ramificationIdxIn B ≠ 0
⊢ p.ramificationIdxIn B ≠ 0

Tactic:
obtain ⟨P⟩ := (inferInstance : Nonempty (primesOver p B))

Premises used: inferInstance
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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)
rw : p.ramificationIdx (↑P : Ideal B) ≠ 0
⊢ p.ramificationIdxIn B ≠ 0

Tactic:
rw [ramificationIdxIn_eq_ramificationIdx p P G]

Premises used: Ideal.ramificationIdxIn_eq_ramificationIdx
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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.ramificationIdx (↑P : Ideal B) ≠ 0

Tactic:
IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver P.1 hp

Premises used: Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver, Subtype.val
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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.ramificationIdx (↑P : Ideal B) ≠ 0

Tactic:
exact IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver P.1 hp

Premises used: Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver, Subtype.val
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
rw : p.inertiaDeg (h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p)) = p.inertiaDeg P
⊢ p.inertiaDegIn B = p.inertiaDeg P

Tactic:
rw [inertiaDegIn, dif_pos h]

Premises used: dif_pos, Ideal.inertiaDegIn
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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.inertiaDeg (h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p)) = p.inertiaDeg P

Tactic:
inertiaDeg_eq_of_isGaloisGroup p h.choose P G

Premises used: Ideal.inertiaDeg_eq_of_isGaloisGroup, Exists.choose
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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.inertiaDeg (h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p)) = p.inertiaDeg P

Tactic:
exact inertiaDeg_eq_of_isGaloisGroup p h.choose P G

Premises used: Ideal.inertiaDeg_eq_of_isGaloisGroup, Exists.choose
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
obtain : ∀ (P : (↑(p.primesOver B) : Type u_2)), p.inertiaDegIn B ≠ 0
⊢ p.inertiaDegIn B ≠ 0

Tactic:
obtain ⟨P⟩ := (inferInstance : Nonempty (primesOver p B))

Premises used: inferInstance
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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)
rw : p.inertiaDeg (↑P : Ideal B) ≠ 0
⊢ p.inertiaDegIn B ≠ 0

Tactic:
rw [inertiaDegIn_eq_inertiaDeg p P G]

Premises used: Ideal.inertiaDegIn_eq_inertiaDeg
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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.inertiaDeg (↑P : Ideal B) ≠ 0

Tactic:
inertiaDeg_ne_zero _ _

Premises used: Ideal.inertiaDeg_ne_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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.inertiaDeg (↑P : Ideal B) ≠ 0

Tactic:
exact inertiaDeg_ne_zero _ _

Premises used: Ideal.inertiaDeg_ne_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
obtain : ∀ (Q : Ideal C), Q.IsPrime → Q.LiesOver P → p.inertiaDegIn B * P.inertiaDegIn C = p.inertiaDegIn C
⊢ p.inertiaDegIn B * P.inertiaDegIn C = p.inertiaDegIn C

Tactic:
obtain ⟨⟨Q, _, _⟩⟩ := P.nonempty_primesOver (S := C)

Premises used: Ideal.nonempty_primesOver
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
⊢ Q.LiesOver p

Tactic:
have : Q.LiesOver p := LiesOver.trans Q P p
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
rw₃ rw₄ : p.inertiaDeg P * P.inertiaDeg Q = p.inertiaDeg P * P.inertiaDeg Q
⊢ p.inertiaDegIn B * 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]

Premises used: Ideal.inertiaDeg_algebra_tower, Ideal.inertiaDegIn_eq_inertiaDeg
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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) ⊥
obtain :
  ∀ (Q : Ideal C),
    Q.IsPrime → ∀ (hQ : Q.LiesOver P), p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
⊢ p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C

Tactic:
obtain ⟨⟨Q, _, hQ⟩⟩ := P.nonempty_primesOver (S := C)

Premises used: Ideal.nonempty_primesOver
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
⊢ Q.LiesOver p

Tactic:
have : Q.LiesOver p := LiesOver.trans Q P p
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
rw : map (F := B →+* C) (algebraMap B C) P ≤ Q
⊢ p.ramificationIdxIn B * 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 hP hp]

Premises used: Ideal.ramificationIdx_algebra_tower, Ideal.ramificationIdxIn_eq_ramificationIdx
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
⊢ map (F := B →+* C) (algebraMap B C) P ≤ Q

Tactic:
over_def Q P ▸ map_comap_le

Premises used: Eq.rec, Ideal.over_def, Ideal.map_comap_le, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
⊢ map (F := B →+* C) (algebraMap B C) P ≤ Q

Tactic:
exact over_def Q P ▸ map_comap_le
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
obtain :
  ∀ (Q : Ideal C),
    Q.IsPrime → ∀ (hQ : Q.LiesOver P), p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
⊢ p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C

Tactic:
obtain ⟨⟨Q, _, hQ⟩⟩ := P.nonempty_primesOver (S := C)

Premises used: Ideal.nonempty_primesOver
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
⊢ Q.LiesOver p

Tactic:
have : Q.LiesOver p := LiesOver.trans Q P p
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
rw₁ : p.ramificationIdx P * P.ramificationIdxIn C = p.ramificationIdx Q
rw₂ : p.ramificationIdx P * P.ramificationIdx Q = p.ramificationIdx Q
rw₃ rw₄ : p.ramificationIdx P * P.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
⊢ p.ramificationIdxIn B * 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]

Premises used: Ideal.ramificationIdxIn_eq_ramificationIdx, Ideal.ramificationIdx_algebra_tower'