internlm/Lean-Github huggingface dataset:
Theorem: norm_add_one_smul_of_isUnit
Proof state before:
case intro
K✝ : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝⁴ : Field K✝
inst✝³ : CharZero K✝
inst✝² : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
hp✝ : p✝ ≠ 2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2
⊢ p = 2
Tactic:
have : (p : ℤ) * (- Algebra.trace ℤ _ x - r * p) = 2 := by
  rw [zsmul_eq_mul, Int.cast_natCast, ← nsmul_eq_mul, e, eq_comm, ← sub_eq_zero] at hr
  rw [eq_comm, ← sub_eq_zero, ← hr]
  ring
Proof state after:
case intro
K✝ : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝⁴ : Field K✝
inst✝³ : CharZero K✝
inst✝² : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
hp✝ : p✝ ≠ 2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2
this : ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 2
⊢ p = 2
Theorem: norm_add_one_smul_of_isUnit
Proof state before:
case intro
K✝ : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝⁴ : Field K✝
inst✝³ : CharZero K✝
inst✝² : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
hp✝ : p✝ ≠ 2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2
this : ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 2
⊢ p = 2
Tactic:
exact (Nat.prime_two.eq_one_or_self_of_dvd _
  (Int.natCast_dvd_natCast.mp ⟨_, this.symm⟩)).resolve_left hpri.ne_one
Proof state after:
no goals
Theorem: norm_add_one_smul_of_isUnit
Proof state before:
K✝ : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝⁴ : Field K✝
inst✝³ : CharZero K✝
inst✝² : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
hp✝ : p✝ ≠ 2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2
⊢ ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 2
Tactic:
rw [zsmul_eq_mul, Int.cast_natCast, ← nsmul_eq_mul, e, eq_comm, ← sub_eq_zero] at hr
Proof state after:
K✝ : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝⁴ : Field K✝
inst✝³ : CharZero K✝
inst✝² : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
hp✝ : p✝ ≠ 2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1 = 0
⊢ ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 2
Theorem: norm_add_one_smul_of_isUnit
Proof state before:
K✝ : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝⁴ : Field K✝
inst✝³ : CharZero K✝
inst✝² : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
hp✝ : p✝ ≠ 2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1 = 0
⊢ ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 2
Tactic:
rw [eq_comm, ← sub_eq_zero, ← hr]
Proof state after:
K✝ : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝⁴ : Field K✝
inst✝³ : CharZero K✝
inst✝² : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
hp✝ : p✝ ≠ 2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1 = 0
⊢ 2 - ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1
Theorem: norm_add_one_smul_of_isUnit
Proof state before:
K✝ : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝⁴ : Field K✝
inst✝³ : CharZero K✝
inst✝² : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
hp✝ : p✝ ≠ 2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1 = 0
⊢ 2 - ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1
Tactic:
ring
Proof state after:
no goals
Theorem: fermatLastTheoremFive
Proof state before:
⊢ FermatLastTheoremFor 5
Tactic:
have : Fact (Nat.Prime 5) := ⟨by norm_num⟩
Proof state after:
this : Fact (Nat.Prime 5)
⊢ FermatLastTheoremFor 5
Theorem: fermatLastTheoremFive
Proof state before:
this : Fact (Nat.Prime 5)
⊢ FermatLastTheoremFor 5
Tactic:
refine flt_regular ?_ (by omega)
Proof state after:
this : Fact (Nat.Prime 5)
⊢ IsRegularPrime 5
Theorem: fermatLastTheoremFive
Proof state before:
this : Fact (Nat.Prime 5)
⊢ IsRegularPrime 5
Tactic:
rw [IsRegularPrime, IsRegularNumber]
Proof state after:
this : Fact (Nat.Prime 5)
⊢ Coprime 5 (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨5, ⋯⟩ ℚ))))
Theorem: fermatLastTheoremFive
Proof state before:
this : Fact (Nat.Prime 5)
⊢ Coprime 5 (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨5, ⋯⟩ ℚ))))
Tactic:
convert coprime_one_right _
Proof state after:
case h.e'_2
this : Fact (Nat.Prime 5)
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨5, ⋯⟩ ℚ))) = 1
Theorem: fermatLastTheoremFive
Proof state before:
case h.e'_2
this : Fact (Nat.Prime 5)
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨5, ⋯⟩ ℚ))) = 1
Tactic:
exact classNumber_eq_one_iff.2 (Rat.five_pid (CyclotomicField _ ℚ))
Proof state after:
no goals
Theorem: fermatLastTheoremFive
Proof state before:
⊢ Nat.Prime 5
Tactic:
norm_num
Proof state after:
no goals
Theorem: fermatLastTheoremFive
Proof state before:
this : Fact (Nat.Prime 5)
⊢ 5 ≠ 2
Tactic:
omega
Proof state after:
no goals
Theorem: prod_primesOverFinset_of_isUnramified
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P = Ideal.map (algebraMap R S) p
Tactic:
classical
have hpbot' : p.map (algebraMap R S) ≠ ⊥ := (Ideal.map_eq_bot_iff_of_injective
  (NoZeroSMulDivisors.iff_algebraMap_injective.mp ‹_›)).not.mpr hp
rw [← associated_iff_eq.mp (factors_pow_count_prod hpbot')]
apply Finset.prod_congr rfl
intros P hP
convert (pow_one _).symm
rw [← Finset.mem_coe, coe_primesOverFinset S p hp] at hP
rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count hpbot' hP.1
  (ne_bot_of_mem_primesOver hp hP)]
exact IsUnramified.isUnramifiedAt _ hp _ hP
Proof state after:
no goals
Theorem: prod_primesOverFinset_of_isUnramified
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P = Ideal.map (algebraMap R S) p
Tactic:
have hpbot' : p.map (algebraMap R S) ≠ ⊥ := (Ideal.map_eq_bot_iff_of_injective
  (NoZeroSMulDivisors.iff_algebraMap_injective.mp ‹_›)).not.mpr hp
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P = Ideal.map (algebraMap R S) p
Theorem: prod_primesOverFinset_of_isUnramified
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P = Ideal.map (algebraMap R S) p
Tactic:
rw [← associated_iff_eq.mp (factors_pow_count_prod hpbot')]
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P =
    ∏ p_1 ∈ (factors (Ideal.map (algebraMap R S) p)).toFinset,
      p_1 ^ Multiset.count p_1 (factors (Ideal.map (algebraMap R S) p))
Theorem: prod_primesOverFinset_of_isUnramified
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P =
    ∏ p_1 ∈ (factors (Ideal.map (algebraMap R S) p)).toFinset,
      p_1 ^ Multiset.count p_1 (factors (Ideal.map (algebraMap R S) p))
Tactic:
apply Finset.prod_congr rfl
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∀ x ∈ primesOverFinset S p, x = x ^ Multiset.count x (factors (Ideal.map (algebraMap R S) p))
Theorem: prod_primesOverFinset_of_isUnramified
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∀ x ∈ primesOverFinset S p, x = x ^ Multiset.count x (factors (Ideal.map (algebraMap R S) p))
Tactic:
intros P hP
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ P = P ^ Multiset.count P (factors (Ideal.map (algebraMap R S) p))
Theorem: prod_primesOverFinset_of_isUnramified
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ P = P ^ Multiset.count P (factors (Ideal.map (algebraMap R S) p))
Tactic:
convert (pow_one _).symm
Proof state after:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Theorem: prod_primesOverFinset_of_isUnramified
Proof state before:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
rw [← Finset.mem_coe, coe_primesOverFinset S p hp] at hP
Proof state after:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Theorem: prod_primesOverFinset_of_isUnramified
Proof state before:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count hpbot' hP.1
  (ne_bot_of_mem_primesOver hp hP)]
Proof state after:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1
Theorem: prod_primesOverFinset_of_isUnramified
Proof state before:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1
Tactic:
exact IsUnramified.isUnramifiedAt _ hp _ hP
Proof state after:
no goals
Theorem: comap_map_eq_of_isUnramified
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
have : IsDomain S :=
  (IsIntegralClosure.equiv R S L (integralClosure R L)).toMulEquiv.isDomain (integralClosure R L)
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this : IsDomain S
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Theorem: comap_map_eq_of_isUnramified
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this : IsDomain S
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
have := IsIntegralClosure.isDedekindDomain R K L S
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Theorem: comap_map_eq_of_isUnramified
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
have hRS : Function.Injective (algebraMap R S) := by
  refine Function.Injective.of_comp (f := algebraMap S L) ?_
  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝ : IsDomain S
this : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I