mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : (algebraMap B L) ((aeval x) (derivative (minpoly A x))) ≠ 0
⊢ ((aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))))⁻¹ ≠ 0

Tactic:
rwa [ne_eq, inv_eq_zero]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
⊢ ∃ y, y ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ w₁ → w ↑y < w ↑x) ∧ |(Algebra.norm ℚ) ↑y| ≤ ↑B

Tactic:
obtain ⟨g, h_geqf, h_gprod⟩ := adjust_f K B this
    obtain ⟨y, h_ynz, h_yle⟩ := exists_ne_zero_mem_ringOfIntegers_lt K (f := g)
      (by rw [convexBodyLT_volume]; convert! hB; exact congr_arg ((↑) : NNReal → ENNReal) h_gprod)
    refine ⟨y, h_ynz, fun w hw ↦ (h_geqf w hw ▸ h_yle w).trans ?_, ?_⟩
    · rw [← Rat.cast_le (K := ℝ), Rat.cast_natCast]
      calc
        _ = ∏ 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)
    · refine div_lt_self ?_ (by simp)
      exact pos_iff.mpr hx'

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

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < 3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = ζ ^ r
⊢ u = η ^ r

Tactic:
ext

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < 3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = ζ ^ r
⊢ ↑↑u = ↑↑(η ^ r)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < 3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = -ζ ^ r
⊢ u = -η ^ r

Tactic:
ext

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < 3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = -ζ ^ r
⊢ ↑↑u = ↑↑(-η ^ r)
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
| fun B ↦ minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B

Tactic:
ext

Goal state after:
case p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
x✝ : ℕ
| minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑x✝
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ λ ^ 2 = -3 * ↑η

Tactic:
ext

Goal state after:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ ↑(λ ^ 2) = ↑(-3 * ↑η)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ ↑⋯.unit ^ 2 + ↑⋯.unit + 1 = 0

Tactic:
ext

Goal state after:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ ↑(↑⋯.unit ^ 2 + ↑⋯.unit + 1) = ↑0
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
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ ⋯.toInteger = hζ.toInteger ^ 2

Tactic:
ext

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ ↑⋯.toInteger = ↑(hζ.toInteger ^ 2)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this✝ : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
this :
  (Ideal.Quotient.mk (Ideal.span {λ})) x = 0 ∨
    (Ideal.Quotient.mk (Ideal.span {λ})) x = 1 ∨ (Ideal.Quotient.mk (Ideal.span {λ})) x = -1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
rcases this with h | h | h

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 0
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = -1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ torsion K = (AddMonoidHom.toMultiplicativeRight (logEmbedding K)).ker

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : (𝓞 K)ˣ
⊢ x✝ ∈ torsion K ↔ x✝ ∈ (AddMonoidHom.toMultiplicativeRight (logEmbedding K)).ker
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

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

Tactic:
← logEmbedding_eq_zero_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : (𝓞 K)ˣ
⊢ (logEmbedding K) (Additive.ofMul x✝) = 0 ↔ (logEmbedding K) (Additive.ofMul x✝) = 0
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case h
n : ℕ
⊢ 2 ^ (n + 1) ∈ {n | Even n ∧ n.Deficient} ∧ n < 2 ^ (n + 1)

Tactic:
constructor

Goal state after:
case h.left
n : ℕ
⊢ 2 ^ (n + 1) ∈ {n | Even n ∧ n.Deficient}

case h.right
n : ℕ
⊢ n < 2 ^ (n + 1)
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case h.left
n : ℕ
⊢ 2 ^ (n + 1) ∈ {n | Even n ∧ n.Deficient}

Tactic:
exact ⟨⟨2 ^ n, by rw [pow_succ, mul_two]⟩, prime_two.deficient_pow⟩

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

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

Tactic:
constructor

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

case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a → ∃ y, ↑y * ↑y = a
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Tactic:
legendreSym,

Goal state after:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑((quadraticChar (ZMod p)) ↑a) = ↑a ^ (p / 2)
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑(legendreSym 2 a) = ↑a ^ (2 / 2)

Tactic:
legendreSym,

Goal state after:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑((quadraticChar (ZMod 2)) ↑a) = ↑a ^ (2 / 2)
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p 0 = 0

Tactic:
legendreSym,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (quadraticChar (ZMod p)) ↑0 = 0
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p 1 = 1

Tactic:
legendreSym,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (quadraticChar (ZMod p)) ↑1 = 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case pos.inl.inr
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : b ^ 3 + a ^ 3 + (-c) ^ 3 = 0
h3b : 3 ∣ b
⊢ {b, a, -c}.gcd id = 1

Tactic:
simp only [← Hgcd, insert_comm, gcd_insert, gcd_singleton, id_eq, ← abs_eq_normalize, abs_neg]

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

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3

Tactic:
· have h₁ := FiniteField.odd_card_of_char_ne_two hF
    rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (one_ne_zero' F)),
      quadraticChar_neg_one hF, χ₄_nat_eq_if_mod_four, h₁]
    lia

Goal state after:
Module: Mathlib.NumberTheory.LucasPrimality

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

Tactic:
constructor

Goal state after:
case left
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
⊢ p ≠ 0

case right
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
⊢ p ≠ 1
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
inst✝¹ : Finite (A ⧸ p)
P Q : Ideal B
inst✝ : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
⊢ P.LiesOver p

Tactic:
constructor

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
inst✝¹ : Finite (A ⧸ p)
P Q : Ideal B
inst✝ : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
⊢ p = Ideal.under A P
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : 2 = ↑2
⊢ legendreSym p 2 = χ₈ ↑p

Tactic:
legendreSym,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : 2 = ↑2
⊢ (quadraticChar (ZMod p)) ↑2 = χ₈ ↑p
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : -2 = ↑(-2)
⊢ legendreSym p (-2) = χ₈' ↑p

Tactic:
legendreSym,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : -2 = ↑(-2)
⊢ (quadraticChar (ZMod p)) ↑(-2) = χ₈' ↑p
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)
n r : ℕ
⊢ ↑↑n = ↑n

Tactic:
by norm_cast

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

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
nc' : ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

Tactic:
legendreSym,

Goal state after:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
nc' : ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)
⊢ (quadraticChar (ZMod q)) ↑↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
nc' : ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)
⊢ (quadraticChar (ZMod q)) ↑↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

Tactic:
legendreSym,

Goal state after:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
nc' : ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)
⊢ (quadraticChar (ZMod q)) ↑↑p * (quadraticChar (ZMod p)) ↑↑q = (-1) ^ (p / 2 * (q / 2))
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

Tactic:
by
  have hp₁ := (Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left hp
  have hq₁ := (Prime.eq_two_or_odd <| @Fact.out q.Prime _).resolve_left hq
  have hq₂ : ringChar (ZMod q) ≠ 2 := (ringChar_zmod_n q).substr hq
  have h :=
    quadraticChar_odd_prime ((ringChar_zmod_n p).substr hp) hq ((ringChar_zmod_n p).substr hpq)
  rw [card p] at h
  have nc : ∀ n r : ℕ, ((n : ℤ) : ZMod r) = n := fun n r => by norm_cast
  have nc' : (((-1) ^ (p / 2) : ℤ) : ZMod q) = (-1) ^ (p / 2) := by norm_cast
  rw [legendreSym, legendreSym, nc, nc, h, map_mul, mul_rotate', mul_comm (p / 2), ← pow_two,
    quadraticChar_sq_one (prime_ne_zero q p hpq.symm), mul_one, pow_mul, χ₄_eq_neg_one_pow hp₁, nc',
    map_pow, quadraticChar_neg_one hq₂, card q, χ₄_eq_neg_one_pow hq₁]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]

Tactic:
constructor

Goal state after:
case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b → 1 ≡ b ^ (n - 1) [MOD n]

case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ 1 ≡ b ^ (n - 1) [MOD n] → n.ProbablePrime b
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case hfin
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ ↑a ^ 2 ^ (n + 1) = 1

Tactic:
· rw [pow_succ, pow_mul, ha1, neg_one_sq]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
⊢ a = 2

Tactic:
contrapose! hn1

Goal state after:
a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
⊢ n = 1
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
⊢ n = 1

Tactic:
let h := Nat.sub_dvd_pow_sub_pow a 1 n

Goal state after:
a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
h : a - 1 ∣ a ^ n - 1 ^ n := Nat.sub_dvd_pow_sub_pow a 1 n
⊢ n = 1
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ ↑(maximalIdeal ℕ) = {1}ᶜ

Tactic:
ext

Goal state after:
x✝ : ℕ
⊢ x✝ ∈ ↑(maximalIdeal ℕ) ↔ x✝ ∈ {1}ᶜ
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ IsGreatest {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k} (m * n - m - n)

Tactic:
constructor

Goal state after:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}

case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ upperBounds {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}
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)
inst✝ : ⊥.IsPrime
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
⊢ B⁰ = ⊥.primeCompl

Tactic:
ext

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)
inst✝ : ⊥.IsPrime
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
x✝ : B
⊢ x✝ ∈ B⁰ ↔ x✝ ∈ ⊥.primeCompl
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inr
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P

Tactic:
constructor

Goal state after:
case inr.mp
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) := ⋯
⊢ ¬P ∣ differentIdeal A B → IsUnramifiedAt A P

case inr.mpr
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) := ⋯
⊢ IsUnramifiedAt A P → ¬P ∣ differentIdeal A B
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inr.mp
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : ¬P ∣ differentIdeal A B
⊢ Algebra.IsSeparable (Ideal.under A P).ResidueField P.ResidueField ∧
    Ideal.map (algebraMap A (Localization.AtPrime P)) (Ideal.under A P) =
      IsLocalRing.maximalIdeal (Localization.AtPrime P)

Tactic:
constructor

Goal state after:
case inr.mp.left
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) := ⋯
H : ¬P ∣ differentIdeal A B
⊢ Algebra.IsSeparable (Ideal.under A P).ResidueField P.ResidueField

case inr.mp.right
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) := ⋯
H : ¬P ∣ differentIdeal A B
⊢ Ideal.map (algebraMap A (Localization.AtPrime P)) (Ideal.under A P) =
    IsLocalRing.maximalIdeal (Localization.AtPrime P)