mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∃ c, IsBigOWith c l f fun x ↦ -g' x) ↔ ∃ c, IsBigOWith c l f g'

Tactic:
exact exists_congr fun _ => isBigOWith_neg_right

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z * z ^ m / ↑((m + 1) * m.factorial)‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖

Tactic:
mul_comm m.succ,

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z * z ^ m / ↑(m.factorial * m.succ)‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case cons.inr
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) L).prod) =o[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) L).prod
h₁ : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
hL : ∃ x ∈ L, f x =o[l] g x
⊢ (fun x ↦ f i x * (List.map (fun x_1 ↦ f x_1 x) L).prod) =o[l] fun x ↦ g i x * (List.map (fun x_1 ↦ g x_1 x) L).prod

Tactic:
exact h₁.1.mul_isLittleO <| ihL h₁.2 hL

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

Goal state before:
pp: x : ℂ
⊢ sinh (x + x) = 2 * sinh x * cosh x

Tactic:
sinh_add

Goal state after:
x : ℂ
⊢ sinh x * cosh x + cosh x * sinh x = 2 * sinh x * cosh x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ sinh (x * I + y * I) = sinh (x * I) * cosh (y * I) + cosh (x * I) * sinh (y * I)

Tactic:
sinh_add

Goal state after:
x y : ℂ
⊢ sinh (x * I) * cosh (y * I) + cosh (x * I) * sinh (y * I) = sinh (x * I) * cosh (y * I) + cosh (x * I) * sinh (y * I)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ sin (x + y) = sin x * cos y + cos x * sin y

Tactic:
rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, add_mul, add_mul, mul_right_comm, ← sinh_mul_I,
    mul_assoc, ← sinh_mul_I, ← cosh_mul_I, ← cosh_mul_I, sinh_add]

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

Goal state before:

Tactic:
‖∑ m ∈ range j with n ≤ m, (x ^ m / m.factorial : ℂ)‖
      = ‖∑ m ∈ range j with n ≤ m, (x ^ n * (x ^ (m - n) / m.factorial) : ℂ)‖ := by
      refine congr_arg norm (sum_congr rfl fun m hm => ?_)
      rw [mem_filter, mem_range] at hm
      rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.2]
    _ ≤ ∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / m.factorial)‖ :=
      IsAbsoluteValue.abv_sum norm ..
    _ ≤ ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / m.factorial) := by
      simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]
      gcongr
      rw [Complex.norm_pow]
      exact pow_le_one₀ (norm_nonneg _) hx
    _ = ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, (1 / m.factorial : ℝ) := by
      simp [← mul_sum]
    _ ≤ ‖x‖ ^ n * (n.succ * (n.factorial * n : ℝ)⁻¹) := by
      gcongr
      exact sum_div_factorial_le _ _ hn

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

Goal state before:
pp: x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x ^ (n + i) / ↑(n + i).factorial‖ ≤ ∑ i ∈ range k, ‖x‖ ^ (n + i) / ↑(n + i).factorial

Tactic:
by
      simp [norm_natCast, Complex.norm_pow]

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

Goal state before:
pp: x : ℂ
⊢ cos x ^ 2 = 1 - sin x ^ 2

Tactic:
rw [← sin_sq_add_cos_sq x, add_sub_cancel_left]

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

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) j

Tactic:
← sum_Ico_eq_sub _ hj

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ k ∈ Ico n j, x ^ k / ↑k.factorial‖ ≤ ↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) j
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos x ^ 2 = 1 - sin x ^ 2

Tactic:
rw [← sin_sq_add_cos_sq x, add_sub_cancel_left]

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

Goal state before:
pp: n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |x ^ n / ↑n.factorial| * |1 + x / (↑n + 1) * a₂ - a₁| ≤
    |x| ^ n / ↑n.factorial * b₁

Tactic:
convert!
    mul_le_mul_of_nonneg_left (a := |x| ^ n / ↑(Nat.factorial n)) (le_sub_iff_add_le'.1 e) ?_
      using 1

Goal state after:
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |x ^ n / ↑n.factorial| * |1 + x / (↑n + 1) * a₂ - a₁| =
    |x| ^ n / ↑n.factorial * (|x| / ↑(n + 1) * b₂ + |1 + x / ↑(n + 1) * a₂ - a₁|)

n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ 0 ≤ |x| ^ n / ↑n.factorial
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
hx' : x < 2
⊢ rexp x ≤ (2 + x) / (2 - x)

Tactic:
obtain rfl | hx₀ := hx.eq_or_lt
  · simp
  · exact (exp_lt_two_add_div_two_sub hx₀ hx').le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ f =o[𝓝 b] g ↔ (f ∘ ⇑e) =o[𝓝 (e.symm b)] (g ∘ ⇑e)

Tactic:
by
  simp only [IsLittleO_def]
  exact forall₂_congr fun c _hc => e.isBigOWith_congr

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

Goal state before:
pp: x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ sin (x / 2) ≤ 0

Tactic:
apply sin_nonpos_of_nonpos_of_neg_pi_le <;> linarith

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto f l (comap cexp (𝓝 0)) ↔ Tendsto (fun x ↦ (f x).re) l atBot

Tactic:
comap_exp_nhds_zero,

Goal state after:
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto f l (comap re atBot) ↔ Tendsto (fun x ↦ (f x).re) l atBot
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
n : N
⊢ ∃ m, f m = n ∧ ‖m‖ < ‖n‖ + ε

Tactic:
obtain ⟨m, rfl⟩ := hquot.surjective n

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ ∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ closedBall 1 δ / s = cthickening δ s⁻¹

Tactic:
by
  simp [div_eq_mul_inv, mul_comm, hs.inv.mul_closedBall_one hδ]

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

Goal state before:
pp: n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Tactic:
have C : 0 < π / 2 ^ (n + 1) := by positivity

Goal state after:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
⊢ (fun n ↦ ↑n ^ k * r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n

Tactic:
have A : (fun n ↦ (n : R) ^ k : ℕ → R) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n :=
    isLittleO_pow_const_const_pow_of_one_lt k ((one_lt_div h0).2 h)

Goal state after:
case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n ↦ ↑n ^ k) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n
⊢ (fun n ↦ ↑n ^ k * r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NontrivialTopology E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : ‖y‖ = r
⊢ (sphere x r).Nonempty

Tactic:
exact ⟨x + y, by simpa using hy⟩

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
⊢ Tendsto (fun n ↦ v (1 / (1 + a ^ n))) atTop (𝓝 1)

Tactic:
map_div₀ v,

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
⊢ Tendsto (fun n ↦ v 1 / v (1 + a ^ n)) atTop (𝓝 1)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u

Tactic:
have : Metric.closedBall (0 : 𝕜) (ε / R) ∈ 𝓝 (0 : 𝕜) := closedBall_mem_nhds _ (div_pos εpos Rpos)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case neg
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n ↦ x ^ n
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
nontriviality R

Goal state after:
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n ↦ x ^ n
a✝ : Nontrivial R
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (1 + x) * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1

Tactic:
rw [add_mul, one_mul, geom_series_mul_shift x h, geom_series_succ x h, two_mul, add_sub_assoc]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
x : E
⊢ cthickening (ε + δ) {x} = Metric.closedBall x (ε + δ)

Tactic:
cthickening_singleton _ (add_nonneg hε hδ.le)

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
x : E
⊢ Metric.closedBall x (ε + δ) = Metric.closedBall x (ε + δ)
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1.inl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
V : Set Y
hKV : (∅, V) ∈ S
⊢ MapsTo ⇑f ∅ V

pp: case refine_1.inr
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
K : Set X
V : Set Y
hKV : (K, V) ∈ S
hKne : K.Nonempty
⊢ MapsTo (⇑f) K V

Tactic:
· exact mapsTo_empty _ _

Goal state after:
case refine_1.inr
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
K : Set X
V : Set Y
hKV : (K, V) ∈ S
hKne : K.Nonempty
⊢ MapsTo (⇑f) K V
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
r : X
f : C(Y, Z)
K : Set Y
hK : IsCompact K
U : Set (X × Z)
hU : IsOpen[instTopologicalSpaceProd] U
H : MapsTo (⇑((const Y (r, f).1).prodMk (r, f).2)) K U
V : Set X
W : Set Z
hV : IsOpen[inst✝²] V
hW : IsOpen[inst✝] W
hrV : {r} ⊆ V
hKW : ⇑f '' K ⊆ W
hVW : V ×ˢ W ⊆ U
r' : X
f' : C(Y, Z)
hr'V : (r', f').1 ∈ V
hf' : (r', f').2 ∈ {x | (fun g ↦ MapsTo (⇑g) K W) x}
x : Y
hxK : x ∈ K
⊢ ((const Y (r', f').1).prodMk (r', f').2) x ∈ U

Tactic:
exact hVW (Set.mk_mem_prod hr'V (hf' hxK))

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
⊢ pathComponent x = pathComponent y

Tactic:
by
  ext z
  constructor
  · intro h'
    rw [pathComponent_symm]
    exact (h.trans h').symm
  · intro h'
    rw [pathComponent_symm] at h' ⊢
    exact h'.trans h

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 g : C(X, Y)
h : ⇑f ⤳ ⇑g
this : ∀ (K : Set X), IsCompact K → ∀ (U : Set Y), IsOpen[inst✝] U → MapsTo (⇑g) K U → MapsTo (⇑f) K U
⊢ f ⤳ g

Tactic:
simpa [specializes_iff_pure, nhds_compactOpen]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U W : Set X
hW : IsPathConnected W
hWU : W ⊆ U
⊢ IsPathConnected (Subtype.val ⁻¹' W)

Tactic:
rwa [IsInducing.subtypeVal.isPathConnected_iff, Subtype.image_preimage_val, inter_eq_right.2 hWU]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ PathConnectedSpace X ↔ IsPathConnected univ

Tactic:
simp [pathConnectedSpace_iff, isPathConnected_iff, nonempty_iff_univ_nonempty]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
this : ∀ x ∈ s, Continuous[inst✝², inst✝¹] (f x)
x : ↑s
y : X
| mkD (f ↑x) g

Tactic:
rw [mkD_of_continuous (this x x.2)]

Goal state after:
X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
this : ∀ x ∈ s, Continuous[inst✝², inst✝¹] (f x)
x : ↑s
y : X
| { toFun := f ↑x, continuous_toFun := ⋯ }
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ γ₂.symm.extend (2 * (1 - t)) = γ₂.extend (2 * t - 1)

Tactic:
extend_symm_apply

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ γ₂.extend (1 - 2 * (1 - t)) = γ₂.extend (2 * t - 1)
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (p.1, f p.2)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] g

Tactic:
by
  have : Continuous fun p : X₀ × Y => g ((Prod.swap p).1, f (Prod.swap p).2) :=
    hg.comp continuous_swap
  have : Continuous fun p : X₀ × Y => (g ∘ Prod.swap) (f p.1, p.2) := this
  exact (hf.continuous_lift_prod_left this).comp continuous_swap

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
this : range f = univ
⊢ range (⇑γ ∘ f) = range ⇑γ

Tactic:
rw [range_comp, this, image_univ]

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

Goal state before:
pp: x y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
⊢ arcsin x = y ↔ x = sin y

Tactic:
simp only [le_antisymm_iff, arcsin_le_iff_le_sin' (mem_Ico_of_Ioo hy),
    le_arcsin_iff_sin_le' (mem_Ioc_of_Ioo hy)]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).re = Real.log ‖↑x‖

Tactic:
ofReal_re,

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ Real.log x = Real.log ‖↑x‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Ioc (-π) π
⊢ x + ↑n * (2 * ↑π * I) = 0

Tactic:
rw [← log_exp this.1 this.2, exp_periodic.int_mul n, h, log_one]

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

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

Tactic:
rw [ne_eq, cpow_eq_zero_iff, not_and_or, ne_eq, not_not]

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

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

Tactic:
by
    rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have : (n : ℝ) / d < -1 := by exact_mod_cast of_decide_eq_true h
    exact Real.log_pos_of_lt_neg_one this

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |θ.cos| = |ψ.sin|

Tactic:
rw [← eq_sub_iff_add_eq, ← two_nsmul_coe_div_two, ← nsmul_sub, two_nsmul_eq_iff] at h

Goal state after:
θ ψ : Angle
h : θ = ↑(π / 2) - ψ ∨ θ = ↑(π / 2) - ψ + ↑π
⊢ |θ.cos| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2

Tactic:
simp only [sign, sin_two_nsmul, nsmul_eq_mul, Nat.cast_ofNat, sign_mul, Nat.ofNat_pos, sign_pos,
    one_mul, mul_right_eq_self₀, _root_.sign_eq_zero_iff, sign_eq_one_iff, sin_eq_zero_iff,
    cos_pos_iff_abs_toReal_lt_pi_div_two]
  have : 0 < π / 2 := by positivity
  grind

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

Goal state before:
pp: case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)

Goal state after:
case neg
x a : ℝ
hyp : Complex.re 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
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 ↦ ?_

Goal state after:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ IsBigOWith c l (fun x ↦ f x ^ r) fun x ↦ g x ^ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y : ℝ
⊢ ‖x ^ ↑y‖ = ‖x‖ ^ y

Tactic:
norm_cpow_of_imp

Goal state after:
x : ℂ
y : ℝ
⊢ ‖x‖ ^ (↑y).re / rexp (x.arg * (↑y).im) = ‖x‖ ^ y

x : ℂ
y : ℝ
⊢ x = 0 → (↑y).re = 0 → ↑y = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ‖↑x ^ y‖ = x ^ y.re

Tactic:
norm_cpow_of_imp

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ‖↑x‖ ^ y.re / rexp ((↑x).arg * y.im) = x ^ y.re

x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ↑x = 0 → y.re = 0 → y = 0
Module: Mathlib.GroupTheory.GroupAction.Pointwise

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst✝³ : SMul M α
inst✝² : SMul N β
inst✝¹ : FunLike F α β
inst✝ : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective fun m ↦ c • m
hc' : Injective fun n ↦ σ c • n
x : α
y : β
hy : y ∈ t
hxy : (fun x ↦ σ c • x) y = σ c • f x
⊢ c • x ∈ c • ⇑f ⁻¹' t

Tactic:
hc'.eq_iff

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst✝³ : SMul M α
inst✝² : SMul N β
inst✝¹ : FunLike F α β
inst✝ : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective fun m ↦ c • m
hc' : Injective fun n ↦ σ c • n
x : α
y : β
hy : y ∈ t
hxy : y = f x
⊢ c • x ∈ c • ⇑f ⁻¹' t
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y z : ℝ
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
obtain rfl | hx₀ := eq_or_ne x 0
  · obtain rfl | hz := eq_or_ne z 0
    · simp [zero_rpow_def]
    · simp +contextual [hz]
  obtain rfl | hx₁ := eq_or_ne x 1
  · simp
  simpa [hx₀, hx₁] using rpow_right_inj (y := y) (z := z) hx₀ hx₁

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

Goal state before:
pp: case inl
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun x ↦ x ^ q) x

Tactic:
exact (continuousAt_rpow (x, q) h).comp₂ continuousAt_id continuousAt_const

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

Goal state before:
pp: case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ 0 < -(↑(x, y).1).re

Tactic:
ofReal_re,

Goal state after:
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ 0 < -(x, y).1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: x : ℝ≥0∞
hx : x ≠ ∞
y : ℝ≥0∞
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y

Tactic:
by
  lift x to ℝ≥0 using hx
  by_cases h : y = ∞
  · exact Eventually.of_forall fun n => h.symm ▸ le_top
  · lift y to ℝ≥0 using h
    have := NNReal.eventually_pow_one_div_le x (mod_cast hy : 1 < y)
    refine this.congr (Eventually.of_forall fun n => ?_)
    rw [← coe_rpow_of_nonneg x (by positivity : 0 ≤ (1 / n : ℝ)), coe_le_coe]

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

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

Tactic:
inv_mul_cancel₀ (by positivity),

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ x ^ 1 = x
Module: Mathlib.Algebra.Order.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : Semiring β
inst✝³ : PartialOrder β
inst✝² : Algebra α β
inst✝¹ : ZeroLEOneClass β
inst✝ : SMulPosMono α β
a : α
ha : 0 ≤ a
⊢ 0 ≤ (algebraMap α β) a

Tactic:
by
  simpa using algebraMap_mono β ha

Goal state after: