mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖const ι (3 / 4 * δ)‖ ≤ δ

Tactic:
← const_def,

Goal state after:
case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖fun x ↦ 3 / 4 * δ‖ ≤ δ
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : T2Space F
u v : E →L[𝕜] F
h_equiv : ↑u ≈ ↑v
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔ IsStrictMap ⇑v ∧ IsClosed[inst✝³] ↑(↑v).range

Tactic:
let A := u.toLinearMap.eqLocus v.toLinearMap
  have : A.CoFG := equiv_iff_eqLocus_coFG.mp h_equiv
  exact ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_eqOn u v A
    LinearMap.eqOn_eqLocus

Goal state after:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖const ι (3 / 4 * δ)‖ ≤ δ

Tactic:
← const_def,

Goal state after:
case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖fun x ↦ 3 / 4 * δ‖ ≤ δ
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ∃ ε > 0, IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (Metric.ball (t₀ / a) ε)

Tactic:
refine ⟨ε / |a|, by positivity, ?_⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (Metric.ball (t₀ / a) (ε / |a|))
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
⊢ picard f (↑t₀) x α.compProj ↑t₀ ∈ closedBall x₀ ↑r

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
⊢ IsFixedPt (next hf hx) α ↔ ∀ (t : ↑(Icc tmin tmax)), α.toFun t = picard f (↑t₀) x α.compProj ↑t

Tactic:
constructor
  · exact fun hα t ↦ congrArg (· t) hα |>.symm
  · intro h
    ext t
    rw [h, next_apply]

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
⊢ EqOn f g (Icc t₀ b)

Tactic:
have hss : Ico t₀ b ⊆ Ioo a b := Ico_subset_Ioo_left ht.1

Goal state after:
case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
hss : Ico t₀ b ⊆ Ioo a b
⊢ EqOn f g (Icc t₀ b)
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: case inl
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
ha : ‖a‖₊ = 1
this : 1 ≤ (p.cauchyBound - 1) * ↑p.natDegree
nh : 1 = p.cauchyBound
⊢ False

Tactic:
simp [← nh, tsub_self] at this

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree < Q.degree
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 0)

Tactic:
by
  rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X] at hdeg
  convert! (div_tendsto_atTop_zero_of_degree_lt _ _ hdeg).comp tendsto_neg_atBot_atTop using 2
  simp

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree < Q.degree
hp : ¬P = 0
hq : Q ≠ 0
⊢ (fun x ↦ eval x P) =o[atTop] fun x ↦ eval x Q

Tactic:
have hPQ : ∀ᶠ x in atTop, Q.eval x = 0 → P.eval x = 0 :=
      mem_of_superset (eventually_atTop_not_isRoot Q hq) fun x h h' ↦ absurd h' h

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree < Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
⊢ (fun x ↦ eval x P) =o[atTop] fun x ↦ eval x Q
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
⊢ (fun x ↦ eval x P) =O[atTop] fun x ↦ eval x Q

Tactic:
have hPQ : ∀ᶠ x in atTop, Q.eval x = 0 → P.eval x = 0 :=
      mem_of_superset (eventually_atTop_not_isRoot Q hq) fun x h h' ↦ absurd h' h

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
⊢ (fun x ↦ eval x P) =O[atTop] fun x ↦ eval x Q
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : ZeroHomClass F R ℝ
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i

Tactic:
by
  by_cases h_supp : p.support.Nonempty
  · simp only [gaussNorm, h_supp]
    obtain ⟨i, hi1, hi2⟩ := Finset.exists_mem_eq_sup' h_supp fun i ↦ (v (p.coeff i) * c ^ i)
    exact ⟨i, hi2⟩
  · simp_all

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inl
R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q = 0
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

pp: case inr
R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

Tactic:
· simp [hpq, hc, gaussNorm_nonneg, mul_nonneg]

Goal state after:
case inr
R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum

Tactic:
nth_rw 1 [(IsAlgClosed.splits p).eq_prod_roots]

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0
⊢ (C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) p.roots).prod).logMahlerMeasure =
    log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
Module: Mathlib.Analysis.Rat.NatSqrt.Real

Goal state before:
pp: x prec : ℕ
h : 0 < prec
this✝¹ : ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2
this✝ : ↑x < ↑((x.ratSqrt prec + 1 / ↑prec) ^ 2)
this : √↑x < √(↑(x.ratSqrt prec + 1 / ↑prec) ^ 2)
⊢ 0 ≤ ↑(x.ratSqrt prec) + 1 / ↑prec

Tactic:
exact add_nonneg (by simpa using ratSqrt_nonneg _ _) (by simp)

Goal state after:
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
⊢ ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊

Tactic:
have := NeZero.ne b
  induction n with
  | zero => simp [Nat.floor_eq_zero.mpr hx.right]
  | succ n ih =>
    rw [Finset.sum_range_succ, mul_add, pow_succ', mul_assoc, ih, ofDigitsTerm, digits, ← pow_succ',
      mul_left_comm, mul_inv_cancel₀ (by positivity), mul_one, mul_comm x, pow_succ', mul_assoc]
    set y := (b : ℝ) ^ n * x
    norm_cast
    rw [← Nat.cast_mul_floor_div_cancel (a := y) (show b ≠ 0 by lia),
      Fin.val_ofNat, Nat.div_add_mod]

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: ⊢ stdPart ω = 0

Tactic:
rw [stdPart_eq_zero]
  exact archimedeanClassMk_omega_neg.ne

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
⊢ ∑ x ∈ S.toFinset, ↑(count x S) * ‖x.prod‖ ≤
    ∑ x ∈ S.toFinset, ↑(count x S) * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
by
      gcongr with x hx
      rw [Finset.prod_multiset_map_count, Finset.prod_multiset_count, norm_prod]
      simp_rw [norm_pow]
      exact this x hx

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
⊢ Irrational (- -x)

Tactic:
by rwa [neg_neg]

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k

Tactic:
rw [W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff₀ (integral_sin_pow_pos _)]

Goal state after:
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) ≤ ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ sinh (arcosh x) / cosh (arcosh x) = √(x ^ 2 - 1) / x

Tactic:
sinh_arcosh hx,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ √(x ^ 2 - 1) / cosh (arcosh x) = √(x ^ 2 - 1) / x
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n m : ℕ
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
suffices ∀ {k}, (agmSequences x y k).1 ≤ (agmSequences x y k).2 by
    obtain h | h := le_total n m
    · exact (agmSequences_fst_monotone h).trans this
    · exact this.trans (agmSequences_snd_antitone h)
  intro k
  induction k generalizing x y with
  | zero => exact sqrt_mul_le_half_add ..
  | succ n ih => exact ih

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Icc (-1) 1
⊢ log √((1 + x) / (1 - x)) = 1 / 2 * log ((1 + x) / (1 - x))

Tactic:
log_sqrt <| div_nonneg (by grind) (by grind),

Goal state after:
x : ℝ
hx : x ∈ Icc (-1) 1
⊢ log ((1 + x) / (1 - x)) / 2 = 1 / 2 * log ((1 + x) / (1 - x))
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
⊢ (x.agmSequences y n).1 < x.agm y

Tactic:
rw [agm_eq_agm_agmSequences_fst_agmSequences_snd n]
  set p := (agmSequences x y n).1
  set q := (agmSequences x y n).2
  apply (?_ : p < sqrt (p * q)).trans_le (agmSequences_fst_le_agm 0)
  have ppos : 0 < p :=
    (show 0 < sqrt (x * y) by positivity).trans_le (agmSequences_fst_monotone zero_le)
  have plq : p < q := agmSequences_fst_lt_snd_of_ne hn ..
  nth_rw 1 [← mul_self_sqrt p, sqrt_mul]
  gcongr

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo 0 1
⊢ artanh 0 < artanh x

Tactic:
artanh_lt_artanh_iff (by grind) (by grind)

Goal state after:
x : ℝ
hx : x ∈ Ioo 0 1
⊢ 0 < x
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 0
⊢ artanh x < artanh 0

Tactic:
artanh_lt_artanh_iff (by grind) (by grind)

Goal state after:
x : ℝ
hx : x ∈ Ioo (-1) 0
⊢ x < 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ DifferentiableAt ℝ binEntropy p ↔ p ≠ 0 ∧ p ≠ 1

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ differentiableAt_binEntropy h.1 h.2⟩
    <;> rintro rfl

Goal state after:
case refine_1
h : DifferentiableAt ℝ binEntropy 0
⊢ False

case refine_2
h : DifferentiableAt ℝ binEntropy 1
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inr.inr
q : ℕ
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ qaryEntropy q p

Tactic:
exact (qaryEntropy_pos hp₀ hp₁).le

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
⊢ I (n + 2) θ * θ ^ 2 = 2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ

Tactic:
rw [recursion' (n + 1)]
  push_cast
  ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case pos.inl.inl
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ Ioo 0 1
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

pp: case pos.inl.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {0}
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

pp: case pos.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {1}
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

Tactic:
· exact monotoneOn_nnrpow_Ioo hp ha hb hab

Goal state after:
case pos.inl.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {0}
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

case pos.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {1}
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
by_cases ht' : t = 0

Goal state after:
case pos
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
ht' : t = 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

case neg
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: ⊢ Tendsto (fun z ↦ z / 2) (𝓝[≠] 0) (𝓝 (0 / 2)) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, n / 2 ∈ {0}ᶜ

Tactic:
exact ⟨(tendsto_id.div_const _).mono_left nhdsWithin_le_nhds,
      eventually_of_mem self_mem_nhdsWithin fun x hx ↦ div_ne_zero hx two_ne_zero⟩

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

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n

Tactic:
eulerMascheroniSeq',

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ (if n + 1 = 0 then 2 else ↑(harmonic (n + 1)) - log ↑(n + 1)) < if n = 0 then 2 else ↑(harmonic n) - log ↑n
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ eulerMascheroniSeq' n = ↑(harmonic n) - log ↑n

Tactic:
eulerMascheroniSeq',

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (if n = 0 then 2 else ↑(harmonic n) - log ↑n) = ↑(harmonic n) - log ↑n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

pp: case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : ¬s = 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Tactic:
· rw [h, (by ring : 2 - 1 = (1 : ℂ)), Gammaℝ_one, Gammaℝ,
    neg_div, (by simp : (1 + 1) / 2 = (1 : ℂ)), Complex.Gamma_one, Gammaℂ_one,
    mul_one, Complex.sin_pi_div_two, mul_one, cpow_neg_one, mul_one, inv_inv,
    div_mul_cancel₀ _ (ofReal_ne_zero.mpr pi_ne_zero), inv_one]

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : ¬s = 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case succ
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
n : ℕ
hn : deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
⊢ deriv f (↑(n + 1) + 1) = deriv f 1 + ↑(harmonic (n + 1))

Tactic:
cast_succ,

Goal state after:
case succ
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
n : ℕ
hn : deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
⊢ deriv f (↑n + 1 + 1) = deriv f 1 + ↑(harmonic (n + 1))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
⊢ IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
    a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ

Tactic:
have hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), rpowIntegrand₀₁ p x 0 = 0 := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi]
    simp

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₀₁ x 0 = 0
⊢ IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
    a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
h : logb b b = 1
h' : log b = 0
⊢ False

Tactic:
by simp [logb, h'] at h

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
⊢ 0 ≤ y / x - 1

Tactic:
rwa [le_sub_iff_add_le, le_div_iff₀ x_pos, zero_add, one_mul]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
⊢ ‖y‖ ≤ dist y ((1 - ε / 4) • x) + ‖(1 - ε / 4) • x‖

Tactic:
by
      simpa using dist_triangle y ((1 - ε / 4) • x) 0

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ (b : ℝ), R ≤ b → ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = b → ‖f l x‖ ≤ u r l
l : ↥L.lattice
hl : l ∈ {x | (fun n ↦ ∀ x ∈ Metric.ball 0 r, ‖f n x‖ ≤ u r n) x}ᶜ
s : ℂ
hs : ‖s‖ < r
hs' : u r l < ‖f l s‖
⊢ ‖l‖ ≤ R

Tactic:
contrapose! hs'

Goal state after:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ (b : ℝ), R ≤ b → ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = b → ‖f l x‖ ≤ u r l
l : ↥L.lattice
hl : l ∈ {x | (fun n ↦ ∀ x ∈ Metric.ball 0 r, ‖f n x‖ ≤ u r n) x}ᶜ
s : ℂ
hs : ‖s‖ < r
hs' : R < ‖l‖
⊢ ‖f l s‖ ≤ u r l