awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
inst_2 : CommRing B
inst_3 : IsDedekindDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
p : Ideal A
P : Ideal B
inst_6 : p.IsMaximal
inst_7 : P.IsMaximal
inst_8 : P.LiesOver p
G : Type u_3
inst_9 : Group G
inst_10 : Finite G
inst_11 : MulSemiringAction G B
inst_12 : IsGaloisGroup G A B
C : Type u_4
inst_13 : CommRing C
inst_14 : IsDedekindDomain C
inst_15 : Algebra A C
inst_16 : Algebra B C
inst_17 : Module.Finite A B
inst_18 : Module.Finite A C
inst_19 : Module.Finite B C
inst_20 : IsTorsionFree A C
inst_21 : IsTorsionFree B C
inst_22 : IsScalarTower A B C
GAC : Type u_5
inst_23 : Group GAC
inst_24 : Finite GAC
inst_25 : MulSemiringAction GAC C
inst_26 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_27 : Group GBC
inst_28 : Finite GBC
inst_29 : MulSemiringAction GBC C
inst_30 : IsGaloisGroup GBC B C
hp : p ≠ ⊥
hP : P ≠ ⊥
this_1 : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
this_2 : MulSemiringAction.{u_5, u_4} GAC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GAC A C (FractionRing A) (FractionRing C)
this_3 : MulSemiringAction.{u_6, u_4} GBC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GBC B C (FractionRing B) (FractionRing C)
this : p.ramificationIdxIn C * p.inertiaDegIn C ≠ 0
rw :
  Nat.card G * (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) = Nat.card GAC
rw₁ : Nat.card G * Nat.card GBC = Nat.card GAC
⊢ Set.ncard (α := Ideal B) (p.primesOver B) * (p.ramificationIdxIn B * p.inertiaDegIn B) *
      (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) =
    Nat.card GAC
have rw₂ : finrank.{u_1, u_2} (FractionRing A) (FractionRing B) * Nat.card GBC = Nat.card GAC
Tactic: rw [ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B G,
        ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hP C GBC,
        (IsGaloisGroup.toFractionRing G A B).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GAC A C).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GBC B C).card_eq_finrank, Module.finrank_mul_finrank]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
inst_2 : CommRing B
inst_3 : IsDedekindDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
p : Ideal A
P : Ideal B
inst_6 : p.IsMaximal
inst_7 : P.IsMaximal
inst_8 : P.LiesOver p
G : Type u_3
inst_9 : Group G
inst_10 : Finite G
inst_11 : MulSemiringAction G B
inst_12 : IsGaloisGroup G A B
C : Type u_4
inst_13 : CommRing C
inst_14 : IsDedekindDomain C
inst_15 : Algebra A C
inst_16 : Algebra B C
inst_17 : Module.Finite A B
inst_18 : Module.Finite A C
inst_19 : Module.Finite B C
inst_20 : IsTorsionFree A C
inst_21 : IsTorsionFree B C
inst_22 : IsScalarTower A B C
GAC : Type u_5
inst_23 : Group GAC
inst_24 : Finite GAC
inst_25 : MulSemiringAction GAC C
inst_26 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_27 : Group GBC
inst_28 : Finite GBC
inst_29 : MulSemiringAction GBC C
inst_30 : IsGaloisGroup GBC B C
hp : p ≠ ⊥
hP : P ≠ ⊥
this_1 : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
this_2 : MulSemiringAction.{u_5, u_4} GAC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GAC A C (FractionRing A) (FractionRing C)
this_3 : MulSemiringAction.{u_6, u_4} GBC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GBC B C (FractionRing B) (FractionRing C)
this : p.ramificationIdxIn C * p.inertiaDegIn C ≠ 0
rw :
  Nat.card G * (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) = Nat.card GAC
rw₁ : Nat.card G * Nat.card GBC = Nat.card GAC
rw₂ : finrank.{u_1, u_2} (FractionRing A) (FractionRing B) * Nat.card GBC = Nat.card GAC
⊢ Set.ncard (α := Ideal B) (p.primesOver B) * (p.ramificationIdxIn B * p.inertiaDegIn B) *
      (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) =
    Nat.card GAC
have rw₃ : finrank.{u_1, u_2} (FractionRing A) (FractionRing B) * Nat.card GBC =
  finrank.{u_1, u_4} (FractionRing A) (FractionRing C)
Tactic: rw [ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B G,
        ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hP C GBC,
        (IsGaloisGroup.toFractionRing G A B).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GAC A C).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GBC B C).card_eq_finrank, Module.finrank_mul_finrank]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
inst_2 : CommRing B
inst_3 : IsDedekindDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
p : Ideal A
P : Ideal B
inst_6 : p.IsMaximal
inst_7 : P.IsMaximal
inst_8 : P.LiesOver p
G : Type u_3
inst_9 : Group G
inst_10 : Finite G
inst_11 : MulSemiringAction G B
inst_12 : IsGaloisGroup G A B
C : Type u_4
inst_13 : CommRing C
inst_14 : IsDedekindDomain C
inst_15 : Algebra A C
inst_16 : Algebra B C
inst_17 : Module.Finite A B
inst_18 : Module.Finite A C
inst_19 : Module.Finite B C
inst_20 : IsTorsionFree A C
inst_21 : IsTorsionFree B C
inst_22 : IsScalarTower A B C
GAC : Type u_5
inst_23 : Group GAC
inst_24 : Finite GAC
inst_25 : MulSemiringAction GAC C
inst_26 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_27 : Group GBC
inst_28 : Finite GBC
inst_29 : MulSemiringAction GBC C
inst_30 : IsGaloisGroup GBC B C
hp : p ≠ ⊥
hP : P ≠ ⊥
this_1 : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
this_2 : MulSemiringAction.{u_5, u_4} GAC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GAC A C (FractionRing A) (FractionRing C)
this_3 : MulSemiringAction.{u_6, u_4} GBC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GBC B C (FractionRing B) (FractionRing C)
this : p.ramificationIdxIn C * p.inertiaDegIn C ≠ 0
rw :
  Nat.card G * (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) = Nat.card GAC
rw₁ : Nat.card G * Nat.card GBC = Nat.card GAC
rw₂ : finrank.{u_1, u_2} (FractionRing A) (FractionRing B) * Nat.card GBC = Nat.card GAC
rw₃ :
  finrank.{u_1, u_2} (FractionRing A) (FractionRing B) * Nat.card GBC =
    finrank.{u_1, u_4} (FractionRing A) (FractionRing C)
⊢ Set.ncard (α := Ideal B) (p.primesOver B) * (p.ramificationIdxIn B * p.inertiaDegIn B) *
      (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) =
    Nat.card GAC
have rw₄ : finrank.{u_1, u_2} (FractionRing A) (FractionRing B) * finrank.{u_2, u_4} (FractionRing B) (FractionRing C) =
  finrank.{u_1, u_4} (FractionRing A) (FractionRing C)
Tactic: rw [ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B G,
        ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hP C GBC,
        (IsGaloisGroup.toFractionRing G A B).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GAC A C).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GBC B C).card_eq_finrank, Module.finrank_mul_finrank]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
inst_2 : CommRing B
inst_3 : IsDedekindDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
p : Ideal A
P : Ideal B
inst_6 : p.IsMaximal
inst_7 : P.IsMaximal
inst_8 : P.LiesOver p
G : Type u_3
inst_9 : Group G
inst_10 : Finite G
inst_11 : MulSemiringAction G B
inst_12 : IsGaloisGroup G A B
C : Type u_4
inst_13 : CommRing C
inst_14 : IsDedekindDomain C
inst_15 : Algebra A C
inst_16 : Algebra B C
inst_17 : Module.Finite A B
inst_18 : Module.Finite A C
inst_19 : Module.Finite B C
inst_20 : IsTorsionFree A C
inst_21 : IsTorsionFree B C
inst_22 : IsScalarTower A B C
GAC : Type u_5
inst_23 : Group GAC
inst_24 : Finite GAC
inst_25 : MulSemiringAction GAC C
inst_26 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_27 : Group GBC
inst_28 : Finite GBC
inst_29 : MulSemiringAction GBC C
inst_30 : IsGaloisGroup GBC B C
hp : p ≠ ⊥
hP : P ≠ ⊥
this_1 : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
this_2 : MulSemiringAction.{u_5, u_4} GAC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GAC A C (FractionRing A) (FractionRing C)
this_3 : MulSemiringAction.{u_6, u_4} GBC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GBC B C (FractionRing B) (FractionRing C)
this : p.ramificationIdxIn C * p.inertiaDegIn C ≠ 0
rw :
  Nat.card G * (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) = Nat.card GAC
rw₁ : Nat.card G * Nat.card GBC = Nat.card GAC
rw₂ : finrank.{u_1, u_2} (FractionRing A) (FractionRing B) * Nat.card GBC = Nat.card GAC
rw₃ :
  finrank.{u_1, u_2} (FractionRing A) (FractionRing B) * Nat.card GBC =
    finrank.{u_1, u_4} (FractionRing A) (FractionRing C)
rw₄ :
  finrank.{u_1, u_2} (FractionRing A) (FractionRing B) * finrank.{u_2, u_4} (FractionRing B) (FractionRing C) =
    finrank.{u_1, u_4} (FractionRing A) (FractionRing C)
⊢ Set.ncard (α := Ideal B) (p.primesOver B) * (p.ramificationIdxIn B * p.inertiaDegIn B) *
      (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) =
    Nat.card GAC
have rw₅ : finrank.{u_1, u_4} (FractionRing A) (FractionRing C) = finrank.{u_1, u_4} (FractionRing A) (FractionRing C)
Tactic: rw [ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B G,
        ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hP C GBC,
        (IsGaloisGroup.toFractionRing G A B).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GAC A C).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GBC B C).card_eq_finrank, Module.finrank_mul_finrank]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
inst_2 : CommRing B
inst_3 : IsDedekindDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
p : Ideal A
P : Ideal B
inst_6 : p.IsMaximal
inst_7 : P.IsMaximal
inst_8 : P.LiesOver p
G : Type u_3
inst_9 : Group G
inst_10 : Finite G
inst_11 : MulSemiringAction G B
inst_12 : IsGaloisGroup G A B
C : Type u_4
inst_13 : CommRing C
inst_14 : IsDedekindDomain C
inst_15 : Algebra A C
inst_16 : Algebra B C
inst_17 : Module.Finite A B
inst_18 : Module.Finite A C
inst_19 : Module.Finite B C
inst_20 : IsTorsionFree A C
inst_21 : IsTorsionFree B C
inst_22 : IsScalarTower A B C
GAC : Type u_5
inst_23 : Group GAC
inst_24 : Finite GAC
inst_25 : MulSemiringAction GAC C
inst_26 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_27 : Group GBC
inst_28 : Finite GBC
inst_29 : MulSemiringAction GBC C
inst_30 : IsGaloisGroup GBC B C
hp : p ≠ ⊥
hP : P ≠ ⊥
this_1 : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
this_2 : MulSemiringAction.{u_5, u_4} GAC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GAC A C (FractionRing A) (FractionRing C)
this_3 : MulSemiringAction.{u_6, u_4} GBC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GBC B C (FractionRing B) (FractionRing C)
this : p.ramificationIdxIn C * p.inertiaDegIn C ≠ 0
⊢ Set.ncard (α := Ideal B) (p.primesOver B) * Set.ncard (α := Ideal C) (P.primesOver C) *
      (p.ramificationIdxIn C * p.inertiaDegIn C) =
    Nat.card GAC
have _ : Set.ncard (α := Ideal B) (p.primesOver B) * Set.ncard (α := Ideal C) (P.primesOver C) *
    (p.ramificationIdxIn C * p.inertiaDegIn C) =
  Set.ncard (α := Ideal B) (p.primesOver B) * (p.ramificationIdxIn B * p.inertiaDegIn B) *
    (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C))
Tactic: calc
    _ = ((p.primesOver B).ncard * (p.ramificationIdxIn B * p.inertiaDegIn B)) *
          ((P.primesOver C).ncard * (P.ramificationIdxIn C * P.inertiaDegIn C)) := by
      rw [← inertiaDegIn_mul_inertiaDegIn p P G C GAC GBC,
        ← ramificationIdxIn_mul_ramificationIdxIn' P G C GAC GBC]
      ring
    _ = Nat.card GAC := by
      rw [ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B G,
        ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hP C GBC,
        (IsGaloisGroup.toFractionRing G A B).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GAC A C).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GBC B C).card_eq_finrank, Module.finrank_mul_finrank]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
inst_2 : CommRing B
inst_3 : IsDedekindDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
p : Ideal A
P : Ideal B
inst_6 : p.IsMaximal
inst_7 : P.IsMaximal
inst_8 : P.LiesOver p
G : Type u_3
inst_9 : Group G
inst_10 : Finite G
inst_11 : MulSemiringAction G B
inst_12 : IsGaloisGroup G A B
C : Type u_4
inst_13 : CommRing C
inst_14 : IsDedekindDomain C
inst_15 : Algebra A C
inst_16 : Algebra B C
inst_17 : Module.Finite A B
inst_18 : Module.Finite A C
inst_19 : Module.Finite B C
inst_20 : IsTorsionFree A C
inst_21 : IsTorsionFree B C
inst_22 : IsScalarTower A B C
GAC : Type u_5
inst_23 : Group GAC
inst_24 : Finite GAC
inst_25 : MulSemiringAction GAC C
inst_26 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_27 : Group GBC
inst_28 : Finite GBC
inst_29 : MulSemiringAction GBC C
inst_30 : IsGaloisGroup GBC B C
hp : p ≠ ⊥
hP : P ≠ ⊥
this_1 : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
this_2 : MulSemiringAction.{u_5, u_4} GAC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GAC A C (FractionRing A) (FractionRing C)
this_3 : MulSemiringAction.{u_6, u_4} GBC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GBC B C (FractionRing B) (FractionRing C)
this : p.ramificationIdxIn C * p.inertiaDegIn C ≠ 0
_ :
  Set.ncard (α := Ideal B) (p.primesOver B) * Set.ncard (α := Ideal C) (P.primesOver C) *
      (p.ramificationIdxIn C * p.inertiaDegIn C) =
    Set.ncard (α := Ideal B) (p.primesOver B) * (p.ramificationIdxIn B * p.inertiaDegIn B) *
      (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C))
⊢ Set.ncard (α := Ideal B) (p.primesOver B) * Set.ncard (α := Ideal C) (P.primesOver C) *
      (p.ramificationIdxIn C * p.inertiaDegIn C) =
    Nat.card GAC
have _₁ : Set.ncard (α := Ideal B) (p.primesOver B) * (p.ramificationIdxIn B * p.inertiaDegIn B) *
    (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) =
  Nat.card GAC
Tactic: calc
    _ = ((p.primesOver B).ncard * (p.ramificationIdxIn B * p.inertiaDegIn B)) *
          ((P.primesOver C).ncard * (P.ramificationIdxIn C * P.inertiaDegIn C)) := by
      rw [← inertiaDegIn_mul_inertiaDegIn p P G C GAC GBC,
        ← ramificationIdxIn_mul_ramificationIdxIn' P G C GAC GBC]
      ring
    _ = Nat.card GAC := by
      rw [ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B G,
        ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hP C GBC,
        (IsGaloisGroup.toFractionRing G A B).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GAC A C).card_eq_finrank,
        (IsGaloisGroup.toFractionRing GBC B C).card_eq_finrank, Module.finrank_mul_finrank]
-- 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
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)
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P)
have this : IsGalois.{u_1, u_2} (R ⧸ p) (S ⧸ P)
Tactic: have : IsGalois (R ⧸ p) (S ⧸ P) := { __ := Ideal.Quotient.normal (A := R) 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
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 : IsGalois.{u_1, u_2} (R ⧸ p) (S ⧸ 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)
have this₁ : Module.Finite.{u_1, u_2} (R ⧸ p) (S ⧸ P)
Tactic: have := Ideal.Quotient.finite_of_isInvariant 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
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 : Module.Finite.{u_1, u_2} (R ⧸ p) (S ⧸ 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)
have 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)
Tactic: have : Subgroup.index _ = _ := Nat.card_congr
    (Quotient.stabilizerQuotientInertiaEquiv G p P).toEquiv
-- 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)
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)
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P)
have 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)
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]
-- 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)
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)
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P)
have 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))
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]
-- 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)
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))
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P)
have 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))
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]
-- 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)
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))
⊢ Nat.card.{u_3} ↥(MulAction.stabilizer G P) = Nat.card.{u_3} ↥(inertia G P) * finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P)
have 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))
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]