mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : X
⊢ x ∈ e.source

Tactic:
rw [h]

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : X
⊢ x ∈ univ
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst✝¹] s
hse : s ⊆ e.source
⊢ IsOpen[inst✝] (↑e '' s)

Tactic:
rw [(image_eq_target_inter_inv_preimage (e := e) hse)]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst✝¹] s
hse : s ⊆ e.source
⊢ IsOpen[inst✝] (e.target ∩ ↑e.symm ⁻¹' s)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : RCLike K
z : K
h : z = ↑‖z‖
⊢ ‖z‖ ≤ re z

Tactic:
rw [h]

Goal state after:
case refine_2
K : Type u_1
inst✝ : RCLike K
z : K
h : z = ↑‖z‖
⊢ ‖↑‖z‖‖ ≤ re ↑‖z‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case inr
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ ∀ᶠ (x : α) in l, ‖∑ i ∈ s, A i x‖ ≤ sSup (C '' ↑s) * ‖∑ i ∈ s, ‖B i x‖‖

Tactic:
filter_upwards [(eventually_all_finset s).mpr hAB]
    with x hx

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ ‖∑ i ∈ s, A i x‖ ≤ sSup (C '' ↑s) * ‖∑ i ∈ s, ‖B i x‖‖
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:
rw [← isLittleO_norm_left]

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 ↦ ‖c • f' x‖) =o[l] g ↔ f' =o[l] g
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
rw [← ih (by simp)]

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

Goal state before:
pp: x : ℂ
⊢ (starRingEnd ℂ) (cexp x - cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x - cexp (-x)) / (starRingEnd ℂ) 2

Tactic:
map_ofNat

Goal state after:
x : ℂ
⊢ (starRingEnd ℂ) (cexp x - cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x - cexp (-x)) / 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ (starRingEnd ℂ) (cexp x + cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x + cexp (-x)) / (starRingEnd ℂ) 2

Tactic:
map_ofNat

Goal state after:
x : ℂ
⊢ (starRingEnd ℂ) (cexp x + cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x + cexp (-x)) / 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin (x * I) = sinh x * I

Tactic:
by
  have h : I * sin (x * I) = -sinh x := by
    rw [mul_comm, ← sinh_mul_I]
    ring_nf
    simp
  rw [← neg_neg (sinh x), ← h]
  apply Complex.ext <;> simp

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

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
h : ∀ (x : α), g'' x = 0 → f'' x = 0
⊢ f'' =O[cofinite] g'' ↔ ∃ C, ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖

Tactic:
by
  classical
  exact ⟨fun h' =>
    let ⟨C, _C₀, hC⟩ := bound_of_isBigO_cofinite h'
    ⟨C, fun x => if hx : g'' x = 0 then by simp [h _ hx, hx] else hC hx⟩,
    fun h => (isBigO_top.2 h).mono le_top⟩

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
⊢ |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))

Tactic:
have hxc : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx

Goal state after:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖↑x‖ ≤ 1
⊢ |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))
Module: Mathlib.Algebra.Order.Field.Power

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

Tactic:
by
  obtain ⟨k, rfl⟩ := hn; rw [zpow_add' (by simp [em'])]; exact mul_self_nonneg _

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

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =O[atTop] fun x ↦ a ^ x
⊢ ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n

Tactic:
rcases bound_of_isBigO_nat_atTop H with ⟨C, hC₀, hC⟩
    refine ⟨a, ha, C, hC₀, fun n ↦ ?_⟩
    simpa only [Real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le] using hC (pow_ne_zero n ha.1.ne')

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝ : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
this✝ : Nonempty ↑{m | ↑m = x}
this : Nonempty ↑{m | ↑m = y}
⊢ ⨅ y_1, dist 1 ↑y_1 ≤ (⨅ y, dist 1 ↑y) + ⨅ y_1, dist 1 ↑y_1

Tactic:
refine le_ciInf_add_ciInf ?_

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝ : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
this✝ : Nonempty ↑{m | ↑m = x}
this : Nonempty ↑{m | ↑m = y}
⊢ ∀ (i : ↑{m | ↑m = x}) (j : ↑{m | ↑m = y}), ⨅ y_1, dist 1 ↑y_1 ≤ dist 1 ↑i + dist 1 ↑j
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
⊢ IsBounded (s * t)

Tactic:
refine isBounded_iff_forall_norm_le'.2 ⟨Rs + Rt, ?_⟩

Goal state after:
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
⊢ ∀ x ∈ s * t, ‖x‖ ≤ Rs + Rt
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ infEDist (c • x) (c • s) = ‖c‖₊ • infEDist x s

Tactic:
infEDist

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ⨅ y ∈ c • s, edist (c • x) y = ‖c‖₊ • ⨅ y ∈ s, edist x y
Module: Mathlib.Analysis.SpecificLimits.Normed

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

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

Tactic:
· refine (isLittleO_zero _ _).congr' (mem_atTop_sets.2 <| ⟨1, fun n hn ↦ ?_⟩) EventuallyEq.rfl
    simp [zero_pow (one_le_iff_ne_zero.1 hn), h0]

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

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

Tactic:
linarith [cos_pi]

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

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
⊢ HasSum (fun n ↦ ξ ^ n) (1 - ξ)⁻¹

Tactic:
by
  have xi_ne_one : ξ ≠ 1 := by
    contrapose! h
    simp [h]
  have A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹)) :=
    ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one h).sub tendsto_const_nhds).mul tendsto_const_nhds
  rw [hasSum_iff_tendsto_nat_of_summable_norm]
  · simpa [geom_sum_eq, xi_ne_one, neg_inv, div_eq_mul_inv] using A
  · simp [norm_pow, summable_geometric_of_lt_one (norm_nonneg _) h]

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

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ Summable fun n ↦ ‖↑(u n) * r ^ n‖

Tactic:
apply summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h)

Goal state after:
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n ↦ ‖↑(u n) * r ^ n‖) =O[atTop] fun n ↦ r' ^ n
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < ↑r
⊢ δ < ↑r

Tactic:
have := hs.trans_lt ((infEDist_le_edist_of_mem hz).trans_lt h)

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < ↑r
this : ENNReal.ofReal δ < ↑r
⊢ δ < ↑r
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
⊢ thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)

Tactic:
rw [← thickening_singleton, thickening_thickening hε hδ, thickening_singleton]

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

Goal state before:
pp: E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)

Tactic:
rw [sub_eq_add_neg, neg_closedBall, closedBall_add_closedBall hε hδ, sub_eq_add_neg]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
hUV : (U ∩ V).Nonempty
⊢ IsPathConnected (U ∪ V)

Tactic:
by
  rcases hUV with ⟨x, xU, xV⟩
  use x, Or.inl xU
  rintro y (yU | yV)
  · exact (hU.joinedIn x xU y yU).mono subset_union_left
  · exact (hV.joinedIn x xV y yV).mono subset_union_right

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
ι : Type u_6
l : Filter ι
F : ι → C(X, Y)
f : C(X, Y)
⊢ Tendsto F l (𝓝 f) ↔ ∀ (K : Set X), IsCompact K → Tendsto (fun i ↦ restrict K (F i)) l (𝓝 (restrict K f))

Tactic:
simp [nhds_iInf, nhds_induced, Filter.tendsto_comap_iff, Function.comp_def]

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

Goal state before:
pp: E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i • z i

Tactic:
by
  have hfa' : Monotone fun n ↦ -f n := fun _ _ hab ↦ neg_le_neg <| hfa hab
  have hf0' : Tendsto (fun n ↦ -f n) atTop (𝓝 0) := by
    convert! hf0.neg
    simp
  convert! (hfa'.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0' hzb).neg
  simp

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

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

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

Goal state after:
case inr
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ |p| / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : p < 0
⊢ ‖↑x‖ = |x|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : ¬-1 ≤ x
h : √(1 - x ^ 2) = 0
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)

Tactic:
rw [h]

Goal state after:
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
h : √(1 - x ^ 2) = 0
⊢ sin (arcsin x) / 0 = x / 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : √(1 - x ^ 2) = 0
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)

Tactic:
rw [h]

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : √(1 - x ^ 2) = 0
⊢ sin (arcsin x) / 0 = x / 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ π / 2 - π = arcsin x ↔ x ≤ -1

Tactic:
div_two_sub_self,

Goal state after:
x : ℝ
⊢ -(π / 2) = arcsin x ↔ x ≤ -1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ (if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) = θ

pp: case neg.inr.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ ¬0 ≤ Real.cos θ

Tactic:
if_pos,

Goal state after:
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ Real.arcsin (-Real.sin θ) + π = θ

case neg.inr.hc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ 0 ≤ Real.sin θ

case neg.inr.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ ¬0 ≤ Real.cos θ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)

Tactic:
· rw [exp_log_eq_abs h_zero]
    exact le_abs_self _

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

Goal state before:
pp: case inl
hπ : 0 < π
⊢ arg 0 ∈ Ioc (-π) π

pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ z.arg ∈ Ioc (-π) π

Tactic:
· simp [hπ, hπ.le]

Goal state after:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ z.arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: ⊢ rexp (log 1) = rexp 0

Tactic:
exp_log zero_lt_one,

Goal state after:
⊢ 1 = rexp 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
r : ℝ
hr : 0 < r
⊢ (↑r * 0).arg = arg 0

pp: case inr
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
⊢ (↑r * x).arg = x.arg

Tactic:
· rw [mul_zero]

Goal state after:
case inr
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
⊢ (↑r * x).arg = x.arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ rexp (log (x * y)) = rexp (log x + log y)

Tactic:
rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_mul]

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

Goal state before:
pp: case hbdd
R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n • g n) atTop (𝓝 t)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖↑⌊x⌋₊ - x‖

Tactic:
· apply isBoundedUnder_of_eventually_le (a := ‖(1 : K)‖)
    apply Eventually.mono _ (fun x h ↦ norm_le_norm_of_abs_le_abs h)
    simpa using ⟨0, fun _ h ↦ mod_cast Nat.abs_floor_sub_le h⟩

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

Goal state before:
pp: case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = π / 2

Tactic:
← arg_I,

Goal state after:
case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = I.arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ ((starRingEnd ℂ) x).arg = if x.re < 0 ∧ x.im = 0 then π else -x.arg

Tactic:
arg,

Goal state after:
x : ℂ
⊢ (if 0 ≤ ((starRingEnd ℂ) x).re then Real.arcsin (((starRingEnd ℂ) x).im / ‖(starRingEnd ℂ) x‖)
    else
      if 0 ≤ ((starRingEnd ℂ) x).im then Real.arcsin ((-(starRingEnd ℂ) x).im / ‖(starRingEnd ℂ) x‖) + π
      else Real.arcsin ((-(starRingEnd ℂ) x).im / ‖(starRingEnd ℂ) 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.Complex.Log

Goal state before:
pp: x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ log (x * y) = log x + log y ↔ x.arg + y.arg ∈ Ioc (-π) π

Tactic:
refine Complex.ext_iff.trans <| Iff.trans ?_ <| arg_mul_eq_add_arg_iff hx₀ hy₀
  simp_rw [add_re, add_im, log_re, log_im, norm_mul,
    Real.log_mul (norm_ne_zero_iff.mpr hx₀) (norm_ne_zero_iff.mpr hy₀), true_and]

Goal state after:
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 * π)
⊢ x = ↑(-n) * (2 * ↑π * I)

Tactic:
rw [Int.cast_neg, neg_mul, eq_neg_iff_add_eq_zero]

Goal state after:
case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ x + ↑n * (2 * ↑π * I) = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
split_ifs <;> simp [*, exp_ne_zero]

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

Goal state before:
pp: case inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im < 0
⊢ (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‖) - π

pp: case inr.inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im = 0
⊢ (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‖) - π

pp: case inr.inr.inr.inr
x : ℂ
hr : 0 < x.re
hi : 0 < x.im
⊢ (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:
· simp [hr.le, hi.ne]

Goal state after:
case inr.inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im = 0
⊢ (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‖) - π

case inr.inr.inr.inr
x : ℂ
hr : 0 < x.re
hi : 0 < x.im
⊢ (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.Complex.Arg

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

Tactic:
arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le

Goal state after:
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ 0 = π - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
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).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

Tactic:
arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le

Goal state after:
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ 0 = π + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
h : x ∈ slitPlane
⊢ ‖x‖ ≠ 0

Tactic:
norm_ne_zero_iff

Goal state after:
x : ℂ
h : x ∈ slitPlane
⊢ x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) - π = a✝.arg

Tactic:
arg,

Goal state after:
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) - π =
    if 0 ≤ a✝.re then Real.arcsin (a✝.im / ‖a✝‖)
    else if 0 ≤ a✝.im then Real.arcsin ((-a✝).im / ‖a✝‖) + π else Real.arcsin ((-a✝).im / ‖a✝‖) - π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ a✝.arg = Real.arcsin ((-a✝).im / ‖a✝‖) + π

Tactic:
arg,

Goal state after:
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ (if 0 ≤ a✝.re then Real.arcsin (a✝.im / ‖a✝‖)
    else if 0 ≤ a✝.im then Real.arcsin ((-a✝).im / ‖a✝‖) + π else Real.arcsin ((-a✝).im / ‖a✝‖) - π) =
    Real.arcsin ((-a✝).im / ‖a✝‖) + π