awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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)
⊢ 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
have rw : (MulAction.orbit G P).ncard * Nat.card.{u_3} ↥(MulAction.stabilizer G P) = Nat.card G
Tactic: rw [mul_assoc, ← card_stabilizer_eq_card_inertia_mul_finrank,
    ← IsInvariant.orbit_eq_primesOver R S G p P]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
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)
⊢ Nat.card.{u_3} ↥(inertia G P) = p.ramificationIdxIn S
have this : p.IsMaximal
Tactic: have := (show p.IsPrime from P.over_def p ▸ inferInstance).isMaximal hp
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
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
⊢ Nat.card.{u_3} ↥(inertia G P) = p.ramificationIdxIn S
have 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
Tactic: have H := ncard_primesOver_mul_card_inertia_mul_finrank (G := G) p P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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
have 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))
Tactic: refine mul_right_injective₀ (IsDedekindDomain.primesOver_ncard_ne_zero p S) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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))
have refine_1 : finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) ≠ 0
Tactic: refine mul_left_injective₀ (b := Module.finrank (R ⧸ p) (S ⧸ P)) ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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
⊢ 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))
have 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)))
Tactic: refine mul_left_injective₀ (b := Module.finrank (R ⧸ p) (S ⧸ P)) ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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
⊢ 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)
have refine_2 : Nat.card G = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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)
⊢ 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)
have refine_2₁ : Nat.card G = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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))
⊢ 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)
have refine_2₂ : Nat.card G = Set.ncard (α := Ideal S) (p.primesOver S) * (p.ramificationIdxIn S * p.inertiaDeg P)
Tactic: rw [H, mul_assoc, ← inertiaDeg_algebraMap, ← inertiaDegIn_eq_inertiaDeg p P G,
    ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp S G]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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)
⊢ 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)
have refine_2₃ : Nat.card G = Set.ncard (α := Ideal S) (p.primesOver S) * (p.ramificationIdxIn S * p.inertiaDegIn S)
Tactic: rw [H, mul_assoc, ← inertiaDeg_algebraMap, ← inertiaDegIn_eq_inertiaDeg p P G,
    ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp S G]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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)
⊢ 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)
have refine_2₄ : Nat.card G = Nat.card G
Tactic: rw [H, mul_assoc, ← inertiaDeg_algebraMap, ← inertiaDegIn_eq_inertiaDeg p P G,
    ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp S G]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
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)
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = p.ramificationIdxIn S * p.inertiaDegIn S
have this : p.IsMaximal
Tactic: have := (show p.IsPrime from P.over_def p ▸ inferInstance).isMaximal hp
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = p.ramificationIdxIn S * p.inertiaDegIn S
have rw : Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = p.ramificationIdxIn S * p.inertiaDegIn S
have rw₁ : p.ramificationIdxIn S * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = p.ramificationIdxIn S * p.inertiaDegIn S
have rw₂ : p.ramificationIdxIn S * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) = p.ramificationIdxIn S * p.inertiaDeg P
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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
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
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = p.ramificationIdxIn S * p.inertiaDegIn S
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
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₂
⊢ ∃ (σ : 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₂
have this : IsDomain S
Tactic: have : IsDomain S :=
    (IsIntegralClosure.equiv R S L (integralClosure R L)).toMulEquiv.isDomain (integralClosure R L)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
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
⊢ ∃ (σ : 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₂
have this₁ : IsDedekindDomain S
Tactic: have := IsIntegralClosure.isDedekindDomain R K L S
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
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
⊢ ∃ (σ : 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₂
have this₁ : Module.Finite R S
Tactic: have : Module.Finite R S := IsIntegralClosure.finite R K L S
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
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
⊢ ∃ (σ : 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₂
have this₁ : P₁.IsPrime
Tactic: have := hP₁.1
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
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
⊢ ∃ (σ : 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₂
have this₁ : P₁.LiesOver p
Tactic: have := hP₁.2
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
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
⊢ ∃ (σ : 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₂
have this₁ : P₂.IsPrime
Tactic: have := hP₂.1