mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
U : ↥(unitary E)
⊢ ‖1‖ = 1

Tactic:
CStarRing.norm_one

Goal state after:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
U : ↥(unitary E)
⊢ 1 = 1
Module: Mathlib.Data.Complex.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
f : α → ℝ
a : α
⊢ ↑(balance f a) = balance (ofReal ∘ f) a

Tactic:
simp [balance]

Goal state after:
Module: Mathlib.Data.Complex.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
f : α → ℂ
a : α
⊢ (balance f a).re = balance (re ∘ f) a

Tactic:
simp [balance]

Goal state after:
Module: Mathlib.Data.Complex.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
f : α → ℂ
a : α
⊢ (balance f a).im = balance (im ∘ f) a

Tactic:
simp [balance]

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ ‖reLm x‖ ≤ 1 * ‖x‖

Tactic:
simp [abs_re_le_norm]

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

Goal state before:
pp: case inl
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.I = 0
⊢ ‖↑(RCLike.re a) + ↑(RCLike.im a) * I‖ = ‖a‖

Tactic:
rw [← RCLike.re_add_im a, RCLike.im_eq_zero h]
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : ↥(selfAdjoint A)
⊢ ↑(ℑ (I • ↑x)) = ↑x

Tactic:
by simp only [imaginaryPart_I_smul, x.property.coe_realPart]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z| ≤ ‖z‖

Tactic:
by
  rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]
  apply im_sq_le_normSq

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : X
⊢ ↑(toPartialHomeomorph f h).symm (f x) = x

Tactic:
rw [← congr_fun (h.toPartialHomeomorph_apply f), PartialHomeomorph.left_inv]
  exact Set.mem_univ _

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ f (↑(toPartialHomeomorph f h).symm x) = x

Tactic:
rw [← congr_fun (h.toPartialHomeomorph_apply f), PartialHomeomorph.right_inv]

Goal state after:
case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ x ∈ (toPartialHomeomorph f h).target
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
rw [le_iff_re_im]

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ re ↑x ≤ re ↑y ∧ im ↑x = im ↑y ↔ x ≤ y
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
x' : X
hx' : ↑e.symm (↑e x') = x'
h : ↑e x' = ↑e x
⊢ x' = ↑e.symm (↑e x')

Tactic:
hx'

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
x' : X
hx' : ↑e.symm (↑e x') = x'
h : ↑e x' = ↑e x
⊢ x' = x'
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z⁻¹ ↔ 0 < z

Tactic:
refine ⟨fun h => ?_, fun h => RCLike.inv_pos_of_pos h⟩

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
h : 0 < z⁻¹
⊢ 0 < z
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
⊢ f =Θ[⊥] g

Tactic:
simp [IsTheta]

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g

Tactic:
simp [IsTheta]

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

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 α
⊢ (f =Θ[l] fun x ↦ ‖g' x‖) ↔ f =Θ[l] g'

Tactic:
simp [IsTheta]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖g x‖ ≤ c' * ‖k x‖ → ‖f x‖ ≤ c * c' * ‖k x‖

Tactic:
hx'

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
⊢ ‖f x‖ ≤ c * c' * ‖k x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ -f' x) =o[l] g ↔ f' =o[l] g

Tactic:
simp only [IsLittleO_def]
  exact forall₂_congr fun _ _ => isBigOWith_neg_left

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
h : IsBigOWith c l u v
y : α
hy : ‖u y‖ ≤ c * ‖v y‖
hv : v y = 0
⊢ u y = 0

Tactic:
by simpa [hv] using hy

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

Goal state before:
pp: x y : ℝ
h : x < y
⊢ rexp x < rexp y

Tactic:
rw [← sub_add_cancel y x, Real.exp_add]
  exact (lt_mul_iff_one_lt_left (exp_pos _)).2
      (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite
C' : ℝ
hC' : ∀ i ∈ Finset.image (fun x ↦ ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

Tactic:
have : ∀ x, C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C' := by simpa using hC'

Goal state after:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite
C' : ℝ
hC' : ∀ i ∈ Finset.image (fun x ↦ ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
sin_sq_add_cos_sq

Goal state after:
x : ℂ
⊢ 1 = 1
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case hbc
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (‖x‖ / ↑n.succ - 1) ≤ (‖x‖ / ↑n.succ) ^ k - 1

Tactic:
trans (-1 : ℝ)
      · linarith
      · simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]
        positivity

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

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

Tactic:
sin_sq_add_cos_sq

Goal state after:
x : ℝ
⊢ 1 = 1
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
by simp [cos_two_mul]

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

Goal state before:
pp: x : ℝ
hx : 0 < cos x
⊢ tan x / √(1 + tan x ^ 2) = sin x

Tactic:
by
  rw [← tan_mul_cos hx.ne', ← inv_sqrt_one_add_tan_sq hx, div_eq_mul_inv]

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:
le_iff_lt_or_eq,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n < 0 ∨ a ^ n = 0 ↔ a ≤ 0
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 ^ n = 0 ↔ a ≤ 0

Tactic:
le_iff_lt_or_eq,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n < 0 ∨ a ^ n = 0 ↔ a < 0 ∨ a = 0
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ f =O[atTop] g

Tactic:
refine isBigO_nat_atTop_induction ?hzero ?hrec
  case hzero => filter_upwards [hf, hg]; grind
  case hrec =>
    filter_upwards [eventually_forall_ge_atTop.mpr hg, eventually_forall_ge_atTop.mpr hf, hrec]
      with n₀ hn₀ hn₀' hnrec
    obtain ⟨C₀, hnrec⟩ := hnrec
    refine ⟨C₀, ?_⟩
    filter_upwards [hnrec, eventually_ge_atTop n₀]
    grind [Real.norm_eq_abs]

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

Goal state before:
pp: r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
⊢ ‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖

Tactic:
have h_sq : ∀ z, ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2 := by
    intro z hz
    have : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 := exp_bound_sq x z hz
    rw [← sub_le_iff_le_add', ← norm_smul z]
    exact (norm_sub_norm_le _ _).trans this

Goal state after:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * ‖z‖ ^ 2
⊢ ‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - 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
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ).succ) ≤ r * ?a

Tactic:
exact h _ (Nat.le_of_succ_le kn)

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x ↦ f (rexp x)) atBot l ↔ Tendsto f (Filter.map rexp atBot) l

Tactic:
tendsto_map'_iff

Goal state after:
α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x ↦ f (rexp x)) atBot l ↔ Tendsto (f ∘ rexp) atBot l
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : (↑1 + ↑(2 * (n / 2))) * π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
Int.cast_one,

Goal state after:
x : ℝ
h : cos x = 1
n : ℤ
hn : (1 + ↑(2 * (n / 2))) * π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
⊢ ‖S.normedMk‖ = 1

Tactic:
refine le_antisymm (norm_normedMk_le S) ?_
  obtain ⟨x, hx⟩ : ∃ x : M, 0 < ‖(x : M ⧸ S)‖ := by
    refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
    exact (norm_nonneg _).lt_of_ne' <| mt norm_mk_eq_zero_iff_mem_closure.1 hx
  refine (le_mul_iff_one_le_left hx).1 ?_
  exact norm_lift_apply_le S.normedMk (fun x ↦ (eq_zero_iff x).2) x

Goal state after:
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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
ext y
  rw [mem_smul_set_iff_inv_smul_mem₀ hc]
  conv_lhs => rw [← inv_smul_smul₀ hc x]
  simp only [mem_sphere, dist_smul₀, norm_inv, ← div_eq_inv_mul, div_eq_iff (norm_pos_iff.2 hc).ne',
    mul_comm r]

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

Goal state before:
pp: ⊢ Tendsto sin (𝓝[>] (-(π / 2))) (𝓝 (-1))

Tactic:
by
  convert! continuous_sin.continuousWithinAt.tendsto using 2
  simp

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

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s

Tactic:
· rw [← closure_thickening hδ, thickening_closure, thickening_thickening hε hδ]

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

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

Tactic:
neg_div,

Goal state after:
⊢ cos (-(↑π / 2)) + sin (-(↑π / 2)) * I = -I
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := ⋯
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
⊢ ℝ

Tactic:
exact C

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
by
  have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)
  rcases this.exists_path_through_family' p fun _i => True.intro with ⟨γ, t, -, h⟩
  exact ⟨γ, t, h⟩

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)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] g

Tactic:
by
  let Gf : C(X₀, C(Y, Z)) := ContinuousMap.curry ⟨_, hg⟩
  have h : ∀ x : X, Continuous fun y => g (x, y) := by
    intro x
    obtain ⟨x₀, rfl⟩ := hf.surjective x
    exact (Gf x₀).continuous
  let G : X → C(Y, Z) := fun x => ⟨_, h x⟩
  have : Continuous G := by
    rw [hf.continuous_iff]
    exact Gf.continuous
  exact ContinuousMap.continuous_uncurry_of_continuous ⟨G, this⟩

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

Goal state before:
pp: n : ℕ
⊢ ‖∑ i ∈ Finset.range n, (-1) ^ i‖ ≤ 1

Tactic:
by
  rw [neg_one_geom_sum]
  split_ifs <;> norm_num

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

Goal state before:
pp: case inr
p : ℝ
hp : p ≠ 0
⊢ |p / 2 - ↑1 * p| = |p| / 2

Tactic:
Int.cast_one,

Goal state after:
case inr
p : ℝ
hp : p ≠ 0
⊢ |p / 2 - 1 * p| = |p| / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin (sin x) = x

Tactic:
exact injOn_sin (arcsin_mem_Icc _) h₂ (sin_arcsin' (sin_mem_Icc x))

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

Goal state before:
pp: x y : ℝ
hx : -1 ≤ x
hlt : x < y
hy : y ≤ 1
⊢ arccos y < arccos x

Tactic:
unfold arccos; gcongr

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

Goal state before:
pp: x y : ℝ
hlt : x ≤ y
⊢ arccos y ≤ arccos x

Tactic:
unfold arccos; gcongr

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

Goal state before:
pp: x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
⊢ Summable fun n ↦ x ^ n / ↑n !

Tactic:
have B : ‖x‖ / (⌊‖x‖⌋₊ + 1) < 1 := (div_lt_one A).2 (Nat.lt_floor_add_one _)

Goal state after:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ Summable fun n ↦ x ^ n / ↑n !
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
hx0 : ¬x < 0
⊢ 2 * x ≤ rexp x

Tactic:
apply le_trans (mul_le_mul_of_nonneg_right _ (le_of_not_gt hx0)) exp_one_mul_le_exp
    have := Real.add_one_le_exp 1
    rwa [one_add_one_eq_two] at this

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

Goal state before:
pp: case inr.inl
n : ℤ
hn : 0 = n
⊢ 0 ≤ log ↑n

Tactic:
simp [hn.symm]

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|

Tactic:
abs_of_neg hy,

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ -y < |x|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ (if 0 ≤ x.re then Real.arcsin (-x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (- -x.im / ‖x‖) + π else Real.arcsin (- -x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then Real.arcsin (-x.im / ‖x‖) + π else Real.arcsin (-x.im / ‖x‖) - π

Tactic:
neg_div,

Goal state after:
x : ℂ
⊢ (if 0 ≤ x.re then Real.arcsin (-(x.im / ‖x‖))
    else if 0 ≤ -x.im then Real.arcsin (- -(x.im / ‖x‖)) + π else Real.arcsin (- -(x.im / ‖x‖)) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then Real.arcsin (-(x.im / ‖x‖)) + π else Real.arcsin (-(x.im / ‖x‖)) - π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ 2 * π = 2 * π * ↑1

Tactic:
Int.cast_one,

Goal state after:
⊢ 2 * π = 2 * π * 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case e_b.e_a
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(π + π / 2 - -π / 2) = 0

Tactic:
neg_div,

Goal state after:
case e_b.e_a
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(π + π / 2 - -(π / 2)) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 = θ + ψ
⊢ ↑θ = -↑ψ

Tactic:
← sub_eq_iff_eq_add

Goal state after:
case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑θ = -↑ψ
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:
rw [NormNum.IsNat.to_eq h rfl]
  apply Real.log_pos
  simpa using w

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

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

Tactic:
exp_mul_I_periodic.sub_zsmul_eq

Goal state after:
case mp.refine_2
θ : ℝ
⊢ cexp (↑θ * I) = cexp (↑θ * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -1 < -z.im / ‖z‖

Tactic:
neg_div,

Goal state after:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -1 < -(z.im / ‖z‖)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]
      simp [hr]

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

Goal state before:
pp: θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
two_nsmul_toReal_eq_two_mul_sub_two_pi

Goal state after:
θ : Angle
⊢ π / 2 < θ.toReal ↔ π / 2 < θ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ (↑0).tan = 0

Tactic:
tan_coe,

Goal state after:
⊢ Real.tan 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ (↑π).tan = 0

Tactic:
tan_coe,

Goal state after:
⊢ Real.tan π = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
x✝ : ℝ
⊢ (↑(x✝ + π)).tan = (↑x✝).tan

Tactic:
tan_coe,

Goal state after:
case h
x✝ : ℝ
⊢ Real.tan (x✝ + π) = (↑x✝).tan
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
tan_coe,

Goal state after:
case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ Real.tan x✝ = (↑x✝¹).tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ Real.tan x✝ = (↑x✝¹).tan⁻¹

Tactic:
tan_coe,

Goal state after:
case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ Real.tan x✝ = (Real.tan x✝¹)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ SignType.sign (Real.sin (-π / 2)) = -1

Tactic:
neg_div,

Goal state after:
⊢ SignType.sign (Real.sin (-(π / 2))) = -1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≤ 0
y : ℂ
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)

Tactic:
rcases hx.eq_or_lt with (rfl | hlt)

Goal state after:
case inl
y : ℂ
hx : 0 ≤ 0
⊢ ↑0 ^ y = (-↑0) ^ y * cexp (↑π * I * y)

case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)
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:
by
  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.Real

Goal state before:
pp: case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

Tactic:
rw [Real.zero_rpow hw, zero_div, zero_cpow, norm_zero]
    exact ne_of_apply_ne re hw

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

Goal state before:
pp: case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ (-p)

Tactic:
exact rpow_pos_of_nonneg (neg_pos.mpr hp_neg)

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

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

Tactic:
le_iff_lt_or_eq,

Goal state after:
x q : ℝ
h : x ≠ 0 ∨ 0 < q ∨ 0 = q
⊢ ContinuousAt (fun x ↦ x ^ q) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ x ^ y < x ^ z

Tactic:
rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]

Goal state after:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < x ^ z

Tactic:
rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]

Goal state after:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < rexp (log x * z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < rexp (log x * z)

Tactic:
rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]

Goal state after:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < rexp (log x * z)