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 : 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
⊢ p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
have rw₂ : p.ramificationIdx P * P.ramificationIdx Q = p.ramificationIdx Q
Tactic: rw [ramificationIdxIn_eq_ramificationIdx p P G, ramificationIdxIn_eq_ramificationIdx p Q GAC,
    ramificationIdxIn_eq_ramificationIdx P Q GBC, ramificationIdx_algebra_tower' p P Q]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
C : Type u_4
inst_7 : CommRing C
inst_8 : IsDomain C
inst_9 : Algebra A C
inst_10 : Algebra B C
inst_11 : Module.Finite B C
inst_12 : IsDomain B
inst_13 : IsTorsionFree B C
inst_14 : IsScalarTower A B C
GAC : Type u_5
inst_15 : Group GAC
inst_16 : Finite GAC
inst_17 : MulSemiringAction GAC C
inst_18 : IsGaloisGroup GAC A C
GBC : Type u_6
inst_19 : Group GBC
inst_20 : Finite GBC
inst_21 : MulSemiringAction GBC C
inst_22 : IsGaloisGroup GBC B C
inst_23 : IsDomain A
inst_24 : IsTorsionFree A B
inst_25 : IsDedekindDomain B
inst_26 : IsDedekindDomain C
inst_27 : P.LiesOver p
Q : Ideal C
left : Q.IsPrime
hQ : Q.LiesOver P
this : Q.LiesOver p
rw : p.ramificationIdx P * P.ramificationIdxIn C = p.ramificationIdxIn C
rw₁ : p.ramificationIdx P * P.ramificationIdxIn C = p.ramificationIdx Q
rw₂ : p.ramificationIdx P * P.ramificationIdx Q = p.ramificationIdx Q
⊢ p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
have rw₃ : p.ramificationIdx P * P.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
Tactic: rw [ramificationIdxIn_eq_ramificationIdx p P G, ramificationIdxIn_eq_ramificationIdx p Q GAC,
    ramificationIdxIn_eq_ramificationIdx P Q GBC, ramificationIdx_algebra_tower' p P Q]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst_2 : p.IsMaximal
B : Type u_2
inst_3 : CommRing B
inst_4 : IsDedekindDomain B
inst_5 : Algebra A B
inst_6 : Module.Finite A B
inst_7 : IsTorsionFree A B
G : Type u_3
inst_8 : Group G
inst_9 : Finite G
inst_10 : MulSemiringAction G B
inst_11 : IsGaloisGroup G A B
K : Type u_1 := FractionRing A
L : Type u_2 := FractionRing B
this : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
⊢ Set.ncard (α := Ideal B) (p.primesOver B) * (p.ramificationIdxIn B * p.inertiaDegIn B) = Nat.card G
have rw : ∑ _x ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdxIn B * p.inertiaDegIn B = Nat.card G
Tactic: rw [← smul_eq_mul, ← IsDedekindDomain.coe_primesOverFinset hpb B, Set.ncard_coe_finset,
    ← Finset.sum_const]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst_2 : p.IsMaximal
B : Type u_2
inst_3 : CommRing B
inst_4 : IsDedekindDomain B
inst_5 : Algebra A B
inst_6 : Module.Finite A B
inst_7 : IsTorsionFree A B
G : Type u_3
inst_8 : Group G
inst_9 : Finite G
inst_10 : MulSemiringAction G B
inst_11 : IsGaloisGroup G A B
K : Type u_1 := FractionRing A
L : Type u_2 := FractionRing B
this : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
⊢ ∑ _x ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdxIn B * p.inertiaDegIn B = Nat.card G
have rw : Eq (α := ℕ) (∑ _x ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdxIn B * p.inertiaDegIn B)
  (∑ P ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdx P * p.inertiaDeg P)
Tactic: rw [(IsGaloisGroup.toFractionRing G A B).card_eq_finrank, ← sum_ramification_inertia B K L hpb]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst_2 : p.IsMaximal
B : Type u_2
inst_3 : CommRing B
inst_4 : IsDedekindDomain B
inst_5 : Algebra A B
inst_6 : Module.Finite A B
inst_7 : IsTorsionFree A B
G : Type u_3
inst_8 : Group G
inst_9 : Finite G
inst_10 : MulSemiringAction G B
inst_11 : IsGaloisGroup G A B
K : Type u_1 := FractionRing A
L : Type u_2 := FractionRing B
this : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
⊢ Eq (α := ℕ) (∑ _x ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdxIn B * p.inertiaDegIn B)
    (∑ P ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdx P * p.inertiaDeg P)
have apply : ∀ (x : Ideal B),
  Membership.mem (γ := Finset (Ideal B)) (IsDedekindDomain.primesOverFinset p B) x →
    p.ramificationIdxIn B * p.inertiaDegIn B = p.ramificationIdx x * p.inertiaDeg x
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst_2 : p.IsMaximal
B : Type u_2
inst_3 : CommRing B
inst_4 : IsDedekindDomain B
inst_5 : Algebra A B
inst_6 : Module.Finite A B
inst_7 : IsTorsionFree A B
G : Type u_3
inst_8 : Group G
inst_9 : Finite G
inst_10 : MulSemiringAction G B
inst_11 : IsGaloisGroup G A B
K : Type u_1 := FractionRing A
L : Type u_2 := FractionRing B
this : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
P : Ideal B
hp : Membership.mem (γ := Finset (Ideal B)) (IsDedekindDomain.primesOverFinset p B) P
⊢ p.ramificationIdxIn B * p.inertiaDegIn B = p.ramificationIdx P * p.inertiaDeg P
have hp₁ : Membership.mem (γ := Set (Ideal B)) (p.primesOver B) P
Tactic: rw [← Finset.mem_coe, IsDedekindDomain.coe_primesOverFinset hpb B] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst_2 : p.IsMaximal
B : Type u_2
inst_3 : CommRing B
inst_4 : IsDedekindDomain B
inst_5 : Algebra A B
inst_6 : Module.Finite A B
inst_7 : IsTorsionFree A B
G : Type u_3
inst_8 : Group G
inst_9 : Finite G
inst_10 : MulSemiringAction G B
inst_11 : IsGaloisGroup G A B
K : Type u_1 := FractionRing A
L : Type u_2 := FractionRing B
this : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
P : Ideal B
hp : Membership.mem (γ := Set (Ideal B)) (p.primesOver B) P
⊢ p.ramificationIdxIn B * p.inertiaDegIn B = p.ramificationIdx P * p.inertiaDeg P
have left : P.IsPrime
Tactic: obtain ⟨_, _⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst_2 : p.IsMaximal
B : Type u_2
inst_3 : CommRing B
inst_4 : IsDedekindDomain B
inst_5 : Algebra A B
inst_6 : Module.Finite A B
inst_7 : IsTorsionFree A B
G : Type u_3
inst_8 : Group G
inst_9 : Finite G
inst_10 : MulSemiringAction G B
inst_11 : IsGaloisGroup G A B
K : Type u_1 := FractionRing A
L : Type u_2 := FractionRing B
this : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
P : Ideal B
hp : Membership.mem (γ := Set (Ideal B)) (p.primesOver B) P
left : P.IsPrime
⊢ p.ramificationIdxIn B * p.inertiaDegIn B = p.ramificationIdx P * p.inertiaDeg P
have right : P.LiesOver p
Tactic: obtain ⟨_, _⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst_2 : p.IsMaximal
B : Type u_2
inst_3 : CommRing B
inst_4 : IsDedekindDomain B
inst_5 : Algebra A B
inst_6 : Module.Finite A B
inst_7 : IsTorsionFree A B
G : Type u_3
inst_8 : Group G
inst_9 : Finite G
inst_10 : MulSemiringAction G B
inst_11 : IsGaloisGroup G A B
K : Type u_1 := FractionRing A
L : Type u_2 := FractionRing B
this : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
P : Ideal B
left : P.IsPrime
right : P.LiesOver p
⊢ p.ramificationIdxIn B * p.inertiaDegIn B = p.ramificationIdx P * p.inertiaDeg P
have rw : p.ramificationIdx P * p.inertiaDegIn B = p.ramificationIdx P * p.inertiaDeg P
Tactic: rw [ramificationIdxIn_eq_ramificationIdx p P G, inertiaDegIn_eq_inertiaDeg p P G]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst_2 : p.IsMaximal
B : Type u_2
inst_3 : CommRing B
inst_4 : IsDedekindDomain B
inst_5 : Algebra A B
inst_6 : Module.Finite A B
inst_7 : IsTorsionFree A B
G : Type u_3
inst_8 : Group G
inst_9 : Finite G
inst_10 : MulSemiringAction G B
inst_11 : IsGaloisGroup G A B
K : Type u_1 := FractionRing A
L : Type u_2 := FractionRing B
this : MulSemiringAction.{u_3, u_2} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
P : Ideal B
left : P.IsPrime
right : P.LiesOver p
rw : p.ramificationIdx P * p.inertiaDegIn B = p.ramificationIdx P * p.inertiaDeg P
⊢ p.ramificationIdxIn B * p.inertiaDegIn B = p.ramificationIdx P * p.inertiaDeg P
have rw₁ : p.ramificationIdx P * p.inertiaDeg P = p.ramificationIdx P * p.inertiaDeg P
Tactic: rw [ramificationIdxIn_eq_ramificationIdx p P G, inertiaDegIn_eq_inertiaDeg p P G]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : 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 ≠ ⊥
⊢ Set.ncard (α := Ideal B) (p.primesOver B) * Set.ncard (α := Ideal C) (P.primesOver C) =
    Set.ncard (α := Ideal C) (p.primesOver C)
have hP : P ≠ ⊥
Tactic: have hP : P ≠ ⊥ := ne_bot_of_liesOver_of_ne_bot hp P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
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 : MulSemiringAction.{u_6, u_4} GBC (FractionRing C) :=
  IsFractionRing.mulSemiringAction GBC B C (FractionRing B) (FractionRing C)
⊢ Set.ncard (α := Ideal B) (p.primesOver B) * Set.ncard (α := Ideal C) (P.primesOver C) =
    Set.ncard (α := Ideal C) (p.primesOver C)
have this₁ : p.ramificationIdxIn C * p.inertiaDegIn C ≠ 0
Tactic: have : p.ramificationIdxIn C * p.inertiaDegIn C ≠ 0 :=
    mul_ne_zero (ramificationIdxIn_ne_zero GAC hp) (inertiaDegIn_ne_zero GAC)
-- 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) =
    Set.ncard (α := Ideal C) (p.primesOver C)
have rw : Set.ncard (α := Ideal B) (p.primesOver B) * Set.ncard (α := Ideal C) (P.primesOver C) *
    (p.ramificationIdxIn C * p.inertiaDegIn C) =
  Nat.card GAC
Tactic: rw [← Nat.mul_left_inj this, ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp C GAC]
-- 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))
have rw : Set.ncard (α := Ideal B) (p.primesOver B) * Set.ncard (α := Ideal C) (P.primesOver C) *
    (p.ramificationIdxIn B * P.ramificationIdxIn C * (p.inertiaDegIn B * 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: rw [← inertiaDegIn_mul_inertiaDegIn p P G C GAC GBC,
        ← ramificationIdxIn_mul_ramificationIdxIn' P G C GAC GBC]
-- 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) * (p.ramificationIdxIn B * p.inertiaDegIn B) *
      (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) =
    Nat.card GAC
have rw : Nat.card G * (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) = 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
⊢ 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₁ : Nat.card G * 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]