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✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
⊢ ∀ a ∈ I, ((traceForm K L) ((algebraMap B L) b)) a ∈ (algebraMap A K).range

Tactic:
intro a

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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
a : L
⊢ a ∈ I → ((traceForm K L) ((algebraMap B L) b)) a ∈ (algebraMap A K).range
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case e_a.zero
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero 0
hK : IsCyclotomicExtension {0} ℚ K
this : NumberField K
⊢ (NumberField.discr K).natAbs = 0 ^ φ 0 / ∏ p ∈ primeFactors 0, p ^ (φ 0 / (p - 1))

Tactic:
| zero =>

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

Goal state before:
pp: case e_a.prime_pow.zero
p : ℕ
hp : Nat.Prime p
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
this✝ : NumberField K
this : Fact (Nat.Prime p)
hn : NeZero (p ^ 0)
hK : IsCyclotomicExtension {p ^ 0} ℚ K
⊢ ((-1) ^ (φ (p ^ 0) / 2) * ↑p ^ (p ^ (0 - 1) * ((p - 1) * 0 - 1))).natAbs =
    (p ^ 0) ^ φ (p ^ 0) / ∏ p_1 ∈ (p ^ 0).primeFactors, p_1 ^ (φ (p ^ 0) / (p_1 - 1))

Tactic:
| zero =>

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsDomain A
inst✝⁷ : IsFractionRing A K
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra.IsSeparable K L
inst✝⁴ : IsIntegralClosure B A L
inst✝³ : IsIntegrallyClosed A
inst✝² : IsDedekindDomain B
inst✝¹ : IsTorsionFree A B
inst✝ : IsFractionRing B L
I : FractionalIdeal B⁰ L
hI : I ≠ 0
⊢ (FractionalIdeal.dual A K 1)⁻¹ ≤ I ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑I⁻¹) ≤ 1

Tactic:
FractionalIdeal.inv_le_comm (by simp) hI,

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsDomain A
inst✝⁷ : IsFractionRing A K
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra.IsSeparable K L
inst✝⁴ : IsIntegralClosure B A L
inst✝³ : IsIntegrallyClosed A
inst✝² : IsDedekindDomain B
inst✝¹ : IsTorsionFree A B
inst✝ : IsFractionRing B L
I : FractionalIdeal B⁰ L
hI : I ≠ 0
⊢ I⁻¹ ≤ FractionalIdeal.dual A K 1 ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑I⁻¹) ≤ 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case zero
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero 0
hK : IsCyclotomicExtension {0} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ 0
this : NumberField K
⊢ ℤ[hζ.toInteger] = ⊤

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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)
hz : p ^ 0 • z ∈ R[B.gen]
⊢ z ∈ R[B.gen]

Tactic:
| zero =>

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

Goal state before:
pp: K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ IsPrincipalIdealRing (𝓞 K)

Tactic:
have : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩

Goal state after:
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ IsPrincipalIdealRing (𝓞 K)
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✝² : NeZero n
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ ℤ[⟨ζ - 1, ⋯⟩] = ⊤

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

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

Goal state before:
pp: 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⟩

Tactic:
rw [Subgroup.orderOf_mk]

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

Goal state before:
pp: case zero
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
w : InfinitePlace K
hw : w ≠ w₁
h : n < 0
⊢ w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB 0)) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))

Tactic:
| zero =>

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

Goal state before:
pp: case zero
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ ((Algebra.norm ℤ) ↑(seq K w₁ hB 0)).natAbs ≤ B

Tactic:
| zero =>

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Metric.closedBall 0 1 ∈ nhds 0

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Metric.closedBall 0 1).Finite

Tactic:
· exact Metric.closedBall_mem_nhds _ (by simp)

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Metric.closedBall 0 1).Finite
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ⊤.FG

Tactic:
← Module.finite_def

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Module.Finite ℤ (Additive ((𝓞 K)ˣ ⧸ torsion K))
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ ∀ (a : ℕ), ∃ b ∈ {n | n.Deficient}, a < b

Tactic:
intro a

Goal state after:
a : ℕ
⊢ ∃ b ∈ {n | n.Deficient}, a < b
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ ∀ (a : ℕ), ∃ b ∈ {n | Even n ∧ n.Abundant}, a < b

Tactic:
intro a

Goal state after:
a : ℕ
⊢ ∃ b ∈ {n | Even n ∧ n.Abundant}, a < b
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ ∀ (a : ℕ), ∃ b ∈ {n | Odd n ∧ n.Abundant}, a < b

Tactic:
intro a

Goal state after:
a : ℕ
⊢ ∃ b ∈ {n | Odd n ∧ n.Abundant}, a < b
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

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

Tactic:
simp only [Units.ext_iff, sq, Units.val_mk0, Units.val_mul]

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

Goal state before:
pp: case inl
inst✝ : Fact (Nat.Prime 2)
⊢ ∀ {a : ZMod 2}, a ≠ 0 → a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1

Tactic:
intro a

Goal state after:
case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
⊢ a ≠ 0 → a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ (quadraticChar F).IsQuadratic

Tactic:
intro a

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ (quadraticChar F) a = 0 ∨ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg.refine_1.zero
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
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x✝ : B
hxQ : x✝ ∈ Q
hx✝ : (intTrace A B) x✝ ∉ p
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
y : B
x : L
hx : x ∈ FractionalIdeal.dual A K 1
⊢ (Algebra.trace K L) (x * (Algebra.linearMap B L) 0) ∈ ↑p

Tactic:
| zero =>

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
h : ¬IsSquare a
⊢ ↑(#s) = (quadraticChar F) a + 1

Tactic:
rw [quadraticChar_neg_one_iff_not_isSquare.mpr h]

Goal state after:
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) = -1 + 1
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case zero
⊢ ∏ k ∈ range 0, k.fermatNumber = fermatNumber 0 - 2

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
⊢ ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2

Tactic:
induction n with | zero => rfl | succ n hn =>
  rw [prod_range_succ, hn, fermatNumber, fermatNumber, mul_comm,
    (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by lia), ← sq_sub_sq]
  ring_nf
  lia

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

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

Tactic:
Nat.le_div_iff_mul_le (Nat.zero_lt_succ _)

Goal state after:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 * a.succ ≤ a ^ b + 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - (1 + (b ^ 2 - 1)) = b ^ (2 * p) - (1 + b ^ 2 - 1)

Tactic:
by rw [Nat.add_sub_assoc hi_bsquared]

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: s : Set ℕ
⊢ {1} ⊆ (↑(span s))ᶜ ↔ s ⊆ {1}ᶜ

Tactic:
rw [Set.subset_compl_comm, ← coe_maximalIdeal, SetLike.coe_subset_coe, span_le]

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_1
P : Ideal ℕ
⊢ (P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ p, Nat.Prime p ∧ P = span {p}) → P.IsPrime

Tactic:
rintro (rfl | rfl | ⟨p, hp, rfl⟩)

Goal state after:
case refine_1.inl
⊢ ⊥.IsPrime

case refine_1.inr.inl
⊢ (maximalIdeal ℕ).IsPrime

case refine_1.inr.inr
p : ℕ
hp : Nat.Prime p
⊢ (span {p}).IsPrime
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_2.«1»
⊢ (![⊥, { asIdeal := span {2}, isPrime := ⋯ }, { asIdeal := maximalIdeal ℕ, isPrime := ⋯ }] ⟨1, ⋯⟩.castSucc,
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ }, { asIdeal := maximalIdeal ℕ, isPrime := ⋯ }] ⟨1, ⋯⟩.succ) ∈
    {x | x.1 < x.2}

Tactic:
Nat.maximalIdeal_eq_span_two_three

Goal state after:
case refine_2.«1»
⊢ (![⊥, { asIdeal := span {2}, isPrime := ⋯ }, { asIdeal := span {2, 3}, isPrime := ⋯ }] ⟨1, ⋯⟩.castSucc,
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ }, { asIdeal := span {2, 3}, isPrime := ⋯ }] ⟨1, ⋯⟩.succ) ∈
    {x | x.1 < x.2}
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: 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}

Tactic:
intro a

Goal state after:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a : ℕ
⊢ ∀ (n_1 : ℕ), a • m + n_1 • n ≠ m * n - m - n
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
k : ℕ
hk : m * n - m - n < k
⊢ m.gcd n ∣ k

Tactic:
by simp [cop.gcd_eq_one]

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

Goal state before:
pp: case inr.inl.refine_3
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
x✝ : λ ∣ ↑η * S'.b
x : 𝓞 K
hx : ↑η * S'.b = λ * x
⊢ S'.b = ↑η * S'.b * ↑η ^ 2

Tactic:
mul_comm _ S'.b,

Goal state after:
case inr.inl.refine_3
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
x✝ : λ ∣ ↑η * S'.b
x : 𝓞 K
hx : ↑η * S'.b = λ * x
⊢ S'.b = S'.b * ↑η * ↑η ^ 2
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inr.refine_3
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 + ↑η ^ 2 * S'.b
x✝ : λ ∣ ↑η ^ 2 * S'.b
x : 𝓞 K
hx : ↑η ^ 2 * S'.b = λ * x
⊢ S'.b = ↑η ^ 2 * S'.b * ↑η

Tactic:
mul_comm _ S'.b,

Goal state after:
case inr.inr.refine_3
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 + ↑η ^ 2 * S'.b
x✝ : λ ∣ ↑η ^ 2 * S'.b
x : 𝓞 K
hx : ↑η ^ 2 * S'.b = λ * x
⊢ S'.b = S'.b * ↑η ^ 2 * ↑η
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
⊢ ∃ n, FrobeniusNumber n s

Tactic:
by
    have ⟨n, hn⟩ := exists_mem_closure_of_ge s
    let P n := n ∉ AddSubmonoid.closure s
    have : P 1 := h.2 ∘ one_mem_closure_iff.mp
    classical
    refine ⟨findGreatest P n, frobeniusNumber_iff.mpr ⟨findGreatest_spec (P := P) (m := 1)
      (le_of_not_gt fun lt ↦ this (hn _ lt.le h.1.dvd)) this, fun k gt ↦ ?_⟩⟩
    obtain le | le := le_total k n
    · exact of_not_not (findGreatest_is_greatest gt le)
    · exact hn k le (h.1.dvd.trans <| one_dvd k)

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

Goal state before:
pp: case zero
⊢ padicValRat 2 (harmonic 0) = -↑(Nat.log 2 0)

Tactic:
| zero =>

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
⊢ IsCoprime (S.Y ^ 3 * ↑S.u₂) (S.Z ^ 3)

Tactic:
← isCoprime_mul_unit_right_right S.u₃.isUnit,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ IsCoprime (S.Y ^ 3 * ↑S.u₂) (S.Z ^ 3 * ↑S.u₃)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
⊢ ∀ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal, a ≠ 0

Tactic:
intro a

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
a : ℝ
⊢ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal → a ≠ 0
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ ↑n ≤ ↑n + 1

Tactic:
simp only [le_add_iff_nonneg_right, zero_le_one]

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

Goal state before:
pp: case zero
⊢ termSum 1 0 = log (↑0 + 1) - ↑(harmonic (0 + 1)) + 1

Tactic:
| zero =>

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

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ ↑n ≤ ↑n + 1

Tactic:
simp only [le_add_iff_nonneg_right, zero_le_one]

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

Goal state before:
pp: case h₂
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
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1) ≤
    (∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (A i)) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

Tactic:
rw [← finprod_mul_distrib (by fun_prop) (by fun_prop)]

Goal state after:
case h₂
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
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1) ≤
    ∏ᶠ (i : ↑nonarchAbsVal), (⨆ i_1, ↑i (A i_1)) * ⨆ i_1, ↑i (x i_1)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type := ⋯
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯
this : NumberField K
⊢ FermatLastTheoremForThreeGen hζ

Tactic:
intro a

Goal state after:
K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := IsCyclotomicExtension.zeta_spec 3 ℚ K
this : NumberField K
a : NumberField.RingOfIntegers K
⊢ ∀ (b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ),
    c ≠ 0 →
      ¬hζ.toInteger - 1 ∣ a → ¬hζ.toInteger - 1 ∣ b → hζ.toInteger - 1 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ ↑u * c ^ 3
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a.zero
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range 0, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑0 + 1) ^ (s - 1))

Tactic:
| zero =>

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

Goal state before:
pp: case e_a.e_a.zero
s : ℝ
hs : 1 < s
⊢ ∑ i ∈ Finset.range 0, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range 0, 1 / (↑n + 1) ^ s - ↑0 / (↑0 + 1) ^ s

Tactic:
| zero =>

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

Goal state before:
pp: case h₂.inl
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
this : Nonempty ι'
v : ↑nonarchAbsVal
j : ι'
h₀ : coeff 0 (p j) = 0
⊢ ↑v (coeff 0 (p j)) ≤ max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
simp [h₀]

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

Goal state before:
pp: K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
this : Nonempty ι'
v : ↑nonarchAbsVal
j : ι'
h₀ : coeff 0 (p j) ≠ 0
⊢ 0 ∈ (p j).support

Tactic:
simp [h₀]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ logHeight₁ (x + y) ≤ ↑(totalWeight K) * log 2 + logHeight₁ x + logHeight₁ y

Tactic:
by
  simp only [logHeight₁_eq_log_mulHeight₁]
  pull (disch := positivity) log
  exact (log_le_log <| by positivity) <| mulHeight₁_add_le ..

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: case refine_1.hy.hy
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico k (m + k)
⊢ 1 ∈ ℤ[μ]

Tactic:
· exact Subalgebra.one_mem _

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
this : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1
⊢ ↑(Fintype.card F - 2) = ↑(Fintype.card F) - 2

Tactic:
Nat.cast_sub <| Nat.add_one_le_of_lt Fintype.one_lt_card,

Goal state after:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
this : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1
⊢ ↑(Fintype.card F) - ↑(1 + 1) = ↑(Fintype.card F) - 2
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ completedRiemannZeta₀ 0 = (↑γ - log (4 * ↑π)) / 2 + 1

Tactic:
rw [← completedRiemannZeta₀_one_sub]
  simp [completedRiemannZeta₀_one]

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
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
⊢ -log (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1) + ↑N * logHeight x ≤ logHeight fun j ↦ (eval x) (p j)

Tactic:
by
  simp only [logHeight_eq_log_mulHeight]
  rcases isEmpty_or_nonempty ι'
  · simp [show q = 0 from Subsingleton.elim .., mulHeight_eval_ge_aux p h,
      max_mulHeightBound_zero_one_eq_one K ι (ι × ι')]
  have : (Nat.card ι' : ℝ) ^ totalWeight K ≠ 0 := by simp
  pull (disch := first | assumption | positivity) log
  exact (log_le_log <| by positivity) <| mulHeight_eval_ge hq p h

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
hv : ∀ (i : Fin 2), ↑(![a, ↑n] i) = ![↑a, ↑n] i
⊢ ↑n ≤ mulHeight₁ x

Tactic:
← mul_div_cancel_left₀ x (mod_cast hn : (n : K) ≠ 0),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
hv : ∀ (i : Fin 2), ↑(![a, ↑n] i) = ![↑a, ↑n] i
⊢ ↑n ≤ mulHeight₁ (↑n * x / ↑n)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case convert_3
s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ riemannZeta =ᶠ[𝓝 s] fun s ↦ (s - 1)⁻¹ + riemannZeta₀ s

Tactic:
· filter_upwards [compl_singleton_mem_nhds hs] using by grind [riemannZeta_eq_inv_sub_add]

Goal state after: