mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ 2 * sin x * sin y = cos (x - y) - cos (x + y)

Tactic:
simp [cos_add, cos_sub]

Goal state after:
x y : ℝ
⊢ 2 * sin x * sin y = sin x * sin y + sin x * sin y
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ 2 * cos x * cos y = cos (x - y) + cos (x + y)

Tactic:
simp [cos_add, cos_sub]

Goal state after:
x y : ℝ
⊢ 2 * cos x * cos y = cos x * cos y + cos x * cos y
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:

Tactic:
c * x
  _ ≤ c * x + 1 := le_add_of_nonneg_right zero_le_one
  _ ≤ _ := Real.add_one_le_exp (c * x)

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

Goal state before:
pp: n : ℕ
⊢ sin (π / 2 ^ (n + 2)) = √(2 - sqrtTwoAddSeries 0 n) / 2

Tactic:
rw [eq_div_iff_mul_eq two_ne_zero, eq_comm, sqrt_eq_iff_eq_sq, mul_pow,
    sin_sq_pi_over_two_pow_succ, sub_mul]
  · congr <;> norm_num
  · rw [sub_nonneg]
    exact (sqrtTwoAddSeries_lt_two _).le
  refine mul_nonneg (sin_nonneg_of_nonneg_of_le_pi ?_ ?_) zero_le_two
  · positivity
  · exact div_le_self pi_pos.le <| one_le_pow₀ one_le_two

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (sphere x r) = ∅

Tactic:
← frontier_closedBall' x,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (frontier (closedBall x r)) = ∅
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ tan (π / 2) = 0

Tactic:
by simp [tan_eq_sin_div_cos]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ HasSum (fun i ↦ x ^ i) (1 - x)⁻¹ʳ

Tactic:
convert! (summable_geometric_of_norm_lt_one h).hasSum
  exact (geom_series_eq_inverse x h).symm

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
s : Set C(X, Y)
⊢ s ∈ 𝓝 f ↔
    ∃ S,
      S.Finite ∧
        (∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen[inst✝] U ∧ MapsTo (⇑f) K U) ∧
          {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s

Tactic:
by
  simp [f.hasBasis_nhds.mem_iff, ← ofPred_forall, and_assoc]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n ↦ ↑n ^ k * r ^ n

Tactic:
by
  refine Nat.strong_induction_on k fun k hk => ?_
  obtain ⟨a, ha⟩ : ∃ (a : ℕ → ℕ), ∀ n, (n + k).descFactorial k
      = n ^ k + ∑ i ∈ range k, a i * n ^ i := by
    let P : Polynomial ℕ := (ascPochhammer ℕ k).comp (Polynomial.X + C 1)
    refine ⟨fun i ↦ P.coeff i, fun n ↦ ?_⟩
    have mP : Monic P := Monic.comp_X_add_C (monic_ascPochhammer ℕ k) _
    have dP : P.natDegree = k := by
      simp only [P, natDegree_comp, ascPochhammer_natDegree, mul_one, natDegree_X_add_C]
    have A : (n + k).descFactorial k = P.eval n := by
      have : n + 1 + k - 1 = n + k := by lia
      simp [P, ascPochhammer_nat_eq_descFactorial, this]
    conv_lhs => rw [A, mP.as_sum, dP]
    simp [eval_finsetSum]
  have : Summable (fun n ↦ (n + k).descFactorial k * r ^ n
      - ∑ i ∈ range k, a i * n ^ (i : ℕ) * r ^ n) := by
    apply (summable_descFactorial_mul_geometric_of_norm_lt_one k hr).sub
    apply summable_sum (fun i hi ↦ ?_)
    simp_rw [mul_assoc]
    simp only [Finset.mem_range] at hi
    exact (hk _ hi).mul_left _
  convert! this using 1
  ext n
  simp [ha n, add_mul, sum_mul]

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
⊢ x ∈ F ∧ y ∈ F

Tactic:
have : γ 0 ∈ F ∧ γ 1 ∈ F := by constructor <;> apply γ_in

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
this : γ 0 ∈ F ∧ γ 1 ∈ F
⊢ x ∈ F ∧ y ∈ F
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F s : Set X
t : Set Y
inst✝¹ : PathConnectedSpace X
inst✝ : PathConnectedSpace Y
⊢ PathConnectedSpace (X × Y)

Tactic:
rw [pathConnectedSpace_iff_univ, ← Set.univ_prod_univ]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F s : Set X
t : Set Y
inst✝¹ : PathConnectedSpace X
inst✝ : PathConnectedSpace Y
⊢ IsPathConnected (univ ×ˢ univ)
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : Unique X
f : C(X, Y)
⊢ const X ((fun f ↦ f default) f) = f

Tactic:
by
    ext x
    rw [Unique.eq_default x]
    rfl

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ γ : Path x y
x' y' : X
hx : x' = x
hy : y' = y
⊢ γ 1 = y'

Tactic:
by simp [hy]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ range f = univ

Tactic:
rw [range_eq_univ]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ Surjective f
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.inr.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ False

Tactic:
have : p ≤ ↑z * p := by nlinarith

Goal state after:
case inr.inr.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
this : p ≤ ↑z * p
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ π / 4 ≤ arcsin x ↔ sin (π / 4) ≤ x

Tactic:
le_arcsin_iff_sin_le'

Goal state after:
x : ℝ
⊢ sin (π / 4) ≤ x ↔ sin (π / 4) ≤ x

x : ℝ
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arccos x) = x

Tactic:
arccos,

Goal state after:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (π / 2 - arcsin x) = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ arccos (cos x) = x

Tactic:
arccos,

Goal state after:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - arcsin (cos x) = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ arccos x = π ↔ x ≤ -1

Tactic:
arccos,

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

Goal state before:
pp: x : ℝ
⊢ arccos (-x) = π / 2 + π / 2 - arccos x

Tactic:
arccos,

Goal state after:
x : ℝ
⊢ π / 2 - arcsin (-x) = π / 2 + π / 2 - arccos x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ π / 2 - -arcsin x = π / 2 + π / 2 - arccos x

Tactic:
arccos,

Goal state after:
x : ℝ
⊢ π / 2 - -arcsin x = π / 2 + π / 2 - (π / 2 - arcsin x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ arccos x = 0

Tactic:
arccos,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ π / 2 - arcsin x = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx : x ≤ -1
⊢ arccos x = π

Tactic:
arccos,

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

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

Tactic:
arccos,

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

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

Tactic:
arccos,

Goal state after:
x : ℝ
⊢ tan (π / 2 - arcsin x) = √(1 - x ^ 2) / x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ ↑x.re + ↑(x.im - toIocDiv Real.two_pi_pos (-π) x.im • (2 * π)) * I =
    x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)

Tactic:
ofReal_sub,

Goal state after:
x : ℂ
⊢ ↑x.re + (↑x.im - ↑(toIocDiv Real.two_pi_pos (-π) x.im • (2 * π))) * I =
    x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ -x⁻¹ ≤ log x

Tactic:
rw [neg_le, ← log_inv]; exact log_le_self <| inv_nonneg.2 hx

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

Goal state before:
pp: x : ℝ
n : ℤ
⊢ ↑(↑n * x) = n • ↑x

Tactic:
simpa only [zsmul_eq_mul] using! coeHom.map_zsmul n x

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

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℤ
hn : x = ↑n * (2 * ↑π * I)
this : 0 ≤ ↑n * (2 * π)
⊢ ∃ n, x = ↑n * (2 * ↑π * I)

Tactic:
lift n to ℕ using by exact_mod_cast nonneg_of_mul_nonneg_left this (by positivity)

Goal state after:
x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℕ
hn : x = ↑↑n * (2 * ↑π * I)
this : 0 ≤ ↑↑n * (2 * π)
⊢ ∃ n, x = ↑n * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
hy : y ≠ 0
⊢ x ^ y ≠ 0 ↔ x ≠ 0

Tactic:
by simp [hy]

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

Goal state before:
pp: case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0

Tactic:
H,

Goal state after:
case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ -2 * sin ((θ + ψ) / 2) * sin (2 * π * ↑k / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ -2 * sin ((θ - -ψ) / 2) * sin ((θ - ψ) / 2) = 0

Tactic:
H,

Goal state after:
case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ -2 * sin (2 * π * ↑k / 2) * sin ((θ - ψ) / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0

Tactic:
H,

Goal state after:
case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ 2 * sin (2 * π * ↑k / 2) * cos ((θ + ψ) / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case mp.refine_2
θ : ℝ
⊢ cexp (↑(θ - toIocDiv ⋯ (-π) θ • (2 * π)) * I) = cexp (↑θ * I)

Tactic:
ofReal_sub,

Goal state after:
case mp.refine_2
θ : ℝ
⊢ cexp ((↑θ - ↑(toIocDiv ⋯ (-π) θ • (2 * π))) * I) = cexp (↑θ * I)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : ↑n * 2 + ↑1 = ↑0
⊢ ↑θ = ↑ψ

Tactic:
← Int.cast_ofNat,

Goal state after:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : ↑n * ↑2 + ↑1 = ↑0
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ ↑((starRingEnd ℂ) x).arg = -↑x.arg

Tactic:
by_cases h : arg x = π

Goal state after:
case pos
x : ℂ
h : x.arg = π
⊢ ↑((starRingEnd ℂ) x).arg = -↑x.arg

case neg
x : ℂ
h : ¬x.arg = π
⊢ ↑((starRingEnd ℂ) x).arg = -↑x.arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ ↑x⁻¹.arg = -↑x.arg

Tactic:
by_cases h : arg x = π

Goal state after:
case pos
x : ℂ
h : x.arg = π
⊢ ↑x⁻¹.arg = -↑x.arg

case neg
x : ℂ
h : ¬x.arg = π
⊢ ↑x⁻¹.arg = -↑x.arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (-θ).sin = -θ.sin

Tactic:
by
  induction θ using Real.Angle.induction_on
  exact Real.sin_neg _

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

Goal state before:
pp: ⊢ cos 0 = 1

Tactic:
by rw [← coe_zero, cos_coe, Real.cos_zero]

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

Goal state before:
pp: x n : ℂ
⊢ (x ^ n)⁻¹ = if x.arg = π then if x.arg = π then (x ^ n)⁻¹ else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else x⁻¹ ^ n

Tactic:
split_ifs with h

Goal state after:
case pos
x n : ℂ
h : x.arg = π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹

case neg
x n : ℂ
h : ¬x.arg = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)

Tactic:
simp only [rpow_def, Complex.cpow_def]

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if ↑x = 0 then if ↑y = 0 then 1 else 0 else Complex.exp (Complex.log ↑x * ↑y)).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + ↑π
⊢ a = b

Tactic:
have : a.sign = (b + π).sign := by aesop

Goal state after:
case mp.inr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + ↑π
this : a.sign = (b + ↑π).sign
⊢ a = b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑θ.toReal + ↑ψ.toReal = ↑π
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
← coe_add

Goal state after:
case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
⊢ |θ.toReal| + |ψ.toReal| = π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≤ 0
y : ℝ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y) * cos (y * π)

Tactic:
split_ifs with h

Goal state after:
case pos
x : ℝ
hx : x ≤ 0
y : ℝ
h : x = 0
h✝ : y = 0
⊢ x ^ y = 1

case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : x = 0
h✝ : ¬y = 0
⊢ x ^ y = 0

case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ x ^ y = rexp (log x * y) * cos (y * π)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
⊢ 0 ^ x ≤ 1

Tactic:
by_cases h : x = 0 <;> simp [h, zero_le_one]

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ 0 ^ x

Tactic:
by_cases h : x = 0 <;> simp [h, zero_le_one]

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

Goal state before:
pp: s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ ‖log x ^ r‖ ≤ log x ^ r'

Tactic:
rw [Real.norm_of_nonneg (by positivity)]

Goal state after:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ log x ^ r ≤ log x ^ r'
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y : ℝ
hy : y ≠ 0
⊢ x ^ y = 0 ↔ x = 0

Tactic:
by simp [hy]

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

Goal state before:
pp: y : ℝ
⊢ 0 ^ y = if y = 0 then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
y : ℝ
h : y = 0
⊢ 0 ^ y = 1

case neg
y : ℝ
h : ¬y = 0
⊢ 0 ^ y = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ≥0
⊢ (y ^ x⁻¹) ^ x = y

Tactic:
← rpow_mul,

Goal state after:
x : ℝ
hx : x ≠ 0
y : ℝ≥0
⊢ y ^ (x⁻¹ * x) = y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ y) ^ y⁻¹ = x

Tactic:
← rpow_mul,

Goal state after:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ x ^ (y * y⁻¹) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ y⁻¹) ^ y = x

Tactic:
← rpow_mul,

Goal state after:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ x ^ (y⁻¹ * y) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x✝ : ℝ≥0
w y✝ z y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ (x ^ (1 / y)) ^ y = x

Tactic:
← rpow_mul,

Goal state after:
x✝ : ℝ≥0
w y✝ z y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ x ^ (1 / y * y) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case neg
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt ((fun a ↦ a ^ y) ∘ ofNNReal) x

Tactic:
convert! continuous_coe.continuousAt.comp (NNReal.continuousAt_rpow_const (Or.inr h.le)) using 1

Goal state after:
case e'_5
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ (fun a ↦ a ^ y) ∘ ofNNReal = ofNNReal ∘ fun z ↦ z ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
hy : 0 < y
x : ℝ≥0∞
⊢ (x ^ (1 / y)) ^ y = x

Tactic:
← rpow_mul,

Goal state after:
y : ℝ
hy : 0 < y
x : ℝ≥0∞
⊢ x ^ (1 / y * y) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
⊢ (x ^ y) ^ y⁻¹ = x

Tactic:
← rpow_mul,

Goal state after:
y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
⊢ x ^ (y * y⁻¹) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
⊢ (x ^ y⁻¹) ^ y = x

Tactic:
← rpow_mul,

Goal state after:
y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
⊢ x ^ (y⁻¹ * y) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ (x ^ ↑n) ^ (↑n)⁻¹ = x

Tactic:
← rpow_mul,

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ x ^ (↑n * (↑n)⁻¹) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ (x ^ (↑n)⁻¹) ^ ↑n = x

Tactic:
← rpow_mul,

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ x ^ ((↑n)⁻¹ * ↑n) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
by
  rw [← rpow_natCast, ← rpow_mul, inv_mul_cancel₀ (by positivity), rpow_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
v : M
hv : v ≠ 0
r : R
hr : r ≠ 0
⊢ SameRay R v (r • v) ↔ 0 < r

Tactic:
simp only [sameRay_smul_right_iff, hv, or_false, hr.symm.le_iff_lt]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.refine_3
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = (r₁ + r₂)⁻¹ • (r₁ • v₁ + r₁ • v₂)

Tactic:
H,

Goal state after:
case inr.inr.refine_3
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = (r₁ + r₂)⁻¹ • (r₂ • v₂ + r₁ • v₂)
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
⊢ Convex 𝕜 (⇑f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ a b ha hb hab
  exact ⟨a • x + b • y, hs hx hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedCore 𝕜 s ⊆ balancedCore 𝕜 s

Tactic:
by
  rintro x ⟨y, hy, rfl⟩
  rw [mem_balancedCore_iff] at hy
  rcases hy with ⟨t, ht1, ht2, hy⟩
  exact ⟨t, ⟨ht1, ht2⟩, ht1 a ha (smul_mem_smul_set hy)⟩

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval i '' S)

Tactic:
by
  simp_rw [isVonNBounded_iff_tendsto_smallSets_nhds, nhds_pi, Filter.pi, smallSets_iInf,
    smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff, Function.comp_def,
    ← image_smul, image_image, eval, Pi.smul_apply, Pi.zero_apply]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a : Set E
ha : IsVonNBounded 𝕜 a
V : Set E
hV : V ∈ 𝓝 0
W : Set E
hW₁ : W ∈ 𝓝 0
hW₂ : IsClosed[inst✝³] W
hW₃ : W ⊆ V
⊢ Absorbs 𝕜 V (closure[inst✝³] a)

Tactic:
specialize ha hW₁

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a V : Set E
hV : V ∈ 𝓝 0
W : Set E
ha : Absorbs 𝕜 W a
hW₁ : W ∈ 𝓝 0
hW₂ : IsClosed[inst✝³] W
hW₃ : W ⊆ V
⊢ Absorbs 𝕜 V (closure[inst✝³] a)
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (DFunLike.coe ∘ F) 1
⊢ Equicontinuous (DFunLike.coe ∘ F)

Tactic:
equicontinuous_iff_continuous

Goal state after:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (DFunLike.coe ∘ F) 1
⊢ Continuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p p₁ p₂ : P
⊢ p ∈ line[k, p₁, p₂] ↔ ∃ r, (AffineMap.lineMap p₁ p₂) r = p

Tactic:
by
  constructor
  · intro h
    rw [← vsub_vadd p p₁, vadd_left_mem_affineSpan_pair] at h
    obtain ⟨r, hr⟩ := h
    refine ⟨r, ?_⟩
    rw [← vsub_vadd p p₁, ← hr, AffineMap.lineMap_apply]
  · rintro ⟨r, rfl⟩
    exact AffineMap.lineMap_mem_affineSpan_pair _ _ _

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ι : Type u_6
s : Finset ι
w : ι → k
p : ι → V
hw : s.sum w = 0
⊢ (s.weightedVSub p) w = ∑ i ∈ s, w i • p i

Tactic:
simp [s.weightedVSub_apply, vsub_eq_sub, smul_sub, ← Finset.sum_smul, hw]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ p -ᵥ p₁ ∈ (affineSpan k (insert p₂ ↑s)).direction ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
direction_affineSpan_insert hp₁,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ p -ᵥ p₁ ∈ k ∙ (p₂ -ᵥ p₁) ⊔ s.direction ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0