mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
w₀ : { w // w.IsComplex }
h : minkowskiBound K I < volume (convexBodyLT' K f w₀)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx✝ : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
hx : x ∈ span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))
h_nz : ⟨x, hx✝⟩ ≠ 0
h_mem : ↑⟨x, hx✝⟩ ∈ convexBodyLT' K f w₀
⊢ ∃ a ∈ ↑I,
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧
        |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2

Tactic:
mem_span_fractionalIdealLatticeBasis

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
w₀ : { w // w.IsComplex }
h : minkowskiBound K I < volume (convexBodyLT' K f w₀)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx✝ : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
hx : x ∈ ⇑(mixedEmbedding K) '' ↑↑I
h_nz : ⟨x, hx✝⟩ ≠ 0
h_mem : ↑⟨x, hx✝⟩ ∈ convexBodyLT' K f w₀
⊢ ∃ a ∈ ↑I,
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧
        |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) :=
  LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (mixedEmbedding K).toRatAlgHom.toLinearMap ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ (mixedEmbedding K).toRatAlgHom ((integralBasis K) i) = (latticeBasis K) i

Tactic:
latticeBasis_apply

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) :=
  LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (mixedEmbedding K).toRatAlgHom.toLinearMap ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ (mixedEmbedding K).toRatAlgHom ((integralBasis K) i) = (mixedEmbedding K) ((integralBasis K) i)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx✝ : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
hx : x ∈ span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))
h_nz : ⟨x, hx✝⟩ ≠ 0
h_mem : ↑⟨x, hx✝⟩ ∈ convexBodySum K B
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
mem_span_fractionalIdealLatticeBasis

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx✝ : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
hx : x ∈ ⇑(mixedEmbedding K) '' ↑↑I
h_nz : ⟨x, hx✝⟩ ≠ 0
h_mem : ↑⟨x, hx✝⟩ ∈ convexBodySum K B
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ volume {x | x w = 0} = 0

Tactic:
by
  let A : AffineSubspace ℝ (realSpace K) :=
    Submodule.toAffineSubspace (Submodule.mk ⟨⟨{x | x w = 0}, by simp_all⟩, rfl⟩ (by simp_all))
  convert! Measure.addHaar_affineSubspace volume A fun h ↦ ?_
  simpa [A] using (h ▸ Set.mem_univ _ : 1 ∈ A)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K ≤ ↑(sqrt ↑N) * ↑(2 ^ rankOfDiscrBdd N)

Tactic:
ENNReal.coe_pow,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K ≤ ↑(sqrt ↑N) * ↑2 ^ rankOfDiscrBdd N
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : I = 0
⊢ I.FG

Tactic:
exact hI ▸ Submodule.fg_bot

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ (Submodule.map (Submodule.mkQ (Ideal.span {x})) I).FG

Tactic:
have := finiteQuotient (I := Ideal.span {x}) (by simp [hx₂])

Goal state after:
case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
this : Finite (R ⧸ Ideal.span {x})
⊢ (Submodule.map (Submodule.mkQ (Ideal.span {x})) I).FG
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_2.refine_2
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
x : K
hx : x ∈ ↑I
⊢ (IsLocalization.map W g hg) ((IsLocalization.map L f hf) x) = (IsLocalization.map W (g.comp f) ⋯) x

Tactic:
· 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
I : FractionalIdeal A⁰ K
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsIntegrallyClosed B
hI : ¬I ≤ 1
⊢ ¬(extendedHom L B) I ≤ 1

Tactic:
SetLike.not_le_iff_exists

Goal state after:
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
I : FractionalIdeal A⁰ K
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsIntegrallyClosed B
hI : ∃ x ∈ I, x ∉ 1
⊢ ∃ x ∈ (extendedHom L B) I, x ∉ 1
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: case inl
S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Finite (S ⧸ I)
⊢ absNorm (under ℤ I) ∣ absNorm I

Tactic:
have : Fintype (S ⧸ I) := Fintype.ofFinite (S ⧸ I)
    have h_main {d : ℕ} : (d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0 := by
      simp_rw [nsmul_eq_mul, ← map_natCast (Ideal.Quotient.mk I), ← Quotient.eq_zero_iff_mem]
      exact ⟨fun h _ ↦ by simp [h], fun h ↦ by simpa using h 1⟩
    rw [Ideal.absNorm_apply I, Submodule.cardQuot_apply, Nat.card_eq_fintype_card]
    simp_rw [absNorm_under_eq_sInf, h_main, ← AddMonoid.exponent_eq_sInf]
    exact AddGroup.exponent_dvd_card (G := S ⧸ I)

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
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h : (pB.basis.repr hζ.toInteger) ⟨1, hdim⟩ = (pB.basis.repr (↑p * x + ↑n)) ⟨1, hdim⟩
this : pB.basis ⟨1, hdim⟩ = pB.gen ^ ↑⟨1, hdim⟩
⊢ False

Tactic:
hζ.integralPowerBasisOfPrimePow_gen

Goal state after:
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
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h : (pB.basis.repr hζ.toInteger) ⟨1, hdim⟩ = (pB.basis.repr (↑p * x + ↑n)) ⟨1, hdim⟩
this : pB.basis ⟨1, hdim⟩ = hζ.toInteger ^ ↑⟨1, hdim⟩
⊢ False
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
x : L
⊢ (x ∈ if hI : I = 0 then 0 else ⟨(↑I)ᵛ, ⋯⟩) ↔ ∀ a ∈ I, ((traceForm K L) x) a ∈ (algebraMap A K).range

Tactic:
dif_neg hI

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
x : L
⊢ x ∈ ⟨(↑I)ᵛ, ⋯⟩ ↔ ∀ a ∈ I, ((traceForm K L) x) a ∈ (algebraMap A K).range
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
hI : I ≠ 0
hIJ : I * J ≤ 1
⊢ J ≤ if hI : I = 0 then 0 else ⟨(↑I)ᵛ, ⋯⟩

Tactic:
dif_neg hI

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
hI : I ≠ 0
hIJ : I * J ≤ 1
⊢ J ≤ ⟨(↑I)ᵛ, ⋯⟩
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: 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₂⟯
this : IsCyclotomicExtension {n₁ * n₂} ℚ ↥⊤
⊢ ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤

Tactic:
have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯

Goal state after:
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₂⟯
this✝ : IsCyclotomicExtension {n₁ * n₂} ℚ ↥⊤
this : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)
⊢ ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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
C : Type u_3
M : Type u_4
inst✝²¹ : CommRing C
inst✝²⁰ : IsDedekindDomain C
inst✝¹⁹ : Field M
inst✝¹⁸ : Algebra C M
inst✝¹⁷ : IsFractionRing C M
inst✝¹⁶ : Algebra A C
inst✝¹⁵ : Algebra B C
inst✝¹⁴ : Algebra A M
inst✝¹³ : Algebra B M
inst✝¹² : Algebra K M
inst✝¹¹ : Algebra L M
inst✝¹⁰ : IsScalarTower A C M
inst✝⁹ : IsScalarTower A K M
inst✝⁸ : IsScalarTower B C M
inst✝⁷ : IsScalarTower B L M
inst✝⁶ : IsScalarTower K L M
inst✝⁵ : IsIntegralClosure C A M
inst✝⁴ : FiniteDimensional K M
inst✝³ : FiniteDimensional L M
inst✝² : Algebra.IsSeparable K M
inst✝¹ : IsIntegralClosure C B M
inst✝ : Algebra.IsSeparable L M
x : L
hx : x ∈ dual A K 1
y : M
hy : y ∈ dual B L 1
⊢ x • y ∈ dual A K 1

Tactic:
simp only [ne_eq, one_ne_zero, not_false_eq_true, mem_dual, mem_one_iff, traceForm_apply,
    RingHom.mem_range, forall_exists_index, forall_apply_eq_imp_iff, mul_comm _ (algebraMap _ _ _),
    ← Algebra.smul_def] at hx hy ⊢

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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
C : Type u_3
M : Type u_4
inst✝²¹ : CommRing C
inst✝²⁰ : IsDedekindDomain C
inst✝¹⁹ : Field M
inst✝¹⁸ : Algebra C M
inst✝¹⁷ : IsFractionRing C M
inst✝¹⁶ : Algebra A C
inst✝¹⁵ : Algebra B C
inst✝¹⁴ : Algebra A M
inst✝¹³ : Algebra B M
inst✝¹² : Algebra K M
inst✝¹¹ : Algebra L M
inst✝¹⁰ : IsScalarTower A C M
inst✝⁹ : IsScalarTower A K M
inst✝⁸ : IsScalarTower B C M
inst✝⁷ : IsScalarTower B L M
inst✝⁶ : IsScalarTower K L M
inst✝⁵ : IsIntegralClosure C A M
inst✝⁴ : FiniteDimensional K M
inst✝³ : FiniteDimensional L M
inst✝² : Algebra.IsSeparable K M
inst✝¹ : IsIntegralClosure C B M
inst✝ : Algebra.IsSeparable L M
x : L
y : M
hx : ∀ (a : B), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K L) (a • x)
hy : ∀ (a : C), ∃ x, (algebraMap B L) x = (Algebra.trace L M) (a • y)
⊢ ∀ (a : C), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K M) (a • x • y)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case prime_pow
p k : ℕ
hp : Nat.Prime p
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ k)
this✝ : NumberField K
this : Fact (Nat.Prime p)
⊢ ℤ[hζ.toInteger] = ℤ[hζ.integralPowerBasisOfPrimePow.gen]

Tactic:
hζ.integralPowerBasisOfPrimePow_gen

Goal state after:
case prime_pow
p k : ℕ
hp : Nat.Prime p
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ k)
this✝ : NumberField K
this : Fact (Nat.Prime p)
⊢ ℤ[hζ.toInteger] = ℤ[hζ.toInteger]
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: 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
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this✝⁴ : NumberField K
this✝³ : NeZero n₁
this✝² : NeZero n₂
this✝¹ : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : ℤ[hζ₁.toInteger] = ⊤
this✝ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : ℤ[hζ₂.toInteger] = ⊤
this : IsCyclotomicExtension {n₁ * n₂} ℚ ↥⊤
⊢ ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤

Tactic:
have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯

Goal state after:
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
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this✝⁵ : NumberField K
this✝⁴ : NeZero n₁
this✝³ : NeZero n₂
this✝² : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : ℤ[hζ₁.toInteger] = ⊤
this✝¹ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : ℤ[hζ₂.toInteger] = ⊤
this✝ : IsCyclotomicExtension {n₁ * n₂} ℚ ↥⊤
this : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)
⊢ ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : AddSubgroup (Additive (𝓞 K)ˣ)
⊢ AddSubgroup.map (logEmbedding K) (s ⊔ Subgroup.toAddSubgroup (torsion K)) = AddSubgroup.map (logEmbedding K) s

Tactic:
by
  rw [← logEmbedding_ker, AddSubgroup.map_eq_map_iff, sup_right_idem]

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

Goal state before:
pp: a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rcases cube_of_not_dvd hdvd.1.1 with ha | ha

Goal state after:
case inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

case inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a b : ℤ
⊢ legendreSym p (a * b) = legendreSym p a * legendreSym p b

Tactic:
by
  simp [legendreSym, Int.cast_mul, map_mul]

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

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

Tactic:
dsimp only [legendreSym]
  rw [Int.cast_pow]
  exact quadraticChar_sq_one' ha

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

Goal state before:
pp: case neg.refine_2
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 A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
⊢ ∀ (x y : L), (Algebra.trace K L) x ∈ ↑p → (Algebra.trace K L) y ∈ ↑p → (Algebra.trace K L) (x + y) ∈ ↑p

Tactic:
simp only [map_add]

Goal state after:
case neg.refine_2
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 A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
⊢ ∀ (x y : L),
    (Algebra.trace K L) x ∈ ↑p → (Algebra.trace K L) y ∈ ↑p → (Algebra.trace K L) x + (Algebra.trace K L) y ∈ ↑p
Module: Mathlib.NumberTheory.LucasPrimality

Goal state before:
pp: p : ℕ
hP : Nat.Prime p
⊢ ∃ a, a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1

Tactic:
have : Fact p.Prime := ⟨hP⟩
  obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := (ZMod p)ˣ)
  have h1 : orderOf g = p - 1 := by
    rwa [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card,
      ← Nat.prime_iff_card_units]
  have h2 := tsub_pos_iff_lt.2 hP.one_lt
  rw [← orderOf_injective (Units.coeHom _) Units.val_injective _, orderOf_eq_iff h2] at h1
  refine ⟨g, h1.1, fun q hq hqd ↦ ?_⟩
  replace hq := hq.one_lt
  exact h1.2 _ (Nat.div_lt_self h2 hq) (Nat.div_pos (Nat.le_of_dvd h2 hqd) (zero_lt_one.trans hq))

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case neg
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ n.Coprime b

Tactic:
· rw [show n = 1 by lia]
    simp

Goal state after: