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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: ⊢ ↑0 = 0

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case e'_5
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
n : ℕ
this :
  ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) =
    ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n
⊢ ↑((n + (k + 1)).choose (k + 1)) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), ↑((k_1 + k).choose k) * r ^ k_1 * r ^ (n - k_1)

Tactic:
simp [this, ← sum_mul, ← Nat.cast_sum, sum_range_add_choose n k, add_assoc]

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

Goal state before:
pp: 𝕜 : Type u_5
inst✝ : NormedDivisionRing 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ 1 / (1 - r) ^ (k + 1) = (1 - r)⁻¹ʳ ^ (k + 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
n : ℕ
⊢ ↑n + 1 = ↑((n + 1).choose 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.CompactOpen

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

Tactic:
hf

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

Tactic:
hf

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
K : Set X
i : ι
hi : {f | MapsTo ⇑f (K, i).1 (U (K, i).2)} ⊆ s
hK : IsCompact (K, i).1
hpi : p (K, i).2
f : C(X, Y)
hf : MapsTo (⇑f) K (interior (U i))
⊢ f ∈ s
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ ⟨h.somePath 0, ⋯⟩ = ⟨x, ⋯⟩

Tactic:
simp

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 : JoinedIn F x y
⊢ ⟨h.somePath 1, ⋯⟩ = ⟨y, ⋯⟩

Tactic:
simp

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
x_in : x ∈ F
y_in : y ∈ F
h : Joined ⟨x, x_in⟩ ⟨y, y_in⟩
⊢ ∀ (t : ↑I), (h.somePath.map ⋯) t ∈ F

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
⊢ JoinedIn F x z

Tactic:
by
  obtain ⟨hx, hy⟩ := hxy.mem
  obtain ⟨hx, hy⟩ := hyz.mem
  simp_all only [joinedIn_iff_joined]
  exact hxy.trans hyz

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 ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ?m.32 }.toFun 0 = x

Tactic:
simp

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 ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ?m.32 }.toFun 1 = y

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : y ∈ pathComponent x
⊢ (Joined.somePath h) 0 = x

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : y ∈ pathComponent x
⊢ (Joined.somePath h) 1 = y

Tactic:
simp

Goal state after:
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
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x✝¹ : G
x✝ : x✝¹ ∈ Subgroup.pathComponentOne G
g : G
γ : Path 1 x✝¹
⊢ { toFun := fun x ↦ g * γ x * g⁻¹, continuous_toFun := ⋯ }.toFun 0 = 1

Tactic:
simp

Goal state after:
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
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x✝¹ : G
x✝ : x✝¹ ∈ Subgroup.pathComponentOne G
g : G
γ : Path 1 x✝¹
⊢ { toFun := fun x ↦ g * γ x * g⁻¹, continuous_toFun := ⋯ }.toFun 1 = g * x✝¹ * g⁻¹

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
⊢ Continuous fun x ↦ x.2.comp x.1

Tactic:
simp_rw [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_compactOpen]
  intro ⟨f, g⟩ K hK U hU (hKU : MapsTo (g ∘ f) K U)
  obtain ⟨L, hKL, hLc, hLU⟩ : ∃ L ∈ 𝓝ˢ (f '' K), IsCompact L ∧ MapsTo g L U :=
    exists_mem_nhdsSet_isCompact_mapsTo g.continuous (hK.image f.continuous) hU
      (mapsTo_image_iff.2 hKU)
  rw [← subset_interior_iff_mem_nhdsSet, ← mapsTo_iff_image_subset] at hKL
  exact ((eventually_mapsTo hK isOpen_interior hKL).prod_nhds
    (eventually_mapsTo hLc hU hLU)).mono fun ⟨f', g'⟩ ⟨hf', hg'⟩ ↦
      hg'.comp <| hf'.mono_right interior_subset

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K✝ : Set X
U✝ : Set Y
inst✝ : RegularSpace Y
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝³] U
⊢ MapsTo (⇑f) K U → ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a)) K U

Tactic:
hf

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K✝ : Set X
U✝ : Set Y
inst✝ : RegularSpace Y
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝³] U
hf : MapsTo (⇑f) K U
⊢ ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a)) K U
Module: Mathlib.Topology.Path

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
γ✝ γ : Path x y
⊢ (⇑γ ∘ σ) 0 = y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ γ : Path x y
⊢ (⇑γ ∘ σ) 1 = x

Tactic:
simp

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

Goal state before:
pp: case snoc.elim0
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
x : X
hp : ∀ (i : Fin 0), i.elim0 ∈ s
hx : x ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin 0), i.elim0 ∈ range ⇑γ

Tactic:
use Path.refl x

Goal state after:
case h
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
x : X
hp : ∀ (i : Fin 0), i.elim0 ∈ s
hx : x ∈ s
⊢ range ⇑(Path.refl x) ⊆ s ∧ ∀ (i : Fin 0), i.elim0 ∈ range ⇑(Path.refl x)
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.extend 0 = x

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.extend 1 = y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ γ : Path x y
γ' : Path y z
⊢ ∀ (x_1 : ℝ), id x_1 = 1 / 2 → γ.extend (2 * x_1) = γ'.extend (2 * x_1 - 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ γ : Path x y
γ' : Path y z
⊢ ((fun t ↦ if t ≤ 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) ∘ Subtype.val) 0 = x

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
rcases h.exists_path_through_family p hp with ⟨γ, hγ⟩
  rcases hγ with ⟨h₁, h₂⟩
  simp only [range, mem_ofPred_eq] at h₂
  rw [range_subset_iff] at h₁
  choose! t ht using h₂
  exact ⟨γ, t, h₁, ht⟩

Goal state after:
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
x y : ℝ
⊢ { toFun := fun t ↦ (1 - ↑t) * x + ↑t * y, continuous_toFun := ⋯ }.toFun 0 = x

Tactic:
simp

Goal state after:
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
x y : ℝ
⊢ { toFun := fun t ↦ (1 - ↑t) * x + ↑t * y, continuous_toFun := ⋯ }.toFun 1 = y

Tactic:
simp

Goal state after:
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 X
t : Set Y
x₁ x₂ : X
y₁ y₂ : Y
hx : JoinedIn s x₁ x₂
hy : JoinedIn t y₁ y₂
⊢ ∀ (t_1 : ↑I), (hx.somePath.prod hy.somePath) t_1 ∈ s ×ˢ t

Tactic:
simp

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

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
s : (i : ι) → Set (Z i)
x y : (i : ι) → Z i
h : ∀ (i : ι), JoinedIn (s i) (x i) (y i)
⊢ ∀ (t : ↑I), (Path.pi fun i ↦ ⋯.somePath) t ∈ univ.pi s

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ γ : Path x y
f : X → Y
h : ContinuousOn f (range ⇑γ)
⊢ (f ∘ ⇑γ) 0 = f x

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ γ : Path x y
f : X → Y
h : ContinuousOn f (range ⇑γ)
⊢ (f ∘ ⇑γ) 1 = f y

Tactic:
simp

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

Goal state before:
pp: case inl
p x : ℝ
⊢ ‖↑(0 * x)‖ = |0| * ‖↑x‖

Tactic:
simp

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

Goal state before:
pp: p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑(-1 * x)‖

Tactic:
simp

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

Goal state before:
pp: case inl
x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
⊢ ‖↑x‖ = |x - ↑(round (0⁻¹ * x)) * 0|

Tactic:
simp

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

Goal state before:
pp: x r : ℝ
hr : ∀ (m : ℝ), ↑m = ↑x → r ≤ ‖m‖
⊢ ↑(fract x - 1) = ↑x

Tactic:
simp

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

Goal state before:
pp: p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = |p * (p⁻¹ * x) - p * ↑(round (p⁻¹ * x))|

Tactic:
mul_inv_cancel_left₀ hp.ne.symm,

Goal state after:
p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = |x - p * ↑(round (p⁻¹ * x))|
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
hfa' : Monotone fun n ↦ -f n
⊢ 0 = -0

Tactic:
simp

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
hfa' : Monotone fun n ↦ -f n
hf0' : Tendsto (fun n ↦ -f n) atTop (𝓝 0)
x✝ : ℕ
⊢ ∑ i ∈ Finset.range x✝, f i • z i = (-fun n ↦ ∑ i ∈ Finset.range n, -f i • z i) x✝

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

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
γ : Path x y
a₁ a₂ a₃ : X
b₁ b₂ b₃ : Y
γ₁ : Path a₁ a₂
γ₂ : Path b₁ b₂
⊢ (γ₁.prodMk γ₂.toContinuousMap).toFun 0 = (a₁, b₁)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

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
γ : Path x y
a₁ a₂ a₃ : X
b₁ b₂ b₃ : Y
γ₁ : Path a₁ a₂
γ₂ : Path b₁ b₂
⊢ (γ₁.prodMk γ₂.toContinuousMap).toFun 1 = (a₂, b₂)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ : Path x y
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ : (i : ι) → Path (as i) (bs i)
⊢ (ContinuousMap.pi fun i ↦ (γ i).toContinuousMap).toFun 0 = as

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ : Path x y
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ : (i : ι) → Path (as i) (bs i)
⊢ (ContinuousMap.pi fun i ↦ (γ i).toContinuousMap).toFun 1 = bs

Tactic:
simp

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 n : ℕ
⊢ (-1) ^ (2 * n) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ : Path x y
a b : X
γ : Path a b
⊢ γ.extend (min 0 1) = a

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ : Path x y
a b : X
γ : Path a b
⊢ γ.extend 1 = b

Tactic:
simp

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

Goal state before:
pp: case inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
⊢ Icc (x + 0 • p - ε) (x + 0 • p + ε) ∩ s = if 0 = 0 then Icc (x - ε) (x + ε) ∩ s else ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ range (⇑γ ∘ f) = range ⇑γ

Tactic:
have : range f = univ := by
    rw [range_eq_univ]
    intro t
    have h₁ : Continuous (Set.IccExtend (zero_le_one' ℝ) f) := by fun_prop
    have := intermediate_value_Icc (zero_le_one' ℝ) h₁.continuousOn
    · rw [IccExtend_left, IccExtend_right, Icc.mk_zero, Icc.mk_one, hf₀, hf₁] at this
      rcases this t.2 with ⟨w, hw₁, hw₂⟩
      rw [IccExtend_of_mem _ _ hw₁] at hw₂
      exact ⟨_, hw₂⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
this : range f = univ
⊢ range (⇑γ ∘ f) = range ⇑γ
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x✝ : ↑I
⊢ ((refl x).reparam f hfcont hf₀ hf₁) x✝ = (refl x) x✝

Tactic:
simp

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)
hfa : Antitone f
k n : ℕ
⊢ (-1) ^ (2 * n) = 1

Tactic:
simp

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

Goal state before:
pp: ⊢ range arcsin = Icc (-(π / 2)) (π / 2)

Tactic:
arcsin,

Goal state after:
⊢ range (Subtype.val ∘ IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) = Icc (-(π / 2)) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x✝ : ℝ
⊢ x✝ ∈ Subtype.val '' range (IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) ↔ x✝ ∈ Icc (-(π / 2)) (π / 2)

Tactic:
simp

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

Goal state before:
pp: x : ℝ
⊢ arcsin ↑(projIcc (-1) 1 ⋯ x) = arcsin x

Tactic:
arcsin,

Goal state after:
x : ℝ
⊢ (Subtype.val ∘ IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) ↑(projIcc (-1) 1 ⋯ x) =
    (Subtype.val ∘ IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) x
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)

Tactic:
have : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1 := sin_sq_add_cos_sq (arcsin x)

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1
⊢ cos (arcsin x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
⊢ ↑‖0‖ * cexp (↑(arg 0) * I) = 0

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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) / 0 = x / 0

Tactic:
simp

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

Goal state before:
pp: x : ℝ
⊢ 1 ≤ ↑⌊‖x‖⌋₊ + 1

Tactic:
simp

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

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ 0 ≤ 2

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
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
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ dist (g x) 0 = ‖g x‖

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ (↑0 + ↑y * I).arg = (↑(-y) * -I).arg

Tactic:
simp

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

Goal state before:
pp: case zero
x : ℝ
⊢ log (x ^ 0) = ↑0 * log x

Tactic:
simp

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

Goal state before:
pp: case succ.inl
n : ℕ
ih : log (0 ^ n) = ↑n * log 0
⊢ log (0 ^ (n + 1)) = ↑(n + 1) * log 0

Tactic:
simp

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

Goal state before:
pp: case inl
hx : 0 ≤ 0
⊢ log 0 ≤ 0

Tactic:
simp

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

Goal state before:
pp: case nil
h : ∀ x ∈ [], x ≠ 0
⊢ log [].prod = (List.map (fun x ↦ log x) []).sum

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ (List.map (fun x ↦ log x) (List.map (fun i ↦ f i) s.toList)).sum = ∑ i ∈ s, log (f i)

Tactic:
simp

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

Goal state before:
pp: case e'_1.e'_3
θ : Angle
⊢ 0 = 2 • 0

Tactic:
simp

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

Goal state before:
pp: case e'_2.e'_2
θ : Angle
⊢ ↑π = 0 + ↑π

Tactic:
simp

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

Goal state before:
pp: case inl
⊢ log ↑0 = (Nat.factorization 0).sum fun p t ↦ ↑t * log ↑p

Tactic:
simp

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

Goal state before:
pp: k N : ℕ
hN : N ≠ 0
n : ℤ
⊢ 2 * ↑π * I ≠ 0

Tactic:
simp

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

Goal state before:
pp: c : ℝ
⊢ Tendsto (fun x ↦ c) atTop (𝓝 c)

Tactic:
simp

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

Goal state before:
pp: x y x✝¹ : ℝ
x✝ : x✝¹ ∈ univ
⊢ log (rexp x✝¹) = x✝¹

Tactic:
simp

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

Goal state before:
pp: case inl.inl
y : ℂ
⊢ 0 ^ (↑0 * y) = (0 ^ y) ^ 0

Tactic:
simp

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

Goal state before:
pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg

Tactic:
arg_of_re_neg_of_im_nonneg hre him

Goal state after:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ Real.arcsin ((-z).im / ‖z‖) + π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
simp

Goal state after: