mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : 2 < n
this : NumberField K
⊢ IsTotallyComplex K

Tactic:
exact nrRealPlaces_eq_zero_iff.mp <| nrRealPlaces_eq_zero K hn

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
hI : I.FG
inst✝ : Finite (R ⧸ I)
n : ℕ
a✝ : Finite (R ⧸ I ^ n)
⊢ Finite (R ⧸ I ^ (n + 1))

Tactic:
| succ n _ =>

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

Goal state before:
pp: case refine_1.refine_3
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 J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ (IsLocalization.map L f hf) (a • y) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Tactic:
rw [Algebra.smul_def, map_mul, map_eq, ← Algebra.smul_def]

Goal state after:
case refine_1.refine_3
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 J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ f a • (IsLocalization.map L f hf) y ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
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
x : L
hx : x ∈ ↑(extended L hf I)
hx' : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
z : K
hz : z ∈ ↑I
⊢ (IsLocalization.map W (g.comp f) ⋯) z = (IsLocalization.map W g hg) ((IsLocalization.map L f hf) z)

Tactic:
rw [IsLocalization.map_map]

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
inst✝¹ : Free R S
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι R S
⊢ Fintype.card ι = finrank R S

Tactic:
finrank_eq_card_basis b

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
inst✝¹ : Free R S
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι R S
⊢ Fintype.card ι = Fintype.card ι
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.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
⊢ P = span {x}

Tactic:
by_cases hP0 : P = ⊥

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : P = ⊥
⊢ P = span {x}

case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
⊢ P = span {x}
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case refine_2
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := (Algebra.traceForm ℚ K).dualBasis ⋯ b
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ Submodule.toAddSubgroup 1 = AddSubgroup.closure (Set.range ⇑b)

Tactic:
apply AddSubgroup.toIntSubmodule.injective

Goal state after:
case refine_2
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := ⋯
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := ⋯
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ AddSubgroup.toIntSubmodule (Submodule.toAddSubgroup 1) =
    AddSubgroup.toIntSubmodule (AddSubgroup.closure (Set.range ⇑b))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case refine_3
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := (Algebra.traceForm ℚ K).dualBasis ⋯ b
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ (↑(FractionalIdeal.dual ℤ ℚ 1)).toAddSubgroup = AddSubgroup.closure (Set.range ⇑b')

Tactic:
apply AddSubgroup.toIntSubmodule.injective

Goal state after:
case refine_3
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := ⋯
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := ⋯
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ AddSubgroup.toIntSubmodule (↑(FractionalIdeal.dual ℤ ℚ 1)).toAddSubgroup =
    AddSubgroup.toIntSubmodule (AddSubgroup.closure (Set.range ⇑b'))
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case inr
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Tactic:
by_cases hP0 : P = ⊥

Goal state after:
case pos
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : P = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

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

Tactic:
← lcoeff_apply,

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
⊢ (lcoeff ℤ i) (∑ i ∈ range p, ↑(p.choose (i + 1)) * X ^ i) ∈ ℤ ∙ ↑p
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝ : p.IsPrime
hp : ¬p = ⊥
h : p ^ finrank R S ≤ (relNorm R) P
⊢ ∃ s, (relNorm R) P = p ^ s

Tactic:
← dvd_iff_le,

Goal state after:
case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝ : p.IsPrime
hp : ¬p = ⊥
h : (relNorm R) P ∣ p ^ finrank R S
⊢ ∃ s, (relNorm R) P = p ^ s
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
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝ : p.IsPrime
hp : ¬p = ⊥
s : ℕ
left✝ : s ≤ finrank R S
hs : Associated ((relNorm R) P) (p ^ s)
⊢ (relNorm R) P = p ^ s

Tactic:
rwa [associated_iff_eq] at hs

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

Goal state before:
pp: case refine_2
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
inst✝ : IsTorsionFree B C
this : IsLocalization (algebraMapSubmonoid C B⁰) M
h : B⁰ ≤ Submonoid.comap (algebraMap B C) C⁰
h_alg : ∀ {x : L}, (algebraMap L M) x = (IsLocalization.map M (algebraMap B C) h) x
⊢ dual B L 1 * (extendedHom M C) (dual A K 1) ≤ dual A K 1

Tactic:
· rw [← FractionalIdeal.coe_le_coe, coe_mul, extendedHom'_apply,
      coe_extended_eq_span, ← span_eq (coeToSubmodule _), span_mul_span, span_le]
    rintro _ ⟨a, ha, _, ⟨b, hb, rfl⟩, rfl⟩
    simp only [SetLike.mem_coe, mem_coe, ← h_alg, mul_comm a, ← Algebra.smul_def] at ha hb ⊢
    exact smul_mem_dual_one A K L B C M hb ha

Goal state after:
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✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : IsTorsionFree A B
x : B
hx : K[(algebraMap B L) x] = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
y : L
hne₁ : (aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))) ≠ 0
⊢ (algebraMap B L) ((aeval x) (derivative (minpoly A x))) ≠ 0

Tactic:
minpoly.isIntegrallyClosed_eq_field_fractions K L hAx,

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✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : IsTorsionFree A B
x : B
hx : K[(algebraMap B L) x] = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
y : L
hne₁ : (aeval ((algebraMap B L) x)) (derivative (Polynomial.map (algebraMap A K) (minpoly A x))) ≠ 0
⊢ (algebraMap B L) ((aeval x) (derivative (minpoly A x))) ≠ 0
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✝²¹ : IsDomain A
inst✝²⁰ : IsDedekindDomain B
inst✝¹⁹ : IsDedekindDomain R₁
inst✝¹⁸ : IsDedekindDomain R₂
inst✝¹⁷ : IsFractionRing B L
inst✝¹⁶ : IsFractionRing R₁ ↥F₁
inst✝¹⁵ : IsFractionRing R₂ ↥F₂
inst✝¹⁴ : IsIntegrallyClosed A
inst✝¹³ : IsIntegralClosure B R₁ L
inst✝¹² : IsTorsionFree R₁ B
inst✝¹¹ : IsTorsionFree R₂ B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Module.Finite A B
inst✝⁸ : IsTorsionFree A B
inst✝⁷ : IsTorsionFree A R₁
inst✝⁶ : IsTorsionFree A R₂
inst✝⁵ : Module.Finite A R₁
inst✝⁴ : Module.Finite R₂ B
inst✝³ : IsScalarTower A R₂ B
inst✝² : Module.Finite R₁ B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝ : IsScalarTower A R₁ B
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))
ι : Type u_7
b : Basis ι A R₂
i : ι
⊢ (ofIsCoprimeDifferentIdeal A B R₁ R₂ h₁ h₂ h₃ b) i = (algebraMap R₂ B) (b i)

Tactic:
simp [Module.Basis.ofIsCoprimeDifferentIdeal]

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

Goal state before:
pp: case inr.refine_2
n : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : NeZero n
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑↑μ) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      (algebraMap (𝓞 K) K) ↑↑μ ^ (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this✝¹ : NeZero (n.lcm (torsionOrder K))
this✝ : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Odd n
this : 2 * n = n.lcm (torsionOrder K)
⊢ torsionOrder K = 2 * n

pp: case inr.refine_1
n : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : NeZero n
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑↑μ) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      (algebraMap (𝓞 K) K) ↑↑μ ^ (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this✝ : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Odd n
⊢ ¬n = n.lcm (torsionOrder K)

Tactic:
· rw [this, eq_comm, Nat.lcm_eq_right_iff_dvd]
      exact dvd_torsionOrder_of_isPrimitiveRoot hζ

Goal state after:
case inr.refine_1
n : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : NeZero n
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑↑μ) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      (algebraMap (𝓞 K) K) ↑↑μ ^ (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this✝ : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Odd n
⊢ ¬n = n.lcm (torsionOrder K)
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ a₂✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
h :
  (MonoidHom.toAdditiveLeft
        ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))).comp
          (QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom))
      a₁✝ =
    (MonoidHom.toAdditiveLeft
        ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))).comp
          (QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom))
      a₂✝
⊢ a₁✝ = a₂✝

Tactic:
simp_rw [MonoidHom.toAdditiveLeft_apply_apply, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom,
    Function.comp_apply, EmbeddingLike.apply_eq_iff_eq] at h

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ a₂✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
h :
  (QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K)))
      ((QuotientGroup.quotientMulEquivOfEq ⋯) (Additive.toMul a₁✝)) =
    (QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K)))
      ((QuotientGroup.quotientMulEquivOfEq ⋯) (Additive.toMul a₂✝))
⊢ a₁✝ = a₂✝
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ AddGroup.FG (Additive (𝓞 K)ˣ)

Tactic:
← Module.Finite.iff_addGroup_fg

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Module.Finite ℤ (Additive (𝓞 K)ˣ)
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i, fundSystem K i ^ f i
⊢ ∑ i, f i • Additive.ofMul ↑(Quotient.out (Additive.toMul ((basisModTorsion K) i))) = ∑ i, f i • (basisModTorsion K) i

Tactic:
QuotientGroup.out_eq',

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i, fundSystem K i ^ f i
⊢ ∑ x, f x • Additive.ofMul (Additive.toMul ((basisModTorsion K) x)) = ∑ i, f i • (basisModTorsion K) 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 y : 𝓞 K
hy : x - 1 = λ * y
this : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))
⊢ λ ^ 4 ∣ x ^ 3 - 1

Tactic:
rw [this, pow_succ]

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
this : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))
⊢ λ ^ 3 * λ ∣ λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
ha : 0 * 0 ≠ 0
⊢ False

Tactic:
simp [mul_zero, ne_eq] at ha

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

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

Tactic:
by
  simp only [legendreSym, intCast_mod]

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬IsUnit a
⊢ quadraticCharFun F a = 0

Tactic:
rw [of_not_not (mt Ne.isUnit ha)]

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬IsUnit a
⊢ quadraticCharFun F 0 = 0