awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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)
rw : ∑ _x ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdxIn B * p.inertiaDegIn B = Nat.card G
⊢ Set.ncard (α := Ideal B) (p.primesOver 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]

Premises used: IsDedekindDomain.coe_primesOverFinset, smul_eq_mul, Set.ncard_coe_finset, Finset.sum_const
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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)
rw :
  Eq (α := ℕ) (∑ _x ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdxIn B * p.inertiaDegIn B)
    (∑ P ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdx P * p.inertiaDeg P)
⊢ ∑ _x ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdxIn B * p.inertiaDegIn B = Nat.card G

Tactic:
rw [(IsGaloisGroup.toFractionRing G A B).card_eq_finrank, ← sum_ramification_inertia B K L hpb]

Premises used: Ideal.sum_ramification_inertia, IsGaloisGroup.card_eq_finrank
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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)
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
⊢ Eq (α := ℕ) (∑ _x ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdxIn B * p.inertiaDegIn B)
    (∑ P ∈ IsDedekindDomain.primesOverFinset p B, p.ramificationIdx P * p.inertiaDeg P)

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
⊢ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) P

Tactic:
rw [← Finset.mem_coe, IsDedekindDomain.coe_primesOverFinset hpb B] at hp

Premises used: IsDedekindDomain.coe_primesOverFinset, Finset.mem_coe
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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.IsPrime

Tactic:
obtain ⟨_, _⟩ := hp
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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.LiesOver p

Tactic:
obtain ⟨_, _⟩ := hp
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
rw₁ rw₂ : p.ramificationIdx P * p.inertiaDeg P = p.ramificationIdx P * p.inertiaDeg P
⊢ p.ramificationIdxIn B * p.inertiaDegIn B = p.ramificationIdx P * p.inertiaDeg P

Tactic:
rw [ramificationIdxIn_eq_ramificationIdx p P G, inertiaDegIn_eq_inertiaDeg p P G]

Premises used: Ideal.ramificationIdxIn_eq_ramificationIdx, Ideal.inertiaDegIn_eq_inertiaDeg
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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 ≠ ⊥
⊢ P ≠ ⊥

Tactic:
have hP : P ≠ ⊥ := ne_bot_of_liesOver_of_ne_bot hp P
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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)
⊢ 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)
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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 :
  Set.ncard (α := Ideal B) (p.primesOver B) * Set.ncard (α := Ideal C) (P.primesOver C) *
      (p.ramificationIdxIn C * p.inertiaDegIn C) =
    Nat.card GAC
⊢ Set.ncard (α := Ideal B) (p.primesOver B) * Set.ncard (α := Ideal C) (P.primesOver C) =
    Set.ncard (α := Ideal C) (p.primesOver C)

Tactic:
rw [← Nat.mul_left_inj this, ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp C GAC]

Premises used: Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, Nat.mul_left_inj
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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 :
  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))
⊢ 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:
rw [← inertiaDegIn_mul_inertiaDegIn p P G C GAC GBC,
        ← ramificationIdxIn_mul_ramificationIdxIn' P G C GAC GBC]

Premises used: Ideal.inertiaDegIn_mul_inertiaDegIn, Ideal.ramificationIdxIn_mul_ramificationIdxIn'
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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 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:
ring
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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)
rw₅ rw₆ : finrank.{u_1, u_4} (FractionRing A) (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

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]

Premises used: Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, Module.finrank_mul_finrank, IsGaloisGroup.card_eq_finrank
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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) * (p.ramificationIdxIn B * p.inertiaDegIn B) *
      (Set.ncard (α := Ideal C) (P.primesOver C) * (P.ramificationIdxIn C * P.inertiaDegIn C)) =
    Nat.card GAC
⊢ Set.ncard (α := Ideal B) (p.primesOver 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]

Premises used: HMul.hMul, Ideal.primesOver, Nat.card, Ideal.inertiaDegIn, Set.ncard, Ideal.ramificationIdxIn
-- 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)
⊢ IsGalois.{u_1, u_2} (R ⧸ p) (S ⧸ P)

Tactic:
have : IsGalois (R ⧸ p) (S ⧸ P) := { __ := Ideal.Quotient.normal (A := R) 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
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)
⊢ Module.Finite.{u_1, u_2} (R ⧸ p) (S ⧸ P)

Tactic:
have := Ideal.Quotient.finite_of_isInvariant 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
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)
⊢ 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