mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : Preorder α
inst✝¹ : IsOrderedMonoid α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (s * ↑(lowerClosure 1))

Tactic:
exact hs.mul_right

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
⊢ ∃ U, f = U.conjContinuousAlgEquiv

Tactic:
by_cases! hV : Subsingleton V

Goal state after:
case pos
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Subsingleton V
⊢ ∃ U, f = U.conjContinuousAlgEquiv

case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
⊢ ∃ U, f = U.conjContinuousAlgEquiv
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
⊢ efixedPoint f hf x hx = efixedPoint f hf y hy

Tactic:
refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
    <;> try apply efixedPoint_isFixedPt
  change Metric.edistLtTopSetoid _ _
  trans x
  · apply Setoid.symm'
    exact hf.edist_efixedPoint_lt_top hx
  trans y
  exacts [lt_top_iff_ne_top.2 h, hf.edist_efixedPoint_lt_top hy]

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

Goal state before:
pp: u b c : ℕ → ℝ
n₀ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n₀ ≤ n
⊢ u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico n₀ n, (1 + c i) =
    (u n₀ + ∑ k ∈ Ico n₀ n, b k) * ∏ i ∈ Ico n₀ n, (1 + c i)

Tactic:
add_mul,

Goal state after:
u b c : ℕ → ℝ
n₀ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n₀ ≤ n
⊢ u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico n₀ n, (1 + c i) =
    u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + (∑ k ∈ Ico n₀ n, b k) * ∏ i ∈ Ico n₀ n, (1 + c i)
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: case e'_1.e'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt ε : ℝ
⊢ Metric.ball (t₀ - dt) ε = -dt +ᵥ Metric.ball t₀ ε

Tactic:
simp [neg_add_eq_sub]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasDerivWithinAt (γ ∘ fun x ↦ x * a) ((a • v ∘ fun x ↦ x * a) t ((γ ∘ fun x ↦ x * a) t)) {t | t * a ∈ s} t

Tactic:
by
  simp only [comp_apply, Pi.smul_apply]
  exact HasDerivWithinAt.scomp t (hγ (t * a) ht) (hasDerivAt_mul_const a).hasDerivWithinAt
    fun _ ht' ↦ ht'

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

Goal state before:
pp: case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ ↑r) (hy : y ∈ closedBall x₀ ↑r) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ ↑L' * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ ↑r
y : E
hy : y ∈ closedBall x₀ ↑r
⊢ dist ((FunSpace.toContinuousMap (α x hx)) (projIcc tmin tmax ⋯ t))
      ((FunSpace.toContinuousMap (α y hy)) (projIcc tmin tmax ⋯ t)) ≤
    ↑L' * dist x y

Tactic:
have : Nonempty (Icc tmin tmax) := ⟨t₀⟩

Goal state after:
case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ ↑r) (hy : y ∈ closedBall x₀ ↑r) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ ↑L' * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ ↑r
y : E
hy : y ∈ closedBall x₀ ↑r
this : Nonempty ↑(Icc tmin tmax)
⊢ dist ((FunSpace.toContinuousMap (α x hx)) (projIcc tmin tmax ⋯ t))
      ((FunSpace.toContinuousMap (α y hy)) (projIcc tmin tmax ⋯ t)) ≤
    ↑L' * dist x y
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
hy : y ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
⊢ dist (next hf hx α) (next hf hy α) = dist x y

Tactic:
have : Nonempty (Icc tmin tmax) := ⟨t₀⟩

Goal state after:
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
hy : y ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
this : Nonempty ↑(Icc tmin tmax)
⊢ dist (next hf hx α) (next hf hy α) = dist x y
Module: Mathlib.Analysis.Polynomial.Basic

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

Tactic:
rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X] at h

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : (P.comp (-X)).degree < (Q.comp (-X)).degree
⊢ (fun x ↦ eval x P) =o[atBot] fun x ↦ eval x Q
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
⊢ (fun x ↦ eval x P) =O[atBot] fun x ↦ eval x Q

Tactic:
rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X] at h

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : (P.comp (-X)).degree ≤ (Q.comp (-X)).degree
⊢ (fun x ↦ eval x P) =O[atBot] fun x ↦ eval x Q
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inr
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
t : σ →₀ ℕ
h :
  max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) =
    v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i
⊢ max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c g

Tactic:
simpa [h] using! le_gaussNorm v c g hbgd t

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

Goal state before:
pp: case cons
a✝ : ℂ[X]
s✝ : Multiset ℂ[X]
ih : s✝.prod.mahlerMeasure = (Multiset.map (fun p ↦ p.mahlerMeasure) s✝).prod
⊢ (a✝ ::ₘ s✝).prod.mahlerMeasure = (Multiset.map (fun p ↦ p.mahlerMeasure) (a✝ ::ₘ s✝)).prod

Tactic:
simp [mahlerMeasure_mul, ih]

Goal state after:
Module: Mathlib.Analysis.RCLike.ContinuousMap

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a✝ : X
⊢ (starRingEnd 𝕜) (f a✝) = f a✝

Tactic:
conv_rhs => rw [← hf.star_eq]

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a✝ : X
⊢ (starRingEnd 𝕜) (f a✝) = (star f) a✝
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ min ↑a ↑b = map₂ min ↑a ↑b

Tactic:
· rw [min_eq_right h, map₂_coe, coe_eq]
      exact h.mono fun i hi => (min_eq_right hi).symm

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

Goal state before:
pp: n : ℕ
⊢ sin (π / 2 ^ (n + 2)) < π / 2 ^ (n + 2)

pp: n : ℕ
⊢ 0 < 2 ^ (n + 2)

Tactic:
focus

Goal state after:
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) < π / 2 ^ (n + 2)
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
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots

Tactic:
mem_toFinset,

Goal state after:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ∈ S
⊢ ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case neg
x : ℝ*
h : ∀ (r : ℝ), 0 ≤ ArchimedeanClass.mk x → stdPart x ≠ r
⊢ ArchimedeanClass.mk x < 0

Tactic:
by_contra! hx

Goal state after:
case neg
x : ℝ*
h : ∀ (r : ℝ), 0 ≤ ArchimedeanClass.mk x → stdPart x ≠ r
hx : 0 ≤ ArchimedeanClass.mk x
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (↑(-q) + (↑q + x))

Tactic:
by rwa [cast_neg, neg_add_cancel_left]

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

Goal state before:
pp: x : ℝ*
⊢ x.Infinite ↔ ArchimedeanClass.mk x < 0

Tactic:
rw [Infinite, infinitePos_iff, infiniteNeg_iff]

Goal state after:
x : ℝ*
⊢ 0 < x ∧ ArchimedeanClass.mk x < 0 ∨ x < 0 ∧ ArchimedeanClass.mk x < 0 ↔ ArchimedeanClass.mk x < 0
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
⊢ 0 < r₁ ∧ ↑r₁ ≤ y

Tactic:
Classical.not_imp,

Goal state after:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : 0 < r₁ ∧ ¬(-↑r₁ < y ∧ y < ↑r₁)
⊢ 0 < r₁ ∧ ↑r₁ ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (cexp (-z.arctan * I) * cexp (z.arctan * I) - cexp (z.arctan * I) * cexp (z.arctan * I)) /
        ((cexp (z.arctan * I) + cexp (-z.arctan * I)) * cexp (z.arctan * I)) *
      I =
    z

Tactic:
add_mul,

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (cexp (-z.arctan * I) * cexp (z.arctan * I) - cexp (z.arctan * I) * cexp (z.arctan * I)) /
        (cexp (z.arctan * I) * cexp (z.arctan * I) + cexp (-z.arctan * I) * cexp (z.arctan * I)) *
      I =
    z
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (1 - cexp (z.arctan * I + z.arctan * I)) / (cexp (z.arctan * I + z.arctan * I) + 1) * I = z

Tactic:
← two_mul

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
⊢ (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z

Tactic:
add_mul,

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
⊢ (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) /
        ((1 + z * I) / (1 - z * I) * (1 - z * I) + 1 * (1 - z * I)) *
      I =
    z
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((1 + sin z / cos z * I) * cos z / ((1 - sin z / cos z * I) * cos z)) = z

Tactic:
add_mul,

Goal state after:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((1 * cos z + sin z / cos z * I * cos z) / ((1 - sin z / cos z * I) * cos z)) = z
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: y : ℝ≥0
⊢ agm 0 y = 0

Tactic:
by
  suffices ∀ n, (agmSequences 0 y n).1 = 0 by simp [agm_eq_ciSup, this]
  intro n
  induction n with
  | zero => simp [agmSequences]
  | succ n ih =>
    rw [agmSequences_succ', ih, zero_mul, sqrt_zero]

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

Goal state before:
pp: θ : ℝ
⊢ (-(2 * 2 * ((↑0 + 1) * (0 ^ 0 * cos θ))) + 2 * (↑0 + 1) * (2 * ↑0 + 1) * I 0 θ) * θ -
      4 * (↑0 + 1) * ↑0 * I (0 - 1) θ * θ =
    4 * sin θ - 4 * θ * cos θ

Tactic:
add_mul,

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

Goal state before:
pp: case neg
A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
ha : ¬IsUnit a
⊢ ((conjSqrt c) a)⁻¹ʳ = (conjSqrt c⁻¹ʳ) a⁻¹ʳ

Tactic:
· have : ¬IsUnit (conjSqrt c a) := by grind [conjSqrt_apply, IsUnit.mul_left_iff]
    simp [inverse_non_unit a ha, inverse_non_unit _ this]

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

Goal state before:
pp: case grind
A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
h✝ : ¬(conjSqrt c⁻¹ʳ) ((conjSqrt c) a) = a
⊢ False

Tactic:
have : sqrt c⁻¹ʳ * sqrt c = 1

Goal state after:
case grind
A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
h✝ : ¬(conjSqrt c⁻¹ʳ) ((conjSqrt c) a) = a
this : sqrt c⁻¹ʳ * sqrt c = 1
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case ha
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ -1 < 0

Tactic:
norm_num [show 0 < log 2 by positivity]

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

Goal state before:
pp: case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ Monotone fun a ↦ a ^ ↑q

Tactic:
← CFC.nnrpow_eq_rpow hq

Goal state after:
case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ Monotone fun a ↦ a ^ q
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ ↑q

Tactic:
← CFC.nnrpow_eq_rpow hq

Goal state after:
case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ q
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
hsub : uIcc a b ⊆ Ioi 0
hf_cint : IntervalIntegrable f volume (c * a) (c * b)
h : IntervalIntegrable (fun x ↦ f (c * x)) volume a (c * b / c)
⊢ IntervalIntegrable (fun x ↦ f (c * x)) volume a b

Tactic:
mul_div_cancel_left₀ b hc.ne'

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
hsub : uIcc a b ⊆ Ioi 0
hf_cint : IntervalIntegrable f volume (c * a) (c * b)
h : IntervalIntegrable (fun x ↦ f (c * x)) volume a b
⊢ IntervalIntegrable (fun x ↦ f (c * x)) volume a b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
⊢ x ≤ y → p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y

Tactic:
hxy

Goal state after:
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≤ y
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (1 / 2)

Tactic:
apply h_diff

Goal state after:
case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ 0 < 1 / 2
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
⊢ DifferentiableAt ℝ Gamma (2 * (1 / 2))

Tactic:
apply h_diff

Goal state after:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ 0 < 2 * (1 / 2)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case e_a.e_a.e_a.hh₂
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (2 * (1 / 2))

Tactic:
apply h_diff

Goal state after:
case e_a.e_a.e_a.hh₂
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ 0 < 2 * (1 / 2)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
⊢ log b 1 = 0

Tactic:
log_of_one_le_right _ le_rfl,

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
⊢ ↑(Nat.log b ⌊1⌋₊) = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
⊢ x ≤ y → (fun x ↦ log x / x) y ≤ (fun x ↦ log x / x) x

Tactic:
hxy

Goal state after:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
⊢ (fun x ↦ log x / x) y ≤ (fun x ↦ log x / x) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
⊢ x ≤ y → (fun x ↦ log x / x ^ a) y ≤ (fun x ↦ log x / x ^ a) x

Tactic:
hxy

Goal state after:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
⊢ (fun x ↦ log x / x ^ a) y ≤ (fun x ↦ log x / x ^ a) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case neg.inl
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 0
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Tactic:
simp_all only [CharP.cast_eq_zero, logb_zero_left, Int.floor_zero, Int.log_zero_left]

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

Goal state before:
pp: case a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ Int.clog b r ≤ ⌈logb (↑b) r⌉

Tactic:
· rw [← Int.le_zpow_iff_clog_le hb hr, ← rpow_intCast b]
      refine (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr).symm.trans_le ?_
      exact rpow_le_rpow_of_exponent_le hb1'.le (Int.le_ceil _)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∀ a ∈ Ioi 0, 0 ≤ g a

Tactic:
intro t t_pos

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
t : ℝ
t_pos : t ∈ Ioi 0
⊢ 0 ≤ g t
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case hab
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖l‖ / 2 ≤ ‖s - l‖

Tactic:
rw [norm_sub_rev]

Goal state after:
case hab
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖l‖ / 2 ≤ ‖l - s‖
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘[L - ↑l₀] z + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) = ℘[L] z

Tactic:
by
  trans ℘[L - l₀] z + ∑' i : L.lattice, if i = l₀.1 then (1 / (z - l₀.1) ^ 2 - 1 / l₀.1 ^ 2) else 0
  · simp
  rw [weierstrassPExcept, ← Summable.tsum_add]
  · congr with w; split_ifs <;> simp only [zero_add, add_zero, *]
  · exact ⟨_, L.hasSum_weierstrassPExcept _ _⟩
  · exact summable_of_hasFiniteSupport ((Set.finite_singleton l₀).subset (by simp))

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume ↔
    Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) volume

Tactic:
by
      rw [MeasureTheory.integrableOn_iff_integrable_of_support_subset]
      intro x hx
      simp only [support_indicator, mem_inter_iff, mem_Ioo, Function.mem_support, ne_eq,
        smul_eq_zero, pow_eq_zero_iff', not_or, not_and, Decidable.not_not] at hx
      refine mem_Ioi.mpr hx.1.1

Goal state after: