awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
hp0 : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
this_1 : P.IsPrime
this : P.LiesOver p
⊢ 1 ≤ p.ramificationIdx P

Tactic:
exact Nat.pos_iff_ne_zero.mpr <| IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver _ hp0

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
hp0 : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
this_1 : P.IsPrime
this : P.LiesOver p
⊢ 1 ≤ p.inertiaDeg P

Tactic:
Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Ideal.inertiaDeg_ne_zero, Nat.lt
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : NoZeroSMulDivisors R S
p : Ideal R
inst_17 : p.IsMaximal
hp0 : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
this_1 : P.IsPrime
this : P.LiesOver p
⊢ 1 ≤ p.inertiaDeg P

Tactic:
exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Ideal.inertiaDeg_ne_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : IsLocalRing S
p : Ideal R
inst_17 : p.IsMaximal
hp0 : p ≠ ⊥
⊢ FaithfulSMul R S

Tactic:
have := FaithfulSMul.of_field_isFractionRing R S K L
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst_4 : Field K
inst_5 : Field L
inst_6 : IsDedekindDomain R
inst_7 : Algebra R K
inst_8 : IsFractionRing R K
inst_9 : Algebra S L
inst_10 : IsFractionRing S L
inst_11 : Algebra K L
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Module.Finite R S
inst_16 : IsLocalRing S
p : Ideal R
inst_17 : p.IsMaximal
hp0 : p ≠ ⊥
this : FaithfulSMul R S
simp_rw :
  p.ramificationIdx (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) =
    ∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx P * p.inertiaDeg P
simp_rw₁ :
  p.ramificationIdx (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) =
    ∑ x ∈ {IsLocalRing.maximalIdeal S}, p.ramificationIdx x * p.inertiaDeg x
⊢ p.ramificationIdx (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) = finrank K L

Tactic:
simp_rw [← sum_ramification_inertia S K L hp0, IsLocalRing.primesOverFinset_eq S hp0,
    Finset.sum_singleton]

Premises used: Ideal.sum_ramification_inertia, Finset.sum_singleton, IsLocalRing.primesOverFinset_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
σ : G
P : (↑(p.primesOver B) : Type u_2)
⊢ (↑(σ • P) : Ideal B) = σ • (↑P : Ideal B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
σ : G
P : Ideal B
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
⊢ (↑(HSMul.hSMul (β := (↑(p.primesOver B) : Type u_2)) σ (primesOver.mk p P)) : Ideal B) = σ • P

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : Algebra B L
inst_11 : Algebra K L
inst_12 : Algebra A L
inst_13 : IsScalarTower A B L
inst_14 : IsScalarTower A K L
inst_15 : IsIntegralClosure B A L
inst_16 : FiniteDimensional K L
σ τ : Gal(L/K)
Q : (↑(p.primesOver B) : Type u_2)
apply : (↑((σ * τ) • Q) : Ideal B) = (↑(σ • τ • Q) : Ideal B)
⊢ (σ * τ) • Q = σ • τ • Q

Tactic:
apply Subtype.val_inj.mp

Premises used: Subtype.val_inj, Iff.mp
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : Algebra B L
inst_11 : Algebra K L
inst_12 : Algebra A L
inst_13 : IsScalarTower A B L
inst_14 : IsScalarTower A K L
inst_15 : IsIntegralClosure B A L
inst_16 : FiniteDimensional K L
σ τ : Gal(L/K)
Q : (↑(p.primesOver B) : Type u_2)
rw :
  Eq (α := Ideal B)
    (map
      (HMul.hMul (α := B ≃ₐ[A] B) (β := B ≃ₐ[A] B)
        (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ : B ≃ₐ[A] B)
        (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) τ : B ≃ₐ[A] B))
      (↑Q : Ideal B))
    (map (R := B) (F := B ≃ₐ[A] B)
      (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ : B ≃ₐ[A] B)
      (map (F := B ≃ₐ[A] B)
        (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) τ : B ≃ₐ[A] B)
        (↑Q : Ideal B)))
⊢ Eq (α := Ideal B)
    (map (F := B ≃ₐ[A] B)
      (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) (σ * τ) :
        B ≃ₐ[A] B)
      (↑Q : Ideal B))
    (map (R := B) (F := B ≃ₐ[A] B)
      (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ : B ≃ₐ[A] B)
      (map (F := B ≃ₐ[A] B)
        (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) τ : B ≃ₐ[A] B)
        (↑Q : Ideal B)))

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : Algebra B L
inst_11 : Algebra K L
inst_12 : Algebra A L
inst_13 : IsScalarTower A B L
inst_14 : IsScalarTower A K L
inst_15 : IsIntegralClosure B A L
inst_16 : FiniteDimensional K L
σ τ : Gal(L/K)
Q : (↑(p.primesOver B) : Type u_2)
⊢ Eq (α := Ideal B)
    (map
      (HMul.hMul (α := B ≃ₐ[A] B) (β := B ≃ₐ[A] B)
        (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ : B ≃ₐ[A] B)
        (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) τ : B ≃ₐ[A] B))
      (↑Q : Ideal B))
    (map (R := B) (F := B ≃ₐ[A] B)
      (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ : B ≃ₐ[A] B)
      (map (F := B ≃ₐ[A] B)
        (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) τ : B ≃ₐ[A] B)
        (↑Q : Ideal B)))

Tactic:
(Q.1.map_map ((galRestrict A K L B) τ).toRingHom ((galRestrict A K L B) σ).toRingHom).symm

Premises used: Set.Mem, setOf, Ideal.map, AlgEquiv.trans, Ideal.map_map, galRestrict, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : Algebra B L
inst_11 : Algebra K L
inst_12 : Algebra A L
inst_13 : IsScalarTower A B L
inst_14 : IsScalarTower A K L
inst_15 : IsIntegralClosure B A L
inst_16 : FiniteDimensional K L
σ τ : Gal(L/K)
Q : (↑(p.primesOver B) : Type u_2)
⊢ Eq (α := Ideal B)
    (map
      (HMul.hMul (α := B ≃ₐ[A] B) (β := B ≃ₐ[A] B)
        (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ : B ≃ₐ[A] B)
        (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) τ : B ≃ₐ[A] B))
      (↑Q : Ideal B))
    (map (R := B) (F := B ≃ₐ[A] B)
      (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ : B ≃ₐ[A] B)
      (map (F := B ≃ₐ[A] B)
        (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) τ : B ≃ₐ[A] B)
        (↑Q : Ideal B)))

Tactic:
exact (Q.1.map_map ((galRestrict A K L B) τ).toRingHom ((galRestrict A K L B) σ).toRingHom).symm

Premises used: Ideal.map_map, galRestrict, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : Algebra B L
inst_11 : Algebra K L
inst_12 : Algebra A L
inst_13 : IsScalarTower A B L
inst_14 : IsScalarTower A K L
inst_15 : IsIntegralClosure B A L
inst_16 : FiniteDimensional K L
Q : (↑(p.primesOver B) : Type u_2)
apply : (↑(HSMul.hSMul.{u_5, u_2, u_2} (α := Gal(L/K)) 1 Q) : Ideal B) = (↑Q : Ideal B)
⊢ HSMul.hSMul.{u_5, u_2, u_2} (α := Gal(L/K)) 1 Q = Q

Tactic:
apply Subtype.val_inj.mp

Premises used: Subtype.val_inj, Iff.mp
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : Algebra B L
inst_11 : Algebra K L
inst_12 : Algebra A L
inst_13 : IsScalarTower A B L
inst_14 : IsScalarTower A K L
inst_15 : IsIntegralClosure B A L
inst_16 : FiniteDimensional K L
Q : (↑(p.primesOver B) : Type u_2)
⊢ map (F := B ≃ₐ[A] B)
      (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) 1)
      (↑Q : Ideal B) =
    (↑Q : Ideal B)

Tactic:
simpa only [map_one] using map_id Q.1

Premises used: Ideal.map_id, map_one, Subtype.val
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
K : Type u_4
L : Type u_5
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra B L
inst_8 : Algebra K L
inst_9 : Algebra A L
inst_10 : IsScalarTower A B L
inst_11 : IsScalarTower A K L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
σ : Gal(L/K)
P : (↑(p.primesOver B) : Type u_2)
⊢ (↑(σ • P) : Ideal B) =
    map (F := B ≃ₐ[A] B)
      (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ : B ≃ₐ[A] B)
      (↑P : Ideal B)

Tactic:
rfl

Premises used: Set.Mem, setOf, Ideal.map, Submodule.span, rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
K : Type u_4
L : Type u_5
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra B L
inst_8 : Algebra K L
inst_9 : Algebra A L
inst_10 : IsScalarTower A B L
inst_11 : IsScalarTower A K L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
σ : Gal(L/K)
P : Ideal B
inst_14 : P.IsPrime
inst_15 : P.LiesOver p
⊢ (↑(HSMul.hSMul (β := (↑(p.primesOver B) : Type u_2)) σ (primesOver.mk p P)) : Ideal B) =
    map (F := B ≃ₐ[A] B)
      (((galRestrict A K L B : MulEquiv.{u_5, u_2} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ : B ≃ₐ[A] B) P

Tactic:
rfl

Premises used: Set.Mem, setOf, Ideal.map, Submodule.span, rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst_3 : Q.LiesOver p
G : Type u_3
inst_4 : Group G
inst_5 : Finite G
inst_6 : MulSemiringAction G B
inst_7 : IsGaloisGroup G A B
rcases : ∀ (σ : G) (hs : Q = σ • P), ∃ (σ : G), σ • P = Q
⊢ ∃ (σ : G), σ • P = Q

Tactic:
rcases IsInvariant.exists_smul_of_under_eq A B G P Q <|
    (over_def P p).symm.trans (over_def Q p) with ⟨σ, hs⟩

Premises used: Algebra.IsInvariant.exists_smul_of_under_eq, Ideal.over_def, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst_3 : Q.LiesOver p
G : Type u_3
inst_4 : Group G
inst_5 : Finite G
inst_6 : MulSemiringAction G B
inst_7 : IsGaloisGroup G A B
σ : G
hs : Q = σ • P
⊢ ∃ (σ : G), σ • P = Q

Tactic:
⟨σ, hs.symm⟩

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst_3 : Q.LiesOver p
G : Type u_3
inst_4 : Group G
inst_5 : Finite G
inst_6 : MulSemiringAction G B
inst_7 : IsGaloisGroup G A B
σ : G
hs : Q = σ • P
⊢ ∃ (σ : G), σ • P = Q

Tactic:
exact ⟨σ, hs.symm⟩
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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_1 Q : Ideal B
hPp : P_1.IsPrime
hp : P_1.LiesOver p
hQp : Q.IsPrime
inst_3 : Q.LiesOver p
G : Type u_3
inst_4 : Group G
inst_5 : Finite G
inst_6 : MulSemiringAction G B
inst_7 : IsGaloisGroup G A B
P : Ideal B
left : P.IsPrime
right : P.LiesOver p
this :
  ∀ (Q : Ideal B) (left_1 : Q.IsPrime) (right_1 : Q.LiesOver p),
    ∃ (g : G),
      HSMul.hSMul (β := (↑(p.primesOver B) : Type u_2)) g
          (Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) P ⋯) =
        Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) Q ⋯
⊢ ∀ (y : (↑(p.primesOver B) : Type u_2)),
    ∃ (g : G),
      HSMul.hSMul (β := (↑(p.primesOver B) : Type u_2)) g
          (Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) P ⋯) =
        y

Tactic:
⟨Q, _, _⟩
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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_1 Q_1 : Ideal B
hPp : P_1.IsPrime
hp : P_1.LiesOver p
hQp : Q_1.IsPrime
inst_3 : Q_1.LiesOver p
G : Type u_3
inst_4 : Group G
inst_5 : Finite G
inst_6 : MulSemiringAction G B
inst_7 : IsGaloisGroup G A B
P : Ideal B
left : P.IsPrime
right : P.LiesOver p
Q : Ideal B
left_1 : Q.IsPrime
right_1 : Q.LiesOver p
rcases :
  ∀ (σ : G) (hs : σ • P = Q),
    ∃ (g : G),
      HSMul.hSMul (β := (↑(p.primesOver B) : Type u_2)) g
          (Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) P ⋯) =
        Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) Q ⋯
⊢ ∃ (g : G),
    HSMul.hSMul (β := (↑(p.primesOver B) : Type u_2)) g
        (Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) P ⋯) =
      Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) Q ⋯

Tactic:
rcases exists_smul_eq_of_isGaloisGroup p P Q G with ⟨σ, hs⟩

Premises used: Ideal.exists_smul_eq_of_isGaloisGroup
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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_1 Q_1 : Ideal B
hPp : P_1.IsPrime
hp : P_1.LiesOver p
hQp : Q_1.IsPrime
inst_3 : Q_1.LiesOver p
G : Type u_3
inst_4 : Group G
inst_5 : Finite G
inst_6 : MulSemiringAction G B
inst_7 : IsGaloisGroup G A B
P : Ideal B
left : P.IsPrime
right : P.LiesOver p
Q : Ideal B
left_1 : Q.IsPrime
right_1 : Q.LiesOver p
σ : G
hs : σ • P = Q
⊢ ∃ (g : G),
    HSMul.hSMul (β := (↑(p.primesOver B) : Type u_2)) g
        (Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) P ⋯) =
      Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) Q ⋯

Tactic:
⟨σ, Subtype.val_inj.mp hs⟩

Premises used: Subtype.val_inj, Exists.intro, Iff.mp
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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_1 Q_1 : Ideal B
hPp : P_1.IsPrime
hp : P_1.LiesOver p
hQp : Q_1.IsPrime
inst_3 : Q_1.LiesOver p
G : Type u_3
inst_4 : Group G
inst_5 : Finite G
inst_6 : MulSemiringAction G B
inst_7 : IsGaloisGroup G A B
P : Ideal B
left : P.IsPrime
right : P.LiesOver p
Q : Ideal B
left_1 : Q.IsPrime
right_1 : Q.LiesOver p
σ : G
hs : σ • P = Q
⊢ ∃ (g : G),
    HSMul.hSMul (β := (↑(p.primesOver B) : Type u_2)) g
        (Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) P ⋯) =
      Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) Q ⋯

Tactic:
exact ⟨σ, Subtype.val_inj.mp hs⟩
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst_3 : Q.LiesOver p
G : Type u_3
inst_4 : Group G
inst_5 : Finite G
inst_6 : MulSemiringAction G B
inst_7 : IsGaloisGroup G A B
rcases : ∀ (σ : G) [hQp : (σ • P).IsPrime] [(σ • P).LiesOver p], p.ramificationIdx P = p.ramificationIdx (σ • P)
⊢ p.ramificationIdx P = p.ramificationIdx Q

Tactic:
rcases exists_smul_eq_of_isGaloisGroup p P Q G with ⟨σ, rfl⟩

Premises used: Ideal.exists_smul_eq_of_isGaloisGroup, rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
σ : G
hQp : (σ • P).IsPrime
inst_7 : (σ • P).LiesOver p
⊢ p.ramificationIdx P = p.ramificationIdx (σ • P)

Tactic:
(ramificationIdx_map_eq p P (MulSemiringAction.toAlgEquiv A B σ)).symm

Premises used: MulSemiringAction.toAlgEquiv, MulSemiringAction.toRingHom, Ideal.map, Ideal.ramificationIdx_map_eq, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
σ : G
hQp : (σ • P).IsPrime
inst_7 : (σ • P).LiesOver p
⊢ p.ramificationIdx P = p.ramificationIdx (σ • P)

Tactic:
exact (ramificationIdx_map_eq p P (MulSemiringAction.toAlgEquiv A B σ)).symm

Premises used: MulSemiringAction.toAlgEquiv, Ideal.ramificationIdx_map_eq, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst_3 : Q.LiesOver p
G : Type u_3
inst_4 : Group G
inst_5 : Finite G
inst_6 : MulSemiringAction G B
inst_7 : IsGaloisGroup G A B
rcases : ∀ (σ : G) [hQp : (σ • P).IsPrime] [(σ • P).LiesOver p], p.inertiaDeg P = p.inertiaDeg (σ • P)
⊢ p.inertiaDeg P = p.inertiaDeg Q

Tactic:
rcases exists_smul_eq_of_isGaloisGroup p P Q G with ⟨σ, rfl⟩

Premises used: Ideal.exists_smul_eq_of_isGaloisGroup, rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
σ : G
hQp : (σ • P).IsPrime
inst_7 : (σ • P).LiesOver p
⊢ p.inertiaDeg P = p.inertiaDeg (σ • P)

Tactic:
(inertiaDeg_map_eq p P (MulSemiringAction.toAlgEquiv A B σ)).symm

Premises used: MulSemiringAction.toAlgEquiv, MulSemiringAction.toRingHom, Ideal.map, Eq.symm, Ideal.inertiaDeg_map_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
σ : G
hQp : (σ • P).IsPrime
inst_7 : (σ • P).LiesOver p
⊢ p.inertiaDeg P = p.inertiaDeg (σ • P)

Tactic:
exact (inertiaDeg_map_eq p P (MulSemiringAction.toAlgEquiv A B σ)).symm

Premises used: MulSemiringAction.toAlgEquiv, Eq.symm, Ideal.inertiaDeg_map_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
⊢ ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p

Tactic:
have h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p := ⟨P, hPp, hp⟩
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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
hp : P.LiesOver p
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : IsGaloisGroup G A B
h : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p
⊢ h.choose (p := fun (P : Ideal B) ↦ P.IsPrime ∧ P.LiesOver p).IsPrime

Tactic:
obtain ⟨_, _⟩ := h.choose_spec

Premises used: Exists.choose_spec