mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: 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
⊢ Nat.card (↥↑(FractionalIdeal.dual ℤ ℚ 1) ⧸ Submodule.comap (↑(FractionalIdeal.dual ℤ ℚ 1)).subtype 1) =
    (discr K).natAbs

Tactic:
qify

Goal state after:
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
⊢ ↑(Nat.card (↥↑(FractionalIdeal.dual ℤ ℚ 1) ⧸ Submodule.comap (↑(FractionalIdeal.dual ℤ ℚ 1)).subtype 1)) =
    |↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

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

Tactic:
← Int.dvd_natAbs,

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
L : Type u_3
inst✝² : Field L
inst✝¹ : NumberField L
inst✝ : Algebra K L
⊢ discr K ^ finrank K L ∣ ↑(discr L).natAbs
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case mp
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝³ : IsDomain 𝒪
this✝² : IsDedekindDomain 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
h : p ∣ discr K
⊢ ∃ P, P.IsMaximal ∧ P.LiesOver (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪

Tactic:
← Int.dvd_natAbs,

Goal state after:
case mp
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝³ : IsDomain 𝒪
this✝² : IsDedekindDomain 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
h : p ∣ ↑(discr K).natAbs
⊢ ∃ P, P.IsMaximal ∧ P.LiesOver (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case mp
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝³ : IsDomain 𝒪
this✝² : IsDedekindDomain 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
h : p ∣ ↑(discr K).natAbs
⊢ ∃ P, P.IsMaximal ∧ P.LiesOver (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪

Tactic:
← absNorm_differentIdeal K 𝒪

Goal state after:
case mp
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝³ : IsDomain 𝒪
this✝² : IsDedekindDomain 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
h : p ∣ ↑(Ideal.absNorm (differentIdeal ℤ 𝒪))
⊢ ∃ P, P.IsMaximal ∧ P.LiesOver (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < p - 1
⊢ p ∣ p.choose (i + 1)

Tactic:
exact hp.out.dvd_choose_self i.succ_ne_zero (lt_tsub_iff_right.1 hi)

Goal state after:
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: case insert
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
x y a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hx : x * y = a * (p i * ∏ x ∈ s, p x)
⊢ ∃ t u b c, t ∪ u = insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i

Tactic:
← mul_assoc

Goal state after:
case insert
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
x y a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hx : x * y = a * p i * ∏ x ∈ s, p x
⊢ ∃ t u b c, t ∪ u = insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ insert i t ∪ u = insert i s

Tactic:
by rw [insert_union, htus]

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

Goal state before:
pp: 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
this : NumberField K
H : (Algebra.norm ℤ) (hζ.toInteger ^ p ^ 0 - 1) = ↑p ^ p ^ 0
⊢ hζ.toInteger - 1 ∣ ↑↑p

Tactic:
rw [pow_zero, pow_one] at H

Goal state after:
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
this : NumberField K
H : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p ^ 1
⊢ hζ.toInteger - 1 ∣ ↑↑p
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case refine_1
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
x : M
hx : x ∈ dual A K 1
a : L
ha : a ∈ ↑(dual A K 1)⁻¹
m : C
⊢ a * (Algebra.trace L M) ((algebraMap C M) m * x) ∈ 1

Tactic:
← FractionalIdeal.coe_one (S := B⁰)

Goal state after:
case refine_1
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
x : M
hx : x ∈ dual A K 1
a : L
ha : a ∈ ↑(dual A K 1)⁻¹
m : C
⊢ a * (Algebra.trace L M) ((algebraMap C M) m * x) ∈ ↑1
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
inst✝ : IsFractionRing B L
I : FractionalIdeal B⁰ L
hI : I ≠ 0
⊢ ↑I⁻¹ ≤ traceDual A K 1 ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑I⁻¹) ≤ 1

Tactic:
refine le_traceDual_iff_map_le_one.trans ?_

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
inst✝ : IsFractionRing B L
I : FractionalIdeal B⁰ L
hI : I ≠ 0
⊢ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A (↑I⁻¹ * 1)) ≤ 1 ↔
    Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑I⁻¹) ≤ 1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsIntegrallyClosed A
inst✝¹³ : IsDedekindDomain B
inst✝¹² : IsTorsionFree A B
C : Type u_3
inst✝¹¹ : IsDomain B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra B C
inst✝⁸ : Algebra A C
inst✝⁷ : IsDedekindDomain C
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.Finite A C
inst✝⁴ : Module.Finite B C
inst✝³ : IsTorsionFree A C
inst✝² : IsTorsionFree B C
inst✝¹ : IsScalarTower A B C
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing C)
⊢ differentIdeal A C = differentIdeal B C * Ideal.map (algebraMap B C) (differentIdeal A B)

Tactic:
have : Algebra.IsSeparable (FractionRing B) (FractionRing C) :=
    isSeparable_tower_top_of_isSeparable (FractionRing A) _ _

Goal state after:
A : Type u_1
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsIntegrallyClosed A
inst✝¹³ : IsDedekindDomain B
inst✝¹² : IsTorsionFree A B
C : Type u_3
inst✝¹¹ : IsDomain B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra B C
inst✝⁸ : Algebra A C
inst✝⁷ : IsDedekindDomain C
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.Finite A C
inst✝⁴ : Module.Finite B C
inst✝³ : IsTorsionFree A C
inst✝² : IsTorsionFree B C
inst✝¹ : IsScalarTower A B C
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing C)
this : Algebra.IsSeparable (FractionRing B) (FractionRing C)
⊢ differentIdeal A C = differentIdeal B C * Ideal.map (algebraMap B C) (differentIdeal A B)
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

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

Goal state after:
Module: Mathlib.RingTheory.Fintype

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

Tactic:
by_cases h : IsUnit a

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

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₀
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:

Tactic:
_ = ∏ w : InfinitePlace K, w (algebraMap _ K y) ^ mult w :=
          (prod_eq_abs_norm (algebraMap _ K y)).symm
        _ ≤ ∏ w : InfinitePlace K, (g w : ℝ) ^ mult w := by gcongr with w; exact (h_yle w).le
        _ ≤ (B : ℝ) := by
          simp_rw [← NNReal.coe_pow, ← NNReal.coe_prod]
          exact le_of_eq (congr_arg toReal h_gprod)

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✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP✝ : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this✝ : Ideal.map (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ x ∈ comap (↑A (Algebra.trace K L)) 1

Tactic:
rw [Submodule.mem_comap, LinearMap.coe_restrictScalars, ← FractionalIdeal.coe_one,
      ← div_self (G₀ := FractionalIdeal A⁰ K) (a := p) (by simpa using hp),
      FractionalIdeal.mem_coe, FractionalIdeal.mem_div_iff_of_ne_zero (by simpa using hp)]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP✝ : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this✝ : Ideal.map (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ ∀ y ∈ ↑p, (Algebra.trace K L) x * y ∈ ↑p
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: a b c : ℤ
hdvd : ¬3 ∣ a * b * c
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3

Tactic:
simp_rw [Int.prime_three.dvd_mul, not_or] at hdvd

Goal state after:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x - (↑⋯.unit + 1)

Tactic:
show x - (η + 1) = x + 1 - (η - 1 + 3) by ring

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x + 1 - (↑η - 1 + 3)
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ n.Deficient

Tactic:
obtain ⟨p, k, hp, -, rfl⟩ := h

Goal state after:
p k : ℕ
hp : _root_.Prime p
⊢ (p ^ k).Deficient
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 : a ≠ 0
⊢ (quadraticChar F) a ^ 2 = 1

Tactic:
by
  rwa [pow_two, ← map_mul, ← pow_two, quadraticChar_sq_one']

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑(x ^ 2 - a * y ^ 2) = 0
⊢ ↑x = 0 ∧ ↑y = 0

Tactic:
push_cast at hxy

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑x ^ 2 - ↑a * ↑y ^ 2 = 0
⊢ ↑x = 0 ∧ ↑y = 0
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
have h := FiniteField.even_card_of_char_two hF
    simp only [FiniteField.isSquare_of_char_two hF, true_iff]
    lia

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

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
have h := FiniteField.even_card_of_char_two hF
    simp only [FiniteField.isSquare_of_char_two hF, true_iff]
    lia

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

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ ¬Fintype.card F % 4 = 3

Tactic:
exact fun hf ↦
      one_ne_zero <|
        (Nat.odd_of_mod_four_eq_three hf).symm.trans <| FiniteField.even_card_of_char_two hF

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

Goal state before:
pp: 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
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ (Algebra.trace K L) x ∈ ↑1

pp: 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
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := ⋯
L : Type u_3 := ⋯
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ Submonoid A

Tactic:
← div_self (G₀ := FractionalIdeal A⁰ K) (a := p) (by simpa using hp),

Goal state after:
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
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ (Algebra.trace K L) x ∈ ↑(↑p / ↑p)