mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ HasFiniteIntegral f μ

Tactic:
refine HasFiniteIntegral.mono hg ?_
  filter_upwards [hnonneg, h] with a hn ha
  apply norm_le_norm_of_abs_le_abs
  rwa [abs_of_nonneg hn, abs_of_nonneg (hn.trans ha)]

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

Goal state before:
pp: a : ℕ
⊢ ⌊√↑a⌋₊ = a.sqrt

Tactic:
rw [Nat.floor_eq_iff (sqrt_nonneg a)]

Goal state after:
a : ℕ
⊢ ↑a.sqrt ≤ √↑a ∧ √↑a < ↑a.sqrt + 1
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
x : α
⊢ i x / f x ≤ g x

Tactic:
exact div_le_of_le_mul' (hi x)

Goal state after:
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: ⊢ ‖I‖₊ = 1

Tactic:
simp [nnnorm]

Goal state after:
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: q : ℚ≥0
⊢ ‖↑q‖₊ = ↑q

Tactic:
simp [nnnorm]

Goal state after:
q : ℚ≥0
⊢ NNReal.mk ↑q ⋯ = ↑q
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ (μ.withDensity fun x ↦ ↑(f x)) (spanningSets μ n ∩ f ⁻¹' Iic ↑n) < ∞

pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
⊢ ⋃ i, spanningSets μ i ∩ f ⁻¹' Iic ↑i = univ

Tactic:
· rw [withDensity_apply']
    apply setLIntegral_lt_top_of_bddAbove
    · exact ((measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ n)).ne
    · exact ⟨n, forall_mem_image.2 fun x hx ↦ hx.2⟩

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
⊢ ⋃ i, spanningSets μ i ∩ f ⁻¹' Iic ↑i = univ
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ I ^ 2 * I = -I

Tactic:
I_sq,

Goal state after:
⊢ -1 * I = -I
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ (I ^ 2) ^ 2 = 1

Tactic:
I_sq,

Goal state after:
⊢ (-1) ^ 2 = 1
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z : ℂ
h : z ≠ 0
⊢ z * z⁻¹ = 1

Tactic:
rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel₀ (mt normSq_eq_zero.1 h),
    ofReal_one]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Tactic:
replace hC := hC x

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : StarAddMonoid E
inst✝ : NormedStarGroup E
x : E
r : ℝ
⊢ (ball x r)⋆ = ball x⋆ r

Tactic:
simpa using star_isometry.preimage_ball (star x) r

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

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : NonUnitalNormedRing E
inst✝ : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
hx : 0 < ‖x⋆‖
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
refine le_of_mul_le_mul_right ?_ hx
          simpa [sq, mul_comm ‖x⋆‖] using h x⋆ |>.trans <| norm_mul_le _ _

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

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x⋆‖ * ‖x‖ ≤ ‖x‖ * ‖x‖

Tactic:
norm_star

Goal state after:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x‖ * ‖x‖ = ‖x⋆‖ * ‖x‖

Tactic:
norm_star

Goal state after:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x‖ * ‖x‖ = ‖x‖ * ‖x‖
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: f : ℂ →ₐ[ℝ] ℂ
⊢ f (I ^ 2) = I ^ 2

Tactic:
I_sq,

Goal state after:
f : ℂ →ₐ[ℝ] ℂ
⊢ f (-1) = -1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖(starRingEnd K) z‖₊ = ‖z‖₊

Tactic:
simp [nnnorm]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑n‖₊ = ↑n

Tactic:
simp [nnnorm]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ‖↑q‖₊ = ↑q

Tactic:
simp [nnnorm]

Goal state after:
K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ NNReal.mk ↑q ⋯ = ↑q
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype]
    (codRestrict (f.target.domRestrict f.invFun) f.source ⋯)

Tactic:
exact ((Equiv.isHomeomorph_iff _).1 h).2

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ ↑x < ↑y ↔ x < y

Tactic:
by
  rw [lt_iff_re_im]
  simp

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ 0 ≤ x ↔ ∃ s, x = star s * s

Tactic:
rw [nonneg_iff]

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ 0 ≤ re x ∧ im x = 0 ↔ ∃ s, x = star s * s
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑e.symm ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
y : Z
hy : y ∈ s ∩ f ⁻¹' e.source
⊢ f y = (↑e.symm ∘ ↑e ∘ f) y

Tactic:
by simp [e.left_inv hy.2]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (z w : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        (z * w) =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w -
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w

Tactic:
by subst h''; exact h.mul_re_ax

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
    (∀ᶠ (x : β) in l', (fun x_1 ↦ f (x_1, x)) =O[l] fun x_1 ↦ g (x_1, x)) ∧
      ∀ᶠ (x : β) in l', (fun x_1 ↦ g (x_1, x)) =O[l] fun x_1 ↦ f (x_1, x)

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_left, h₂.fiberwise_left⟩

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a✝ : α
hx₁ : ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖
hx₂ : ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖
⊢ c₁ * c₂ * (‖g₁ a✝‖ * ‖g₂ a✝‖) = c₁ * ‖g₁ a✝‖ * (c₂ * ‖g₂ a✝‖)

Tactic:
mul_mul_mul_comm

Goal state after:
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a✝ : α
hx₁ : ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖
hx₂ : ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖
⊢ c₁ * ‖g₁ a✝‖ * (c₂ * ‖g₂ a✝‖) = c₁ * ‖g₁ a✝‖ * (c₂ * ‖g₂ a✝‖)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a✝ : α
hx₁ : ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖
hx₂ : ‖f' a✝‖ ≤ c' * ‖g' a✝‖
⊢ c * c' * (‖k₂ a✝‖ * ‖g' a✝‖) = c * ‖k₂ a✝‖ * (c' * ‖g' a✝‖)

Tactic:
mul_mul_mul_comm

Goal state after:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a✝ : α
hx₁ : ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖
hx₂ : ‖f' a✝‖ ≤ c' * ‖g' a✝‖
⊢ c * ‖k₂ a✝‖ * (c' * ‖g' a✝‖) = c * ‖k₂ a✝‖ * (c' * ‖g' a✝‖)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1 + 1), 0 ^ m / ↑m.factorial - 1‖ = 0

Tactic:
| succ j ih =>

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case neg
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
hf : ¬f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
le_div_iff₀ (by positivity)

Goal state after:
case neg
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ * ‖f x‖ ≤ ‖g x‖
hf : ¬f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: z : ℂ
⊢ cos z = cos ↑z.re * cosh ↑z.im - sin ↑z.re * sinh ↑z.im * I

Tactic:
convert! cos_add_mul_I z.re z.im; exact (re_add_im z).symm

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : E'' → F''
s : Set E''
x₀ : E''
n : ℕ
h : f =O[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : n ≠ 0
⊢ ‖x₀ - x₀‖ ^ n = 0

Tactic:
simp_rw [sub_self, norm_zero, zero_pow hn]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos x - sin x * I = cexp (-x * I)

Tactic:
by
  rw [neg_mul, ← cosh_sub_sinh, sinh_mul_I, cosh_mul_I]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin x ^ 2 + cos x ^ 2 = cos x ^ 2 - sin x ^ 2 * I ^ 2

Tactic:
I_sq,

Goal state after:
x : ℂ
⊢ sin x ^ 2 + cos x ^ 2 = cos x ^ 2 - sin x ^ 2 * -1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
h : cos x ≠ 0
⊢ (1 + tan x ^ 2) * cos x ^ 2 = 1

Tactic:
by
  conv_rhs => rw [← sin_sq_add_cos_sq x, ← tan_mul_cos h]
  ring

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cosh (2 * x)) = ↑(cosh x ^ 2 + sinh x ^ 2)

Tactic:
simp [cosh_two_mul]

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x r : ℝ
⊢ expNear 0 x r = r

Tactic:
simp [expNear]

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

Goal state before:
pp: ⊢ Summable fun n ↦ rexp (-↑n)

Tactic:
simpa only [mul_neg_one] using summable_exp_nat_mul_iff.mpr neg_one_lt_zero

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} / ball 1 δ = ball x δ

Tactic:
by
  rw [singleton_div_ball, div_one]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case convert_3
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖y - x‖ * c < r * 1

Tactic:
rw [mem_closedBall, dist_eq_norm] at hy

Goal state after:
case convert_3
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖y - x‖ * c < r * 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inl
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : (2 * cos (π / 3) - 1) ^ 2 = 0
⊢ cos (π / 3) = 1 / 2

pp: case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2

Tactic:
· linarith [eq_zero_of_pow_eq_zero h]

Goal state after:
case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ y, dist x y = b * dist x z ∧ dist y z = a * dist x z

Tactic:
by
  use a • x + b • z
  nth_rw 1 [← one_smul ℝ x]
  nth_rw 4 [← one_smul ℝ z]
  simp [dist_eq_norm, ← hab, add_smul, ← smul_sub, norm_smul_of_nonneg, ha, hb]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cexp (-↑π / 2 * I) = -I

Tactic:
by
  rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: 𝕜 : Type u_5
inst✝ : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ HasSum (fun n ↦ ↑n * r ^ n) (r / (1 - r) ^ 2)

Tactic:
convert! hasSum_coe_mul_geometric_of_norm_lt_one' hr using 1

Goal state after:
𝕜 : Type u_5
inst✝ : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ r / (1 - r) ^ 2 = r * (1 - r)⁻¹ʳ ^ 2
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ∀ {γ₁ γ₂ : Path x y}, ⇑γ₁ = ⇑γ₂ → γ₁ = γ₂

Tactic:
rintro ⟨⟨x, h11⟩, h12, h13⟩ ⟨⟨x, h21⟩, h22, h23⟩ rfl
  rfl

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b : ι → X
γ : (t : ι) → Path (a t) (b t)
h : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ t).extend

Tactic:
apply h.comp (continuous_id.prodMap continuous_projIcc)
  exact zero_le_one

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ arccos x ≤ π / 4 ↔ √2 / 2 ≤ x

Tactic:
rw [arccos, ← pi_div_four_le_arcsin]

Goal state after:
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ (tan (arcsin x))⁻¹ = √(1 - x ^ 2) / x

Tactic:
tan_arcsin,

Goal state after:
x : ℝ
⊢ (x / √(1 - x ^ 2))⁻¹ = √(1 - x ^ 2) / x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : x < -1
this : 1 < -x
⊢ 0 < log (-x)

Tactic:
exact log_pos this

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
θ ψ : ℝ
Hcos : (-2 = 0 ∨ sin ((θ + ψ) / 2) = 0) ∨ sin ((θ - ψ) / 2) = 0
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

Tactic:
neg_eq_zero,

Goal state after:
case mp
θ ψ : ℝ
Hcos : (2 = 0 ∨ sin ((θ + ψ) / 2) = 0) ∨ sin ((θ - ψ) / 2) = 0
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log (↑n / ↑d)

Tactic:
have : 1 < (n : ℝ) / d := by
      simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h)

Goal state after:
e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
this : 1 < ↑n / ↑d
⊢ 0 < Real.log (↑n / ↑d)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: n : ℕ
h : n ≠ 0
θ : Angle
⊢ (n • θ).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)

Tactic:
by
  nth_rw 1 [← coe_toReal θ]
  have h' : 0 < (n : ℝ) := mod_cast Nat.pos_of_ne_zero h
  rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff₀' h',
    le_div_iff₀' h']

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑r * (cos ↑θ + sin ↑θ * I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
rw [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr, toIocMod_sub_self, toIocDiv_eq_neg_floor,
    zsmul_eq_mul]
  ring_nf

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b → a = b ∨ a = b + ↑π

Tactic:
· intro h
    aesop

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

Goal state before:
pp: x y : ℝ
hx_nonneg : 0 ≤ x
⊢ ‖x ^ y‖ = ‖x‖ ^ y

Tactic:
simp_rw [Real.norm_eq_abs]

Goal state after:
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y

Tactic:
exact abs_rpow_of_nonneg hx_nonneg

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

Goal state before:
pp: a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * x + c))) = x ^ (a / (b * x + c))

Tactic:
← exp_log (rpow_pos_of_pos hx (a / (b * x + c))),

Goal state after:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * x + c))) = rexp (log (x ^ (a / (b * x + c))))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
by_cases h : y + z = 0

Goal state after:
case pos
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

case neg
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s b : ℝ
hb : 0 < b
⊢ (fun x ↦ rexp (b * x) / x ^ s)⁻¹ =ᶠ[atTop] fun x ↦ x ^ s * rexp (-b * x)

Tactic:
filter_upwards with x using by simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]

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

Goal state before:
pp: α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
⊢ (fun x ↦ f x ^ r) =o[l] fun x ↦ g x ^ r

Tactic:
refine .of_isBigOWith fun c hc ↦ ?_
  rw [← rpow_inv_rpow hc.le hr.ne']
  refine (h.forall_isBigOWith ?_).rpow ?_ ?_ hg <;> positivity

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

Goal state before:
pp: case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (fun x ↦ rexp (-a * x) / x ^ b) atTop (𝓝 0)

Tactic:
· refine (tendsto_exp_mul_div_rpow_atTop (-b) a ha).inv_tendsto_atTop.congr' ?_
    refine (eventually_ge_atTop 0).mono fun t ht => ?_
    simp [field, Real.exp_neg, rpow_neg ht]

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y + ↑n ≠ 0
⊢ x ^ y * x ^ ↑n = x ^ y * x ^ n

Tactic:
rpow_intCast

Goal state after:
x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y + ↑n ≠ 0
⊢ x ^ y * x ^ n = x ^ y * x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y - ↑n ≠ 0
⊢ x ^ y / x ^ ↑n = x ^ y / x ^ n

Tactic:
rpow_intCast

Goal state after:
x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y - ↑n ≠ 0
⊢ x ^ y / x ^ n = x ^ y / x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℤ
z : ℝ
⊢ (x ^ ↑n) ^ z = (x ^ n) ^ z

Tactic:
rpow_intCast

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℤ
z : ℝ
⊢ (x ^ n) ^ z = (x ^ n) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
⊢ (x ^ y) ^ ↑n = (x ^ y) ^ n

Tactic:
rpow_intCast

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
⊢ (x ^ y) ^ n = (x ^ y) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
n : ℤ
z : ℝ
⊢ (x ^ ↑n) ^ z = (x ^ n) ^ z

Tactic:
rpow_intCast

Goal state after:
x : ℝ≥0
n : ℤ
z : ℝ
⊢ (x ^ n) ^ z = (x ^ n) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y : ℝ
n : ℤ
⊢ (x ^ y) ^ ↑n = (x ^ y) ^ n

Tactic:
rpow_intCast

Goal state after:
x : ℝ≥0
y : ℝ
n : ℤ
⊢ (x ^ y) ^ n = (x ^ y) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top
⊢ ∞ ^ 1 = ∞

pp: case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 1 = ↑x✝

Tactic:
· exact dif_pos zero_lt_one

Goal state after:
case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 1 = ↑x✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a ↦ a ^ y) x

Tactic:
simp_rw [hz, rpow_neg]

Goal state after:
case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a ↦ (a ^ z)⁻¹) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x ^ n ≤ y ↔ x ^ ↑n ≤ y

Tactic:
rpow_intCast

Goal state after:
x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x ^ n ≤ y ↔ x ^ n ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x ^ n < y ↔ x ^ ↑n < y

Tactic:
rpow_intCast

Goal state after:
x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x ^ n < y ↔ x ^ n < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
⊢ ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]

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

Goal state before:
pp: hb : 1 ≤ 1
⊢ Monotone fun x ↦ 1 ^ x

Tactic:
intro _ _ _; simp

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

Goal state before:
pp: hb₀ : 0 < 1
hb₁ : 1 ≤ 1
⊢ Antitone fun x ↦ 1 ^ x

Tactic:
intro _ _ _; simp

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

Goal state before:
pp: x : ℝ≥0∞
n : ℤ
z : ℝ
⊢ (x ^ ↑n) ^ z = (x ^ n) ^ z

Tactic:
rpow_intCast

Goal state after:
x : ℝ≥0∞
n : ℤ
z : ℝ
⊢ (x ^ n) ^ z = (x ^ n) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
n : ℤ
⊢ (x ^ y) ^ ↑n = (x ^ y) ^ n

Tactic:
rpow_intCast

Goal state after:
x : ℝ≥0∞
y : ℝ
n : ℤ
⊢ (x ^ y) ^ n = (x ^ y) ^ n