mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³² : CommRing A
inst✝³¹ : CommRing B
inst✝³⁰ : CommRing B₂
inst✝²⁹ : CommRing B₃
inst✝²⁸ : Algebra A B
inst✝²⁷ : Algebra A B₂
inst✝²⁶ : Algebra A B₃
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Field L₂
inst✝²² : Field L₃
inst✝²¹ : Algebra A K
inst✝²⁰ : IsFractionRing A K
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : Algebra K L₂
inst✝¹⁵ : Algebra A L₂
inst✝¹⁴ : IsScalarTower A K L₂
inst✝¹³ : Algebra K L₃
inst✝¹² : Algebra A L₃
inst✝¹¹ : IsScalarTower A K L₃
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsIntegralClosure B A L
inst✝⁷ : Algebra B₂ L₂
inst✝⁶ : IsScalarTower A B₂ L₂
inst✝⁵ : IsIntegralClosure B₂ A L₂
inst✝⁴ : Algebra B₃ L₃
inst✝³ : IsScalarTower A B₃ L₃
inst✝² : IsIntegralClosure B₃ A L₃
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : Algebra.IsAlgebraic K L₂
σ : B ≃ₐ[A] B₂
⊢ (galLift K L L₂ ↑σ).comp (galLift K L₂ L ↑σ.symm) = AlgHom.id K L₂

Tactic:
simp [← galLift_comp]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³² : CommRing A
inst✝³¹ : CommRing B
inst✝³⁰ : CommRing B₂
inst✝²⁹ : CommRing B₃
inst✝²⁸ : Algebra A B
inst✝²⁷ : Algebra A B₂
inst✝²⁶ : Algebra A B₃
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Field L₂
inst✝²² : Field L₃
inst✝²¹ : Algebra A K
inst✝²⁰ : IsFractionRing A K
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : Algebra K L₂
inst✝¹⁵ : Algebra A L₂
inst✝¹⁴ : IsScalarTower A K L₂
inst✝¹³ : Algebra K L₃
inst✝¹² : Algebra A L₃
inst✝¹¹ : IsScalarTower A K L₃
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsIntegralClosure B A L
inst✝⁷ : Algebra B₂ L₂
inst✝⁶ : IsScalarTower A B₂ L₂
inst✝⁵ : IsIntegralClosure B₂ A L₂
inst✝⁴ : Algebra B₃ L₃
inst✝³ : IsScalarTower A B₃ L₃
inst✝² : IsIntegralClosure B₃ A L₃
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : Algebra.IsAlgebraic K L₂
σ : B ≃ₐ[A] B₂
⊢ (galLift K L₂ L ↑σ.symm).comp (galLift K L L₂ ↑σ) = AlgHom.id K L

Tactic:
simp [← galLift_comp]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
B : Type u_6
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsTorsionFree A B
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
x : B
⊢ (intNorm A B) x = 0 ↔ x = 0

Tactic:
by
  rw [← (IsFractionRing.injective A (FractionRing A)).eq_iff,
    ← (IsFractionRing.injective B (FractionRing B)).eq_iff]
  simp only [algebraMap_intNorm_fractionRing, map_zero, norm_eq_zero_iff]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∀ P ∈ (span {↑p}).primesOver (𝓞 K),
        p ^ P.inertiaDeg ℤ ≤
            ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ →
          Submodule.IsPrincipal P
x✝ : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : P ∈ (Ideal (𝓞 K))⁰
hP : (↑⟨P, HP⟩).IsPrime
hPN :
  ↑(absNorm ↑⟨P, HP⟩) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : (under ℤ P).IsPrime → _root_.Prime p
⊢ P.LiesOver (span {p})

Tactic:
rcases abs_choice p with h | h <;>
    simpa [h, span_singleton_neg p, ← submodule_span_eq, ← hp] using over_under P

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤ ↔ span R s = ⊤

Tactic:
have H : (span (R ⧸ p) ((Ideal.Quotient.mk (I := pS)) '' s)).restrictScalars R =
      (span R s).map (IsScalarTower.toAlgHom R S (S ⧸ pS) : S →ₗ[R] S ⧸ pS) := by
    rw [map_span, ← restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective,
      LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤ ↔ span R s = ⊤
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝¹¹ : CommRing A
B : Type u_2
inst✝¹⁰ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁹ : CommRing K
inst✝⁸ : Algebra A K
inst✝⁷ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝⁶ : CommRing L
inst✝⁵ : Algebra B L
inst✝⁴ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
⊢ extended W hg (extended L hf I) = extended W ⋯ I

Tactic:
by
  rw [← coeToSubmodule_inj, coe_extended_eq_span, coe_extended_eq_span]
  refine Submodule.span_eq_span ?_ ?_
  · rintro _ ⟨x, hx, rfl⟩
    have hx' : x ∈ span B (IsLocalization.map L f hf '' (I : Set K)) :=
      (mem_extended_iff L hf I x).1 hx
    refine span_induction (fun y hy ↦ ?_) (by simp) (fun y z _ _ hy hz ↦ ?_) (fun b y _ hy ↦ ?_) hx'
    · rcases hy with ⟨z, hz, rfl⟩
      exact Submodule.subset_span ⟨z, hz, by rw [IsLocalization.map_map]⟩
    · rw [map_add]
      exact add_mem hy hz
    · rw [IsLocalization.map_smul]
      exact smul_mem _ (g b) hy
  · rintro _ ⟨x, hx, rfl⟩
    refine Submodule.subset_span ⟨IsLocalization.map L f hf x, ?_, ?_⟩
    · exact (mem_extended_iff L hf I _).2 <| Submodule.subset_span ⟨x, hx, rfl⟩
    · rw [IsLocalization.map_map]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDomain A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : IsDomain B
inst✝¹⁴ : Algebra A B
inst✝¹³ : IsTorsionFree A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
⊢ Function.Injective fun I ↦ (extendedHom L B) I

Tactic:
by
  intro I J h
  dsimp only at h
  by_cases hI : I = 0
  · rwa [hI, map_zero, eq_comm, extendedHom_eq_zero_iff L B, eq_comm, ← hI] at h
  by_cases hJ : J = 0
  · rwa [hJ, map_zero, extendedHom_eq_zero_iff L B, ← hJ] at h
  rwa [← mul_inv_eq_one₀ ((extendedHom_eq_zero_iff _ _).not.mpr hJ), ← map_inv₀, ← map_mul,
    extendedHom_eq_one_iff _ _ (mul_ne_zero hI (inv_ne_zero hJ)), mul_inv_eq_one₀ hJ] at h

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

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.IsTorsionFree R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
⊢ P ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p)

Tactic:
by
  have non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰ :=
    map_le_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective _ _)
      p.primeCompl_le_nonZeroDivisors
  let : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
  have : IsScalarTower R (Localization.AtPrime p) Sₚ :=
    IsScalarTower.of_algebraMap_eq fun x => by
      rw [IsScalarTower.algebraMap_apply R S]
      exact (IsLocalization.map_eq (T := Algebra.algebraMapSubmonoid S (primeCompl p))
        (Submonoid.le_comap_map _) x).symm
  obtain ⟨pid, p', ⟨hp'0, hp'p⟩, hpu⟩ :=
    (IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime (Localization.AtPrime p)).mp
      (IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain R hp0 _)
  have : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥ := by
    rw [Submodule.ne_bot_iff] at hp0 ⊢
    obtain ⟨x, x_mem, x_ne⟩ := hp0
    exact
      ⟨algebraMap _ _ x, (IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _).mpr x_mem,
        IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors _ p.primeCompl_le_nonZeroDivisors
          (mem_nonZeroDivisors_of_ne_zero x_ne)⟩
  rw [← Multiset.singleton_le, ← normalize_eq P, ←
    normalizedFactors_irreducible (Ideal.prime_of_isPrime hP0 hP).irreducible, ←
    dvd_iff_normalizedFactors_le_normalizedFactors hP0, dvd_iff_le,
    IsScalarTower.algebraMap_eq R (Localization.AtPrime p) Sₚ, ← Ideal.map_map,
    Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_le_iff_le_comap,
    hpu (IsLocalRing.maximalIdeal _) ⟨this, _⟩, hpu (comap _ _) ⟨_, _⟩]
  · have : Algebra.IsIntegral (Localization.AtPrime p) Sₚ := ⟨isIntegral_localization⟩
    exact mt (Ideal.eq_bot_of_comap_eq_bot) hP0
  · exact Ideal.comap_isPrime (algebraMap (Localization.AtPrime p) Sₚ) P
  · exact (IsLocalRing.maximalIdeal.isMaximal _).isPrime
  · rw [Ne, zero_eq_bot, Ideal.map_eq_bot_iff_of_injective]
    · assumption
    rw [IsScalarTower.algebraMap_eq R S Sₚ]
    exact
      (IsLocalization.injective Sₚ non_zero_div).comp (FaithfulSMul.algebraMap_injective _ _)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : Ideal R
d : ℤ
⊢ ↑d ∈ I ↔ d ∈ span {↑(absNorm (under ℤ I))}

Tactic:
ideal_span_absNorm_eq_self,

Goal state after:
R : Type u_1
inst✝ : Ring R
I : Ideal R
d : ℤ
⊢ ↑d ∈ I ↔ d ∈ under ℤ I
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
L : Type u_3
inst✝² : Field L
inst✝¹ : NumberField L
inst✝ : Algebra K L
⊢ discr K ∣ discr L

Tactic:
suffices discr K ^ Module.finrank K L ∣ discr L from
    dvd_trans (dvd_pow_self _ (Nat.ne_zero_of_lt Module.finrank_pos)) this
  rw [← Int.dvd_natAbs, natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow K (𝓞 K) L (𝓞 L),
    Nat.cast_mul, Nat.cast_pow, ← Int.mul_sign_self, mul_pow, ← mul_assoc,
    mul_comm _ (discr K ^ _), mul_assoc]
  exact Int.dvd_mul_right _ _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.zero
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic (p ^ (0 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ (0 + 1)) ℤ).comp (X + 1)).coeff i ∈ ℤ ∙ ↑p

Tactic:
Nat.zero_add,

Goal state after:
case refine_2.zero
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic (p ^ 1) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ 1) ℤ).comp (X + 1)).coeff i ∈ ℤ ∙ ↑p
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
x y a : R
s : Finset α
p : α → R
hp : ∀ i ∈ s, Prime (p i)
hx : 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

Tactic:
induction s using Finset.induction generalizing x y a with

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

Goal state before:
pp: p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K

Tactic:
rw [← pow_one p] at hζ hcycl

Goal state after:
p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ 1)
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - ↑n = ↑p * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ pB.dim = p ^ k * (p - 1)

Tactic:
simp [integralPowerBasisOfPrimePow_dim, pB, Nat.totient_prime_pow hp.1 (Nat.zero_lt_succ k)]

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

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - ↑n = ↑p * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
⊢ p ^ k * (p - 1) ≠ 0

Tactic:
simp only [ne_eq, mul_eq_zero, NeZero.ne _, Nat.sub_eq_zero_iff_le, false_or,
      not_le, Nat.Prime.one_lt hp.out]

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

Goal state before:
pp: case neg
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h✝ : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
h : ∀ (q : ℕ), Nat.Prime q → ∀ (t : ℕ), q ^ t ≠ n
⊢ ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n

Tactic:
exact fun {p} a k ↦ h p a k

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

Goal state before:
pp: n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ (NumberField.discr K).sign * ↑(NumberField.discr K).natAbs =
    (-1) ^ (φ n / 2) * (↑n ^ φ n / ↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))))

Tactic:
sign_discr,

Goal state after:
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ (-1) ^ InfinitePlace.nrComplexPlaces K * ↑(NumberField.discr K).natAbs =
    (-1) ^ (φ n / 2) * (↑n ^ φ n / ↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))))
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case neg.hi
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
⊢ j + 1 ∈ range (Q.natDegree + 1) → p ∣ Q.coeff (j + 1)

Tactic:
| hi j hind =>

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∑ w, ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0
⊢ ∑ w, (logEmbedding K) (Additive.ofMul x) w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))

Tactic:
rw [Fintype.sum_eq_add_sum_subtype_ne _ w₀, add_comm, add_eq_zero_iff_eq_neg, ← neg_mul] at h

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∑ i, ↑(↑i).mult * Real.log (↑i ((algebraMap (𝓞 K) K) ↑x)) = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))
⊢ ∑ w, (logEmbedding K) (Additive.ofMul x) w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))
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
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hP : Ideal.map (algebraMap A B) p = 0
ha : Ideal.map (algebraMap A B) p = ⊥ ^ (e - 1) * a
⊢ Ideal.map (algebraMap A B) p = ⊥

Tactic:
Ideal.zero_eq_bot

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
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hP : Ideal.map (algebraMap A B) p = ⊥
ha : Ideal.map (algebraMap A B) p = ⊥ ^ (e - 1) * a
⊢ Ideal.map (algebraMap A B) p = ⊥
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0

Tactic:
have hu := Ideal.span_singleton_eq_span_singleton.mp h

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 1
⊢ (Ideal.Quotient.mk (Ideal.span {λ})) (x - 1) = 0

Tactic:
rw [RingHom.map_sub, h, RingHom.map_one, sub_self]

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.Deficient ↔ ¬n.Abundant ∧ ¬n.Perfect

Tactic:
grind [Perfect, Abundant, Deficient]

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
hn : 0 ≠ n
⊢ n.Perfect ↔ ¬n.Abundant ∧ ¬n.Deficient

Tactic:
grind [Perfect, Abundant, Deficient]

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
hn : 0 ≠ n
⊢ n.Abundant ↔ ¬n.Perfect ∧ ¬n.Deficient

Tactic:
grind [Perfect, Abundant, Deficient]

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
hn : 0 ≠ n
⊢ n.Deficient ∨ n.Abundant ∨ n.Perfect

Tactic:
grind [Perfect, Abundant, Deficient]

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ ∑ i ∈ m.divisors, i * k ≤ ∑ i ∈ (m * k).divisors, i

Tactic:
exact (sum_image (f := fun i ↦ i) (mul_left_injective₀ hk0).injOn).symm.trans_le
    (sum_le_sum_of_subset (by grind [mul_dvd_mul_iff_right hk0]))

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Tactic:
by
  rcases eq_or_ne (ringChar (ZMod p)) 2 with hc | hc
  · by_cases ha : (a : ZMod p) = 0
    · rw [legendreSym, ha, quadraticChar_zero,
        zero_pow (Nat.div_pos (@Fact.out p.Prime).two_le (succ_pos 1)).ne']
      norm_cast
    · have := (ringChar_zmod_n p).symm.trans hc
      -- p = 2
      subst p
      rw [legendreSym, quadraticChar_eq_one_of_char_two hc ha]
      revert ha
      push_cast
      generalize (a : ZMod 2) = b; fin_cases b
      · tauto
      · simp
  · convert! quadraticChar_eq_pow_of_char_ne_two' hc (a : ZMod p)
    exact (card p).symm

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case pos.inr
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 + (-c) ^ 3 = 0
h3c : 3 ∣ c
⊢ False

Tactic:
· rw [add_comm _ ((-c) ^ 3), ← add_assoc] at hF
    refine fermatLastTheoremThree_of_dvd_a_of_gcd_eq_one_of_case2 (neg_ne_zero.2 hc) (by simp [h3c])
      ?_ H hF
    rw [Finset.insert_comm (-c), Finset.pair_comm (-c) b]
    simp only [← Hgcd, gcd_insert, gcd_singleton, id_eq, ← abs_eq_normalize, abs_neg]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ 3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ False

Tactic:
refine hζ.toInteger_sub_one_not_dvd_two (by decide) ⟨S'.u * λ ^ 2 * z ^ 3 - λ ^ 3 * (x + y), ?_⟩

Goal state after:
case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ 3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ 2 = (hζ.toInteger - 1) * (↑S'.u * (hζ✝.toInteger - 1) ^ 2 * z ^ 3 - (hζ✝.toInteger - 1) ^ 3 * (x + y))
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : 1 ≡ b ^ (n - 1) [MOD n]
⊢ n.ProbablePrime b

Tactic:
exact mod_cast Nat.ModEq.dvd h₁

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ a ^ 2 * a = a ^ 3

Tactic:
by rw [Nat.pow_succ a 2]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ^ 4 ∣ S'.c ^ 3

Tactic:
rcases a_cube_b_cube_congr_one_or_neg_one S' with
    ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ | ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ <;>
  · refine ⟨S'.u⁻¹ * (x + y), ?_⟩
    symm
    calc _ = S'.u⁻¹ * (λ ^ 4 * x + λ ^ 4 * y) := by ring
    _ = S'.u⁻¹ * (S'.a ^ 3 + S'.b ^ 3) := by rw [← hx, ← hy]; ring
    _ = S'.u⁻¹ * (S'.u * S'.c ^ 3) := by rw [S'.H]
    _ = S'.c ^ 3 := by simp

Goal state after: