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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ dirichletDensity S ≤ 1

Tactic:
by
  rw [dirichletDensity]
  split_ifs with h
  · exact h.choose_spec.le_one
  · exact zero_le_one

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤
    ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖

Tactic:
by
      rw [← inverse_basisMatrix_mulVec_eq_repr]
      exact norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := ⋯
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⋯
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb x (1 / 2) ≤ logb M (1 / 2)

Tactic:
simp only [one_div, ← log_div_log, log_inv, neg_div, ← div_neg, hM]

Goal state after:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ Real.log 2 / -Real.log x ≤ Real.log 2 / -Real.log (max (f ↑p) (f ↑m))
Module: Mathlib.NumberTheory.Padics.ProperSpace

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
this : {y | ‖y‖ ≤ 1} ∈ 𝓝 0
⊢ IsCompact {y | ‖y‖ ≤ 1}

Tactic:
simpa only [isCompact_iff_compactSpace] using! PadicInt.compactSpace p

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
hs0 : 0 < s
n : ℕ
h : 1 < n
⊢ ↑m ≠ 1

Tactic:
norm_cast; omega

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
hs0 : 0 < s
n : ℕ
h : 1 < n
hfm : f ↑m = ↑m ^ s
⊢ ↑n ≠ 1

Tactic:
norm_cast; omega

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n : ℕ
⊢ ‖-∑ j ∈ range (p ^ t - 1), (p ^ t).choose (j + 1) • Δ_[1]^[n + (j + 1)] (⇑f) 0‖ ≤
    ↑((range (p ^ t - 1)).sup fun j ↦ ‖Δ_[1]^[n + (j + 1)] (⇑f) 0‖₊ / ↑p)

Tactic:
rw [norm_neg, ← coe_nnnorm, coe_le_coe]

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n : ℕ
⊢ ‖∑ j ∈ range (p ^ t - 1), (p ^ t).choose (j + 1) • Δ_[1]^[n + (j + 1)] (⇑f) 0‖₊ ≤
    (range (p ^ t - 1)).sup fun j ↦ ‖Δ_[1]^[n + (j + 1)] (⇑f) 0‖₊ / ↑p
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖↑(-1) ^ (n - i) * ↑(n.choose i)‖ * ‖f (↑i + ↑(p ^ t)) - f ↑i‖ ≤ ‖f (↑i + ↑(p ^ t)) - f ↑i‖

Tactic:
apply mul_le_of_le_one_left (norm_nonneg _)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖↑(-1) ^ (n - i) * ↑(n.choose i)‖ ≤ 1
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
⊢ ∃ n W, (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ i, ↑(W j) ⊆ ↑(U i)) ∧ univ ⊆ ⋃ j, ↑(W j) ∧ Pairwise (Disjoint on W)

Tactic:
by
  classical
  obtain ⟨n, V, hVle, hVun⟩ := hU.exists_finite_clopen_cover
  obtain ⟨W, hWle, hWun, hWd⟩ := Fintype.exists_disjointed_le V
  simp only [← SetLike.coe_set_eq, Clopens.coe_finset_sup, Finset.mem_univ, iUnion_true] at hWun
  let t : Finset (Fin n) := {j | W j ≠ ⊥}
  refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩
  · exact (Finset.mem_filter.mp (t.equivFin.symm k).2).2
  · exact match hVle (t.equivFin.symm k) with | ⟨i, hi⟩ => ⟨i, subset_trans (hWle _) hi⟩
  · obtain ⟨j, hj⟩ := mem_iUnion.mp <| (hWun ▸ hVun) hx
    have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩
    exact mem_iUnion.mpr ⟨t.equivFin ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, this⟩⟩, by simpa⟩
  · exact hWd.comp_of_injective <| Subtype.val_injective.comp t.equivFin.symm.injective

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : T2Space X
inst✝⁸ : CompactSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : AddCommGroup V
inst✝⁴ : UniformSpace V
inst✝³ : IsUniformAddGroup V
S : Set (V × V)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
⊢ {fg | ∀ x ∈ Set.univ, (fg.1 x, fg.2 x) ∈ S} ⊆ {(f, g) | ∀ (y : Y), (f y, g y) ∈ S}

Tactic:
by simp only [Set.mem_univ, true_implies, subset_refl]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
⊢ ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ U ×ˢ U ⊆ S

Tactic:
have : S ∈ 𝓝 (x, x) := mem_nhdsSet_iff_forall.mp hS _ rfl

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
this : S ∈ 𝓝 (x, x)
⊢ ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ U ×ˢ U ⊆ S
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 g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S

Tactic:
obtain ⟨n, E, hEne, hES, hEuniv, hEdis⟩ :=
    exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal f hS

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)
⊢ ∃ n g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S
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
x y z : ℤ_[p]
hz : (Polynomial.aeval x) F - (Polynomial.aeval y) F = z * (x - y)
⊢ ‖(Polynomial.aeval x) F - (Polynomial.aeval y) F‖ = ‖z‖ * ‖x - y‖

Tactic:
by simp [hz]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
⊢ ↑x₁ ≤ b.x

Tactic:
rw [hb'] at hb ⊢

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < ↑b.x.toNat
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
⊢ ↑x₁ ≤ ↑b.x.toNat
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x * a₁.y * a₁.x ≤ a.y * a₁.x * a₁.x

Tactic:
have := h.1; have := x_mul_y_le_y_mul_x h hax hay; gcongr

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r ≤ ↑j
⊢ j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1

Tactic:
exact Or.inr ⟨⌊(j + 1) / r⌋, (le_div_iff₀ h).2 ‹_›, Int.lt_floor_add_one _⟩

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

Goal state before:
pp: x : ℤ[i]
⊢ |norm x| = |x.re| * |x.re| + |x.im| * |x.im|

Tactic:
rw [abs_norm (by simp)]

Goal state after:
x : ℤ[i]
⊢ norm x = |x.re| * |x.re| + |x.im| * |x.im|
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
x✝ : ↑p ∣ { re := ↑k, im := -1 }
x : ℤ[i]
hx : { re := ↑k, im := -1 } = ↑p * x
hx0 : x = 0
⊢ -1 = 0

Tactic:
by simpa [hx0] using! congr_arg Zsqrtd.im hx

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
x✝ : ↑p ∣ { re := ↑k, im := 1 }
x : ℤ[i]
hx : { re := ↑k, im := 1 } = ↑p * x
hx0 : x = 0
⊢ 1 = 0

Tactic:
by simpa [hx0] using! congr_arg Zsqrtd.im hx

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
x : ℝ
h : max x 1 = 1 ∧ x < 1
⊢ x ≤ max x 1 ^ p

Tactic:
h.1,

Goal state after:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
x : ℝ
h : max x 1 = 1 ∧ x < 1
⊢ x ≤ 1 ^ p
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case one
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 1

Tactic:
exact ⟨1, 0, 0, 0, rfl⟩

Goal state after:
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
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
r : ℂ
hr : map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r
⊢ (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1)) * map (algebraMap ℤ ℂ) (f ^ p)

Tactic:
f.map_pow

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
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
r : ℂ
hr : map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r
⊢ (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1)) * map (algebraMap ℤ ℂ) f ^ p
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: ⊢ ∀ᶠ (x : ℝ) in residual ℝ, Liouville x

Tactic:
rw [Filter.Eventually, setOfPred_liouville_eq_irrational_inter_iInter_iUnion]

Goal state after:
⊢ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ∈ residual ℝ
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)
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))
⊢ ‖cexp r * (algebraMap ℤ ℂ) (eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p))) - (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:
← aeval_algebraMap_apply_eq_algebraMap_eval,

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))
⊢ ‖cexp r * (aeval ((algebraMap ℤ ℂ) 0)) (sumIDeriv (X ^ (p - 1) * f ^ p)) -
        (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 : ℚ
hr : r ≠ 0
h : LiouvilleWith p (x * ↑r)
⊢ LiouvilleWith p x

Tactic:
by
    simpa only [mul_assoc, ← Rat.cast_mul, mul_inv_cancel₀ hr, Rat.cast_one, mul_one] using
      h.mul_rat (inv_ne_zero hr)

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x, ↑x = -1

Tactic:
← Units.coeHom_apply,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x, (Units.coeHom (ZMod p)) x = -1
Module: Mathlib.Order.Bounds.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ IsGLB (range u) c ↔ IsGLB (⋃ i, s i) c

Tactic:
refine isGLB_congr ?_

Goal state after:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ lowerBounds (range u) = lowerBounds (⋃ i, s i)
Module: Mathlib.Order.Bounds.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ IsGLB (range u) c ↔ IsGLB (⋃ i, s i) c

Tactic:
refine isGLB_congr ?_
  simp_rw [range_eq_iUnion, lowerBounds_iUnion, lowerBounds_singleton, (hs _).lowerBounds_eq]

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

Goal state before:
pp: ⊢ volume
      (⋃ m,
        (fun x ↦ x + ↑m) ⁻¹'
          ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0

Tactic:
rw [measure_iUnion_null_iff]

Goal state after:
⊢ ∀ (i : ℤ),
    volume
        ((fun x ↦ x + ↑i) ⁻¹'
          ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
      0
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a x✝ : α
⊢ x✝ ∈ Iic a ↔ x✝ ∈ (ofObject (fun x1 x2 ↦ x1 ≤ x2) a).extent

Tactic:
simpa [mem_lowerPolar_iff] using! forall_ge_iff_le.symm

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a b : α
hb : b ≤ a
ha : a ∈ c.extent
⊢ b ∈ c.extent

Tactic:
obtain rfl | hb := hb.eq_or_lt

Goal state after:
case inl
α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
b : α
hb : b ≤ b
ha : b ∈ c.extent
⊢ b ∈ c.extent

case inr
α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a b : α
hb✝ : b ≤ a
ha : a ∈ c.extent
hb : b < a
⊢ b ∈ c.extent
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a b : α
hb : a ≤ b
ha : a ∈ c.intent
⊢ b ∈ c.intent

Tactic:
obtain rfl | hb := hb.eq_or_lt

Goal state after:
case inl
α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a : α
ha : a ∈ c.intent
hb : a ≤ a
⊢ a ∈ c.intent

case inr
α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a b : α
hb✝ : a ≤ b
ha : a ∈ c.intent
hb : a < b
⊢ b ∈ c.intent
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
s : Set α
f : α → β
⊢ Tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ PTendsto (PFun.res f s) l₁ l₂

Tactic:
simp only [Tendsto, PTendsto, pmap_res]

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ DirectedOn (fun x1 x2 ↦ x1 ≥ x2) (↑I)ᶜ

pp: case right.refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ

Tactic:
· intro x hx y hy
    exact ⟨x ⊓ y, fun h => (hI h).elim hx hy, inf_le_left, inf_le_right⟩

Goal state after:
case right.refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
⊢ y ∈ I

Tactic:
have hxcI : xᶜ ∈ I := h.resolve_left hxI

Goal state after:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
hxcI : xᶜ ∈ I
⊢ y ∈ I
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ ∃ t ∈ P, x ∈ t

Tactic:
by
  refine ⟨fun hx ↦ ?_, fun ⟨t, htP, hxt⟩ ↦ subset_of_mem htP hxt⟩
  rwa [← P.sUnion_eq, mem_sUnion] at hx

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case pos
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : α
ha : a ∈ u
h : ∃ b, P.Rel a ↑b
⊢ P.Rel a (f₀ h.choose)

pp: case neg
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : α
ha : a ∈ u
h : ¬∃ b, P.Rel a ↑b
⊢ P.Rel a (P.rep ⋯)

Tactic:
· exact h.choose_spec.trans <| h_mem h.choose h.choose_spec.right_mem

Goal state after:
case neg
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : α
ha : a ∈ u
h : ¬∃ b, P.Rel a ↑b
⊢ P.Rel a (P.rep ⋯)
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
⊢ ⊤ ≤ sInf {s | ⊤ ≤ ↑s}

Tactic:
change _ ≤ restrictAux S ⊤

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
⊢ ⊤ ≤ Sublocale.restrictAux✝ S ⊤
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type (Lex (PUnit.{u + 1} × α)) = type α

Tactic:
exact (Prod.Lex.uniqueProd PUnit α).type_congr

Goal state after: