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✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
⊢ x ∈ comap (↑(↑(FractionRing.algEquiv B L)).symm) (traceDual A (FractionRing A) I) ↔
    x ∈ (comap (↑(↑(FractionRing.algEquiv B L)).symm) I)ᵛ

Tactic:
simp only [traceDual, Submodule.mem_comap]

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✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
⊢ ↑(↑(FractionRing.algEquiv B L)).symm x ∈
      {
        toAddSubmonoid :=
          ((traceForm (FractionRing A) (FractionRing B)).dualSubmodule (Submodule.restrictScalars A I)).toAddSubmonoid,
        smul_mem' := ⋯ } ↔
    x ∈
      {
        toAddSubmonoid :=
          ((traceForm K L).dualSubmodule
              (Submodule.restrictScalars A (comap (↑(↑(FractionRing.algEquiv B L)).symm) I))).toAddSubmonoid,
        smul_mem' := ⋯ }
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✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
this✝ : (FractionalIdeal.dual A (FractionRing A) 1)⁻¹ ≤ 1
this : ↑1 / traceDual A (FractionRing A) ↑1 ≤ ↑1
⊢ 1 / traceDual A (FractionRing A) 1 ≤ (Algebra.linearMap B (FractionRing B)).range

Tactic:
simpa only [FractionalIdeal.coe_one, Submodule.one_eq_range] using this

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

Goal state before:
pp: n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ ((-1) ^ (φ n / 2) * (↑n ^ φ n / ↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))))).natAbs =
    n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))

Tactic:
Int.natAbs_mul,

Goal state after:
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ ((-1) ^ (φ n / 2)).natAbs * (↑n ^ φ n / ↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)))).natAbs =
    n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ span A (Set.range ⇑((traceForm K L).dualBasis hnondeg pb.basis)) =
    ((aeval x) (derivative (minpoly K x)))⁻¹ • span A (Set.range (minpolyDiv A x).coeff)

Tactic:
Submodule.smul_span,

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ span A (Set.range ⇑((traceForm K L).dualBasis hnondeg pb.basis)) =
    span A (((aeval x) (derivative (minpoly K x)))⁻¹ • Set.range (minpolyDiv A x).coeff)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case succ
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
hei : (minpoly R B.gen).IsEisensteinAt (R ∙ p)
n : ℕ
hn : p ^ n • z ∈ R[B.gen] → z ∈ R[B.gen]
hz : p • p ^ n • z ∈ R[B.gen]
⊢ z ∈ R[B.gen]

Tactic:
exact
      hn (mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt hp hBint (hzint.smul _) hz hei)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ x✝ : Additive (𝓞 K)ˣ
⊢ (fun w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul (x✝¹ + x✝))))) =
    (fun w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul x✝¹)))) + fun w ↦
      ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul x✝)))

Tactic:
simp [Real.log_mul, mul_add]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ x✝ : Additive (𝓞 K)ˣ
⊢ (fun w ↦
      ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul x✝¹))) +
        ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul x✝)))) =
    (fun w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul x✝¹)))) + fun w ↦
      ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul x✝)))
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬w ((algebraMap (𝓞 K) K) ↑x) = -1

pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬w ((algebraMap (𝓞 K) K) ↑x) = 0

pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬↑w.mult = 0

Tactic:
· linarith [(apply_nonneg _ _ : 0 ≤ w x)]

Goal state after:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬w ((algebraMap (𝓞 K) K) ↑x) = 0

K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬↑w.mult = 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : NeZero n
ζ : K
hζ✝ : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot ⋯.unit n
⊢ n ∣ torsionOrder K

Tactic:
convert! orderOf_dvd_natCard (⟨(hζ.isUnit (NeZero.ne n)).unit, ?_⟩ : torsion K)

Goal state after:
case e'_3
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : NeZero n
ζ : K
hζ✝ : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot ⋯.unit n
⊢ n = orderOf ⟨↑⋯.unit, ?m.41⟩

n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : NeZero n
ζ : K
hζ✝ : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot ⋯.unit n
⊢ ↑⋯.unit ∈ torsion K
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 ≠ ⊥
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 ≠ ⊥
b : Ideal B
hb : Ideal.map (algebraMap A B) p = P ^ e * b
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e

Tactic:
apply_fun (· ^ e : Ideal B → _) at ha

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 ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
hb : Ideal.map (algebraMap A B) p = P ^ e * b
ha : Ideal.map (algebraMap A B) p ^ e = (P ^ (e - 1) * a) ^ e
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e
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:
apply card_le_card
    rw [Finset.univ_of_card_le_two (Nat.lt_succ_iff.1 h)]
    simp

Goal state after:
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
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
by
  classical
  have := hζ.finite_quotient_toInteger_sub_one (by decide)
  let _ := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
  let _ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing -- to speed up instance synthesis
  let _ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup -- ditto
  have := Finset.mem_univ (Ideal.Quotient.mk (Ideal.span {λ}) x)
  have h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3 := by
    rw [← Nat.card_eq_fintype_card, hζ.card_quotient_toInteger_sub_one,
      hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)]
    simp only [Nat.cast_ofNat, Int.reduceAbs]
  rw [Finset.univ_of_card_le_three h3.le] at this
  simp only [Finset.mem_insert, Finset.mem_singleton] at this
  rcases this with h | h | h
  · left
    exact Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 h
  · right; left
    refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_
    rw [RingHom.map_sub, h, RingHom.map_one, sub_self]
  · right; right
    refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_
    rw [RingHom.map_add, h, RingHom.map_one, neg_add_cancel]

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
⊢ ∃ b ∈ {n | Odd n ∧ n.Deficient}, n < b

Tactic:
obtain ⟨p, ⟨_, h2⟩⟩ := exists_infinite_primes (max (n + 1) 3)

Goal state after:
n p : ℕ
left✝ : max (n + 1) 3 ≤ p
h2 : Prime p
⊢ ∃ b ∈ {n | Odd n ∧ n.Deficient}, n < b
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : {a, b, c}.gcd id = 1
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ a ^ 3 + b ^ 3 + c ^ 3 ≠ 0

Tactic:
intro HF

Goal state after:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : {a, b, c}.gcd id = 1
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

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

Tactic:
← ZMod.intCast_zmod_eq_zero_iff_dvd

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.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:
have hp₁ := (Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left hp

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
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ b < (a ^ b - 1) / (a - 1)

Tactic:
by
  rw [← Nat.geomSum_eq ha]
  calc
    b = ∑ _ ∈ Finset.range b, (1 : ℕ) := by simp
    _ < _ := by
      refine Finset.sum_lt_sum (fun i hi => Nat.one_le_pow _ _ (by lia)) ?_
      exact ⟨1, Finset.mem_range.mpr (by lia), by simpa using! ha⟩

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

Goal state before:

Tactic:
_ = S'.a^3+S'.a^2*S'.b*(η^2+η+1)+S'.a*S'.b^2*(η^2+η+η^3)+η^3*S'.b^3 := by ring
  _ = S'.a^3+S'.a^2*S'.b*(η^2+η+1)+S'.a*S'.b^2*(η^2+η+1)+S'.b^3 := by
    simp [hζ.toInteger_cube_eq_one]
  _ = S'.a ^ 3 + S'.b ^ 3 := by rw [eta_sq]; ring

Goal state after:
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 : emultiplicity λ (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)
ht : emultiplicity λ (S'.a + hζ.toInteger * S'.b) = ⊤
⊢ False

Tactic:
simp [ht] at h2

Goal state after:
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)
this :
  ↑(2 * 3) ≤ ↑(multiplicity λ (S'.a + S'.b) + multiplicity λ (S'.a + ↑η * S'.b) + multiplicity λ (S'.a + ↑η ^ 2 * S'.b))
⊢ False

Tactic:
Nat.cast_le

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)
this : 2 * 3 ≤ multiplicity λ (S'.a + S'.b) + multiplicity λ (S'.a + ↑η * S'.b) + multiplicity λ (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ζ
⊢ λ ∣ S.a + ↑η ^ 2 * S.b

Tactic:
rw [show S.a + η ^ 2 * S.b = (S.a + S.b) + λ ^ 2 * S.b + 2 * λ * S.b by rw [coe_eta]; ring]

Goal state after:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ λ ∣ S.a + S.b + λ ^ 2 * S.b + 2 * λ * S.b
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: f : Fin 2 → ℝ
⊢ iSup f = max (f 0) (f 1)

Tactic:
rw [show f = ![f 0, f 1] from List.ofFn_inj.mp rfl]
  exact (max_eq_iSup ..).symm

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

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

Tactic:
← div_div,

Goal state after:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ x / x / x ^ s - ↑n / (x * x ^ s) = x ^ (-s) - ↑n * x ^ (-(s + 1))
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : (X - 1) * ∑ i ∈ range (n + 1), X ^ i = ∏ i ∈ range (n + 1), (X - C (μ ^ i * 1))
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Tactic:
prod_range_succ',

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : (X - 1) * ∑ i ∈ range (n + 1), X ^ i = (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) * (X - C (μ ^ 0 * 1))
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1) ≤
    ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (1 + 1)

Tactic:
simp_rw [intervalIntegral.integral_of_le (by linarith : (↑(n + 1) : ℝ) ≤ ↑(n + 1) + 1)]
    refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc (fun x hx ↦ ?_)
    · exact (term_welldef n.succ_pos (zero_lt_one.trans_le hs)).1
    · exact (term_welldef n.succ_pos zero_lt_one).1
    · have : 1 ≤ x := le_trans (by simp) hx.1.le
      gcongr
      · exact sub_nonneg.mpr hx.1.le
      · exact hs

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
⊢ ∑' (a : ℕ), (starRingEnd ℂ) (1 / ↑a ^ (starRingEnd ℂ) z) = riemannZeta z

Tactic:
zeta_eq_tsum_one_div_nat_cpow hz

Goal state after:
s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
⊢ ∑' (a : ℕ), (starRingEnd ℂ) (1 / ↑a ^ (starRingEnd ℂ) z) = ∑' (n : ℕ), 1 / ↑n ^ z
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : IsAlgebraic ℤ x
m : ℕ
r : 𝓞 K
hm : m ≠ 0
hmr : m • x = ↑r
n : ℕ := (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hndef : n = (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hn : n ≠ 0
a : 𝓞 K
ha' : ↑m * a = ↑n * r
ha : ↑n * x = ↑a
⊢ n * absNorm (span {↑n, a}) = n * n ^ (finrank ℚ K - 1)

Tactic:
hndef

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : IsAlgebraic ℤ x
m : ℕ
r : 𝓞 K
hm : m ≠ 0
hmr : m • x = ↑r
n : ℕ := (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hndef : n = (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hn : n ≠ 0
a : 𝓞 K
ha' : ↑m * a = ↑n * r
ha : ↑n * x = ↑a
⊢ (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r})) * absNorm (span {↑n, a}) =
    n * n ^ (finrank ℚ K - 1)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ψ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

Tactic:
hχ₀,

Goal state after:
case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ψ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum 1 ψ = -1 + z * (μ - 1) ^ 2
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ¬ψ = 1
⊢ jacobiSum χ ψ = -1 + 0 * (μ - 1) ^ 2

Tactic:
hχ₀,

Goal state after:
case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ¬ψ = 1
⊢ jacobiSum 1 ψ = -1 + 0 * (μ - 1) ^ 2
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
| h.repr (x + y) %ₘ f

Tactic:
rw [← h.map_repr x, ← h.map_repr y, ← map_add, h.modByMonic_repr_map, add_modByMonic]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
| h.repr x %ₘ f + h.repr y %ₘ f
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case hf
m : ℕ
m0 : m ≠ 0
x✝ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
⊢ HasDerivAt (fun x ↦ bernoulliFun (k + 1) (↑m * x)) (↑m * ((↑k + 1) * bernoulliFun k (↑m * x))) x

Tactic:
mul_comm (m : ℝ) _,

Goal state after:
case hf
m : ℕ
m0 : m ≠ 0
x✝ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
⊢ HasDerivAt (fun x ↦ bernoulliFun (k + 1) (↑m * x)) ((↑k + 1) * bernoulliFun k (↑m * x) * ↑m) x
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / (2 * ↑k * Complex.Gamma (2 * ↑k)) =
    (-1) ^ (k + 1) / (2 * ↑k) / (2 * ((2 * ↑π) ^ (2 * ↑k))⁻¹ * Complex.Gamma (2 * ↑k))

Tactic:
← div_div,

Goal state after:
case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / 2 / ↑k / Complex.Gamma (2 * ↑k) =
    (-1) ^ (k + 1) / 2 / ↑k / 2 / ((2 * ↑π) ^ (2 * ↑k))⁻¹ / Complex.Gamma (2 * ↑k)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ((2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)) =
    (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ((2 * ↑π) ^ (2 * ↑k + 1))⁻¹ * Complex.Gamma (2 * ↑k + 1))

Tactic:
← div_div,

Goal state after:
case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / (2 * ↑k + 1) / Complex.Gamma (2 * ↑k + 1) =
    (-1) ^ (k + 1) / (2 * ↑k + 1) / 2 / ((2 * ↑π) ^ (2 * ↑k + 1))⁻¹ / Complex.Gamma (2 * ↑k + 1)