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

Goal state before:
pp: case inr.hi
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
chn0 : ringChar k ≠ 0
d : ℕ
ih_d :
  ∀ m ≤ d,
    ∀ {a b c : k[X]},
      C u * a ^ p + C v * b ^ q + C w * c ^ r = 0 → a ≠ 0 → b ≠ 0 → c ≠ 0 → IsCoprime a b → a.natDegree = m → m = 0
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
⊢ d + 1 = 0

Tactic:
obtain ⟨ad, bd, cd⟩ := flt_catalan_deriv
        hp hq hr hineq chp chq chr ha hb hc hab hu hv hw heq
      -- find contracts `ca, cb, cc` so that `a(k) = ca(k^ch)`
      obtain ⟨ca, ca_nz, eq_a, eq_deg_a⟩ := find_contract ha ad chn0
      obtain ⟨cb, cb_nz, eq_b, eq_deg_b⟩ := find_contract hb bd chn0
      obtain ⟨cc, cc_nz, eq_c, eq_deg_c⟩ := find_contract hc cd chn0
      set ch := ringChar k
      suffices hca : ca.natDegree = 0 by
        rw [← eq_d, eq_deg_a, hca, zero_mul]
      by_contra hnca; apply hnca
      apply ih_d _ _ _ ca_nz cb_nz cc_nz <;> clear ih_d <;> try rfl
      · apply (isCoprime_expand chn0).mp
        rwa [← eq_a, ← eq_b]
      · have _ : ch ≠ 1 := CharP.ringChar_ne_one
        have hch2 : 2 ≤ ch := by lia
        rw [← add_le_add_iff_right 1, ← eq_d, eq_deg_a]
        grw [← hch2]
        lia
      · rw [eq_a, eq_b, eq_c, ← expand_C ch u, ← expand_C ch v, ← expand_C ch w] at heq
        simp_rw [← map_pow, ← map_mul, ← map_add] at heq
        rwa [Polynomial.expand_eq_zero (zero_lt_iff.mpr chn0)] at heq

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ (canonicalEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
rw [← Basis.sum_repr (integralBasis K) x, map_sum]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1, (canonicalEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))
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
⊢ (w.comap ↑f).IsReal ↔ w.IsReal

Tactic:
rw [← mk_embedding w, comap_mk, isReal_mk_iff, isReal_mk_iff, ComplexEmbedding.isReal_comp_iff]

Goal state after:
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✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset =
    (Fintype.card ↑(MulAction.orbit Gal(K/k) w) * if IsUnramified k w then 1 else 2) / 2

Tactic:
if_neg,

Goal state after:
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Fintype.card ↑(MulAction.orbit Gal(K/k) w) * 2 / 2

case hnc
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ ¬IsUnramified k w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ (mixedEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
rw [← Basis.sum_repr (integralBasis K) x, map_sum]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1, (mixedEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_bd :
  ↑|(Algebra.norm ℚ) ↑x| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
⊢ 1 ≤ |(Algebra.norm ℤ) x|

Tactic:
exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr h_nz)

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)
⊢ (intNorm A B) 0 = 0

Tactic:
have : IsIntegralClosure B A (FractionRing B) :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
  apply IsFractionRing.injective A (FractionRing A)
  simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4) < ↑(finrank ℚ K)
⊢ ↑↑N < 4 / 9 * (3 * π / 4) ^ finrank ℚ K

Tactic:
rw [← Real.rpow_natCast]

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4) < ↑(finrank ℚ K)
⊢ ↑↑N < 4 / 9 * (3 * π / 4) ^ ↑(finrank ℚ K)
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: case pos
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
⊢ x ∣ (algebraMap A B) ((intNorm A B) x)

Tactic:
exact ⟨1, by simp [hx]⟩

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.IsPrime
inst✝¹⁴ : P.LiesOver p
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : Finite G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : IsGaloisGroup G A B
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : FaithfulSMul B C
inst✝⁴ : IsScalarTower A B C
GAC : Type u_5
inst✝³ : Group GAC
inst✝² : Finite GAC
inst✝¹ : MulSemiringAction GAC C
inst✝ : IsGaloisGroup GAC A C
this✝² : Algebra.IsIntegral A C
this✝¹ : Algebra.IsIntegral B C
f : GAC →* G := restrictHom GAC G A B C
H : Subgroup GAC := Subgroup.comap f (stabilizer G P)
key : ∀ (Q Q' : Ideal C) [Q.LiesOver P] [Q'.LiesOver P] (g : GAC), g • Q = Q' → g ∈ H
Q : Ideal C
left✝¹ : Q.IsPrime
right✝¹ : Q.LiesOver P
this✝ : Q.LiesOver p
Q' : Ideal C
left✝ : Q'.IsPrime
right✝ : Q'.LiesOver P
this : Q'.LiesOver p
g : GAC
hg : Q' = g • Q
⊢ (fun m ↦ m • Q) ⟨g, ⋯⟩ = Q'

Tactic:
by simpa [Subgroup.smul_def] using hg.symm

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

Goal state before:
pp: case a
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
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) (R ⧸ p) (S ⧸ pS) := ⋯
b' : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS) → S
hb' : ∀ (i : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)), (Ideal.Quotient.mk pS) (b' i) = b i
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' Set.range b') = ⊤

Tactic:
← Set.range_comp,

Goal state after:
case a
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
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) (R ⧸ p) (S ⧸ pS) := Free.chooseBasis (R ⧸ p) (S ⧸ pS)
b' : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS) → S
hb' : ∀ (i : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)), (Ideal.Quotient.mk pS) (b' i) = b i
⊢ span (R ⧸ p) (Set.range (⇑(Ideal.Quotient.mk pS) ∘ b')) = ⊤
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case a
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : (algebraMap R A) c = a M * b M'
hu : ∀ (i : Ideal R), i ≠ M' ∧ i ∈ s → u M' ∈ i
⊢ (algebraMap R A) (u M' * c) ∈ IsLocalization.coeSubmodule A M

Tactic:
exact Submodule.mem_map_of_mem <| M.mul_mem_right _ <| hu M ⟨hM'.1.symm, hM⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : IsDomain T
inst✝⁵ : Algebra R S
P : Ideal R
inst✝⁴ : P.IsPrime
inst✝³ : FaithfulSMul R S
inst✝² : Algebra S T
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ IsLocalization (algebraMapSubmonoid T P') Tₚ

Tactic:
rw [show algebraMapSubmonoid T P' = P'' by simp]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : IsDomain T
inst✝⁵ : Algebra R S
P : Ideal R
inst✝⁴ : P.IsPrime
inst✝³ : FaithfulSMul R S
inst✝² : Algebra S T
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ IsLocalization P'' Tₚ
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: 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
r : S
x : R
hx : x ∈ ⇑(Algebra.intNorm R S) '' ↑(span {r})
⊢ (Algebra.intNorm R S) r ∣ x

Tactic:
obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx

Goal state after:
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
r x : S
hx' : x ∈ ↑(span {r})
hx : (Algebra.intNorm R S) x ∈ ⇑(Algebra.intNorm R S) '' ↑(span {r})
⊢ (Algebra.intNorm R S) r ∣ (Algebra.intNorm R S) x
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: 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
I : Ideal S
T : Type u_4
inst✝ : Semiring T
f : R →+* T
⊢ map f (spanNorm R I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)

Tactic:
spanNorm

Goal state after:
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
I : Ideal S
T : Type u_4
inst✝ : Semiring T
f : R →+* T
⊢ map f (map (Algebra.intNorm R S) I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: 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
I J : Ideal S
⊢ map (Algebra.intNorm R S) I * map (Algebra.intNorm R S) J ≤ spanNorm R (I * J)

Tactic:
spanNorm

Goal state after:
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
I J : Ideal S
⊢ map (Algebra.intNorm R S) I * map (Algebra.intNorm R S) J ≤ map (Algebra.intNorm R S) (I * J)
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₂
⊢ ∃ y, (algebraMap B L) y = (algebraMap B L) ((algebraMap R₂ B) ((Free.chooseBasis A R₂) i))

Tactic:
exact ⟨_, rfl⟩

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} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ (algebraMap (𝓞 K) K) ((adjoin.powerBasis' ⋯).map hζ.adjoinEquivRingOfIntegersOfPrimePow).gen = ↑hζ.toInteger

Tactic:
PowerBasis.map_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} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ (algebraMap (𝓞 K) K) (hζ.adjoinEquivRingOfIntegersOfPrimePow (adjoin.powerBasis' ⋯).gen) = ↑hζ.toInteger
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✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ ∃ y, (algebraMap B L) y = (Algebra.linearMap B L) x

Tactic:
exact ⟨_, rfl⟩

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

Goal state before:
pp: case refine_3
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : ↑p ∣ 2
⊢ p ∣ 2

Tactic:
exact Int.ofNat_dvd.mp h

Goal state after:
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
⊢ ℤ[hζ.toInteger] = ⊤

Tactic:
have : Fact (p.Prime) := ⟨hp⟩
    rw [← hζ.integralPowerBasisOfPrimePow.adjoin_gen_eq_top, hζ.integralPowerBasisOfPrimePow_gen]

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

Goal state before:
pp: n : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : NeZero n
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ (algebraMap (𝓞 K) K) ((adjoin.powerBasis' ⋯).map hζ.adjoinEquivRingOfIntegers).gen = ↑hζ.toInteger

Tactic:
PowerBasis.map_gen,

Goal state after:
n : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : NeZero n
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ (algebraMap (𝓞 K) K) (hζ.adjoinEquivRingOfIntegers (adjoin.powerBasis' ⋯).gen) = ↑hζ.toInteger
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : Additive (𝓞 K)ˣ
⊢ x ∈ (logEmbedding K).ker ↔ x ∈ Subgroup.toAddSubgroup (torsion K)

Tactic:
rw [AddMonoidHom.mem_ker, ← ofMul_toMul x, logEmbedding_eq_zero_iff]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : Additive (𝓞 K)ˣ
⊢ Additive.toMul x ∈ torsion K ↔ Additive.ofMul (Additive.toMul x) ∈ Subgroup.toAddSubgroup (torsion K)
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: case neg
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : Finite M₀
a : M₀
h : ¬IsUnit a
⊢ orderOf a < Nat.card M₀

Tactic:
orderOf_eq_zero_iff'.mpr fun n hn ha ↦ h <| IsUnit.of_pow_eq_one ha hn.ne'

Goal state after:
case neg
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : Finite M₀
a : M₀
h : ¬IsUnit a
⊢ 0 < Nat.card M₀
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℤ (Additive (𝓞 K)ˣ) = rank K

Tactic:
by
  simpa [← finrank_modTorsion] using! finrank_quotient_torsion_eq.symm

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

Goal state before:
pp: case pos
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 = ⊥
⊢ ¬P ∣ differentIdeal A B

Tactic:
subst hp
    simp only [Ideal.map_bot, Ideal.mul_eq_bot] at hP
    obtain (rfl | rfl) := hP
    · rw [← Ideal.zero_eq_bot, zero_dvd_iff]
      exact differentIdeal_ne_bot
    · obtain rfl := hxQ
      simp at hx

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

Goal state before:
pp: case neg
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 : differentIdeal A B * Q ≤ Ideal.map (algebraMap A B) p
⊢ False

Tactic:
replace H := (FractionalIdeal.coeIdeal_le_coeIdeal' _ (P := L) le_rfl).mpr H

Goal state after:
case neg
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 : ↑(differentIdeal A B * Q) ≤ ↑(Ideal.map (algebraMap A B) p)
⊢ False
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) ≤ ↑(∑ i ∈ (m * k).divisors, i) / ↑k

Tactic:
le_div_iff₀ (by grind [cast_pos]),

Goal state after:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ ↑(∑ i ∈ m.divisors, i) * ↑k ≤ ↑(∑ i ∈ (m * k).divisors, i)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with H | H | H
  · contradiction
  · left
    exact lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ H
  · right
    exact lambda_pow_four_dvd_cube_add_one_of_dvd_add_one hζ H

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

Goal state before:
pp: case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a → ∃ y, ↑y * ↑y = a

Tactic:
rintro ⟨y, rfl⟩
    have hy : y ≠ 0 := by
      rintro rfl
      simp [mul_zero, ne_eq] at ha
    refine ⟨Units.mk0 y hy, ?_⟩; simp

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

Goal state before:
pp: case neg.refine_1.mem
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
y✝ : B
x : L
hx : x ∈ FractionalIdeal.dual A K 1
y : A
hy : y ∈ ↑p
⊢ (Algebra.trace K L) (x * (Algebra.linearMap B L) ((algebraMap A B) y)) ∈ ↑p

Tactic:
obtain ⟨z, hz⟩ :=
        (FractionalIdeal.mem_dual (by simp)).mp hx 1 ⟨1, trivial, (algebraMap B L).map_one⟩

Goal state after:
case neg.refine_1.mem
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
y✝ : B
x : L
hx : x ∈ FractionalIdeal.dual A K 1
y : A
hy : y ∈ ↑p
z : A
hz : (algebraMap A K) z = ((traceForm K L) x) 1
⊢ (Algebra.trace K L) (x * (Algebra.linearMap B L) ((algebraMap A B) y)) ∈ ↑p