mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).coeff i ∈ ℤ ∙ ↑p

Tactic:
Ideal.submodule_span_eq,

Goal state after:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).coeff i ∈ span {↑p}
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDomain R
S : Type u_3
inst✝¹¹ : CommRing S
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : Algebra R S
inst✝⁶ : Module.Finite R S
inst✝⁵ : IsTorsionFree R S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝² : p.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
⊢ (relNorm R) P = p ^ P.inertiaDeg R

Tactic:
obtain ⟨s, hs⟩ := exists_relNorm_eq_pow_of_isPrime P p

Goal state after:
case neg
R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDomain R
S : Type u_3
inst✝¹¹ : CommRing S
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : Algebra R S
inst✝⁶ : Module.Finite R S
inst✝⁵ : IsTorsionFree R S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝² : p.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R) P = p ^ s
⊢ (relNorm R) P = p ^ P.inertiaDeg R
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn : ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff k ∈ ℤ ∙ ↑p
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff k = 0

Tactic:
Ideal.submodule_span_eq,

Goal state after:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn : ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff k ∈ span {↑p}
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff k = 0
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
hiu : i ∉ u
⊢ b * c = p i * a

Tactic:
rw [← hbc, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝³⁴ : CommRing A
inst✝³³ : Field K
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : CommRing B
inst✝²⁹ : Field L
inst✝²⁸ : Algebra B L
inst✝²⁷ : Algebra A L
inst✝²⁶ : Algebra K L
inst✝²⁵ : FiniteDimensional K L
inst✝²⁴ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝²³ : CommRing R₁
inst✝²² : CommRing R₂
inst✝²¹ : IsDomain R₁
inst✝²⁰ : Algebra A R₁
inst✝¹⁹ : Algebra A R₂
inst✝¹⁸ : Algebra R₁ B
inst✝¹⁷ : Algebra R₂ B
inst✝¹⁶ : Algebra R₁ L
inst✝¹⁵ : Algebra R₂ L
inst✝¹⁴ : IsScalarTower A R₁ L
inst✝¹³ : IsScalarTower R₁ B L
inst✝¹² : IsScalarTower R₂ B L
inst✝¹¹ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝¹⁰ : Algebra R₁ ↥F₁
inst✝⁹ : Algebra R₂ ↥F₂
inst✝⁸ : IsTorsionFree R₁ ↥F₁
inst✝⁷ : IsScalarTower A (↥F₂) L
inst✝⁶ : IsScalarTower A R₂ ↥F₂
inst✝⁵ : IsScalarTower R₁ (↥F₁) L
inst✝⁴ : IsScalarTower R₂ (↥F₂) L
inst✝³ : Algebra.IsSeparable K ↥F₂
inst✝² : Algebra.IsSeparable (↥F₁) L
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : x ∈ restrictScalars R₁ (traceDual R₁ (↥F₁) 1)
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
b₂ : Basis (Free.ChooseBasisIndex A R₂) K ↥F₂ := Basis.localizationLocalization K A⁰ (↥F₂) (Free.chooseBasis A R₂)
B₁ : Basis (Free.ChooseBasisIndex A R₂) (↥F₁) L := h₁.basisOfBasisRight h₂' b₂
i : Free.ChooseBasisIndex A R₂
⊢ (algebraMap R₂ L) ((Free.chooseBasis A R₂) i) ∈ 1

Tactic:
IsScalarTower.algebraMap_apply R₂ B L,

Goal state after:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝³⁴ : CommRing A
inst✝³³ : Field K
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : CommRing B
inst✝²⁹ : Field L
inst✝²⁸ : Algebra B L
inst✝²⁷ : Algebra A L
inst✝²⁶ : Algebra K L
inst✝²⁵ : FiniteDimensional K L
inst✝²⁴ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝²³ : CommRing R₁
inst✝²² : CommRing R₂
inst✝²¹ : IsDomain R₁
inst✝²⁰ : Algebra A R₁
inst✝¹⁹ : Algebra A R₂
inst✝¹⁸ : Algebra R₁ B
inst✝¹⁷ : Algebra R₂ B
inst✝¹⁶ : Algebra R₁ L
inst✝¹⁵ : Algebra R₂ L
inst✝¹⁴ : IsScalarTower A R₁ L
inst✝¹³ : IsScalarTower R₁ B L
inst✝¹² : IsScalarTower R₂ B L
inst✝¹¹ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝¹⁰ : Algebra R₁ ↥F₁
inst✝⁹ : Algebra R₂ ↥F₂
inst✝⁸ : IsTorsionFree R₁ ↥F₁
inst✝⁷ : IsScalarTower A (↥F₂) L
inst✝⁶ : IsScalarTower A R₂ ↥F₂
inst✝⁵ : IsScalarTower R₁ (↥F₁) L
inst✝⁴ : IsScalarTower R₂ (↥F₂) L
inst✝³ : Algebra.IsSeparable K ↥F₂
inst✝² : Algebra.IsSeparable (↥F₁) L
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : x ∈ restrictScalars R₁ (traceDual R₁ (↥F₁) 1)
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
b₂ : Basis (Free.ChooseBasisIndex A R₂) K ↥F₂ := Basis.localizationLocalization K A⁰ (↥F₂) (Free.chooseBasis A R₂)
B₁ : Basis (Free.ChooseBasisIndex A R₂) (↥F₁) L := h₁.basisOfBasisRight h₂' b₂
i : Free.ChooseBasisIndex A R₂
⊢ (algebraMap B L) ((algebraMap R₂ B) ((Free.chooseBasis A R₂) i)) ∈ 1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
⊢ dual A K I ≠ 0

Tactic:
suffices algebraMap B L b ∈ dual A K I by
    intro e
    rw [e, mem_zero_iff, ← (algebraMap B L).map_zero,
      (IsIntegralClosure.algebraMap_injective B A L).eq_iff] at this
    exact mem_nonZeroDivisors_iff_ne_zero.mp hb this

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
⊢ (algebraMap B L) b ∈ dual A K I
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
⊢ dual A K 1 / dual A K 1 * (J⁻¹ / I⁻¹) = I / J

Tactic:
div_self,

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
⊢ 1 * (J⁻¹ / I⁻¹) = I / J

A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
⊢ dual A K 1 ≠ 0
Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: case hJ
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝⁵⁶ : CommRing A
inst✝⁵⁵ : Field K
inst✝⁵⁴ : Algebra A K
inst✝⁵³ : IsFractionRing A K
inst✝⁵² : CommRing B
inst✝⁵¹ : Field L
inst✝⁵⁰ : Algebra B L
inst✝⁴⁹ : Algebra A L
inst✝⁴⁸ : Algebra K L
inst✝⁴⁷ : FiniteDimensional K L
inst✝⁴⁶ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝⁴⁵ : CommRing R₁
inst✝⁴⁴ : CommRing R₂
inst✝⁴³ : IsDomain R₁
inst✝⁴² : Algebra A R₁
inst✝⁴¹ : Algebra A R₂
inst✝⁴⁰ : Algebra R₁ B
inst✝³⁹ : Algebra R₂ B
inst✝³⁸ : Algebra R₁ L
inst✝³⁷ : Algebra R₂ L
inst✝³⁶ : IsScalarTower A R₁ L
inst✝³⁵ : IsScalarTower R₁ B L
inst✝³⁴ : IsScalarTower R₂ B L
inst✝³³ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝³² : Algebra R₁ ↥F₁
inst✝³¹ : Algebra R₂ ↥F₂
inst✝³⁰ : IsTorsionFree R₁ ↥F₁
inst✝²⁹ : IsScalarTower A (↥F₂) L
inst✝²⁸ : IsScalarTower A R₂ ↥F₂
inst✝²⁷ : IsScalarTower R₁ (↥F₁) L
inst✝²⁶ : IsScalarTower R₂ (↥F₂) L
inst✝²⁵ : Algebra.IsSeparable K ↥F₂
inst✝²⁴ : Algebra.IsSeparable (↥F₁) L
inst✝²³ : IsDomain A
inst✝²² : IsDedekindDomain B
inst✝²¹ : IsDedekindDomain R₁
inst✝²⁰ : IsDedekindDomain R₂
inst✝¹⁹ : IsFractionRing B L
inst✝¹⁸ : IsFractionRing R₁ ↥F₁
inst✝¹⁷ : IsFractionRing R₂ ↥F₂
inst✝¹⁶ : IsIntegrallyClosed A
inst✝¹⁵ : IsIntegralClosure B R₁ L
inst✝¹⁴ : IsTorsionFree R₁ B
inst✝¹³ : IsTorsionFree R₂ B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.Finite A B
inst✝¹⁰ : IsTorsionFree A B
inst✝⁹ : IsTorsionFree A R₁
inst✝⁸ : IsTorsionFree A R₂
inst✝⁷ : Module.Finite A R₁
inst✝⁶ : Module.Finite R₂ B
inst✝⁵ : IsScalarTower A R₂ B
inst✝⁴ : Module.Finite R₁ B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝² : IsScalarTower A R₁ B
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))
this✝ : Algebra.IsSeparable (FractionRing A) (FractionRing R₂)
this : (dual R₁ (↥F₁) 1)⁻¹ ≤ ↑(Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))
⊢ ¬differentIdeal A R₂ = ⊥

Tactic:
exact differentIdeal_ne_bot

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case e_a.coprime
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝⁴ : NumberField K
this✝³ : NeZero n₁
this✝² : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this✝¹ : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this✝ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this : IsGalois ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤
h_cpr : IsCoprime (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯)
h_dsj : ℚ⟮ζ ^ n₂⟯.LinearDisjoint ↥ℚ⟮ζ ^ n₁⟯
h_div₁ : ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁
h_div₂ : ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)) ∣ n₂ ^ φ n₂
⊢ (n₁ ^ φ n₁) ^ φ n₂ * (n₂ ^ φ n₂) ^ φ n₁ /
      ((∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))) ^ φ n₂ * (∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))) ^ φ n₁) =
    (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))

Tactic:
primeFactors_mul (NeZero.ne _) (NeZero.ne _),

Goal state after:
case e_a.coprime
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝⁴ : NumberField K
this✝³ : NeZero n₁
this✝² : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this✝¹ : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this✝ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this : IsGalois ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤
h_cpr : IsCoprime (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯)
h_dsj : ℚ⟮ζ ^ n₂⟯.LinearDisjoint ↥ℚ⟮ζ ^ n₁⟯
h_div₁ : ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁
h_div₂ : ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)) ∣ n₂ ^ φ n₂
⊢ (n₁ ^ φ n₁) ^ φ n₂ * (n₂ ^ φ n₂) ^ φ n₁ /
      ((∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))) ^ φ n₂ * (∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))) ^ φ n₁) =
    (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ n₁.primeFactors ∪ n₂.primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : Ideal.map (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ (Ideal.Quotient.mk p) ((intTrace A B) x) = 0

Tactic:
← trace_quotient_eq_of_isDedekindDomain,

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : Ideal.map (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ (Algebra.trace (A ⧸ p) (B ⧸ Ideal.map (algebraMap A B) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x) = 0
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case pos.inl
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
Q : Ideal B
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ ⊥
⊢ ¬differentIdeal A B = 0

Tactic:
exact differentIdeal_ne_bot

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inl.«0»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ ≠ 0 → (fun i ↦ i) ⟨0, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i ↦ i) ⟨0, ⋯⟩ ^ (2 / 2) = -1

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (2 * (p / 2)) = 1

Tactic:
two_mul_odd_div_two hp_odd

Goal state after:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p - 1) = 1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case neg.«_@».Mathlib.NumberTheory.LegendreSymbol.Basic.2777296637._hygCtx._hyg.53.«0»
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬(fun i ↦ i) ⟨0, ⋯⟩ = 0 → 1 = (fun i ↦ i) ⟨0, ⋯⟩ ^ 1

Tactic:
tauto

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inl
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝ : ⊥.IsPrime
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this : IsLocalization B⁰ (Localization.AtPrime ⊥)
⊢ FormallyUnramified A L

Tactic:
have : Algebra.FormallyUnramified K L := by
      rwa [Algebra.FormallyUnramified.iff_isSeparable]

Goal state after:
case inl
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝ : ⊥.IsPrime
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization B⁰ (Localization.AtPrime ⊥)
this : FormallyUnramified K L
⊢ FormallyUnramified A L
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inr.mp
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : ¬P ∣ differentIdeal A B
⊢ IsUnramifiedAt A P

Tactic:
Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)

Goal state after:
case inr.mp
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : ¬P ∣ differentIdeal A B
⊢ Algebra.IsSeparable (Ideal.under A P).ResidueField P.ResidueField ∧
    Ideal.map (algebraMap A (Localization.AtPrime P)) (Ideal.under A P) =
      IsLocalRing.maximalIdeal (Localization.AtPrime P)
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
ha₇ : A * B ∣ b ^ (2 * p) - 1
⊢ (A * B).ProbablePrime b

Tactic:
obtain ⟨q, hq⟩ := ha₆

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₇ : A * B ∣ b ^ (2 * p) - 1
q : ℕ
hq : A * B - 1 = 2 * p * q
⊢ (A * B).ProbablePrime b
Module: Mathlib.NumberTheory.Harmonic.Int

Goal state before:
pp: n : ℕ
⊢ padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
    rcases eq_or_ne n 0 with rfl | hn
    · simp
    rw [harmonic_succ]
    have key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹ := by
      rw [ih, padicValRat.inv, padicValRat.of_nat, Ne, neg_inj, Nat.cast_inj]
      exact Nat.log_ne_padicValNat_succ hn
    rw [padicValRat.add_eq_min (harmonic_succ n ▸ (harmonic_pos n.succ_ne_zero).ne')
        (harmonic_pos hn).ne' (inv_ne_zero (Nat.cast_ne_zero.mpr n.succ_ne_zero)) key, ih,
        padicValRat.inv, padicValRat.of_nat, min_neg_neg, neg_inj, ← Nat.cast_max, Nat.cast_inj]
    exact Nat.max_log_padicValNat_succ_eq_log_succ n

Goal state after: