mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : NonarchimedeanRing R
inst✝ : CompleteSpace R
f : α → R
g : β → R
hf : Summable f
hg : Summable g
⊢ Summable fun i ↦ f i.1 * g i.2

Tactic:
rw [NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero] at *
  exact tendsto_mul_cofinite_nhds_zero hf hg

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ Tendsto (fun k ↦ (↑m * f ↑m / (f ↑m - 1)) ^ (↑k)⁻¹ * f ↑m ^ logb ↑m ↑n) atTop (𝓝 (1 * f ↑m ^ logb ↑m ↑n))

Tactic:
exact (tendsto_const_rpow_inv (expr_pos hm notbdd)).mul_const _

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]
    refine nnnorm_sum_le_of_forall_le (fun i hi ↦ Finset.le_sup_of_le hi ?_)
    rw [← Nat.cast_smul_eq_nsmul ℤ_[p], div_eq_inv_mul]
    refine (nnnorm_smul_le _ _).trans <| mul_le_mul_of_nonneg_right ?_ (by simp only [zero_le])
    -- remains to show norm of binomial coeff is `≤ p⁻¹`
    rw [mem_range] at hi
    have : 0 < (p ^ t).choose (i + 1) := Nat.choose_pos (by omega)
    rw [← zpow_neg_one, ← coe_le_coe, coe_nnnorm, PadicInt.norm_eq_zpow_neg_valuation
      (mod_cast this.ne'), coe_zpow, NNReal.coe_natCast,
      zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt), neg_le_neg_iff,
      ← PadicInt.valuation_coe, PadicInt.coe_natCast, Padic.valuation_natCast, Nat.one_le_cast]
    exact one_le_padicValNat_of_dvd this.ne' <| hp.out.dvd_choose_pow (by lia) (by omega)

Goal state after:
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]
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
n : ℕ
⊢ ‖mahlerTerm (Δ_[1]^[n] (⇑f) 0) n‖ ≤
    ‖({ toFun := fun f ↦ { toFun := fun x ↦ Δ_[1]^[x] (⇑f) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }
          (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f) 0) b)).toBCF‖

Tactic:
refine le_trans (le_of_eq ?_) (BoundedContinuousFunction.norm_coe_le_norm _ n)

Goal state after:
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]
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
n : ℕ
⊢ ‖mahlerTerm (Δ_[1]^[n] (⇑f) 0) n‖ =
    ‖({ toFun := fun f ↦ { toFun := fun x ↦ Δ_[1]^[x] (⇑f) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ }
            (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f) 0) b)).toBCF
        n‖
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]
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
⊢ ‖f‖ ≤
    ‖({ toFun := fun f ↦ { toFun := fun x ↦ Δ_[1]^[x] (⇑f) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }
          f).toBCF‖

Tactic:
rw [← (hasSum_mahler f).tsum_eq]
      refine (norm_tsum_le _).trans (ciSup_le fun n ↦ ?_)
      refine le_trans (le_of_eq ?_) (BoundedContinuousFunction.norm_coe_le_norm _ n)
      simp [(hasSum_mahler f).tsum_eq]

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
this : S ∈ 𝓝 (x, x)
⊢ ?m.37

Tactic:
mem_nhds_prod_iff'

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
this✝ : S ∈ 𝓝 (x, x)
this : ∃ u v, IsOpen[inst✝] u ∧ x ∈ u ∧ IsOpen[inst✝] v ∧ x ∈ v ∧ u ×ˢ v ⊆ S
⊢ ?m.37
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²¹ : Field K
inst✝²⁰ : Field L
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.LiesOver p
inst✝¹⁴ : FiniteDimensional K L
inst✝¹³ : MulSemiringAction Gal(L/K) B
inst✝¹² : IsGaloisGroup Gal(L/K) A B
inst✝¹¹ : IsDedekindDomain A
inst✝¹⁰ : IsDedekindDomain B
inst✝⁹ : Module.Finite A B
inst✝⁸ : Module.IsTorsionFree A B
inst✝⁷ : Ring.HasFiniteQuotients A
inst✝⁶ : P.IsMaximal
E : Type u_6
inst✝⁵ : Field E
inst✝⁴ : Algebra E L
inst✝³ : IsInertiaField K L P E
inst✝² : IsGalois K L
inst✝¹ : Algebra K E
inst✝ : IsScalarTower K E L
hp : p ≠ ⊥
this : p.IsMaximal
⊢ Module.finrank K E = (p.primesOver B).ncard * p.inertiaDegIn B

Tactic:
have : FiniteDimensional E L := FiniteDimensional.right K E L

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²¹ : Field K
inst✝²⁰ : Field L
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.LiesOver p
inst✝¹⁴ : FiniteDimensional K L
inst✝¹³ : MulSemiringAction Gal(L/K) B
inst✝¹² : IsGaloisGroup Gal(L/K) A B
inst✝¹¹ : IsDedekindDomain A
inst✝¹⁰ : IsDedekindDomain B
inst✝⁹ : Module.Finite A B
inst✝⁸ : Module.IsTorsionFree A B
inst✝⁷ : Ring.HasFiniteQuotients A
inst✝⁶ : P.IsMaximal
E : Type u_6
inst✝⁵ : Field E
inst✝⁴ : Algebra E L
inst✝³ : IsInertiaField K L P E
inst✝² : IsGalois K L
inst✝¹ : Algebra K E
inst✝ : IsScalarTower K E L
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : FiniteDimensional E L
⊢ Module.finrank K E = (p.primesOver B).ncard * p.inertiaDegIn B
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ ∀ (d1 d2 : ℕ), (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)

Tactic:
simp +contextual [← and_assoc, Nat.dvd_lcm_left, Nat.dvd_lcm_right]

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

Goal state before:
pp: case hH.refine_2
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
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
γ : Γˣ
x✝ : ∃ a, ¬a = 0 ∧ ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
ka : ℤ
hab : v ↑πᵥ ^ ka * ↑γ = v b
hka : v a = v ↑πᵥ ^ ka
kb : ℤ
hkb : v b = v ↑πᵥ ^ kb
⊢ ∃ k, ⋯.unit ^ k = γ

Tactic:
hkb

Goal state after:
case hH.refine_2
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
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
γ : Γˣ
x✝ : ∃ a, ¬a = 0 ∧ ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
ka : ℤ
hka : v a = v ↑πᵥ ^ ka
kb : ℤ
hab : v ↑πᵥ ^ ka * ↑γ = v ↑πᵥ ^ kb
hkb : v b = v ↑πᵥ ^ kb
⊢ ∃ k, ⋯.unit ^ k = γ
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
⊢ (if n = 1 then 1 else 0) ≤
    ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0

Tactic:
split_ifs

Goal state after:
case pos
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : n = 1
⊢ 1 ≤ ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0

case neg
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
⊢ 0 ≤ ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m

Tactic:
obtain ⟨i, hσ⟩ := this (fun x => ↑(f x)) <| by
    rw [← @zero_mul (ZMod 2) _ m, ← show ((2 : ℤ) : ZMod 2) = 0 from rfl, ← Int.cast_mul, ← h]
    simp only [Int.cast_add, Int.cast_pow]
    rfl

Goal state after:
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
hσ : ↑(f i) ^ 2 + ↑(f ((swap i 0) 1)) ^ 2 = 0 ∧ ↑(f ((swap i 0) 2)) ^ 2 + ↑(f ((swap i 0) 3)) ^ 2 = 0
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
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.IsRankOneDiscrete
inst✝¹ : IsTrivialOn K v
inst✝ : DecidableEq K⟮X⟯
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u, v.IsEquiv (valuation K⟮X⟯ u))

Tactic:
rcases lt_or_ge 1 (v X) with hlt | hge
  /- Infinity case -/
  · have hv := valuation_isEquiv_inftyValuation_of_one_lt_valuation_X hlt
    refine .inl ⟨hv, ?_⟩
    simp only [ExistsUnique, not_exists, not_and, not_forall]
    intro pw hw
    exact absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw)
  /- Prime case -/
  · obtain ⟨pw, hw⟩ := valuation_isEquiv_adic_of_valuation_X_le_one hge
    exact .inr ⟨⟨pw, hw, fun pw' hw' ↦ eq_of_valuation_isEquiv_valuation (hw'.symm.trans hw)⟩,
      fun hv ↦ absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw)⟩

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a.a
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes
⊢ s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹ =
    ∑ l ∈ s.prodPrimes.divisors, if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0

Tactic:
simp_rw [nu_inv_eq_sum_divisors_inv_selbergTerms hgcd_dvd, ← sum_filter, mul_sum]

Goal state after:
case a.a
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes
⊢ ∑ i ∈ s.prodPrimes.divisors with i ∣ d1.gcd d2, s.nu d1 * w d1 * s.nu d2 * w d2 * (selbergTerms i)⁻¹ =
    ∑ a ∈ s.prodPrimes.divisors with a ∣ d1.gcd d2, (selbergTerms a)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2)
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
⊢ (toComplex (x / y)).im = ↑(round (toComplex x / toComplex y).im)

Tactic:
by
  rw [div_def, ← @Rat.round_cast ℝ _ _, ← @Rat.round_cast ℝ _ _]
  simp [-Rat.round_cast, mul_assoc, div_eq_mul_inv, add_mul]

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ IsSquare (-1) ↔ ∀ q ∈ n.primeFactors, q % 4 ≠ 3

Tactic:
by
  refine ⟨fun H q hq ↦ Nat.mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one hq H,
    fun H ↦ ?_⟩
  induction n using induction_on_primes with
  | zero => exact False.elim (hn.ne_zero rfl)
  | one => exact ⟨0, by simp only [mul_zero, eq_iff_true_of_subsingleton]⟩
  | prime_mul p n hpp ih =>
    have : Fact p.Prime := ⟨hpp⟩
    have hcp : p.Coprime n := by
      by_contra hc
      exact hpp.not_isUnit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
    have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr <| H _ <|
      Nat.mem_primeFactors.mpr ⟨hpp, Nat.dvd_mul_right .., Squarefree.ne_zero hn⟩
    exact ZMod.isSquare_neg_one_mul hcp hp₁ <| ih hn.of_mul_right fun q hqp => H q <|
        Nat.mem_primeFactors.mpr ⟨Nat.prime_of_mem_primeFactors hqp,
          dvd_mul_of_dvd_right (Nat.dvd_of_mem_primeFactors hqp) _, Squarefree.ne_zero hn⟩

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case inr
n : ℕ
hn₀ : n > 0
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)

Tactic:
refine eq_sq_add_sq_iff_eq_sq_mul.trans ⟨fun ⟨a, b, h₁, h₂⟩ q hq h ↦ ?_, fun H ↦ ?_⟩

Goal state after:
case inr.refine_1
n : ℕ
hn₀ : n > 0
x✝ : ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
q : ℕ
hq : q ∈ n.primeFactors
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
⊢ Even (padicValNat q n)

case inr.refine_2
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
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 ≤ 1 ^ p

Tactic:
one_pow

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
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case pos
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
hx1 : x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ 1 ^ p

Tactic:
one_pow

Goal state after:
case pos
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
hx1 : x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ 1
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case pos
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
hx1 : x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ 1

Tactic:
exact pow_le_one₀ (mul_nonneg hx.1.le (norm_nonneg _)) hx1

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

Goal state before:
pp: m : ℝ
hm : 1 < m
k : ℕ
⊢ Summable fun i ↦ 1 / m ^ (i + (k + 1))!

Tactic:
convert! (summable_nat_add_iff (k + 1)).2 (LiouvilleNumber.summable hm)

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

Goal state before:
pp: case e'_3
r : ℚ
n : ℕ
⊢ ↑r.num * 2 / (↑r.den * 2) = ↑r

Tactic:
Eq.refl (2 : ℝ)

Goal state after:
case e'_3
r : ℚ
n : ℕ
⊢ ↑r.num * 2 / (↑r.den * 2) = ↑r
Module: Mathlib.NumberTheory.Wilson

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

Tactic:
conv =>
    congr
    congr
    rw [← Nat.add_one_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x ∈ Ico 1 (p - succ 0).succ, ↑x = -1
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
⊢ False

Tactic:
have hm : m ∣ (n - 1)! := Nat.dvd_factorial (pos_of_gt hm2) (le_pred_of_lt hm3)

Goal state after:
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ False
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
a b : α
r : α → α → Prop
⊢ ¬IncompRel r a b ↔ SymmGen r a b

Tactic:
by
  rw [← not_symmGen_iff, not_not]

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
⊢ x ⊔ y ∈ carrier

Tactic:
by
    suffices x ⊔ y = sSup {x, y} by exact this ▸ sSupClosed' (fun z hz ↦ by aesop)
    simp [sSup_singleton]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: 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
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun y ↦ x + y) ∘ fun y ↦ p • y
this :
  (fun y ↦ x + y) '' (fun y ↦ p • y) '' approxAddOrderOf 𝕊 n (δ n) ⊆
    (fun y ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) (↑p * δ n)
⊢ (fun y ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) (↑p * δ n) ⊆ approxAddOrderOf 𝕊 n (↑p * δ n)

Tactic:
convert! approxAddOrderOf.vadd_subset_of_coprime (p * δ n) h_cop

Goal state after:
case e'_4
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
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun y ↦ x + y) ∘ fun y ↦ p • y
this :
  (fun y ↦ x + y) '' (fun y ↦ p • y) '' approxAddOrderOf 𝕊 n (δ n) ⊆
    (fun y ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) (↑p * δ n)
⊢ n = addOrderOf x * (n / p)
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case refine_1
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
inst✝¹ : CardinalInterFilter l₁ c
inst✝ : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #↑S < c
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
⊢ ⋂₀ S ∈ l₁

Tactic:
refine (cardinal_sInter_mem hSc).2 fun s hs => ?_

Goal state after:
case refine_1
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
inst✝¹ : CardinalInterFilter l₁ c
inst✝ : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #↑S < c
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₁
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case refine_2
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
inst✝¹ : CardinalInterFilter l₁ c
inst✝ : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #↑S < c
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
⊢ ⋂₀ S ∈ l₂

Tactic:
refine (cardinal_sInter_mem hSc).2 fun s hs => ?_

Goal state after:
case refine_2
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
inst✝¹ : CardinalInterFilter l₁ c
inst✝ : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #↑S < c
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₂
Module: Mathlib.Order.Interval.Set.SurjOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
⊢ SurjOn f (Icc a b) (Icc (f a) (f b))

Tactic:
by
  intro p hp
  rcases eq_endpoints_or_mem_Ioo_of_mem_Icc hp with (rfl | rfl | hp')
  · exact ⟨a, left_mem_Icc.mpr hab, rfl⟩
  · exact ⟨b, right_mem_Icc.mpr hab, rfl⟩
  · exact image_mono Ioo_subset_Icc_self <|
      surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'

Goal state after:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
i j k : ι
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) (Prod.Lex (fun x1 x2 ↦ x1 < x2) WellOrderingRel) (f i, g i, i) (f j, g j, j) →
    MonovaryOrder f g j k → MonovaryOrder f g i k

Tactic:
exact _root_.trans

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
⊢ r w x✝ → r y✝ z✝ → r (w ⊓ y✝) (x✝ ⊓ z✝)

Tactic:
h1

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
h1 : r w x✝
⊢ r y✝ z✝ → r (w ⊓ y✝) (x✝ ⊓ z✝)
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
⊢ r w x✝ → r y✝ z✝ → r (w ⊔ y✝) (x✝ ⊔ z✝)

Tactic:
h1

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
h1 : r w x✝
⊢ r y✝ z✝ → r (w ⊔ y✝) (x✝ ⊔ z✝)
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
hyJ : y ∈ ↑J
⊢ y ∈ I

Tactic:
coe_sup_eq

Goal state after:
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
hyJ : y ∈ {x_1 | ∃ i ∈ I, ∃ j ∈ principal x, x_1 = i ⊔ j}
⊢ y ∈ I
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ f a b ≤ ⨆ y ∈ Y, f a y

Tactic:
apply le_iSup₂ b hb

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ f a b ≤ ⨆ y ∈ Y, f a y

Tactic:
apply le_iSup₂ b hb

Goal state after: