mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝¹⁴ : CommRing R
inst✝¹³ : IsDomain R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : IsIntegrallyClosed R
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : Algebra R S
inst✝⁷ : Module.Finite R S
inst✝⁶ : IsTorsionFree R S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ absNorm ((relNorm R) 1) = absNorm 1

pp: case neg.refine_3
R : Type u_1
inst✝¹⁴ : CommRing R
inst✝¹³ : IsDomain R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : IsIntegrallyClosed R
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : Algebra R S
inst✝⁷ : Module.Finite R S
inst✝⁶ : IsTorsionFree R S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ ∀ a ∈ normalizedFactors I, absNorm ((relNorm R) a) = absNorm a

Tactic:
· simp

Goal state after:
case neg.refine_3
R : Type u_1
inst✝¹⁴ : CommRing R
inst✝¹³ : IsDomain R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : IsIntegrallyClosed R
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : Algebra R S
inst✝⁷ : Module.Finite R S
inst✝⁶ : IsTorsionFree R S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ ∀ a ∈ normalizedFactors I, absNorm ((relNorm R) a) = absNorm a
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
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → Q.coeff m = p * g m
⊢ ∀ k ∈ range (j + 1), Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k

Tactic:
intro k hk

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
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → Q.coeff m = p * g m
k : ℕ
hk : k ∈ range (j + 1)
⊢ Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k
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
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ k ∈ range (j + 1), Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k
f : ℕ → L
hf :
  ∀ (i : ℕ),
    (Polynomial.map (algebraMap R L) (minpoly R B.gen)).natDegree ≤ i →
      f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
⊢ ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      (algebraMap R L) p * Q.coeff (j + 1 + k) • f (k + P.natDegree - 1)

Tactic:
intro k hk

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
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ k ∈ range (j + 1), Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k
f : ℕ → L
hf :
  ∀ (i : ℕ),
    (Polynomial.map (algebraMap R L) (minpoly R B.gen)).natDegree ≤ i →
      f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
k : ℕ
hk : k ∈ (range (Q.natDegree - j)).erase 0
⊢ Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
    (algebraMap R L) p * Q.coeff (j + 1 + k) • f (k + P.natDegree - 1)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case neg
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
this : NumberField K
H : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p ^ 1
⊢ ↑p ^ 1 ∣ ↑p

pp: case neg.hx
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
this : NumberField K
H : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p ^ 1
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
· simp

Goal state after:
case neg.hx
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
this : NumberField K
H : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p ^ 1
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case pos
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this✝ : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
hq' : q = 2
⊢ ↑p ∣ ↑q ^ Module.finrank (↥ℚ⟮ζ⟯) K

Tactic:
cases r with

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

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s

Tactic:
by
    obtain hn | hn := lt_or_eq_of_le hn
    · by_cases! h : ∃ q, q.Prime ∧ ∃ t, q ^ t = n
      · obtain ⟨q, hq, t, hn'⟩ := h
        have : Fact (Nat.Prime q) := ⟨hq⟩
        cases t with
        | zero => simp [← hn'] at hn
        | succ r =>
          rw [← hn'] at hC hμ
          refine ⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩
          by_cases hq' : q = 2
          · cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
          · rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp
      · rw [IsPrimitiveRoot.norm_toInteger_sub_one_eq_one hμ hn, one_pow,
          Int.natCast_dvd_ofNat, Nat.dvd_one] at hp
        · exact (Nat.Prime.ne_one hF.out hp).elim
        · exact fun {p} a k ↦ h p a k
    · rw [← hn] at hμ hC ⊢
      refine ⟨2, Nat.prime_two, 1, Module.finrank ℚ⟮ζ⟯ K, one_ne_zero, by rw [pow_one], ?_⟩
      rwa [hμ.norm_toInteger_sub_one_of_eq_two, neg_eq_neg_one_mul, mul_pow, IsUnit.dvd_mul_left
        ((isUnit_pow_iff Module.finrank_pos.ne').mpr isUnit_neg_one)] at hp

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

Goal state before:
pp: case refine_1
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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
C : Type u_3
M : Type u_4
inst✝²² : CommRing C
inst✝²¹ : IsDedekindDomain C
inst✝²⁰ : Field M
inst✝¹⁹ : Algebra C M
inst✝¹⁸ : IsFractionRing C M
inst✝¹⁷ : Algebra A C
inst✝¹⁶ : Algebra B C
inst✝¹⁵ : Algebra A M
inst✝¹⁴ : Algebra B M
inst✝¹³ : Algebra K M
inst✝¹² : Algebra L M
inst✝¹¹ : IsScalarTower A C M
inst✝¹⁰ : IsScalarTower A K M
inst✝⁹ : IsScalarTower B C M
inst✝⁸ : IsScalarTower B L M
inst✝⁷ : IsScalarTower K L M
inst✝⁶ : IsIntegralClosure C A M
inst✝⁵ : FiniteDimensional K M
inst✝⁴ : FiniteDimensional L M
inst✝³ : Algebra.IsSeparable K M
inst✝² : IsIntegralClosure C B M
inst✝¹ : Algebra.IsSeparable L M
inst✝ : IsTorsionFree B C
this : IsLocalization (algebraMapSubmonoid C B⁰) M
h : B⁰ ≤ Submonoid.comap (algebraMap B C) C⁰
h_alg : ∀ {x : L}, (algebraMap L M) x = (IsLocalization.map M (algebraMap B C) h) x
⊢ dual A K 1 ≤ dual B L 1 * (extendedHom M C) (dual A K 1)

Tactic:
intro x hx
    rw [← spanSingleton_le_iff_mem, ← mul_inv_le_iff₀ (bot_lt_iff_ne_bot.mpr
      (by simp [-extendedHom'_apply])), ← map_inv₀, ← FractionalIdeal.coe_le_coe,
        extendedHom'_apply, coe_mul, coe_spanSingleton, coe_extended_eq_span, coe_dual_one,
        span_mul_span, span_le]
    rintro _ ⟨x, rfl, _, ⟨a, ha, rfl⟩, rfl⟩ _ ⟨m, rfl⟩
    simp only [← h_alg, mul_comm _ (algebraMap _ _ _), ← Algebra.smul_def a, map_smul,
      LinearMap.toSpanSingleton_apply, Algebra.smul_def m, mul_one,
      LinearMap.smul_apply, traceForm_apply, smul_eq_mul]
    rw [← FractionalIdeal.coe_one (S := B⁰)]
    refine (mem_inv_iff (by simp)).mp ha _ (trace_mem_dual_one A K L B C M _ ?_)
    exact Algebra.smul_def m x ▸ smul_mem _ _ hx

Goal state after:
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ 0 ∉ {1, -1}

Tactic:
· simp

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

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

Tactic:
| succ n =>

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0

Tactic:
obtain ⟨B, hB⟩ : ∃ B : ℕ, minkowskiBound K 1 < (convexBodyLTFactor K) * B := by
    conv => congr; ext; rw [mul_comm]
    exact ENNReal.exists_nat_mul_gt (ENNReal.coe_ne_zero.mpr (convexBodyLTFactor_ne_zero K))
      (ne_of_lt (minkowskiBound_lt_top K 1))

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0

Tactic:
refine ⟨hu.choose, fun w hw ↦ Real.log_neg (pos_at_place hu.choose w) ?_⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ w ((algebraMap (𝓞 K) K) ↑(Exists.choose hu)) < 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ ↑(Quotient.out (Additive.toMul ((basisModTorsion K) i))) = Additive.ofMul.symm ((basisModTorsion K) i)

Tactic:
Additive.ofMul_symm_eq,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ ↑(Quotient.out (Additive.toMul ((basisModTorsion K) i))) = Additive.toMul ((basisModTorsion K) i)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:

Tactic:
_ = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (η + 1)) := by
          simp only [coe_eta, cube_sub_one_eq_mul hζ x]; ring
    _ = _ := by rw [hy]; ring

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n p : ℕ
left✝ : max (n + 1) 3 ≤ p
h2 : Prime p
⊢ 2 < p

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n p : ℕ
left✝ : max (n + 1) 3 ≤ p
h2 : Prime p
⊢ n < p

Tactic:
by grind

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) ≤ ↑(∑ i ∈ (m * k).divisors, i) / ↑k

Tactic:
rw [le_div_iff₀ (by grind [cast_pos]), ← cast_mul, cast_le, sum_mul]

Goal state after:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ ∑ i ∈ m.divisors, i * k ≤ ∑ i ∈ (m * k).divisors, i
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inl.«1»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0 → (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = -1

Tactic:
· simp

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

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

Tactic:
by
  have hbc : IsCoprime (-b) (-c) := by
    refine IsCoprime.neg_neg ?_
    rw [add_comm (a ^ 3), add_assoc, add_comm (a ^ 3), ← add_assoc] at HF
    refine isCoprime_of_gcd_eq_one_of_FLT ?_ HF
    convert! Hgcd using 2
    rw [Finset.pair_comm, Finset.insert_comm]
  by_contra! h3b
  by_cases h3c : 3 ∣ c
  · apply h3b
    rw [add_assoc, add_comm (b ^ 3), ← add_assoc] at HF
    exact dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT Int.prime_three h3a h3c HF
  · refine H (-b) (-c) a ha (by simp [h3b]) (by simp [h3c]) h3a hbc ?_
    rw [add_eq_zero_iff_eq_neg, ← (show Odd 3 by decide).neg_pow] at HF
    rw [← HF]
    ring

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

Goal state before:
pp: case neg.«_@».Mathlib.NumberTheory.LegendreSymbol.Basic.2777296637._hygCtx._hyg.53.«1»
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬(fun i ↦ i) ⟨1, ⋯⟩ = 0 → 1 = (fun i ↦ i) ⟨1, ⋯⟩ ^ 1

Tactic:
· simp

Goal state after:
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

Tactic:
eq_one_of_sq_sub_mul_sq_eq_zero' ha hx hxy,

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

Goal state before:
pp: case inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
h : (quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1
n : ℕ
h₂ : Odd n
⊢ (if (-1) ^ n = 1 then 1 else -1) = (-1) ^ n

Tactic:
· simp only [Odd.neg_one_pow h₂, Ring.neg_one_ne_one_of_char_ne_two hF, ite_false]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

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

Tactic:
have ha0 : 0 < a := one_pos.trans ha1

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

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

Tactic:
intro k hk

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

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : (b ^ 2 - 1) * (A * B - 1) = b ^ (2 * p) - 1 - (b ^ 2 - 1)
⊢ 1 ≤ p

Tactic:
by grind

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

Goal state before:
pp: case h₂.calc_1
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ d ∈ Finset.Ico 2 (n + 1), (↑d)⁻¹ = ∑ d ∈ Finset.Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹

Tactic:
Nat.cast_add,

Goal state after:
case h₂.calc_1
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ d ∈ Finset.Ico 2 (n + 1), (↑d)⁻¹ = ∑ x ∈ Finset.Ico 2 (n + 1), (↑x + ↑1 - 1)⁻¹
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: case neg
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ Real.log y ≤ ↑(harmonic ⌊y⌋₊)

Tactic:
calc
      _ ≤ Real.log ↑(Nat.floor y + 1) := ?_
      _ ≤ _ := log_add_one_le_harmonic _

Goal state after:
case neg
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ Real.log y ≤ Real.log ↑(⌊y⌋₊ + 1)
Module: Mathlib.NumberTheory.Harmonic.Int

Goal state before:
pp: case succ.inl
ih : padicValRat 2 (harmonic 0) = -↑(Nat.log 2 0)
⊢ padicValRat 2 (harmonic (0 + 1)) = -↑(Nat.log 2 (0 + 1))

pp: case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
⊢ padicValRat 2 (harmonic (n + 1)) = -↑(Nat.log 2 (n + 1))

Tactic:
· simp

Goal state after:
case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
⊢ padicValRat 2 (harmonic (n + 1)) = -↑(Nat.log 2 (n + 1))
Module: Mathlib.NumberTheory.HeckeRing.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
Δ : Submonoid G
H₁ H₂ : Subgroup G
inst✝ : IsHeckeTriple Δ H₁ H₂
g : ↥Δ
⊢ (ConjAct.toConjAct ↑g • H₂).Commensurable H₁

Tactic:
have hg : Commensurable (ConjAct.toConjAct (g : G) • H₂) H₂ := mem_commensurator_right H₁ g

Goal state after:
G : Type u_1
inst✝¹ : Group G
Δ : Submonoid G
H₁ H₂ : Subgroup G
inst✝ : IsHeckeTriple Δ H₁ H₂
g : ↥Δ
hg : (ConjAct.toConjAct ↑g • H₂).Commensurable H₂
⊢ (ConjAct.toConjAct ↑g • H₂).Commensurable H₁
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
e : ι ≃ ι'
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v (0 (e i)) = ⨆ i, v (0 i)
⊢ mulHeight (0 ∘ ⇑e) = mulHeight 0

pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
e : ι ≃ ι'
x : ι' → K
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v (x (e i)) = ⨆ i, v (x i)
hx : x ≠ 0
⊢ mulHeight (x ∘ ⇑e) = mulHeight x

Tactic:
· simp

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
e : ι ≃ ι'
x : ι' → K
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v (x (e i)) = ⨆ i, v (x i)
hx : x ≠ 0
⊢ mulHeight (x ∘ ⇑e) = mulHeight x
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
hx : x ≠ 0
this✝ : Nonempty { j // x j ≠ 0 }
this : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
⊢ HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)

Tactic:
convert! this with v

Goal state after:
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, ↑v (x i) = ⨆ i, ↑v (x ↑i)
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 ι
⊢ 1 ≤ mulHeight 0

pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
⊢ 1 ≤ mulHeight x

Tactic:
· simp

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
⊢ 1 ≤ mulHeight x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
h₀ : 0 ∘ f ≠ 0
⊢ mulHeight (0 ∘ f) ≤ mulHeight 0

pp: case inr.inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
⊢ mulHeight (x ∘ f) ≤ mulHeight x

Tactic:
· simp

Goal state after:
case inr.inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
⊢ mulHeight (x ∘ f) ≤ mulHeight x
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : FunLike F β ℝ
inst✝² : NonnegHomClass F β ℝ
inst✝¹ : ZeroHomClass F β ℝ
v : F
l : α → β
inst✝ : Fintype α
hv : IsNonarchimedean ⇑v
⊢ ∀ (i : α), i ∈ Finset.univ

Tactic:
by grind

Goal state after: