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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ ∀ᶠ (x : α) in l, ‖f₁ x + f₂ x‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
filter_upwards [h₁, h₂] with x hx₁ hx₂

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ ‖f₁ x + f₂ x‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
⊢ (fun x ↦ f₁ x + f₂ x) =o[l] fun x ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
refine (h₁.trans_le fun x => ?_).add (h₂.trans_le ?_)

Goal state after:
case refine_1
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
x : α
⊢ ‖g₁ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

case refine_2
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
⊢ ∀ (x : α), ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k : ℕ
hi :
  abv (∑ i ∈ range (k + max n i), f i + -∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (k + max n i), a k + -∑ k ∈ range (max n i), a k
⊢ abv (f (k + max n i) + (∑ x ∈ range (k + max n i), f x + -∑ x ∈ range (max n i), f x)) ≤
    a (k + max n i) + (∑ x ∈ range (k + max n i), a x + -∑ x ∈ range (max n i), a x)

Tactic:
abv_add abv,

Goal state after:
case succ
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k : ℕ
hi :
  abv (∑ i ∈ range (k + max n i), f i + -∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (k + max n i), a k + -∑ k ∈ range (max n i), a k
⊢ abv (f (k + max n i)) + abv (∑ x ∈ range (k + max n i), f x + -∑ x ∈ range (max n i), f x) ≤
    a (k + max n i) + (∑ x ∈ range (k + max n i), a x + -∑ x ∈ range (max n i), a x)
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
⊢ ∃ i,
    ∀ j ≥ i, abv ((∑ k ∈ range j, f k) * ∑ k ∈ range j, g k - ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε

Tactic:
let ⟨P, hP⟩ := ha.bounded

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
⊢ ∃ i,
    ∀ j ≥ i, abv ((∑ k ∈ range j, f k) * ∑ k ∈ range j, g k - ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x ↦ ‖c‖ * ‖f' x‖) =O[l] g ↔ f' =O[l] g

Tactic:
isBigO_const_mul_left_iff cne0,

Goal state after:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x ↦ ‖f' x‖) =O[l] g ↔ f' =O[l] g
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atBot
⊢ f =o[l] g

Tactic:
refine IsLittleO.of_neg_left (IsLittleO.of_tendsto_div_atTop ?_)

Goal state after:
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atBot
⊢ Tendsto (fun x ↦ g x / -f x) l atTop
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v) → u =O[l] v

Tactic:
rintro ⟨φ, ⟨c, hφ⟩, huvφ⟩

Goal state after:
case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
huvφ : u =ᶠ[l] φ * v
c : ℝ
hφ : ∀ᶠ (x : ℝ) in map (norm ∘ φ) l, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ u =O[l] v
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Tactic:
have h₂ : (n.succ : α) ≠ 0 := by positivity

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x ↦ f x i) g'

Tactic:
have this (x) : 0 ≤ C * ‖g' x‖ := by positivity

Goal state after:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
this : ∀ (x : α), 0 ≤ C * ‖g' x‖
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x ↦ f x i) g'
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
by
  simp [cos_add, cos_sub]
  ring

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

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

Tactic:
by
  simp [cos_add, cos_sub]
  ring

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

Goal state before:
pp: x : ℝ
⊢ sin x ^ 2 = 1 / 2 - cos (2 * x) / 2

Tactic:
rw [sin_sq, cos_sq, ← sub_sub, sub_half]

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0

Tactic:
refine ⟨lt_imp_lt_of_le_imp_le (zpow_nonneg · _), fun ha ↦ ?_⟩
  obtain ⟨k, rfl⟩ := hn
  rw [zpow_add_one₀ ha.ne]
  exact mul_neg_of_pos_of_neg (Even.zpow_pos (even_two_mul _) ha.ne) ha

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

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x < 1
⊢ rexp x ≤ 1 / (1 - x)

Tactic:
by
  rcases eq_or_lt_of_le h1 with (rfl | h1)
  · simp
  · exact (exp_bound_div_one_sub_of_interval' h1 h2).le

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

Goal state before:
pp: n : ℕ
t : ℝ
ht' : t ≤ ↑n
⊢ (1 - t / ↑n) ^ n ≤ rexp (-t)

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)
  · simp
    rwa [Nat.cast_zero] at ht'
  calc
    (1 - t / n) ^ n ≤ rexp (-(t / n)) ^ n := by
      gcongr
      · exact sub_nonneg.2 <| div_le_one_of_le₀ ht' n.cast_nonneg
      · exact one_sub_le_exp_neg _
    _ = rexp (-t) := by rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity

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

Goal state before:
pp: n : ℕ
⊢ (1 + (↑n)⁻¹) ^ n ≤ rexp 1

Tactic:
convert one_sub_div_pow_le_exp_neg (n := n) (t := -1) (by grind) using 1
  · field
  · simp

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

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

Tactic:
by
  rw [← abs_sin_half, abs_of_nonpos, neg_neg]
  apply sin_nonpos_of_nonpos_of_neg_pi_le <;> linarith

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam ((fun x ↦ c⁻¹ • x) '' (c • s)) ≤ ‖c⁻¹‖₊ • ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)

Tactic:
Set.image_smul,

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam (c⁻¹ • c • s) ≤ ‖c⁻¹‖₊ • ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
linarith [sqrtTwoAddSeries_nonneg le_rfl n]

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

Goal state before:
pp: case hx
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
linarith [sqrtTwoAddSeries_nonneg le_rfl n]

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

Goal state before:
pp: case hc
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ 2 ≠ 0

Tactic:
linarith [sqrtTwoAddSeries_nonneg le_rfl n]

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

Goal state before:
pp: case hl
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ -π ≤ π / 2 ^ (n + 1)

Tactic:
linarith [sqrtTwoAddSeries_nonneg le_rfl n]

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

Goal state before:
pp: case hr
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ π / 2 ^ (n + 1) ≤ π

Tactic:
linarith [sqrtTwoAddSeries_nonneg le_rfl n]

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

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) ⊆ ball x r

Tactic:
intro y

Goal state after:
case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
y : E
⊢ y ∈ interior (closedBall x r) → y ∈ ball x r
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
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
⊢ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s) ⊆ u

Tactic:
intro y

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 : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
⊢ y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s) → y ∈ u
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ √2 / 2 / (√2 / 2) = 1

Tactic:
have h : √2 / 2 > 0 := by positivity

Goal state after:
h : √2 / 2 > 0
⊢ √2 / 2 / (√2 / 2) = 1
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y

Tactic:
intro y

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
y : X
⊢ y ∈ F → JoinedIn F x y
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
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst✝¹] (Function.uncurry f)
⊢ Continuous[inst✝, _] fun x ↦ mkD (f x) g

Tactic:
by
  have (x : _) : Continuous (f x) := f_cont.comp (Continuous.prodMk_right x)
  refine continuous_of_continuous_uncurry _ ?_
  conv in mkD _ _ => rw [mkD_of_continuous (this x)]
  exact f_cont

Goal state after:
Module: Mathlib.Topology.Path

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

Tactic:
extend_apply _ ⟨ht₀, by linarith⟩,

Goal state after:
case inr
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ (γ₁.trans γ₂) ⟨t, ⋯⟩ = γ₁.extend (2 * t)
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 : Set X
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), PathConnectedSpace (Z i)
⊢ PathConnectedSpace ((i : ι) → Z i)

Tactic:
by
  rw [pathConnectedSpace_iff_univ, ← Set.pi_univ]
  exact .pi fun _ ↦ isPathConnected_univ

Goal state after:
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 : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous[inst✝², inst✝¹] fun y ↦ g (x, y)
G : X → C(Y, Z) := fun x ↦ { toFun := fun y ↦ g (x, y), continuous_toFun := ⋯ }
⊢ Continuous[inst✝³, _] G

Tactic:
rw [hf.continuous_iff]

Goal state after:
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 : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous[inst✝², inst✝¹] fun y ↦ g (x, y)
G : X → C(Y, Z) := fun x ↦ { toFun := fun y ↦ g (x, y), continuous_toFun := ⋯ }
⊢ Continuous[inst✝⁴, _] (G ∘ f)
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inl
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ |p| / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : 0 < p
⊢ ‖↑x‖ = |x|

Tactic:
rw [abs_eq_self.mpr hp.le] at hx
      exact this p hp hx

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

Goal state before:
pp: x : ℝ
h : 0 < x
⊢ log x < 0 ↔ x < 1

Tactic:
by
  rw [← log_one]
  exact log_lt_log_iff h zero_lt_one

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ log x ≤ 0 ↔ x ≤ 1

Tactic:
by
  rcases hx.eq_or_lt with (rfl | hx)
  · simp [zero_le_one]
  rw [← not_lt, log_pos_iff hx.le, not_lt]

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

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

Tactic:
neg_le,

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ -log x ≤ x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ = -θ ↔ θ = 0 ∨ θ = ↑π

Tactic:
eq_neg_self_iff

Goal state after:
θ : Angle
⊢ θ = 0 ∨ θ = ↑π ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
eq_false (two_ne_zero' ℝ),

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

Goal state before:
pp: x : ℂ
hx : ¬x = 0
⊢ x ^ 1 = x

Tactic:
by rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]

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

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log e

Tactic:
by
  rw [NormNum.IsNat.to_eq h rfl]
  apply Real.log_pos
  simpa using w

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

Goal state before:
pp: θ : Angle
ψ : ℝ
⊢ θ.cos = Real.cos ψ ↔ θ = ↑ψ ∨ θ = -↑ψ

Tactic:
induction θ using Real.Angle.induction_on
  exact cos_eq_iff_coe_eq_or_eq_neg

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

Goal state before:
pp: θ : Angle
⊢ θ.sin = sin 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
rw [sin_eq_iff_eq_or_add_eq_pi]

Goal state after:
θ : Angle
⊢ θ = 0 ∨ θ + 0 = ↑π ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl
x : ℂ
hi : x.im = 0
⊢ (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0

Tactic:
rw [(ext rfl hi : x = x.re)]
    rcases lt_trichotomy x.re 0 with (hr | hr | hr)
    · rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]
      simp [hr]
    · simp [hr, Real.pi_ne_zero]
    · rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
      simp [hr.not_gt, ← add_eq_zero_iff_eq_neg, Real.pi_ne_zero]

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

Goal state before:
pp: x y : ℂ
⊢ ↑x.arg = ↑y.arg ↔ x.arg = y.arg

Tactic:
by
  simp_rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]

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

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

Tactic:
inv_mul_cancel₀ hy,

Goal state after:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ x ^ 1 = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
rpow_mul,

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
n : ℕ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul, rpow_natCast]

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

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

Tactic:
rpow_mul,

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

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

Tactic:
rw [rpow_mul, rpow_natCast]

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_mul,

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_mul,

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

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

Tactic:
inv_mul_cancel₀ hy,

Goal state after:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ x ^ 1 = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ x ^ y ≤ x ^ z ↔ z ≤ y

Tactic:
rw [← log_le_log_iff (rpow_pos_of_pos hx0 y) (rpow_pos_of_pos hx0 z), log_rpow hx0, log_rpow hx0,
    mul_le_mul_right_of_neg (log_neg hx0 hx1)]

Goal state after:
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:
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.NNReal

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
rpow_mul,

Goal state after:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ (x ^ z) ^ z⁻¹ ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
rpow_mul,

Goal state after:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ (x ^ z) ^ z⁻¹ < y ^ z⁻¹ ↔ x ^ z < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Tactic:
nth_rw 1 [← ENNReal.rpow_one y]

Goal state after:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ^ 1 ↔ x ≤ y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z < 0
⊢ 1 ≤ x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx2 coe_lt_top)

Goal state after:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < ↑x
hx2 : ↑x ≤ 1
⊢ 1 ≤ ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
inv_mul_cancel₀ hy,

Goal state after:
y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
⊢ x ^ 1 = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
rpow_mul,

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∞
n : ℕ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul, rpow_natCast]

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

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

Tactic:
rpow_mul,

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

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

Tactic:
rw [rpow_mul, rpow_natCast]

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_mul,

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_mul,

Goal state after:
x : ℝ≥0∞
y : ℝ
n : ℤ
⊢ (x ^ y) ^ ↑n = (x ^ y) ^ n
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R✝ : Type u_1
inst✝⁶ : CommRing R✝
inst✝⁵ : PartialOrder R✝
inst✝⁴ : IsStrictOrderedRing R✝
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ M
inst✝ : Module R✝ N
x y : M
R : Type u_4
v : RayVector R M
⊢ - -v = v

Tactic:
RayVector.ext_iff,

Goal state after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
inst✝⁵ : PartialOrder R✝
inst✝⁴ : IsStrictOrderedRing R✝
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ M
inst✝ : Module R✝ N
x y : M
R : Type u_4
v : RayVector R M
⊢ ↑((equiv R M) (- -v)) = ↑((equiv R M) v)