mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
ca' : k
ha : d ≠ 0 ∧ ca' ≠ 0
ha' : C ca' = a'
cb' : k
hb' : C cb' = b'
cc' : k
hc' : C cc' = c'
⊢ IsUnit (C ca') ∧ IsUnit (C cb') ∧ IsUnit (C cc')

Tactic:
← hb',

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
ca' : k
ha : d ≠ 0 ∧ ca' ≠ 0
ha' : C ca' = a'
cb' : k
hb : d ≠ 0 ∧ C cb' ≠ 0
hb' : C cb' = b'
cc' : k
hc' : C cc' = c'
⊢ IsUnit (C ca') ∧ IsUnit (C cb') ∧ IsUnit (C cc')
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
ca' : k
ha : d ≠ 0 ∧ ca' ≠ 0
ha' : C ca' = a'
cb' : k
hb : d ≠ 0 ∧ cb' ≠ 0
hb' : C cb' = b'
cc' : k
hc' : C cc' = c'
⊢ IsUnit (C ca') ∧ IsUnit (C cb') ∧ IsUnit (C cc')

Tactic:
rw [← hc', C_ne_zero] at hc

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
eq_c : c = c' * d
ca' : k
ha : d ≠ 0 ∧ ca' ≠ 0
ha' : C ca' = a'
cb' : k
hb : d ≠ 0 ∧ cb' ≠ 0
hb' : C cb' = b'
cc' : k
hc : d ≠ 0 ∧ cc' ≠ 0
hc' : C cc' = c'
⊢ IsUnit (C ca') ∧ IsUnit (C cb') ∧ IsUnit (C cc')
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ volume {a | |a.1| < 1 ∧ |a.2| < ↑B ^ 2} = 4 * ↑B ^ 2

Tactic:
show {a : ℝ × ℝ | |a.1| < 1 ∧ |a.2| < B ^ 2} =
        Set.Ioo (-1 : ℝ) (1 : ℝ) ×ˢ Set.Ioo (-(B : ℝ) ^ 2) ((B : ℝ) ^ 2) by
          ext; simp_rw [Set.mem_ofPred_eq, Set.mem_prod, Set.mem_Ioo, abs_lt]

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ volume (Set.Ioo (-1) 1 ×ˢ Set.Ioo (-↑B ^ 2) (↑B ^ 2)) = 4 * ↑B ^ 2
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)

Tactic:
← isReal_mk_iff,

Goal state after:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
⊢ (mk (w.embedding.comp f)).IsReal
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
hw : ComplexEmbedding.IsReal (w.embedding.comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal w.embedding

Tactic:
← isReal_mk_iff,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
hw : (mk (w.embedding.comp (algebraMap k K))).IsReal
⊢ ComplexEmbedding.IsReal w.embedding
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
hw : IsSelfAdjoint (w.embedding.comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)

Tactic:
← isReal_mk_iff,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
hw : (mk (w.embedding.comp (algebraMap k K))).IsReal
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ : K →+* ℂ
⊢ IsUnramified k (mk φ) ↔ ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1

Tactic:
refine ⟨fun H σ hσ ↦ hσ.isUnramified_mk_iff.mp H,
    fun H ↦ ?_⟩

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
⊢ IsUnramified k (mk φ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
⊢ mixedEmbedding.norm (fun x ↦ c, fun x ↦ ↑c) = |c| ^ finrank ℚ K

Tactic:
rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, norm_smul, map_one,
    mul_one]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ fundamentalDomain (stdBasis K) =
    (Set.univ.pi fun x ↦ Set.Ico 0 1) ×ˢ Set.univ.pi fun x ↦ ⇑measurableEquivPi ⁻¹' Set.univ.pi fun x ↦ Set.Ico 0 1

Tactic:
ext
  simp [stdBasis, mem_fundamentalDomain, Complex.measurableEquivPi]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ (latticeBasis K) i = (mixedEmbedding K) ((integralBasis K) i)

Tactic:
simp only [latticeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, Function.comp_apply,
    canonicalEmbedding.latticeBasis_apply, integralBasis_apply, commMap_canonical_eq_mixed]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ ‖((negAt s) x).2 ⟨w, hw⟩‖ = ‖x.2 ⟨w, hw⟩‖

Tactic:
negAt_apply_isComplex

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
⊢ (normAtPlace w) ((negAt s) x) = (normAtPlace w) x

Tactic:
by
  obtain hw | hw := isReal_or_isComplex w
  · simp_rw [normAtPlace_apply_of_isReal hw, negAt_apply_norm_isReal]
  · simp_rw [normAtPlace_apply_of_isComplex hw, negAt_apply_isComplex]

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

Goal state before:
pp: case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ ↑(m + 1) ^ (m * 2) * ↑(m + 1) * ↑(m + 1) /
      ((4 / π) ^ m * (4 / π) * (↑(m + 1).factorial ^ 0 * ↑(m + 1).factorial * ↑(m + 1).factorial)) =
    ↑m ^ (m * 2) / ((4 / π) ^ m * (↑m.factorial ^ 0 * ↑m.factorial * ↑m.factorial)) * (1 + 1 / ↑m) ^ (2 * m) / (4 / π)

Tactic:
Nat.factorial_succ

Goal state after:
case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ ↑(m + 1) ^ (m * 2) * ↑(m + 1) * ↑(m + 1) /
      ((4 / π) ^ m * (4 / π) * (↑((m + 1) * m.factorial) ^ 0 * ↑((m + 1) * m.factorial) * ↑((m + 1) * m.factorial))) =
    ↑m ^ (m * 2) / ((4 / π) ^ m * (↑m.factorial ^ 0 * ↑m.factorial * ↑m.factorial)) * (1 + 1 / ↑m) ^ (2 * m) / (4 / π)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ ↑(m + 1) ^ (m * 2) * ↑(m + 1) * ↑(m + 1) /
      ((4 / π) ^ m * (4 / π) * (↑((m + 1) * m.factorial) ^ 0 * ↑((m + 1) * m.factorial) * ↑((m + 1) * m.factorial))) =
    ↑m ^ (m * 2) / ((4 / π) ^ m * (↑m.factorial ^ 0 * ↑m.factorial * ↑m.factorial)) * (1 + 1 / ↑m) ^ (2 * m) / (4 / π)

Tactic:
field_simp

Goal state after:
case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ ↑(m + 1) ^ (m * 2) * ↑(m + 1) ^ 2 * ↑m.factorial ^ 2 =
    ↑((m + 1) * m.factorial) ^ 2 * ↑m ^ (m * 2) * ((↑m + 1) / ↑m) ^ (2 * m)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_2.inr.refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ A
hx : ∀ (a : { w // w.IsReal }), ¬x.1 a = 0
w : { w // w.IsReal }
hw : w ∈ signSet x
⊢ x.1 w < 0

pp: case refine_2.inr.refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ A
hx : ∀ (a : { w // w.IsReal }), ¬x.1 a = 0
w : { w // w.IsReal }
hw : w ∉ signSet x
⊢ x.1 w > 0

Tactic:
· exact lt_of_le_of_ne hw (hx w)

Goal state after:
case refine_2.inr.refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ A
hx : ∀ (a : { w // w.IsReal }), ¬x.1 a = 0
w : { w // w.IsReal }
hw : w ∉ signSet x
⊢ x.1 w > 0
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case convert_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a m * (1 + 1 / ↑m) ^ (2 * m) / (4 / π)

Tactic:
rw [_root_.le_div_iff₀ (by positivity), pow_succ]
          convert! (mul_le_mul h_m this (by positivity) (by positivity)) using 1
          field

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : IsDomain A
p : Ideal A
inst✝⁹ : p.IsPrime
B : Type u_2
inst✝⁸ : CommRing B
inst✝⁷ : IsDomain B
inst✝⁶ : Algebra A B
inst✝⁵ : Module.Finite A B
inst✝⁴ : Flat A B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
⊢ (p.primesOver B).ncard * (p.ramificationIdxIn B * p.inertiaDegIn B) = Nat.card G

Tactic:
have : Fintype (primesOver p B) := (QuasiFinite.finite_primesOver p).fintype
  rw [← smul_eq_mul, ← Set.fintypeCard_eq_ncard, ← Finset.card_univ, ← Finset.sum_const,
    ← sum_ramification_inertia_eq_card p B]
  apply Finset.sum_congr rfl
  intro P hp
  rw [ramificationIdxIn_eq_ramificationIdx p P G, inertiaDegIn_eq_inertiaDeg p P G]

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

Goal state before:
pp: case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ IsIntegral A ((toAlgHom A L E) (((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x)))

Tactic:
coe_toAlgHom',

Goal state after:
case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ IsIntegral A ((algebraMap L E) (((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x)))
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ ¬minpoly K ((algebraMap B L) x) = 0 ∧ (aeval ((algebraMap B E) x)) (minpoly K ((algebraMap B L) x)) = 0

Tactic:
refine ⟨minpoly.ne_zero (IsIntegral.isIntegral _), ?_⟩

Goal state after:
case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ (aeval ((algebraMap B E) x)) (minpoly K ((algebraMap B L) x)) = 0
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 ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ Function.Injective ⇑(algebraMap R Sₚ)

Tactic:
rw [IsScalarTower.algebraMap_eq R S Sₚ]

Goal state after:
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 ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ Function.Injective ⇑((algebraMap S Sₚ).comp (algebraMap R S))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: L : Type u_3
inst✝⁶ : Field L
K₁ : Type u_4
K₂ : Type u_5
inst✝⁵ : Field K₁
inst✝⁴ : NumberField K₁
inst✝³ : Field K₂
inst✝² : NumberField K₂
inst✝¹ : Algebra K₁ L
inst✝ : Algebra K₂ L
h : IsCoprime (discr K₁) (discr K₂)
⊢ IsCoprime (Ideal.map (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
    (Ideal.map (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))

Tactic:
obtain ⟨u, v, h⟩ := h

Goal state after:
L : Type u_3
inst✝⁶ : Field L
K₁ : Type u_4
K₂ : Type u_5
inst✝⁵ : Field K₁
inst✝⁴ : NumberField K₁
inst✝³ : Field K₂
inst✝² : NumberField K₂
inst✝¹ : Algebra K₁ L
inst✝ : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ IsCoprime (Ideal.map (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
    (Ideal.map (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_4
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✝³ : FiniteDimensional K L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_3
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι K L
hb : restrictScalars A I = span A (Set.range ⇑b)
⊢ restrictScalars A Iᵛ = span A (Set.range ⇑b.traceDual)

Tactic:
rw [restrictScalars_traceDual, hb]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_4
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✝³ : FiniteDimensional K L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_3
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι K L
hb : restrictScalars A I = span A (Set.range ⇑b)
⊢ (traceForm K L).dualSubmodule (span A (Set.range ⇑b)) = span A (Set.range ⇑b.traceDual)
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg
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
h : ¬restrictScalars A (Algebra.trace K L).range ≤ 1
⊢ ⊤ᵛ = ⊥

Tactic:
· simp only [SetLike.le_def, restrictScalars_mem, LinearMap.mem_range, mem_one,
      forall_exists_index, forall_apply_eq_imp_iff, not_forall, not_exists] at h
    obtain ⟨b, hb⟩ := h
    simp_rw [eq_bot_iff, SetLike.le_def, mem_bot, mem_traceDual, mem_top, true_implies,
      traceForm_apply, RingHom.mem_range]
    contrapose! hb with hx'
    obtain ⟨c, hc, hc0⟩ := hx'
    simpa [hc0] using hc (c⁻¹ * b)

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))
⊢ hζ.toInteger - 1 ∣ ↑p

Tactic:
by_cases htwo : p ^ (k + 1) = 2

Goal state after:
case pos
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
⊢ hζ.toInteger - 1 ∣ ↑p

case neg
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
⊢ hζ.toInteger - 1 ∣ ↑p
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
μ : ↥ℚ⟮ζ⟯
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
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
hq' : ¬q = 2
⊢ ↑p ∣ ↑q ^ Module.finrank (↥ℚ⟮ζ⟯) K

Tactic:
hμ.norm_toInteger_sub_one_of_prime_ne_two hq'

Goal state after:
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
μ : ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
q : ℕ
hp : ↑p ∣ ↑q ^ Module.finrank (↥ℚ⟮ζ⟯) K
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
hq' : ¬q = 2
⊢ ↑p ∣ ↑q ^ Module.finrank (↥ℚ⟮ζ⟯) K
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₁
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))

Tactic:
have h_div₂ := prod_primeFactors_pow_totient_ediv_dvd n₂.pos_of_neZero

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₂
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))