mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
w : InfinitePlace K
h : w = w₀
⊢ 0 = y w

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
w : InfinitePlace K
h : ¬w = w₀
⊢ y w = y w

Tactic:
· simpa [h, eq_comm] using hy w₀

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
w : InfinitePlace K
h : ¬w = w₀
⊢ y w = y w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ closure (↑expMapBasis '' paramSet K) ⊆ compactSet K

Tactic:
refine (isCompact_compactSet K).isClosed.closure_subset_iff.mpr ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ↑expMapBasis '' paramSet K ⊆ compactSet K
Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion

Goal state before:
pp: case mpr.left
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s ↦ ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ Summable (⇑toCompl ∘ f)

pp: case mpr.right
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s ↦ ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Tactic:
· apply summable_iff_cauchySeq_finset.mpr
      simp_rw [Function.comp_apply, ← map_sum]
      exact h_cauchy.map (uniformContinuous_coe α)

Goal state after:
case mpr.right
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s ↦ ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : CompactSpace M
inst✝² : AddCommMonoid M
inst✝¹ : SeminormedAddCommGroup G
inst✝ : IsUltrametricDist G
h : M
f : C(M, G)
m : M
n : ℕ
⊢ ‖Δ_[h]^[n] (⇑f) m‖ ≤ ‖f‖

Tactic:
rw [fwdDiff_iter_eq_sum_shift]

Goal state after:
M : Type u_1
G : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : CompactSpace M
inst✝² : AddCommMonoid M
inst✝¹ : SeminormedAddCommGroup G
inst✝ : IsUltrametricDist G
h : M
f : C(M, G)
m : M
n : ℕ
⊢ ‖∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (m + k • h)‖ ≤ ‖f‖
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℤ_[p] E
inst✝ : IsBoundedSMul ℤ_[p] E
a : E
n : ℕ
⊢ ∀ (x : ℤ_[p]), ‖(mahlerTerm a n) x‖ ≤ ‖a‖

Tactic:
refine fun _ ↦ (norm_smul_le _ _).trans <| mul_le_of_le_one_left (norm_nonneg _) (norm_le_one _)

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES : ∀ (i : Fin n), ∀ y ∈ E i, ∀ z ∈ E i, (f y, f z) ∈ S
hEuniv : univ ⊆ ⋃ i, ↑(E i)
hEdis : Pairwise (Disjoint on E)
h_uniq : ∀ (x : X), ∃! i, x ∈ E i
⊢ ∃ n g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S

Tactic:
choose g hg hg' using h_uniq

Goal state after:
X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES : ∀ (i : Fin n), ∀ y ∈ E i, ∀ z ∈ E i, (f y, f z) ∈ S
hEuniv : univ ⊆ ⋃ i, ↑(E i)
hEdis : Pairwise (Disjoint on E)
g : X → Fin n
hg : ∀ (x : X), (fun i ↦ x ∈ E i) (g x)
hg' : ∀ (x : X) (y : Fin n), (fun i ↦ x ∈ E i) y → y = g x
⊢ ∃ n g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S
Module: Mathlib.NumberTheory.PowModTotient

Goal state before:
pp: x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ k % n * (x ^ φ n % n) % n = x ^ k % n

Tactic:
pow_totient_mod_eq_one hn h

Goal state after:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ k % n * 1 % n = x ^ k % n
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ a.y ≠ 0

Tactic:
intro hy

Goal state after:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
⊢ False
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
ih : 0 < (a ^ n).x
⊢ 0 < (a ^ (n + 1)).x

Tactic:
pow_succ

Goal state after:
case succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
ih : 0 < (a ^ n).x
⊢ 0 < (a ^ n * a).x
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
⊢ ∃ a, IsFundamental a

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := exists_pos_of_not_isSquare h₀ hd
  -- convert to `x : ℕ` to be able to use `Nat.find`
  have P : ∃ x' : ℕ, 1 < x' ∧ ∃ y' : ℤ, 0 < y' ∧ (x' : ℤ) ^ 2 - d * y' ^ 2 = 1 := by
    have hax := a.prop
    lift a.x to ℕ using by positivity with ax
    norm_cast at ha₁
    exact ⟨ax, ha₁, a.y, ha₂, hax⟩
  classical
  -- to avoid having to show that the predicate is decidable
  let x₁ := Nat.find P
  obtain ⟨hx, y₁, hy₀, hy₁⟩ := Nat.find_spec P
  refine ⟨mk x₁ y₁ hy₁, by rw [x_mk]; exact mod_cast hx, hy₀, fun {b} hb => ?_⟩
  rw [x_mk]
  have hb' := (Int.toNat_of_nonneg <| zero_le_one.trans hb.le).symm
  have hb'' := hb
  rw [hb'] at hb ⊢
  norm_cast at hb ⊢
  refine Nat.find_min' P ⟨hb, |b.y|, abs_pos.mpr <| y_ne_zero_of_one_lt_x hb'', ?_⟩
  rw [← hb', sq_abs]
  exact b.prop

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
n : ℕ
⊢ 2 ≤ 2 ^ (n + 1)

Tactic:
have := pow_right_mono₀ (by simp : 1 ≤ 2) (Nat.le_add_left _ _ : 1 ≤ n + 1)

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
n : ℕ
this : (fun x ↦ 2 ^ x) 1 ≤ (fun x ↦ 2 ^ x) (n + 1)
⊢ 2 ≤ 2 ^ (n + 1)
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
z : ℤ_[p]
hev : (Polynomial.aeval z) F = 0
hnlt : ‖z - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
⊢ ‖z - soln‖ = ‖z - a + (a - soln)‖

Tactic:
by rw [sub_add_sub_cancel]

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
⊢ Irreducible (⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne)

Tactic:
by
  set πᵥ := degree_lt_wf.min _ hne
  have hπᵥ : v πᵥ < 1 ∧ πᵥ ≠ 0 := degree_lt_wf.min_mem _ hne
  refine irreducible_iff.mpr ⟨?_, fun a b hab ↦ ?_⟩
  · simp only [Polynomial.isUnit_iff, isUnit_iff_ne_zero]
    intro ⟨a, ha0, ha⟩
    rw [← ha, coePolynomial, algebraMap_C, ← algebraMap_eq_C] at hπᵥ
    grind
  · by_contra! H
    simp only [hab, ne_eq, mul_eq_zero, not_or] at hπᵥ
    have hva := one_le_valuation_factor hne hπᵥ hab H.2
    simp only [mul_comm a b, @and_comm (¬a = 0)] at hπᵥ hab
    have := Right.one_le_mul (one_le_valuation_factor hne hπᵥ hab H.1) hva
    simp only [coePolynomial_eq_algebraMap, map_mul] at hπᵥ this
    grind

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
⊢ v ↑πᵥ < 1

Tactic:
simpa using! (degree_lt_wf.min_mem _
    (setOfPred_polynomial_valuation_lt_one_and_ne_zero_nonempty hle)).1

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
⊢ v ((algebraMap K[X] K⟮X⟯) p) = v (↑π ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors)

Tactic:
have hπ : π ∈ _ := degree_lt_wf.min_mem _ hne

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : π ∈ {p | v ↑p < 1 ∧ p ≠ 0}
⊢ v ((algebraMap K[X] K⟮X⟯) p) = v (↑π ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors)
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case neg.a.a
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ weights d2 * weights d1 = ∑ x ∈ n.divisors, if x = d1.lcm d2 then weights d1 * weights d2 else 0

Tactic:
sum_ite_eq_of_mem',

Goal state after:
case neg.a.a
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ weights d2 * weights d1 = weights d1 * weights d2

case neg.a.a.h
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ d1.lcm d2 ∈ n.divisors
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x : ℤ[i]
⊢ toComplex (star x) = (starRingEnd ℂ) (toComplex x)

Tactic:
by
  rw [toComplex_def₂, toComplex_def₂]
  exact congr_arg₂ _ rfl (Int.cast_neg _)

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
⊢ normSq
      (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
        (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I) ≤
    normSq (1 / 2 + 1 / 2 * I)

Tactic:
by
      have : |(2⁻¹ : ℝ)| = 2⁻¹ := abs_of_nonneg (by simp)
      exact normSq_le_normSq_of_re_le_of_im_le
        (by rw [toComplex_re_div]; simp [normSq, this]; simpa using abs_sub_round (x / y : ℂ).re)
        (by rw [toComplex_im_div]; simp [normSq, this]; simpa using abs_sub_round (x / y : ℂ).im)

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inl
p : ℕ
hp : Prime p
this : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
a b c d : ℕ
hmin : ∀ m < 1, ¬(m < p ∧ 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p)
hmp : 1 < p
hm₀ : 0 < 1
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 1 * p
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Tactic:
use a, b, c, d; simpa using habcd

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n : ℕ
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ |liouvilleNumber ↑m - ↑a / ↑b| < 1 / ↑b ^ n

Tactic:
rcases partialSum_eq_rat (zero_lt_two.trans_le hm) n with ⟨p, hp⟩

Goal state after:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ |liouvilleNumber ↑m - ↑a / ↑b| < 1 / ↑b ^ n
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ C, ∃ (_ : 0 < C), ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p

Tactic:
refine ⟨max C 1, zero_lt_one.trans_le <| le_max_right _ _, ?_⟩

Goal state after:
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < max C 1 / ↑n ^ p
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
⊢ ‖↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
        (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)))‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0) ^
      p

Tactic:
have :
      ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
        (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
      ((p - 1)! • ↑(eval 0 (f ^ p)) + p ! • ↑(eval 0 gp') : ℤ) * cexp r -
        (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) := by
    simp; ring

Goal state after:
case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this✝ :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
this :
  ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
      (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
    ↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))
⊢ ‖↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
        (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)))‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0) ^
      p
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
⊢ LiouvilleWith p (x * ↑r)

Tactic:
rcases h.exists_pos with ⟨C, _hC₀, hC⟩
  refine ⟨r.den ^ p * (|r| * C), (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩
  rintro n ⟨_hn, m, hne, hlt⟩
  have A : (↑(r.num * m) : ℝ) / ↑(r.den • id n) = m / n * r := by
    simp [← div_mul_div_comm, ← r.cast_def, mul_comm]
  refine ⟨r.num * m, ?_, ?_⟩
  · rw [A]; simp [hne, hr]
  · rw [A, ← sub_mul, abs_mul]
    simp only [smul_eq_mul, id, Nat.cast_mul]
    calc _ < C / ↑n ^ p * |↑r| := by gcongr
      _ = ↑r.den ^ p * (↑|r| * C) / (↑r.den * ↑n) ^ p := ?_
    rw [mul_rpow, mul_div_mul_left, mul_comm, mul_div_assoc]
    · simp only [Rat.cast_abs]
    all_goals positivity

Goal state after:
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : SemilatticeSup α
a : α
⊢ Unbounded (fun x1 x2 ↦ x1 ≤ x2) (s ∩ {b | ¬b ≤ a}) ↔ Unbounded (fun x1 x2 ↦ x1 ≤ x2) s

Tactic:
by
  rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
  exact bounded_le_inter_not_le a

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ (∀ b ∈ A.left, b ≤ x✝) ↔ x✝ ∈ A.right

Tactic:
← upperBounds_left,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ (∀ b ∈ A.left, b ≤ x✝) ↔ x✝ ∈ upperBounds A.left
Module: Mathlib.Order.Filter.ListTraverse

Goal state before:
pp: α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
⊢ t ∈ traverse f fs ↔ ∃ us, Forall₂ (fun b s ↦ s ∈ f b) fs us ∧ sequence us ⊆ t

Tactic:
by
  constructor
  · induction fs generalizing t with
    | nil =>
      simp only [sequence, mem_pure, imp_self, forall₂_nil_left_iff, exists_eq_left, Set.pure_def,
        singleton_subset_iff, traverse_nil]
    | cons b fs ih =>
      intro ht
      rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
      rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hwu⟩
      rcases ih v hv with ⟨us, hus, hu⟩
      exact ⟨w::us, Forall₂.cons hw hus, (Set.seq_mono hwu hu).trans ht⟩
  · rintro ⟨us, hus, hs⟩
    exact mem_of_superset (mem_traverse _ _ hus) hs

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h

Tactic:
simp only [biInter_eq_iInter]

Goal state after:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h

Tactic:
by
  simp only [biInter_eq_iInter]
  exact EventuallyLE.cardinal_iInter hS fun i => h i i.2

Goal state after:
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a ⇨ b)

Tactic:
rw [IsRegular, compl_compl_himp_distrib, ha.eq, hb.eq]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case neg.inr
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
p : Nat.Primes
h✝ : ¬B ↑p =ᵐ[μ] ∅
⊢ A ↑p ∪ B ↑p ∪ C ↑p =ᵐ[volume] univ

Tactic:
· rcases hB p with _ | h; · contradiction
      simp only [μ, h, union_ae_eq_univ_of_ae_eq_univ_left,
        union_ae_eq_univ_of_ae_eq_univ_right]

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α : Type u
inst✝² : LinearOrder α
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
⊢ type α = 1

Tactic:
cases nonempty_unique α

Goal state after:
case intro
α : Type u
inst✝² : LinearOrder α
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
val✝ : Unique α
⊢ type α = 1
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case step
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
i j : ℕ
s : Set Ω
hs : MeasurableSet s
m✝ : ℕ
hk₁ : i.le m✝
hk₂ : ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f m✝ ω ∂μ
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f m✝.succ ω ∂μ

Tactic:
| step hk₁ hk₂ =>

Goal state after:
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : upperCrossingTime a b f N (n + 1) ω ≠ N
⊢ b ≤ stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (n + 1) ω)) ω

Tactic:
obtain ⟨j, hj₁, hj₂⟩ :=
    (hittingBtwn_le_iff_of_lt _ (lt_of_le_of_ne upperCrossingTime_le h)).1 le_rfl
  exact stoppedValue_hittingBtwn_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 (hittingBtwn_le _)⟩, hj₂⟩

Goal state after:
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ upcrossingStrat a b f N n ω ≤ 1

Tactic:
upcrossingStrat,

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ ∑ k ∈ Finset.range N, (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator 1 n ≤
    1
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i | ↑𝒢 i] =ᵐ[μ] 0
i : ℕ
⊢ μ[f (i + 1) | ↑𝒢 i] =ᵐ[μ] μ[f i | ↑𝒢 i]

Tactic:
eventuallyEq_iff_sub

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i | ↑𝒢 i] =ᵐ[μ] 0
i : ℕ
⊢ μ[f (i + 1) | ↑𝒢 i] - μ[f i | ↑𝒢 i] =ᵐ[μ] 0
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) = sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s})

Tactic:
refine le_antisymm ?_ (by gcongr; exacts [bddBelow_Icc.inter_of_left, ⟨j, hj₁, hj₂⟩])

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) ≤ sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s})
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h' : upperCrossingTime a b f N 0 ω < N
j : ℕ
hj₁ : j ∈ Set.Ico (upperCrossingTime a b f N 0 ω) N
hj₂ : f j ω ∈ Set.Iic a
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a

Tactic:
exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩

Goal state after: