awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
p : Ideal R
inst_7 : p.IsMaximal
P : Ideal S
inst_8 : P.LiesOver p
inst_9 : P.IsMaximal
inst_10 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
this_1 : IsGalois.{u_1, u_2} (R ⧸ p) (S ⧸ P)
this_2 : Module.Finite.{u_1, u_2} (R ⧸ p) (S ⧸ P)
this :
  Subgroup.index (G := ↥(MulAction.stabilizer G P)) (Subgroup.subgroupOf (inertia G P) (MulAction.stabilizer G P)) =
    Nat.card.{u_2} Gal((S ⧸ P)/R ⧸ p)
rw : Nat.card.{u_3} ↥(MulAction.stabilizer G P) = Nat.card.{u_3} ↥(inertia G P) * Nat.card.{u_2} Gal((S ⧸ P)/R ⧸ p)
rw₁ :
  Nat.card.{u_3} ↥(MulAction.stabilizer G P) =
    Nat.card.{u_3} ↥(inertia G P) *
      Subgroup.index (G := ↥(MulAction.stabilizer G P)) (Subgroup.subgroupOf (inertia G P) (MulAction.stabilizer G P))
rw₂ :
  Nat.card.{u_3} ↥(Subgroup.subgroupOf (inertia G P) (MulAction.stabilizer G P)) *
      Subgroup.index (G := ↥(MulAction.stabilizer G P)) (Subgroup.subgroupOf (inertia G P) (MulAction.stabilizer G P)) =
    Nat.card.{u_3} ↥(inertia G P) *
      Subgroup.index (G := ↥(MulAction.stabilizer G P)) (Subgroup.subgroupOf (inertia G P) (MulAction.stabilizer G P))
rw₃ rw₄ :
  Nat.card.{u_3} ↥(inertia G P) *
      Subgroup.index (G := ↥(MulAction.stabilizer G P)) (Subgroup.subgroupOf (inertia G P) (MulAction.stabilizer G P)) =
    Nat.card.{u_3} ↥(inertia G P) *
      Subgroup.index (G := ↥(MulAction.stabilizer G P)) (Subgroup.subgroupOf (inertia G P) (MulAction.stabilizer G P))
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P)

Tactic:
rw [← IsGalois.card_aut_eq_finrank, ← this,
    ← ((inertia G P).subgroupOf (MulAction.stabilizer G P)).card_mul_index,
    Nat.card_congr (Subgroup.subgroupOfEquivOfLe (inertia_le_stabilizer (M := G) P)).toEquiv]

Premises used: IsGalois.card_aut_eq_finrank, Subgroup.subgroupOf, Ideal.inertia_le_stabilizer, Ideal.inertia, MulEquiv.toEquiv, Nat.card_congr, Subgroup.subgroupOfEquivOfLe, MulAction.stabilizer, Subgroup.card_mul_index
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
p : Ideal R
inst_7 : p.IsMaximal
P : Ideal S
inst_8 : P.LiesOver p
inst_9 : P.IsMaximal
inst_10 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
rw : (MulAction.orbit G P).ncard * Nat.card.{u_3} ↥(MulAction.stabilizer G P) = Nat.card G
⊢ Set.ncard (α := Ideal S) (p.primesOver S) * Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) =
    Nat.card G

Tactic:
rw [mul_assoc, ← card_stabilizer_eq_card_inertia_mul_finrank,
    ← IsInvariant.orbit_eq_primesOver R S G p P]

Premises used: mul_assoc, Algebra.IsInvariant.orbit_eq_primesOver, Ideal.card_stabilizer_eq_card_inertia_mul_finrank
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
p : Ideal R
inst_7 : p.IsMaximal
P : Ideal S
inst_8 : P.LiesOver p
inst_9 : P.IsMaximal
inst_10 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
⊢ (MulAction.orbit G P).ncard * Nat.card.{u_3} ↥(MulAction.stabilizer G P) = Nat.card G

Tactic:
simpa using Nat.card_congr (MulAction.orbitProdStabilizerEquivGroup G P)

Premises used: Nat.card_congr, MulAction.orbitProdStabilizerEquivGroup
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
inst_7 : IsDedekindDomain R
inst_8 : IsDedekindDomain S
inst_9 : Module.Finite R S
inst_10 : IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
inst_11 : P.LiesOver p
inst_12 : P.IsMaximal
inst_13 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
⊢ p.IsMaximal

Tactic:
have := (show p.IsPrime from P.over_def p ▸ inferInstance).isMaximal hp
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
inst_7 : IsDedekindDomain R
inst_8 : IsDedekindDomain S
inst_9 : Module.Finite R S
inst_10 : IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
inst_11 : P.LiesOver p
inst_12 : P.IsMaximal
inst_13 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
this : p.IsMaximal
⊢ Set.ncard (α := Ideal S) (p.primesOver S) * Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) =
    Nat.card G

Tactic:
have H := ncard_primesOver_mul_card_inertia_mul_finrank (G := G) p P
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
inst_7 : IsDedekindDomain R
inst_8 : IsDedekindDomain S
inst_9 : Module.Finite R S
inst_10 : IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
inst_11 : P.LiesOver p
inst_12 : P.IsMaximal
inst_13 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
this : p.IsMaximal
H :
  Set.ncard (α := Ideal S) (p.primesOver S) * Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) =
    Nat.card G
⊢ Nat.card.{u_3} ↥(inertia G P) = p.ramificationIdxIn S

Tactic:
mul_right_injective₀ (IsDedekindDomain.primesOver_ncard_ne_zero p S) ?_

Premises used: IsDedekindDomain.primesOver_ncard_ne_zero, mul_right_injective₀
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
inst_7 : IsDedekindDomain R
inst_8 : IsDedekindDomain S
inst_9 : Module.Finite R S
inst_10 : IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
inst_11 : P.LiesOver p
inst_12 : P.IsMaximal
inst_13 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
this : p.IsMaximal
H :
  Set.ncard (α := Ideal S) (p.primesOver S) * Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) =
    Nat.card G
refine :
  Eq (α := ℕ) ((fun (x : ℕ) ↦ Set.ncard (α := Ideal S) (p.primesOver S) * x) (Nat.card.{u_3} ↥(inertia G P)))
    ((fun (x : ℕ) ↦ Set.ncard (α := Ideal S) (p.primesOver S) * x) (p.ramificationIdxIn S))
⊢ Nat.card.{u_3} ↥(inertia G P) = p.ramificationIdxIn S

Tactic:
refine mul_right_injective₀ (IsDedekindDomain.primesOver_ncard_ne_zero p S) ?_

Premises used: IsDedekindDomain.primesOver_ncard_ne_zero, mul_right_injective₀
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
inst_7 : IsDedekindDomain R
inst_8 : IsDedekindDomain S
inst_9 : Module.Finite R S
inst_10 : IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
inst_11 : P.LiesOver p
inst_12 : P.IsMaximal
inst_13 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
this : p.IsMaximal
H :
  Set.ncard (α := Ideal S) (p.primesOver S) * Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) =
    Nat.card G
⊢ Eq (α := ℕ) ((fun (x : ℕ) ↦ Set.ncard (α := Ideal S) (p.primesOver S) * x) (Nat.card.{u_3} ↥(inertia G P)))
    ((fun (x : ℕ) ↦ Set.ncard (α := Ideal S) (p.primesOver S) * x) (p.ramificationIdxIn S))

Tactic:
mul_left_injective₀ (b := Module.finrank (R ⧸ p) (S ⧸ P)) ?_ ?_

Premises used: mul_left_injective₀
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
inst_7 : IsDedekindDomain R
inst_8 : IsDedekindDomain S
inst_9 : Module.Finite R S
inst_10 : IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
inst_11 : P.LiesOver p
inst_12 : P.IsMaximal
inst_13 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
this : p.IsMaximal
H :
  Set.ncard (α := Ideal S) (p.primesOver S) * Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) =
    Nat.card G
refine_1 : finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) ≠ 0
refine_2 :
  Eq (α := ℕ)
    ((fun (a : ℕ) ↦ a * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P))
      ((fun (x : ℕ) ↦ Set.ncard (α := Ideal S) (p.primesOver S) * x) (Nat.card.{u_3} ↥(inertia G P))))
    ((fun (a : ℕ) ↦ a * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P))
      ((fun (x : ℕ) ↦ Set.ncard (α := Ideal S) (p.primesOver S) * x) (p.ramificationIdxIn S)))
⊢ Eq (α := ℕ) ((fun (x : ℕ) ↦ Set.ncard (α := Ideal S) (p.primesOver S) * x) (Nat.card.{u_3} ↥(inertia G P)))
    ((fun (x : ℕ) ↦ Set.ncard (α := Ideal S) (p.primesOver S) * x) (p.ramificationIdxIn S))

Tactic:
refine mul_left_injective₀ (b := Module.finrank (R ⧸ p) (S ⧸ P)) ?_ ?_

Premises used: mul_left_injective₀
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
inst_7 : IsDedekindDomain R
inst_8 : IsDedekindDomain S
inst_9 : Module.Finite R S
inst_10 : IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
inst_11 : P.LiesOver p
inst_12 : P.IsMaximal
inst_13 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
this : p.IsMaximal
H :
  Set.ncard (α := Ideal S) (p.primesOver S) * Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) =
    Nat.card G
e : finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) = 0
⊢ False

Tactic:
simp [e, eq_comm, Nat.card_eq_zero, ‹Finite G›.not_infinite] at H

Premises used: eq_comm, Finite.not_infinite, Nat.card_eq_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
inst_7 : IsDedekindDomain R
inst_8 : IsDedekindDomain S
inst_9 : Module.Finite R S
inst_10 : IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
inst_11 : P.LiesOver p
inst_12 : P.IsMaximal
inst_13 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
this : p.IsMaximal
H :
  Set.ncard (α := Ideal S) (p.primesOver S) * Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) =
    Nat.card G
refine_2 :
  Nat.card G = Set.ncard (α := Ideal S) (p.primesOver S) * p.ramificationIdxIn S * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P)
refine_2₁ :
  Nat.card G = Set.ncard (α := Ideal S) (p.primesOver S) * (p.ramificationIdxIn S * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P))
refine_2₂ : Nat.card G = Set.ncard (α := Ideal S) (p.primesOver S) * (p.ramificationIdxIn S * p.inertiaDeg P)
refine_2₃ : Nat.card G = Set.ncard (α := Ideal S) (p.primesOver S) * (p.ramificationIdxIn S * p.inertiaDegIn S)
refine_2₄ refine_2₅ : Nat.card G = Nat.card G
⊢ Set.ncard (α := Ideal S) (p.primesOver S) * Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) =
    Set.ncard (α := Ideal S) (p.primesOver S) * p.ramificationIdxIn S * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P)

Tactic:
rw [H, mul_assoc, ← inertiaDeg_algebraMap, ← inertiaDegIn_eq_inertiaDeg p P G,
    ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp S G]

Premises used: Ideal.inertiaDeg_algebraMap, mul_assoc, Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, Ideal.inertiaDegIn_eq_inertiaDeg
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : IsGaloisGroup G R S
inst_6 : Finite G
inst_7 : IsDedekindDomain R
inst_8 : IsDedekindDomain S
inst_9 : Module.Finite R S
inst_10 : IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
inst_11 : P.LiesOver p
inst_12 : P.IsMaximal
inst_13 : Algebra.IsSeparable.{u_1, u_2} (R ⧸ p) (S ⧸ P)
this : p.IsMaximal
rw : Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) = p.ramificationIdxIn S * p.inertiaDegIn S
rw₁ : p.ramificationIdxIn S * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) = p.ramificationIdxIn S * p.inertiaDegIn S
rw₂ : p.ramificationIdxIn S * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) = p.ramificationIdxIn S * p.inertiaDeg P
rw₃ rw₄ :
  p.ramificationIdxIn S * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) =
    p.ramificationIdxIn S * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P)
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = p.ramificationIdxIn S * p.inertiaDegIn S

Tactic:
rw [card_stabilizer_eq_card_inertia_mul_finrank p P, card_inertia_eq_ramificationIdxIn p hp,
    inertiaDegIn_eq_inertiaDeg p P G, inertiaDeg_algebraMap]

Premises used: Ideal.inertiaDeg_algebraMap, Ideal.card_inertia_eq_ramificationIdxIn, Ideal.card_stabilizer_eq_card_inertia_mul_finrank, Ideal.inertiaDegIn_eq_inertiaDeg
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
⊢ IsDomain S

Tactic:
have : IsDomain S :=
    (IsIntegralClosure.equiv R S L (integralClosure R L)).toMulEquiv.isDomain (integralClosure R L)
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this : IsDomain S
⊢ IsDedekindDomain S

Tactic:
have := IsIntegralClosure.isDedekindDomain R K L S
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this : IsDedekindDomain S
⊢ Module.Finite R S

Tactic:
have : Module.Finite R S := IsIntegralClosure.finite R K L S
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this : Module.Finite R S
⊢ P₁.IsPrime

Tactic:
have := hP₁.1
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this_3 : Module.Finite R S
this : P₁.IsPrime
⊢ P₁.LiesOver p

Tactic:
have := hP₁.2
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this_3 : Module.Finite R S
this_4 : P₁.IsPrime
this : P₁.LiesOver p
⊢ P₂.IsPrime

Tactic:
have := hP₂.1
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this_3 : Module.Finite R S
this_4 : P₁.IsPrime
this_5 : P₁.LiesOver p
this : P₂.IsPrime
⊢ P₂.LiesOver p

Tactic:
have := hP₂.2
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this_3 : Module.Finite R S
this_4 : P₁.IsPrime
this_5 : P₁.LiesOver p
this_6 : P₂.IsPrime
this : P₂.LiesOver p
⊢ IsFractionRing S L

Tactic:
have : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this_3 : Module.Finite R S
this_4 : P₁.IsPrime
this_5 : P₁.LiesOver p
this_6 : P₂.IsPrime
this_7 : P₂.LiesOver p
this_8 : IsFractionRing S L
this : MulSemiringAction.{u_3, u_4} Gal(L/K) S := IsIntegralClosure.MulSemiringAction R K L S
⊢ IsGaloisGroup.{u_3, u_1, u_4} Gal(L/K) R S

Tactic:
have : IsGaloisGroup Gal(L/K) R S := IsGaloisGroup.of_isFractionRing _ _ _ K L
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this_3 : Module.Finite R S
this_4 : P₁.IsPrime
this_5 : P₁.LiesOver p
this_6 : P₂.IsPrime
this_7 : P₂.LiesOver p
this_8 : IsFractionRing S L
this_9 : MulSemiringAction.{u_3, u_4} Gal(L/K) S := IsIntegralClosure.MulSemiringAction R K L S
this : IsGaloisGroup.{u_3, u_1, u_4} Gal(L/K) R S
obtain :
  ∀ (σ : Gal(L/K)) (hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) (σ • P₂)) (this : (σ • P₂).IsPrime)
    (this : (σ • P₂).LiesOver p),
    ∃ (σ_1 : Gal(L/K)),
      comap (F := S ≃ₐ[R] S)
          (((galRestrict R K L S : MulEquiv.{u_3, u_4} Gal(L/K) (S ≃ₐ[R] S)) : (a : Gal(L/K)) → S ≃ₐ[R] S) σ_1 :
            S ≃ₐ[R] S)
          (σ • P₂) =
        P₂
⊢ ∃ (σ : Gal(L/K)),
    comap (F := S ≃ₐ[R] S)
        (((galRestrict R K L S : MulEquiv.{u_3, u_4} Gal(L/K) (S ≃ₐ[R] S)) : (a : Gal(L/K)) → S ≃ₐ[R] S) σ : S ≃ₐ[R] S)
        P₁ =
      P₂

Tactic:
obtain ⟨σ, rfl⟩ := exists_smul_eq_of_isGaloisGroup p P₂ P₁ Gal(L/K)

Premises used: Ideal.exists_smul_eq_of_isGaloisGroup, AlgEquiv, rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₂ : Ideal S
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this_3 : Module.Finite R S
this_4 : P₂.IsPrime
this_5 : P₂.LiesOver p
this_6 : IsFractionRing S L
this_7 : MulSemiringAction.{u_3, u_4} Gal(L/K) S := IsIntegralClosure.MulSemiringAction R K L S
this_8 : IsGaloisGroup.{u_3, u_1, u_4} Gal(L/K) R S
σ : Gal(L/K)
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) (σ • P₂)
this_9 : (σ • P₂).IsPrime
this : (σ • P₂).LiesOver p
⊢ ∃ (σ_1 : Gal(L/K)),
    comap (F := S ≃ₐ[R] S)
        (((galRestrict R K L S : MulEquiv.{u_3, u_4} Gal(L/K) (S ≃ₐ[R] S)) : (a : Gal(L/K)) → S ≃ₐ[R] S) σ_1 :
          S ≃ₐ[R] S)
        (σ • P₂) =
      P₂

Tactic:
⟨σ, comap_map_of_bijective _ ((galRestrict R K L S σ).bijective)⟩

Premises used: Ideal.comap_map_of_bijective, galRestrict, Exists.intro, AlgEquiv.bijective, DFunLike.coe