awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : ¬p = ⊥
hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P
⊢ p.ramificationIdx P ≤
    p.ramificationIdx P * p.inertiaDeg P +
      ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x
have neg : 0 < p.inertiaDeg P
Tactic: refine le_trans (Nat.le_mul_of_pos_right _ ?_) (Nat.le_add_right _ _)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
⊢ p.ramificationIdx P ≤ finrank K L
have pos : ∀ (hp0 : p = ⊥), p.ramificationIdx P ≤ finrank K L
Tactic: classical
  by_cases hp0 : p = ⊥
  · simp [hp0]
  have hP : P ∈ IsDedekindDomain.primesOverFinset p S :=
    (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
  rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]
  refine le_trans (Nat.le_mul_of_pos_right _ ?_) (Nat.le_add_right _ _)
  exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
pos : ∀ (hp0 : p = ⊥), p.ramificationIdx P ≤ finrank K L
⊢ p.ramificationIdx P ≤ finrank K L
have neg : ∀ (hp0 : ¬p = ⊥), p.ramificationIdx P ≤ finrank K L
Tactic: classical
  by_cases hp0 : p = ⊥
  · simp [hp0]
  have hP : P ∈ IsDedekindDomain.primesOverFinset p S :=
    (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
  rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]
  refine le_trans (Nat.le_mul_of_pos_right _ ?_) (Nat.le_add_right _ _)
  exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
pos : ∀ (hp0 : p = ⊥), p.ramificationIdx P ≤ finrank K L
neg neg₁ : ∀ (hp0 : ¬p = ⊥), p.ramificationIdx P ≤ finrank K L
⊢ p.ramificationIdx P ≤ finrank K L
have neg₂ : ∀ (hp0 : ¬p = ⊥) (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
  p.ramificationIdx P ≤ finrank K L
Tactic: classical
  by_cases hp0 : p = ⊥
  · simp [hp0]
  have hP : P ∈ IsDedekindDomain.primesOverFinset p S :=
    (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
  rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]
  refine le_trans (Nat.le_mul_of_pos_right _ ?_) (Nat.le_add_right _ _)
  exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
pos : ∀ (hp0 : p = ⊥), p.ramificationIdx P ≤ finrank K L
neg neg₁ : ∀ (hp0 : ¬p = ⊥), p.ramificationIdx P ≤ finrank K L
neg₂ :
  ∀ (hp0 : ¬p = ⊥) (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
    p.ramificationIdx P ≤ finrank K L
⊢ p.ramificationIdx P ≤ finrank K L
have neg₃ : ∀ (hp0 : ¬p = ⊥) (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
  p.ramificationIdx P ≤
    p.ramificationIdx P * p.inertiaDeg P +
      ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x
Tactic: classical
  by_cases hp0 : p = ⊥
  · simp [hp0]
  have hP : P ∈ IsDedekindDomain.primesOverFinset p S :=
    (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
  rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]
  refine le_trans (Nat.le_mul_of_pos_right _ ?_) (Nat.le_add_right _ _)
  exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
pos : ∀ (hp0 : p = ⊥), p.ramificationIdx P ≤ finrank K L
neg neg₁ : ∀ (hp0 : ¬p = ⊥), p.ramificationIdx P ≤ finrank K L
neg₂ :
  ∀ (hp0 : ¬p = ⊥) (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
    p.ramificationIdx P ≤ finrank K L
neg₃ :
  ∀ (hp0 : ¬p = ⊥) (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
    p.ramificationIdx P ≤
      p.ramificationIdx P * p.inertiaDeg P +
        ∑ x ∈ Finset.erase (IsDedekindDomain.primesOverFinset p S) P, p.ramificationIdx x * p.inertiaDeg x
⊢ p.ramificationIdx P ≤ finrank K L
have neg₄ : ∀ (hp0 : ¬p = ⊥) (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
  0 < p.inertiaDeg P
Tactic: classical
  by_cases hp0 : p = ⊥
  · simp [hp0]
  have hP : P ∈ IsDedekindDomain.primesOverFinset p S :=
    (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
  rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]
  refine le_trans (Nat.le_mul_of_pos_right _ ?_) (Nat.le_add_right _ _)
  exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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 ≠ ⊥
⊢ Finset.card (α := Ideal S) (IsDedekindDomain.primesOverFinset p S) ≤ finrank K L
have rw : LE.le (α := ℕ) (∑ x ∈ IsDedekindDomain.primesOverFinset p S, 1)
  (∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx P * p.inertiaDeg P)
Tactic: rw [← sum_ramification_inertia S K L hp0, Finset.card_eq_sum_ones]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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 ≠ ⊥
⊢ LE.le (α := ℕ) (∑ x ∈ IsDedekindDomain.primesOverFinset p S, 1)
    (∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx P * p.inertiaDeg P)
have refine : ∀ (P : Ideal S) (hP : Membership.mem (γ := Finset (Ideal S)) (IsDedekindDomain.primesOverFinset p S) P),
  1 ≤ p.ramificationIdx P * p.inertiaDeg P
Tactic: refine Finset.sum_le_sum fun P hP ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
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
⊢ 1 ≤ p.ramificationIdx P * p.inertiaDeg P
have this : P.IsPrime
Tactic: have : P.IsPrime := ((IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mp hP).1
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
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 : P.IsPrime
⊢ 1 ≤ p.ramificationIdx P * p.inertiaDeg P
have this₁ : P.LiesOver p
Tactic: have : P.LiesOver p := ((IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mp hP).2
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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 * p.inertiaDeg P
have refine_1 : 1 ≤ p.ramificationIdx P
Tactic: refine Right.one_le_mul ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
refine_1 : 1 ≤ p.ramificationIdx P
⊢ 1 ≤ p.ramificationIdx P * p.inertiaDeg P
have refine_2 : 1 ≤ p.inertiaDeg P
Tactic: refine Right.one_le_mul ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
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 ≠ ⊥
⊢ p.ramificationIdx (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) = finrank K L
have this : FaithfulSMul R S
Tactic: have := FaithfulSMul.of_field_isFractionRing R S K L
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
⊢ p.ramificationIdx (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) = finrank K L
have simp_rw : p.ramificationIdx (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) =
  ∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx P * p.inertiaDeg P
Tactic: simp_rw [← sum_ramification_inertia S K L hp0, IsLocalRing.primesOverFinset_eq S hp0,
    Finset.sum_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
⊢ p.ramificationIdx (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) = finrank K L
have simp_rw₁ : p.ramificationIdx (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) =
  ∑ x ∈ {IsLocalRing.maximalIdeal S}, p.ramificationIdx x * p.inertiaDeg x
Tactic: simp_rw [← sum_ramification_inertia S K L hp0, IsLocalRing.primesOverFinset_eq S hp0,
    Finset.sum_singleton]
-- 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
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)
⊢ (σ * τ) • Q = σ • τ • Q
have apply : (↑((σ * τ) • Q) : Ideal B) = (↑(σ • τ • Q) : Ideal B)
Tactic: apply Subtype.val_inj.mp
-- 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
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 (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)))
have 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)))
Tactic: rw [map_mul]
-- 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
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)
⊢ HSMul.hSMul.{u_5, u_2, u_2} (α := Gal(L/K)) 1 Q = Q
have apply : (↑(HSMul.hSMul.{u_5, u_2, u_2} (α := Gal(L/K)) 1 Q) : Ideal B) = (↑Q : Ideal B)
Tactic: apply Subtype.val_inj.mp
-- 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 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), σ • P = Q
have rcases : ∀ (σ : G) (hs : Q = σ • P), ∃ (σ : 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⟩
-- 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_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
⊢ ∀ (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
have 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 sorry) =
      Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) Q sorry
Tactic: ⟨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_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 : 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 ⋯
have 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 sorry) =
      Subtype.mk (p := fun (x : Ideal B) ↦ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x) Q sorry
Tactic: rcases exists_smul_eq_of_isGaloisGroup p P Q G with ⟨σ, hs⟩
-- 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 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
⊢ p.ramificationIdx P = p.ramificationIdx Q
have rcases : ∀ (σ : G) [hQp : (σ • P).IsPrime] [(σ • P).LiesOver p], p.ramificationIdx P = p.ramificationIdx (σ • P)
Tactic: rcases exists_smul_eq_of_isGaloisGroup p P Q G with ⟨σ, rfl⟩
Cleared hypotheses: Q, hQp, inst_3
-- 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 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
⊢ p.inertiaDeg P = p.inertiaDeg Q
have rcases : ∀ (σ : G) [hQp : (σ • P).IsPrime] [(σ • P).LiesOver p], p.inertiaDeg P = p.inertiaDeg (σ • P)
Tactic: rcases exists_smul_eq_of_isGaloisGroup p P Q G with ⟨σ, rfl⟩
Cleared hypotheses: Q, hQp, inst_3
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
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.ramificationIdxIn B = p.ramificationIdx P
have h : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p
Tactic: have h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p := ⟨P, hPp, hp⟩