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

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : finrank ℚ K ≤ 1
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
· exact le_max_of_le_left h

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

Goal state before:
pp: case _a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ ↑‖discr K‖₊ ≤ ↑↑N

Tactic:
coe_nnnorm,

Goal state after:
case _a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ ‖discr K‖ ≤ ↑↑N
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

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

Tactic:
simp [algebraMap_apply B L E, aeval_algebraMap_apply]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
⊢ IsNoetherianRing R

Tactic:
refine (isNoetherianRing_iff_ideal_fg R).mpr fun I ↦ ?_
  by_cases hI : I = 0
  · exact hI ▸ Submodule.fg_bot
  obtain ⟨x, hx₁, hx₂⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
  refine Submodule.fg_of_fg_map_of_fg_inf_ker (Submodule.mkQ (Ideal.span {x})) ?_ ?_
  · have := finiteQuotient (I := Ideal.span {x}) (by simp [hx₂])
    exact Submodule.FG.of_finite
  · rw [Submodule.ker_mkQ, inf_eq_right.mpr ((Ideal.span_singleton_le_iff_mem I).mpr hx₁)]
    exact Submodule.fg_span_singleton x

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
x : R
hx : x ≠ 0
⊢ {I | x ∈ I}.Finite

Tactic:
have := finiteQuotient (mt Ideal.span_singleton_eq_bot.mp hx)
  have : {I | Ideal.comap (Ideal.Quotient.mk (Ideal.span {x})) ⊥ ≤ I}.Finite :=
    .of_equiv _ (Ideal.relIsoOfSurjective _ Ideal.Quotient.mk_surjective).toEquiv
  simpa [← RingHom.ker_eq_comap_bot] using this

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : I ∈ {I | I.cardQuot ≤ B} \ {⊥}
⊢ I ∈ ⋃ x ∈ t, {I | x ∈ I}

Tactic:
rw [Set.mem_sdiff, Set.mem_ofPred, Submodule.cardQuot_apply] at hI

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card (R ⧸ I) ≤ B ∧ I ∉ {⊥}
⊢ I ∈ ⋃ x ∈ t, {I | x ∈ I}
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
N : Submodule R M
inst✝ : Finite (R ⧸ I)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
H : (Finsupp.linearCombination R Subtype.val).range = N
f : (↥s →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
x : ↥N
y : ↥s →₀ R
hy : (Finsupp.linearCombination R Subtype.val) y = ↑x
⊢ ∃ a, f a = x

Tactic:
exact ⟨y, Subtype.ext hy⟩

Goal state after:
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
x : K
x✝ : L
⊢ x✝ ∈ span B (⇑(IsLocalization.map L f hf) '' ↑(spanSingleton M x)) ↔ x✝ ∈ B ∙ (IsLocalization.map L f hf) x

Tactic:
refine ⟨fun hy ↦ span_le.2 ?_ hy, fun hy ↦ span_le.2 (fun _ h ↦ ?_) hy⟩

Goal state after:
case refine_1
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
x : K
x✝ : L
hy : x✝ ∈ span B (⇑(IsLocalization.map L f hf) '' ↑(spanSingleton M x))
⊢ ⇑(IsLocalization.map L f hf) '' ↑(spanSingleton M x) ⊆ ↑(B ∙ (IsLocalization.map L f hf) x)

case 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
x : K
x✝¹ : L
hy : x✝¹ ∈ B ∙ (IsLocalization.map L f hf) x
x✝ : L
h : x✝ ∈ {(IsLocalization.map L f hf) x}
⊢ x✝ ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑(spanSingleton M x)))
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsMaximal}.Finite
I : Ideal R
⊢ Submodule.IsPrincipal I

Tactic:
obtain rfl | hI := eq_or_ne I ⊥

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsMaximal}.Finite
⊢ Submodule.IsPrincipal ⊥

case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I ≠ ⊥
⊢ Submodule.IsPrincipal I
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
⊢ IsTorsionFree S Sₚ

Tactic:
rw [isTorsionFree_iff_algebraMap_injective,
    injective_iff_isRegular (algebraMapSubmonoid S P.primeCompl)]

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
⊢ ∀ (c : ↥P'), IsRegular ↑c
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case inr
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 : ↑(Ideal.absNorm (differentIdeal ℤ 𝒪)) ∈ differentIdeal ℤ 𝒪
h : discr K = -↑(discr K).natAbs
⊢ ↑(discr K) ∈ differentIdeal ℤ 𝒪

Tactic:
| inr h =>

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

Goal state before:
pp: L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = Ideal.absNorm (differentIdeal (𝓞 ↥K₂) (𝓞 L)) * (discr ↥K₂).natAbs ^ finrank (↥K₂) L
⊢ K₂.LinearDisjoint ↥K₁

Tactic:
by rwa [linearDisjoint_comm]

Goal state after:
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x y a p : R
n : ℕ
hp : Prime p
hx : x * y = a * p ^ n
⊢ ∃ i j b c, i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j

Tactic:
rcases mul_eq_mul_prime_prod (fun _ _ ↦ hp)
    (show x * y = a * (range n).prod fun _ ↦ p by simpa) with
      ⟨t, u, b, c, htus, htu, rfl, rfl, rfl⟩
  exact ⟨#t, #u, b, c, by rw [← card_union_of_disjoint htu, htus, card_range], by simp⟩

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

Goal state before:
pp: p k n : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ ℤ[⟨ζ - 1, ⋯⟩] = ⊤

Tactic:
by
    refine hζ.integralPowerBasisOfPrimePow.adjoin_eq_top_of_gen_mem_adjoin ?_
    convert! Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)
    simp [RingOfIntegers.ext_iff, integralPowerBasisOfPrimePow_gen, toInteger]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
H : (algebraMap R L) p = 0
⊢ Function.Injective ⇑(algebraMap R L)

Tactic:
algebraMap_eq R K L

Goal state after:
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
H : (algebraMap R L) p = 0
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
by
  have := hζ.norm_toInteger_sub_one_of_prime_ne_two hodd
  rw [this]
  exact Nat.prime_iff_prime_int.1 hp.out

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

Goal state before:
pp: case pos
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k + 1 = 1
⊢ hζ.toInteger - 1 ∣ ↑p

Tactic:
simp only [add_eq_right] at hk

Goal state after:
case pos
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
⊢ hζ.toInteger - 1 ∣ ↑p
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
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hP : 0 ∣ Ideal.map (algebraMap A B) p
ha : Ideal.map (algebraMap A B) p = ⊥ ^ (e - 1) * a
⊢ Ideal.map (algebraMap A B) p = ⊥

Tactic:
zero_dvd_iff,

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
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hP : Ideal.map (algebraMap A B) p = 0
ha : Ideal.map (algebraMap A B) p = ⊥ ^ (e - 1) * a
⊢ Ideal.map (algebraMap A B) p = ⊥
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n p : ℕ
left✝ : max (n + 1) 3 ≤ p
h2 : Prime p
⊢ ∃ b ∈ {n | Odd n ∧ n.Deficient}, n < b

Tactic:
exact ⟨p, Set.mem_ofPred.mpr ⟨Prime.odd_of_ne_two h2 (Ne.symm (ne_of_lt (by grind))),
    Prime.deficient h2⟩, by grind⟩

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0 * y⁻¹ ^ 2
⊢ legendreSym p a = 1

Tactic:
simp only [zero_mul] at hxy

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0
⊢ legendreSym p a = 1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hx : ¬x = 0
⊢ False

pp: case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hy : ¬y = 0
⊢ False

Tactic:
· rw [eq_one_of_sq_sub_mul_sq_eq_zero' ha hx hxy, CharZero.eq_neg_self_iff] at h
    exact one_ne_zero h

Goal state after:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hy : ¬y = 0
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

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

Tactic:
simp only [legendreSym, card p, quadraticChar_neg_one ((ringChar_zmod_n p).substr hp),
    Int.cast_neg, Int.cast_one]

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
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
⊢ ↑(#s) = (quadraticChar F) a + 1

Tactic:
by_cases h : IsSquare a

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : IsSquare a
⊢ ↑(#s) = (quadraticChar F) a + 1

case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : ¬IsSquare a
⊢ ↑(#s) = (quadraticChar F) a + 1
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)) ↑((-1) ^ (p / 2)) = ((-1) ^ (q / 2)) ^ (p / 2)

Tactic:
nc',

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)) ((-1) ^ (p / 2)) = ((-1) ^ (q / 2)) ^ (p / 2)
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case h
a k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
ha : 1 < a ^ 2 ^ k
h : a ^ 2 ^ k + 1 ∣ (a ^ 2 ^ k) ^ m + 1 ^ m := Odd.nat_add_dvd_pow_add_pow (a ^ 2 ^ k) 1 hm
⊢ 2 ^ k * m = 2 ^ k

Tactic:
rw [one_pow, hP.dvd_iff_eq (Nat.lt_add_right 1 ha).ne', add_left_inj, pow_eq_self_iff ha] at h

Goal state after:
case h
a k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
ha : 1 < a ^ 2 ^ k
h : m = 1
⊢ 2 ^ k * m = 2 ^ k
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ ∀ (q : ℕ), Prime q → q ∣ 2 ^ 2 ^ n + 1 - 1 → 3 ^ ((2 ^ 2 ^ n + 1 - 1) / q) ≠ 1

Tactic:
intro p hp1 hp2
    rw [Nat.add_sub_cancel, (Nat.prime_dvd_prime_iff_eq hp1 prime_two).mp (hp1.dvd_of_dvd_pow hp2),
        key, pow_succ, Nat.mul_div_cancel _ two_pos, ← pow_succ, ← key, h]
    exact neg_one_ne_one

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ 2 ∣ S'.a + ↑η * S'.b
⊢ ∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'

Tactic:
refine ⟨S'.a, η * S'.b, ?_, ?_, S'.ha, fun ⟨x, hx⟩ ↦ S'.hb ⟨η ^ 2 * x, ?_⟩, h⟩
    · simp [mul_pow, hζ.toInteger_cube_eq_one, one_mul, S'.H]
    · refine (isCoprime_mul_unit_left_right (Units.isUnit η) _ _).2 S'.coprime
    · rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ', coe_eta,
        hζ.toInteger_cube_eq_one, mul_one]

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
⊢ ∃ t n, ↑t ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → m ∈ span ↑t

Tactic:
by_cases h0 : setGcd s = 0
  · refine ⟨∅, 0, by simp, fun _ _ dvd ↦ by cases zero_dvd_iff.mp (h0 ▸ dvd); exact zero_mem _⟩
  -- Write the gcd of `s` as a ℤ-linear combination of a finite subset `t`.
  have ⟨t, hts, a, eq⟩ := (Submodule.mem_span_image_iff_exists_fun _).mp
    (span_singleton_setGcd s ▸ mem_span_singleton_self _)
  -- Let `x` be an arbitrary nonzero element in `s`.
  have ⟨x, hxs, hx⟩ := exists_ne_zero_of_setGcd_ne_zero h0
  let n := (x / setGcd s) * ∑ i, (-a i).toNat * i
  refine ⟨insert x t, n, by simpa [Set.insert_subset_iff] using ⟨hxs, hts⟩, fun m ge dvd ↦ ?_⟩
  -- For `m ≥ n`, write `m = q * x + (r + n)` with 0 ≤ r < x.
  obtain ⟨c, rfl⟩ := exists_add_of_le ge
  rw [← c.div_add_mod' x]
  set q := c / x
  set r := c % x
  rw [add_comm, add_assoc]
  refine add_mem (mul_mem_left _ q (subset_span (Finset.mem_insert_self ..)))
    (Submodule.span_mono (s := t) (Finset.subset_insert ..) ?_)
  -- It suffices to show `r + n` lies in the ℕ-span of `t`.
  obtain ⟨rx, hrx⟩ : setGcd s ∣ r := (dvd_mod_iff (setGcd_dvd_of_mem hxs)).mpr <|
    (Nat.dvd_add_right <| dvd_mul_of_dvd_right (Finset.dvd_sum fun i _ ↦
      dvd_mul_of_dvd_right (setGcd_dvd_of_mem (hts i.2)) _) _).mp dvd
  convert!
    (sum_mem fun i _ ↦ mul_mem_left _ _ (subset_span i.2) :
      -- an explicit ℕ-linear combination of elements of `t` that is equal to `r + n`
       ∑ i : t, (if 0 ≤ a i then rx else x / setGcd s - rx) * (a i).natAbs * i ∈ span t)
  simp_rw [← Int.natCast_inj, hrx, n, Finset.mul_sum, mul_comm _ rx, cast_add, cast_sum, cast_mul,
    ← eq, Finset.mul_sum, smul_eq_mul, ← mul_assoc, ← Finset.sum_add_distrib, ← add_mul]
  congr! 2 with i
  split_ifs with hai
  · rw [Int.toNat_eq_zero.mpr (by lia), cast_zero, mul_zero, add_zero,
      Int.natCast_natAbs, abs_eq_self.mpr hai]
  · rw [cast_sub, Int.natCast_natAbs, abs_eq_neg_self.mpr (by lia), sub_mul,
      ← Int.eq_natCast_toNat.mpr (by lia), mul_neg (rx : ℤ), sub_neg_eq_add, add_comm]
    rw [← Nat.mul_le_mul_left_iff (pos_of_ne_zero h0), ← hrx,
      Nat.mul_div_cancel' (setGcd_dvd_of_mem hxs)]
    exact (c.mod_lt (pos_of_ne_zero hx)).le

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: case calc_2
n : ℕ
⊢ ∫ (x : ℝ) in ↑1..↑(n + 1), x⁻¹ ≤ ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹

Tactic:
exact (inv_antitoneOn_Icc_right <| by simp).integral_le_sum_Ico (Nat.le_add_left 1 n)

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
⊢ ∃ᶠ (n : ℕ) in Filter.atTop, n.FermatPsp b

Tactic:
refine Filter.frequently_atTop.2 fun n => ?_

Goal state after:
b : ℕ
h : 1 ≤ b
n : ℕ
⊢ ∃ b_1, n ≤ b_1 ∧ b_1.FermatPsp b
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ HasFiniteMulSupport fun v ↦ max (↑v x) 1

Tactic:
fun_prop

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
hcx : c • x ≠ 0
⊢ HasFiniteMulSupport fun v ↦ ↑v c

Tactic:
fun_prop

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
hcx : c • x ≠ 0
⊢ HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case refine_1
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ ContinuousAt (fun x ↦ x - ↑n) x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ContinuousOn (fun x ↦ x) (uIcc (↑n) (↑n + 1))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ContinuousOn (fun x ↦ x ^ 2) (uIcc (↑n) (↑n + 1))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a.e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 1 / x ^ 2 = x ^ (-2)

Tactic:
rpow_neg,

Goal state after:
case e_a.e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 1 / x ^ 2 = (x ^ 2)⁻¹

case e_a.e_a.hx
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 0 ≤ x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
n : ℕ
⊢ mulHeight (0 ^ n) = mulHeight 0 ^ n

pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
⊢ mulHeight (x ^ n) = mulHeight x ^ n

Tactic:
· cases n <;> simp

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
⊢ mulHeight (x ^ n) = mulHeight x ^ n
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (A i)

Tactic:
fun_prop

Goal state after: