mathlib-initiative/mathlib-tactics huggingface dataset:
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))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
⊢ IsPrimitiveRoot ζ 2

Tactic:
rwa [hk, zero_add, pow_one, hp2] at hζ

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✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
⊢ 1 ≤ 1ᵛ

Tactic:
le_traceDual_iff_map_le_one,

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✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
⊢ map (↑A (Algebra.trace K L)) (restrictScalars A (1 * 1)) ≤ 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)
this✝³ : Algebra.IsSeparable (FractionRing B) (FractionRing C)
this✝² : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝¹ : FiniteDimensional (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing C)
this : FiniteDimensional (FractionRing B) (FractionRing C)
⊢ (dual A (FractionRing A) 1)⁻¹ = (dual B (FractionRing B) 1)⁻¹ * ↑(Ideal.map (algebraMap B C) (differentIdeal A B))

Tactic:
← extendedHom_coeIdeal_eq_map (K := FractionRing B),

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)
this✝² : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝¹ : FiniteDimensional (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing C)
this : FiniteDimensional (FractionRing B) (FractionRing C)
⊢ (dual A (FractionRing A) 1)⁻¹ = (dual B (FractionRing B) 1)⁻¹ * (extendedHom (FractionRing C) C) ↑(differentIdeal A B)
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
hne₂ : ((aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))))⁻¹ ≠ 0
this : IsIntegral A ((algebraMap B L) x)
⊢ (∀ (z : B),
      ∀ y_1 ∈ A[(algebraMap B L) x],
        (Algebra.trace K L)
            (((algebraMap B L) ((aeval x) (derivative (minpoly A x))))⁻¹ * (y * ((algebraMap B L) z * y_1))) ∈
          1) ↔
    ∀ (a : B),
      (Algebra.trace K L) (((algebraMap B L) ((aeval x) (derivative (minpoly A x))))⁻¹ * (y * (algebraMap B L) a)) ∈
        (algebraMap A K).range

Tactic:
simp_rw [← IsScalarTower.toAlgHom_apply A B L x, ← AlgHom.map_adjoin_singleton]

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 (minpoly K ((algebraMap B L) x))) ≠ 0
this✝ : (algebraMap B L) ((aeval x) (derivative (minpoly A x))) ≠ 0
hne₂ : ((aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))))⁻¹ ≠ 0
this : IsIntegral A ((algebraMap B L) x)
⊢ (∀ (z : B),
      ∀ y_1 ∈ Subalgebra.map (IsScalarTower.toAlgHom A B L) A[x],
        (Algebra.trace K L)
            (((algebraMap B L) ((aeval x) (derivative (minpoly A x))))⁻¹ * (y * ((algebraMap B L) z * y_1))) ∈
          1) ↔
    ∀ (a : B),
      (Algebra.trace K L) (((algebraMap B L) ((aeval x) (derivative (minpoly A x))))⁻¹ * (y * (algebraMap B L) a)) ∈
        (algebraMap A K).range
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₂))
inst✝ : Free A R₂
B₁ : Basis (Free.ChooseBasisIndex A R₂) R₁ B :=
  Basis.ofIsCoprimeDifferentIdeal A B R₁ R₂ h₁ h₂ h₃ (Free.chooseBasis A R₂)
x : B
i : Free.ChooseBasisIndex A R₂
x✝ : i ∈ Finset.univ
⊢ (algebraMap R₁ B) ((B₁.repr x) i) * B₁ i ∈
    (IsScalarTower.toAlgHom A R₁ B).range ⊔ (IsScalarTower.toAlgHom A R₂ B).range

Tactic:
exact Subalgebra.mul_mem _ (Algebra.mem_sup_left (by simp)) (Algebra.mem_sup_right (by simp [B₁]))

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
x : Additive (𝓞 K)ˣ
left✝ : x ∈ ↑⊤
hx : (logEmbedding K).toIntLinearMap x ∈ Metric.closedBall 0 r
w : InfinitePlace K
⊢ Real.log (w ((algebraMap (𝓞 K) K) ↑x)) ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
· rw [mem_closedBall_zero_iff] at hx
        exact (le_abs_self _).trans (log_le_of_logEmbedding_le hr hx w)

Goal state after:
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
⊢ univ ⊆ {0, 1, -1}

Tactic:
Finset.univ_of_card_le_two (Nat.lt_succ_iff.1 h)

Goal state after:
case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
⊢ {0, 1} ⊆ {0, 1, -1}
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 ∨ u = -η ^ r

Tactic:
· right; ext; exact h

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ ↑(∑ i ∈ m.divisors, i) / ↑m ≤ ↑(∑ i ∈ n.divisors, i) / ↑n

Tactic:
hk,

Goal state after:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ ↑(∑ i ∈ m.divisors, i) / ↑m ≤ ↑(∑ i ∈ (m * k).divisors, i) / ↑(m * k)
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
ha2 : a = 2
⊢ a = 2 ∧ Prime n

Tactic:
subst ha2

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h1 : ↑(multiplicity λ (S'.a + S'.b)) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False

Tactic:
Nat.cast_lt

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : ↑(multiplicity λ (S'.a + ↑η * S'.b)) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False

Tactic:
Nat.cast_lt

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : ↑(multiplicity λ (S'.a + ↑η ^ 2 * S'.b)) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False

Tactic:
Nat.cast_lt

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case pos
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : ↑t ⊆ s
a : ↥t → ℤ
eq : ∑ i, a i • ↑↑i = ↑(setGcd s)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i, (-a i).toNat * ↑i
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
a✝ : i ∈ Finset.univ
hai : 0 ≤ a i
⊢ ↑rx * a i + ↑(x / setGcd s) * ↑(-a i).toNat = ↑rx * ↑(a i).natAbs

Tactic:
rw [Int.toNat_eq_zero.mpr (by lia), cast_zero, mul_zero, add_zero,
      Int.natCast_natAbs, abs_eq_self.mpr hai]

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case pos
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : ↑t ⊆ s
a : ↥t → ℤ
eq : ∑ i, a i • ↑↑i = ↑(setGcd s)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i, (-a i).toNat * ↑i
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
a✝ : i ∈ Finset.univ
hai : 0 ≤ a i
⊢ ↑rx * a i + ↑(x / setGcd s) * ↑(-a i).toNat = ↑rx * ↑(a i).natAbs

pp: case neg
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : ↑t ⊆ s
a : ↥t → ℤ
eq : ∑ i, a i • ↑↑i = ↑(setGcd s)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i, (-a i).toNat * ↑i
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
a✝ : i ∈ Finset.univ
hai : ¬0 ≤ a i
⊢ ↑rx * a i + ↑(x / setGcd s) * ↑(-a i).toNat = ↑(x / setGcd s - rx) * ↑(a i).natAbs

Tactic:
· rw [Int.toNat_eq_zero.mpr (by lia), cast_zero, mul_zero, add_zero,
      Int.natCast_natAbs, abs_eq_self.mpr hai]

Goal state after:
case neg
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : ↑t ⊆ s
a : ↥t → ℤ
eq : ∑ i, a i • ↑↑i = ↑(setGcd s)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i, (-a i).toNat * ↑i
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
a✝ : i ∈ Finset.univ
hai : ¬0 ≤ a i
⊢ ↑rx * a i + ↑(x / setGcd s) * ↑(-a i).toNat = ↑(x / setGcd s - rx) * ↑(a i).natAbs
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.u₄ = 1 ∨ S.u₄ = -1

Tactic:
have : λ ^ 2 ∣ λ ^ 4 := ⟨λ ^ 2, by ring⟩

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
⊢ S.u₄ = 1 ∨ S.u₄ = -1
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 ι
x : ι → K
hx : x ≠ 0
this✝¹ : Nonempty { j // x j ≠ 0 }
this✝ : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
v : ↑nonarchAbsVal
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
h : x j = 0
⊢ ↑v (x j) ≤ ⨆ i, ↑v (x ↑i)

Tactic:
rw [h, v.val.map_zero]
      exact Real.iSup_nonneg' ⟨⟨i, hi⟩, v.val.nonneg ..⟩

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

Goal state before:
pp: case inr.inr.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
← mulHeight_fun_mul_eq hx hy,

Goal state after:
case inr.inr.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
⊢ mulHeight (x * y) ≤ mulHeight fun a ↦ x a.1 * y a.2
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: N : ℕ
s : ℝ
hs : 1 < s
⊢ termSum s N =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
simp only [termSum]
  conv => enter [1, 2, n]; rw [term_of_lt (by simp) hs]
  rw [Finset.sum_sub_distrib]
  congr 1
  · induction N with
    | zero => simp
    | succ N hN =>
      rw [Finset.sum_range_succ, hN, Nat.cast_add_one]
      ring_nf
  · simp_rw [mul_comm (_ / _), ← mul_div_assoc, div_eq_mul_inv _ s, ← Finset.sum_mul, mul_one]
    congr 1
    induction N with
    | zero => simp
    | succ N hN =>
      simp_rw [Finset.sum_range_succ, hN, Nat.cast_add_one, sub_eq_add_neg, add_assoc]
      congr 1
      ring_nf

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x, (χ x + ψ (1 - x) - 1) + ∑ x, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x, χ x + ∑ x, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
sum_sub_distrib,

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x, (χ x + ψ (1 - x)) - ∑ x, 1 + ∑ x, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x, χ x + ∑ x, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₂.refine_1
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
v : ↑nonarchAbsVal
j : ι'
⊢ ↑v ((eval x) (p j)) ≤ (⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) * (⨆ i, ↑v (x i)) ^ N

Tactic:
(isNonarchimedean _ v.prop).eval_mvPolynomial_le (hp j) x

Goal state after:
case h₂.refine_1
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
v : ↑nonarchAbsVal
j : ι'
⊢ (⨆ s, ↑v (coeff (↑s) (p j))) * (⨆ i, ↑v (x i)) ^ N ≤ (⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) * (⨆ i, ↑v (x i)) ^ N
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x, χ x + ∑ i, ψ i - ∑ x, 1 + ∑ x, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x, χ x + ∑ x, ψ x - ↑(∑ _a, 1) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
Nat.cast_sum,

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x, χ x + ∑ i, ψ i - ∑ x, 1 + ∑ x, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x, χ x + ∑ x, ψ x - ∑ x, ↑1 + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ riemannZeta 1 = (↑γ - log (4 * ↑π)) / 2

Tactic:
by
  have := (HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one 0).mono_left
    <| nhdsWithin_le_nhds (s := {1}ᶜ)
  simp only [HurwitzZeta.hurwitzZetaEven_zero, div_right_comm _ _ (Gammaℝ _)] at this
  exact tendsto_nhds_unique this ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ

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

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
⊢ ∃ C > 0,
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K},
      (∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)) →
        C * mulHeight x ^ N ≤ mulHeight fun j ↦ (eval x) (p j)

Tactic:
by
  rcases isEmpty_or_nonempty ι'
  · exact ⟨1, zero_lt_one, fun p _ h ↦ by simp [mulHeight_eval_ge_aux p h]⟩
  have : 0 < Nat.card ι' := Nat.card_pos
  exact ⟨_, by positivity, mulHeight_eval_ge hq⟩

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

Goal state before:
pp: ⊢ deriv riemannZeta₁ 1 = ↑γ

Tactic:
by
  unfold riemannZeta₁
  rw [deriv_const_add, deriv_fun_mul (by fun_prop) (by fun_prop)]
  simp

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : Finset.univ.gcd x = 1
hx₀ : Int.cast ∘ x ≠ 0
⊢ mulHeight (Int.cast ∘ x) = ↑(⨆ i, |x i|)

Tactic:
Finite.map_iSup_of_monotone _ Int.cast_mono,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : Finset.univ.gcd x = 1
hx₀ : Int.cast ∘ x ≠ 0
⊢ mulHeight (Int.cast ∘ x) = ⨆ i, ↑|x i|
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (LFunction Φ) s

Tactic:
by
  refine .mul (by fun_prop) ?_
  rcases ne_or_eq s 1 with hs' | rfl
  · exact .fun_sum fun j _ ↦ (differentiableAt_hurwitzZeta _ hs').const_mul _
  · have := DifferentiableAt.fun_sum (u := univ) fun j _ ↦
      (differentiableAt_hurwitzZeta_sub_one_div (toAddCircle j)).const_mul (Φ j)
    simpa only [mul_sub, sum_sub_distrib, ← sum_mul, hs.neg_resolve_left rfl, zero_mul, sub_zero]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
⊢ ∃ s_1 ∈ 𝓝 s, Set.EqOn (LFunctionTrivChar₁ n) (fun w ↦ (w - 1) * LFunctionTrivChar n w) s_1

Tactic:
exact ⟨_, isOpen_ne.mem_nhds hs, fun _ hw ↦ Function.update_of_ne (Set.mem_ofPred.mp hw) ..⟩

Goal state after: