mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
x : E
⊢ x ∈ (fun x ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r) ↔ x ∈ ball 0 (b * r) \ closedBall 0 (a * r)

Tactic:
;

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
x : E
⊢ x ∈ (fun x ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r) ↔ x ∈ ball 0 (b * r) \ closedBall 0 (a * r)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ π - 2 * θ = 2 * θ + θ

Tactic:
;

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ π - 2 * θ = 2 * θ + θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inl
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / (2 * 4)
⊢ (2 + 2 * √5) / (2 * 4) = (1 + √5) / 4

Tactic:
;

Goal state after:
case inl
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / (2 * 4)
⊢ (2 + 2 * √5) / (2 * 4) = (1 + √5) / 4
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case h₁
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
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n)‖ ≤ ↑(u n) * ‖1‖

Tactic:
;

Goal state after:
case h₁
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
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n)‖ ≤ ↑(u n) * ‖1‖
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 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : ℝ≥0∞
h : edist x z < r
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < r

Tactic:
cases r with
  | top =>
    exact add_lt_top.2 ⟨lt_top_iff_ne_top.2 <| infEDist_ne_top ⟨z, self_subset_thickening hδ _ hz⟩,
      ofReal_lt_top⟩
  | coe r =>
    have hr : 0 < ↑r - δ := by
      refine sub_pos_of_lt ?_
      have := hs.trans_lt ((infEDist_le_edist_of_mem hz).trans_lt h)
      rw [ofReal_eq_coe_nnreal hδ.le] at this
      exact mod_cast this
    rw [edist_lt_coe, ← dist_lt_coe, ← add_sub_cancel δ ↑r] at h
    obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hr hδ h
    refine (ENNReal.add_lt_add_right ofReal_ne_top <|
      infEDist_lt_iff.2 ⟨_, mem_thickening_iff.2 ⟨_, hz, hyz⟩, edist_lt_ofReal.2 hxy⟩).trans_le ?_
    rw [← ofReal_add hr.le hδ.le, sub_add_cancel, ofReal_coe_nnreal]

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

Goal state before:
pp: ⊢ cos (↑π / 2) = cos ↑(π / 2)

Tactic:
;

Goal state after:
⊢ cos (↑π / 2) = cos ↑(π / 2)
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 < δ
s : Set E
x : E
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (thickening δ s)

Tactic:
mem_cthickening_iff,

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal (ε + δ) → infEDist x (thickening δ s) ≤ ENNReal.ofReal ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (↑π / 2) = sin ↑(π / 2)

Tactic:
;

Goal state after:
⊢ sin (↑π / 2) = sin ↑(π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ ↑0 = 0

Tactic:
;

Goal state after:
⊢ ↑0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ ↑(-1) = -1

Tactic:
;

Goal state after:
⊢ ↑(-1) = -1
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 ≤ δ
s : Set E
x : E
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (cthickening δ s)

Tactic:
mem_cthickening_iff,

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal (ε + δ) → infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case refine_1
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ Real.cos b ≤ Real.cos |z.im|

Tactic:
exact
      Real.cos_le_cos_of_nonneg_of_le_pi (_root_.abs_nonneg _)
        (hb.trans <| half_le_self <| Real.pi_pos.le) hz

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn F y
x✝ : X
⊢ x✝ ∈ pathComponentIn F x ↔ x✝ ∈ pathComponentIn F y

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn F y
x✝ : X
⊢ x✝ ∈ pathComponentIn F x ↔ x✝ ∈ pathComponentIn F y
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
⊢ f ⤳ g

Tactic:
suffices ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → MapsTo f K U by
    simpa [specializes_iff_pure, nhds_compactOpen]

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
h : ⇑f ⤳ ⇑g
⊢ ∀ (K : Set X), IsCompact K → ∀ (U : Set Y), IsOpen[inst✝] U → MapsTo (⇑g) K U → MapsTo (⇑f) K U
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPathConnected (⇑h.symm '' s) ↔ IsPathConnected s

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPathConnected (⇑h.symm '' s) ↔ IsPathConnected s
Module: Mathlib.Topology.Path

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ₂ : Path x y
toContinuousMap✝ : C(↑I, X)
source'✝ : toContinuousMap✝.toFun 0 = x
target'✝ : toContinuousMap✝.toFun 1 = y
h :
  { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ }.toContinuousMap = γ₂.toContinuousMap
⊢ { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ } = γ₂

Tactic:
;

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ₂ : Path x y
toContinuousMap✝ : C(↑I, X)
source'✝ : toContinuousMap✝.toFun 0 = x
target'✝ : toContinuousMap✝.toFun 1 = y
h :
  { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ }.toContinuousMap = γ₂.toContinuousMap
⊢ { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ } = γ₂
Module: Mathlib.Topology.Path

Goal state before:
pp: case mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
toContinuousMap✝¹ : C(↑I, X)
source'✝¹ : toContinuousMap✝¹.toFun 0 = x
target'✝¹ : toContinuousMap✝¹.toFun 1 = y
toContinuousMap✝ : C(↑I, X)
source'✝ : toContinuousMap✝.toFun 0 = x
target'✝ : toContinuousMap✝.toFun 1 = y
h :
  { toContinuousMap := toContinuousMap✝¹, source' := source'✝¹, target' := target'✝¹ }.toContinuousMap =
    { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ }.toContinuousMap
⊢ { toContinuousMap := toContinuousMap✝¹, source' := source'✝¹, target' := target'✝¹ } =
    { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ }

Tactic:
;

Goal state after:
case mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
toContinuousMap✝¹ : C(↑I, X)
source'✝¹ : toContinuousMap✝¹.toFun 0 = x
target'✝¹ : toContinuousMap✝¹.toFun 1 = y
toContinuousMap✝ : C(↑I, X)
source'✝ : toContinuousMap✝.toFun 0 = x
target'✝ : toContinuousMap✝.toFun 1 = y
h :
  { toContinuousMap := toContinuousMap✝¹, source' := source'✝¹, target' := target'✝¹ }.toContinuousMap =
    { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ }.toContinuousMap
⊢ { toContinuousMap := toContinuousMap✝¹, source' := source'✝¹, target' := target'✝¹ } =
    { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ }
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n✝ n : ℕ
| ‖f n * w ^ n‖ ≤ C

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n✝ n : ℕ
| ‖f n * w ^ n‖ ≤ C
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
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
⊢ ContinuousOn (fun x ↦ mkD (t.domRestrict (f x)) g) s

Tactic:
by
  have (x) (hx : x ∈ s) : ContinuousOn (f x) t :=
    f_cont.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨hx, hz⟩
  simp_rw [continuousOn_iff_continuous_domRestrict, s.domRestrict_def]
  refine continuous_of_continuous_uncurry _ ?_
  conv in mkD _ _ => rw [mkD_of_continuousOn (this x x.2)]
  exact f_cont.comp_continuous (.prodMap continuous_subtype_val continuous_subtype_val)
    fun xz ↦ ⟨xz.1.2, xz.2.2⟩

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
x✝ : C(X × Y, Z)
⊢ x✝.curry.uncurry = x✝

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
x✝ : C(X × Y, Z)
⊢ x✝.curry.uncurry = x✝
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
x✝ : C(X × Y, Z)
a✝ : X × Y
⊢ x✝.curry.uncurry a✝ = x✝ a✝

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
x✝ : C(X × Y, Z)
a✝ : X × Y
⊢ x✝.curry.uncurry a✝ = x✝ a✝
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
x✝ : C(X, C(Y, Z))
⊢ x✝.uncurry.curry = x✝

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
x✝ : C(X, C(Y, Z))
⊢ x✝.uncurry.curry = x✝
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
x✝ : C(X, C(Y, Z))
a✝¹ : X
a✝ : Y
⊢ (x✝.uncurry.curry a✝¹) a✝ = (x✝ a✝¹) a✝

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
x✝ : C(X, C(Y, Z))
a✝¹ : X
a✝ : Y
⊢ (x✝.uncurry.curry a✝¹) a✝ = (x✝ a✝¹) a✝
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x' y' : X
⊢ Bijective fun x ↦ x.cast ⋯ ⋯

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x' y' : X
⊢ Bijective fun x ↦ x.cast ⋯ ⋯
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inl
⊢ ‖↑(0 / 2)‖ = |0| / 2

pp: case inr
p : ℝ
hp : p ≠ 0
⊢ ‖↑(p / 2)‖ = |p| / 2

Tactic:
;

Goal state after:
case inl
⊢ ‖↑(0 / 2)‖ = |0| / 2

case inr
p : ℝ
hp : p ≠ 0
⊢ ‖↑(p / 2)‖ = |p| / 2
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p : ℝ
hp : p ≠ 0
⊢ ‖↑(p / 2)‖ = |p| / 2

Tactic:
rw [norm_eq, ← mul_div_assoc, inv_mul_cancel₀ hp, one_div, round_two_inv, Int.cast_one,
    one_mul, (by linarith : p / 2 - p = -(p / 2)), abs_neg, abs_div, abs_two]

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

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n

Tactic:
;

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k : ℕ
hm : Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n + 1

Tactic:
;

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k : ℕ
hm : Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n + 1
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
hm : Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n

Tactic:
;

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
hm : Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n + 1

Tactic:
;

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n + 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ arcsin (-x) = -arcsin x

Tactic:
rcases le_total x (-1) with hx₁ | hx₁
  · rw [arcsin_of_le_neg_one hx₁, neg_neg, arcsin_of_one_le (le_neg.2 hx₁)]
  rcases le_total 1 x with hx₂ | hx₂
  · rw [arcsin_of_one_le hx₂, arcsin_of_le_neg_one (neg_le_neg hx₂)]
  refine arcsin_eq_of_sin_eq ?_ ?_
  · rw [sin_neg, sin_arcsin hx₁ hx₂]
  · exact ⟨neg_le_neg (arcsin_le_pi_div_two _), neg_le.2 (neg_pi_div_two_le_arcsin _)⟩

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

Goal state before:
pp: x : ℂ
⊢ Real.sin
      (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‖) - π) =
    x.im / ‖x‖

Tactic:
;

Goal state after:
x : ℂ
⊢ Real.sin
      (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‖) - π) =
    x.im / ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

pp: case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
;

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
;

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

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

Tactic:
;

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)

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

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

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

Tactic:
;

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)

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

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

Tactic:
;

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ π / 2 - arcsin x

Tactic:
;

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

Goal state before:
pp: x y : ℝ
hx : -1 ≤ x
hlt : x < y
hy : y ≤ 1
⊢ π / 2 - arcsin y < π / 2 - arcsin x

Tactic:
;

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

Goal state before:
pp: x y : ℝ
hlt : x ≤ y
⊢ π / 2 - arcsin y ≤ π / 2 - arcsin x

Tactic:
;

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

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

pp: case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
;

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
;

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
⊢ 0 ≤ arg 0 ↔ 0 ≤ im 0

pp: case inr
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im

Tactic:
;

Goal state after:
case inl
⊢ 0 ≤ arg 0 ↔ 0 ≤ im 0

case inr
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im
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:
;

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

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: case pos
x : ℝ
hx : x = 0
⊢ log x⁻¹ = -log x

pp: case neg
x : ℝ
hx : ¬x = 0
⊢ log x⁻¹ = -log x

Tactic:
;

Goal state after:
case pos
x : ℝ
hx : x = 0
⊢ log x⁻¹ = -log x

case neg
x : ℝ
hx : ¬x = 0
⊢ log x⁻¹ = -log x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

pp: case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Tactic:
;

Goal state after:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

pp: case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

Tactic:
;

Goal state after:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: n : ℤ
hn : 0 < -n
⊢ 1 ≤ -↑n

Tactic:
;

Goal state after:
n : ℤ
hn : 0 < -n
⊢ 1 ≤ -↑n
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
;

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ log x⁻¹ ≤ x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ (1 + x) * (x + 2 - x) = x + 2 + x

Tactic:
;

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ (1 + x) * (x + 2 - x) = x + 2 + x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ x < x + 2

Tactic:
;

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ x < x + 2
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ (1 + x) * (x + 2 - x) = x + 2 + x

Tactic:
;

Goal state after:
x : ℝ
hx : 0 < x
⊢ (1 + x) * (x + 2 - x) = x + 2 + x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ x < x + 2

Tactic:
;

Goal state after:
x : ℝ
hx : 0 < x
⊢ x < x + 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

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

Tactic:
;

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

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (rexp ∘ fun x ↦ log (x + y) - log x) atTop (𝓝 (1 + 0))

Tactic:
refine this.congr' ?_

Goal state after:
y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
⊢ (fun x ↦ 1 + y / x) =ᶠ[atTop] rexp ∘ fun x ↦ log (x + y) - log x