mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case inr.inr.inr.inr.inl
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p r : ℝ≥0∞
e : (i : ι) → E i
f : (i : ι) → F i
he : Memℓp e p
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
h : Nonempty ι
hK : 0 ≤ K
hp : 0 < p.toReal
hpqr : p.HolderTriple ∞ p
hf : Memℓp f ∞
hpqr' : r = p
⊢ Memℓp (fun i ↦ ((B i) (e i)) (f i)) p

Tactic:
exact he.bilin_of_top_right B hBK hf

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
v : F →L[𝕜] E
hvu : (LinearMap.id.eqLocus (↑v ∘ₗ ↑u)).CoFG
huv : (LinearMap.id.eqLocus (↑u ∘ₗ ↑v)).CoFG
E₁ : Submodule 𝕜 E := (↑(ContinuousLinearMap.id 𝕜 E)).eqLocus ↑(v ∘SL u)
F₁ : Submodule 𝕜 F := (↑(ContinuousLinearMap.id 𝕜 F)).eqLocus ↑(u ∘SL v)
u_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
⊢ ∃ E₁ F₁,
    IsClosed[inst✝³] ↑E₁ ∧
      IsClosed[inst✝²] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible

Tactic:
have v_mapsto : MapsTo v F₁ E₁ := fun x hx ↦ congr(v $hx)

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
v : F →L[𝕜] E
hvu : (LinearMap.id.eqLocus (↑v ∘ₗ ↑u)).CoFG
huv : (LinearMap.id.eqLocus (↑u ∘ₗ ↑v)).CoFG
E₁ : Submodule 𝕜 E := (↑(ContinuousLinearMap.id 𝕜 E)).eqLocus ↑(v ∘SL u)
F₁ : Submodule 𝕜 F := (↑(ContinuousLinearMap.id 𝕜 F)).eqLocus ↑(u ∘SL v)
u_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
v_mapsto : MapsTo ⇑v ↑F₁ ↑E₁
⊢ ∃ E₁ F₁,
    IsClosed[inst✝³] ↑E₁ ∧
      IsClosed[inst✝²] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case inr.inr
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fact (1 ≤ q)
inst✝ : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
e : ↥(lp E p)
f : ↥(lp F q)
hp : 1 ≤ p.toReal
hq : 1 ≤ q.toReal
⊢ ‖((holderₗ r B hBK) e) f‖ ≤ ↑K * ‖e‖ * ‖f‖

Tactic:
have hpqr := hpqr.toReal r (zero_lt_one.trans_le hp) (zero_lt_one.trans_le hq)
      have hp := hpqr.pos
      have hq := hpqr.symm.pos
      refine norm_le_of_forall_sum_le hpqr.pos' (by positivity) fun s ↦ ?_
      simp only [holderₗ_apply_apply_coe]
      calc
        _ ≤ K ^ r.toReal * (‖e‖ ^ p.toReal) ^ (r.toReal / p.toReal) *
          (‖f‖ ^ q.toReal) ^ (r.toReal / q.toReal) :=
          Memℓp.holder_gen_bound r hp hq B hBK (by positivity) (by positivity)
            (sum_rpow_le_norm_rpow hp e) (sum_rpow_le_norm_rpow hq f) s
        _ ≤ _ := by
          rw [← Real.rpow_mul, ← Real.rpow_mul]
          · simp only [← mul_div_assoc, ne_eq, hp.ne', not_false_eq_true, mul_div_cancel_left₀,
            hq.ne', fieldLe]
            rw [Real.mul_rpow, Real.mul_rpow]
            all_goals positivity
          all_goals positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case h₂
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (F i)
p q : ℝ≥0∞
H : Type u_6
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : NormedSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fact (1 ≤ q)
inst✝ : p.HolderConjugate q
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
⊢ ‖holderL 1 B hBK‖ ≤ ↑K

Tactic:
exact norm_holderL_le 1 B hBK

Goal state after:
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
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
N : Submodule 𝕜 E := A ⊓ (↑u).ker
π : E →L[𝕜] E ⧸ N := N.mkQL
v : E ⧸ N →L[𝕜] F := N.liftQL u ⋯
π_quot : IsOpenQuotientMap ⇑π
u_eq : u = v ∘SL π
B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A
B_cofg : B.CoFG
v_ker : Disjoint (↑v).ker B
comap_B : comap (↑π) B = A
A_mapsTo_B : MapsTo ⇑π ↑A ↑B
B_closed : IsClosed[QuotientModule.Quotient.topologicalSpace N] ↑B
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔
    IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range

Tactic:
have step4_output : (IsStrictMap v ∧ IsClosed (v.range : Set F)) ↔
      (IsStrictMap (v.domRestrict B) ∧ IsClosed ((v.domRestrict B).range : Set F)) :=
    step4 v B B_closed v_ker

Goal state after:
𝕜 : 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
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
N : Submodule 𝕜 E := A ⊓ (↑u).ker
π : E →L[𝕜] E ⧸ N := N.mkQL
v : E ⧸ N →L[𝕜] F := N.liftQL u ⋯
π_quot : IsOpenQuotientMap ⇑π
u_eq : u = v ∘SL π
B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A
B_cofg : B.CoFG
v_ker : Disjoint (↑v).ker B
comap_B : comap (↑π) B = A
A_mapsTo_B : MapsTo ⇑π ↑A ↑B
B_closed : IsClosed[QuotientModule.Quotient.topologicalSpace N] ↑B
step4_output :
  IsStrictMap ⇑v ∧ IsClosed[inst✝³] ↑(↑v).range ↔
    IsStrictMap ⇑(v.domRestrict B) ∧ IsClosed[inst✝³] ↑(↑(v.domRestrict B)).range
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔
    IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (cthickening ε s)

Tactic:
cthickening_eq_iInter_thickening''

Goal state after:
α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (⋂ ε_1, ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (cthickening ε s)

Tactic:
cthickening_eq_iInter_thickening''

Goal state after:
α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (⋂ ε_1, ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: K x : ℝ
⊢ gronwallBound 0 K 0 x = 0

Tactic:
by
  simp only [gronwallBound_ε0, zero_mul]

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

Goal state before:
pp: case hB
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ ∀ (x : ℝ), HasDerivAt (fun x ↦ gronwallBound δ K ε' (x - a)) (?m.108 x) x

Tactic:
exact fun x => hasDerivAt_gronwallBound_shift δ K ε' x a

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r
t : ↑(Icc tmin tmax)
⊢ ‖α.toFun t - α.toFun t₀‖ ≤ ↑L * |↑t - ↑t₀|

Tactic:
rw [← dist_eq_norm]

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r
t : ↑(Icc tmin tmax)
⊢ dist (α.toFun t) (α.toFun t₀) ≤ ↑L * |↑t - ↑t₀|
Module: Mathlib.Analysis.Polynomial.Basic

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

Tactic:
by
  refine ⟨fun h => ?_, div_tendsto_atTop_zero_of_degree_lt P Q⟩
  by_cases hPQ : P.leadingCoeff / Q.leadingCoeff = 0
  · simp only [div_eq_mul_inv, inv_eq_zero, mul_eq_zero] at hPQ
    rcases hPQ with hP0 | hQ0
    · rw [leadingCoeff_eq_zero.1 hP0, degree_zero]
      exact bot_lt_iff_ne_bot.2 fun hQ' => hQ (degree_eq_bot.1 hQ')
    · exact absurd (leadingCoeff_eq_zero.1 hQ0) hQ
  · have := (isEquivalent_atTop_div P Q).tendsto_nhds h
    rw [tendsto_const_mul_zpow_atTop_nhds_iff hPQ] at this
    rcases this with h | h
    · exact absurd h.2 hPQ
    · rw [sub_lt_iff_lt_add, zero_add, Int.ofNat_lt] at h
      exact degree_lt_degree h.1

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

Goal state before:
pp: P Q : ℤ[X]
h : Q.degree < P.degree
o : (fun x ↦ eval x Q) =o[cofinite] fun x ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
⊢ {x | |eval x P| ≤ |eval x Q|}.Finite

Tactic:
have key := o.eventuallyLT_norm_of_eventually_pos (nr.congr (.of_forall (by simp)))

Goal state after:
P Q : ℤ[X]
h : Q.degree < P.degree
o : (fun x ↦ eval x Q) =o[cofinite] fun x ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
key : ∀ᶠ (x : ℤ) in cofinite, ‖eval x Q‖ < ‖eval x P‖
⊢ {x | |eval x P| ≤ |eval x Q|}.Finite
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 ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
i : ℕ
⊢ v (p.coeff i) * c ^ i ≤ gaussNorm v c p

Tactic:
← gaussNorm_coe_powerSeries _ _ hc,

Goal state after:
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 ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
i : ℕ
⊢ v (p.coeff i) * c ^ i ≤ PowerSeries.gaussNorm (⇑v) c ↑p
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
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
⊢ IsNonarchimedean (gaussNorm v c)

Tactic:
intro p q
  rcases eq_or_ne p 0 with hp | _
  · simp [hp]
  rcases eq_or_ne q 0 with hq | _
  · simp [hq]
  rcases eq_or_ne (p + q) 0 with hpq | hpq
  · simp [hpq, hc, gaussNorm_nonneg]
  simp only [gaussNorm, support_nonempty, ne_eq, hpq, not_false_eq_true, ↓reduceDIte,
    Finset.sup'_le_iff]
  intro i _
  calc
  v ((p + q).coeff i) * c ^ i
    ≤ max (v (p.coeff i)) (v (q.coeff i)) * c ^ i := by
    rw [coeff_add]
    gcongr
    exact hna (p.coeff i) (q.coeff i)
  _ = max (v (p.coeff i) * c ^ i) (v (q.coeff i) * c ^ i) := by
    rw [max_mul_of_nonneg _ _ (pow_nonneg hc _)]
  _ ≤ max (gaussNorm v c p) (gaussNorm v c q) := by
    apply max_le_max <;>
    exact le_gaussNorm v _ hc i

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

Goal state before:
pp: p : ℂ[X]
hp : ¬p = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0

Tactic:
grind [Multiset.mem_map]

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

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(min x y) = min ↑x ↑y

Tactic:
min_def,

Goal state after:
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(min x y) = map₂ min ↑x ↑y
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ Summable fun i ↦ ‖ofDigitsTerm (x.digits b) i‖

Tactic:
exact summable_ofDigitsTerm.abs

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

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ^ n ≠ 0
hv : multiplicity (↑p) (0 ^ n) % n ≠ 0
⊢ False

Tactic:
zero_pow hnpos.ne'

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ≠ 0
hv : multiplicity (↑p) (0 ^ n) % n ≠ 0
⊢ False
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ x.st = sSup {y | ↑y < x}

Tactic:
rw [st_eq]
  exact stdPart_eq_sSup coeRingHom x

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

Goal state before:
pp: case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ ∀ ⦃y : ℝ⦄,
    dist y 1 < 1 →
      y ∈ Set.Iio 1 → ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y

Tactic:
intro y hy1 hy2

Goal state after:
case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : dist y 1 < 1
hy2 : y ∈ Set.Iio 1
⊢ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑((x + y) / 2 - sqrt (x * y)) ≤ ↑((x + y) / 2 - x)

Tactic:
gcongr
      rw [le_sqrt_iff_sq_le, sq]
      gcongr

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

Goal state before:
pp: case pos
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ deriv negMulLog p + -deriv negMulLog (1 - p) = log (1 - p) - log p

pp: case pos.hf
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ negMulLog p

pp: case pos.hg
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p ↦ (1 - p).negMulLog) p

Tactic:
deriv_negMulLog hp₀,

Goal state after:
case pos
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ -log p - 1 + -deriv negMulLog (1 - p) = log (1 - p) - log p

case pos.hf
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ negMulLog p

case pos.hg
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p ↦ (1 - p).negMulLog) p
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:
recursion' (n + 1)

Goal state after:
θ : ℝ
n : ℕ
⊢ -(2 * 2 * ((↑(n + 1) + 1) * (0 ^ (n + 1) * cos θ))) + 2 * (↑(n + 1) + 1) * (2 * ↑(n + 1) + 1) * I (n + 1) θ -
      4 * (↑(n + 1) + 1) * ↑(n + 1) * I (n + 1 - 1) θ =
    2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
⊢ I 1 θ * θ ^ 3 = 4 * sin θ - 4 * θ * cos θ

Tactic:
rw [_root_.pow_succ, ← mul_assoc, recursion' 0, sub_mul, add_mul, mul_assoc _ (I 0 θ), I_zero]

Goal state after:
θ : ℝ
⊢ -(2 * 2 * ((↑0 + 1) * (0 ^ 0 * cos θ))) * θ + 2 * (↑0 + 1) * (2 * ↑0 + 1) * (2 * sin θ) -
      4 * (↑0 + 1) * ↑0 * I (0 - 1) θ * θ =
    4 * sin θ - 4 * θ * cos θ
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
⊢ StrictMonoOn (qaryEntropy q) (Icc 0 (1 - 1 / ↑q))

Tactic:
by
  intro p1 hp1 p2 hp2 p1le2
  apply strictMonoOn_of_deriv_pos (convex_Icc 0 (1 - 1 / (q : ℝ))) _ _ hp1 hp2 p1le2
  · exact qaryEntropy_continuous.continuousOn
  · intro p hp
    have : 2 ≤ (q : ℝ) := Nat.ofNat_le_cast.mpr qLe2
    have zero_le_qinv : 0 < (q : ℝ)⁻¹ := by positivity
    have : 0 < 1 - p := by
      simp only [sub_pos]
      have p_lt_1_minus_qinv : p < 1 - (q : ℝ)⁻¹ := by
        simp_all only [inv_pos, interior_Icc, mem_Ioo, one_div]
      linarith
    simp only [one_div, interior_Icc, mem_Ioo] at hp
    rw [deriv_qaryEntropy (by linarith)]
    · simp only [sub_pos, gt_iff_lt]
      rw [← log_mul (by linarith) (by linarith)]
      apply Real.strictMonoOn_log (mem_Ioi.mpr hp.1)
      · simp_all only [mem_Ioi, mul_pos_iff_of_pos_left, show 0 < (q : ℝ) - 1 by linarith]
      · have qpos : 0 < (q : ℝ) := by positivity
        have : q * p < q - 1 := by
          convert! mul_lt_mul_of_pos_left hp.2 qpos using 1
          simp only [mul_sub, mul_one, isUnit_iff_ne_zero, ne_eq, ne_of_gt qpos, not_false_eq_true,
            IsUnit.mul_inv_cancel]
        linarith
    exact (ne_of_gt (lt_add_neg_iff_lt.mp this : p < 1)).symm

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

Goal state before:
pp: case a
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
⊢ (↑q - 1) * (1 - p) < p

Tactic:
have qpos : 0 < (q : ℝ) := by positivity
        ring_nf
        have : (q : ℝ) - 1 < p * q := by
          have h1 := mul_lt_mul_of_pos_right hp.1 qpos
          have h2 : (1 - (q : ℝ)⁻¹) * ↑q = q - 1 := by calc (1 - (q : ℝ)⁻¹) * ↑q
            _ = q - (q : ℝ)⁻¹ * (q : ℝ) := by ring
            _ = q - 1 := by simp [qpos.ne']
          rwa [h2] at h1
        nlinarith

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
a : A
ha : a ∈ {a | IsStrictlyPositive a}
⊢ (fun a ↦ if a ∈ {b | IsStrictlyPositive b} then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0) a =
    (fun a ↦ p⁻¹ • (a ^ p - 1)) a

Tactic:
simp only [ha, ↓reduceIte, ← smul_eq_mul]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
a : A
ha : a ∈ {a | IsStrictlyPositive a}
⊢ cfc (fun x ↦ p⁻¹ • (x ^ p - 1)) a = p⁻¹ • (a ^ p - 1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
ht : 0 < t
x : ℝ
hx : x ∈ Ici 0
⊢ t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) = t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹)

Tactic:
rw [Real.rpow_sub_one ht.ne']
          ring

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 1 2
hx : 0 ≤ x
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₁₂ x_1 x) (Ioi 0) volume

Tactic:
by
  have hmain : (rpowIntegrand₁₂ p · x)
      =ᵐ[volume.restrict (Ioi 0)] (x * rpowIntegrand₀₁ (p-1) · x) := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with a ha
    rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ha]
  rw [integrableOn_congr_fun_ae hmain]
  refine Integrable.const_mul ?_ _
  exact integrableOn_rpowIntegrand₀₁_Ioi (by grind) hx

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

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

Tactic:
generalize (Gammaℝ (s - 1))⁻¹ = A

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
A : ℂ
⊢ (s - 1).Gammaℂ * sin (↑π * (s / 2)) * A =
    (s - 1).Gammaℂ * ((s - 1) / 2 / ↑π) * sin (↑π * (s / 2)) * (A * ((s - 1) / 2 / ↑π)⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 1 2
⊢ ∃ μ,
    ∀ x ∈ Ici 0,
      IntegrableOn (fun t ↦ p.rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₁₂ t x ∂μ

Tactic:
by
  let C : ℝ≥0 := .mk
    (∫ t in Ioi 0, rpowIntegrand₀₁ (p - 1) t 1)⁻¹ <| by
      rw [inv_nonneg]
      exact le_of_lt <| integral_rpowIntegrand₀₁_one_pos (by grind)
  let μ : Measure ℝ := C • volume
  refine ⟨μ, fun x hx => ⟨?_, ?_⟩⟩
  · unfold μ IntegrableOn
    rw [Measure.restrict_smul]
    exact Integrable.smul_measure_nnreal <| integrableOn_rpowIntegrand₁₂ hp hx
  · rw [Measure.restrict_smul, integral_smul_nnreal_measure,
      rpow_eq_const_mul_integral_rpowIntegrand₁₂ hp hx]
    simp [C, NNReal.smul_def]

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

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)

Tactic:
refine (h_diff one_half_pos).hasDerivAt.congr_deriv ?_

Goal state after:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv Gamma (1 / 2) = -√π * (γ + 2 * log 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : a < 0
b s : ℝ
⊢ (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] fun x ↦ x ^ s

Tactic:
suffices (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] (fun x ↦ rexp (-x)) by
    refine this.trans ?_
    simpa only [neg_one_mul] using isLittleO_exp_neg_mul_rpow_atTop zero_lt_one s
  rw [isLittleO_exp_comp_exp_comp]
  have : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1)) := by
    ext1 x; ring_nf
  rw [this]
  exact tendsto_id.atTop_mul_atTop₀ <| tendsto_atTop_add_const_right _ _ <|
    tendsto_id.const_mul_atTop (neg_pos.mpr ha)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, IsCompact K ∧ r < μ K

pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K

Tactic:
· rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
    exact ⟨closure K, closure_minimal hK1 hA, hK2, hK3.trans_le (measure_mono subset_closure)⟩

Goal state after:
case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K