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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact ((fun a ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB ((fun a ↦ ‖a‖) '' f '' s) (sInf ((fun a ↦ ‖a‖) '' f '' s))
⊢ 0 < sInf (Norm.norm '' f '' s)

Tactic:
obtain ⟨_, ⟨x, hx, hCx⟩, hnormCx⟩ := hs.sInf_mem h_sInf.nonempty

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x✝ : α
hx✝ : x✝ ∈ s
hs : IsCompact ((fun a ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB ((fun a ↦ ‖a‖) '' f '' s) (sInf ((fun a ↦ ‖a‖) '' f '' s))
w✝ : E
hnormCx : (fun a ↦ ‖a‖) w✝ = sInf ((fun a ↦ ‖a‖) '' f '' s)
x : α
hx : x ∈ s
hCx : f x = w✝
⊢ 0 < sInf (Norm.norm '' f '' s)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: x z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖cexp (x + z) - cexp x - z * cexp x‖ = ‖cexp x * (cexp z - 1 - z)‖

Tactic:
congr
      rw [exp_add]
      ring

Goal state after:
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
⊢ k + n.succ ≥ n.succ

Tactic:
← zero_add n.succ

Goal state after:
α : 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
⊢ k + (0 + n.succ) ≥ 0 + n.succ
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
⊢ n.succ ≤ 0 + n.succ

Tactic:
by simp

Goal state after:
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
⊢ n.succ ≤ k + n.succ

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case inr.succ
α : 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
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
| succ k ih =>

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

Goal state before:
pp: ⊢ 1 ≤ 2

Tactic:
by simp

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

Goal state before:
pp: ⊢ 0 < 2

Tactic:
by simp

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

Goal state before:
pp: ⊢ comap rexp (𝓝[Set.range rexp] 0) = atBot

Tactic:
by simp

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 ε : ℝ
⊢ 1 ∈ {m | ↑m = 1}

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ m ∈ {m_1 | ↑m_1 = ↑m}

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ {x | infEDist x s < ENNReal.ofReal δ}⁻¹ = {x | infEDist x s⁻¹ < ENNReal.ofReal δ}

Tactic:
← infEDist_inv

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ {x | infEDist x s < ENNReal.ofReal δ}⁻¹ = {x | infEDist x⁻¹ s < ENNReal.ofReal δ}
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ {x | infEDist x s ≤ ENNReal.ofReal δ}⁻¹ = {x | infEDist x s⁻¹ ≤ ENNReal.ofReal δ}

Tactic:
← infEDist_inv

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ {x | infEDist x s ≤ ENNReal.ofReal δ}⁻¹ = {x | infEDist x⁻¹ s ≤ ENNReal.ofReal δ}
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} * ball 1 δ = ball x δ

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball 1 δ * {x} = ball x δ

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} * closedBall 1 δ = closedBall x δ

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ closedBall 1 δ * {x} = closedBall x δ

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ closedBall 1 δ / {x} = closedBall x⁻¹ δ

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ x • closedBall 1 δ = closedBall x δ

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} * sphere 1 δ = sphere x δ

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ sphere 1 δ * {x} = sphere x δ

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ sphere 1 δ / {x} = sphere x⁻¹ δ

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ x • sphere 1 δ = sphere x δ

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ (fun m_1 ↦ ‖m + m_1‖) 0 = ‖m‖

Tactic:
by simp

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

Goal state before:
pp: ⊢ -1 < 1

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
⊢ x.sqrtTwoAddSeries 0 = x

Tactic:
by simp

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

Goal state before:
pp: ⊢ sqrtTwoAddSeries 0 1 = √2

Tactic:
by simp

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

Goal state before:
pp: ⊢ sqrtTwoAddSeries 0 2 = √(2 + √2)

Tactic:
by simp

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

Goal state before:
pp: ⊢ sqrtTwoAddSeries 0 0 < 2

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R M
S T : Submodule R M
⊢ map S.mkQ T = map S.mkQ (S ⊔ T)

Tactic:
by simp

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

Goal state before:
pp: ⊢ cos (π / 2 ^ (0 + 1)) = sqrtTwoAddSeries 0 0 / 2

Tactic:
by simp

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
h_add : Tendsto (fun x ↦ 1 + v a ^ x) atTop (𝓝 (1 + 0))
h_sub : Tendsto (fun x ↦ 1 - v a ^ x) atTop (𝓝 (1 - 0))
n : ℕ
⊢ 1 - v a ^ n ≤ v 1 - v (a ^ n)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
h_add : Tendsto (fun x ↦ 1 + v a ^ x) atTop (𝓝 (1 + 0))
h_sub : Tendsto (fun x ↦ 1 - v a ^ x) atTop (𝓝 (1 - 0))
n : ℕ
⊢ v 1 + v (a ^ n) ≤ 1 + v a ^ n

Tactic:
by simp

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

Goal state before:
pp: ⊢ sin (π / 3) ^ 2 = 3 / 4

Tactic:
by
  rw [← cos_pi_div_two_sub, ← sq_cos_pi_div_six]
  congr
  ring

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

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

Tactic:
sin_pi_sub

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

Goal state before:
pp: c : ℝ := cos (π / 5)
⊢ 4 * c ^ 2 + -2 * c + -1 = 0

Tactic:
neg_mul,

Goal state after:
c : ℝ := cos (π / 5)
⊢ 4 * c ^ 2 + -(2 * c) + -1 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
by simp

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

Goal state before:
pp: ⊢ -1 < 0

Tactic:
by simp

Goal state after:
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 ∈ thickening (ε + δ) s → x ∈ thickening ε (thickening δ s)

Tactic:
simp_rw [mem_thickening_iff]
    rintro ⟨z, hz, hxz⟩
    rw [add_comm] at hxz
    obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hε hδ hxz
    exact ⟨y, ⟨_, hz, hyz⟩, hxy⟩

Goal state after:
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
⊢ infEDist x s ≤ ENNReal.ofReal (ε + δ) → infEDist x (thickening δ s) ≤ ENNReal.ofReal ε

Tactic:
ENNReal.ofReal_add hε hδ.le,

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 ε + ENNReal.ofReal δ → infEDist x (thickening δ s) ≤ ENNReal.ofReal ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: ⊢ -1 * I = -I

Tactic:
neg_mul,

Goal state after:
⊢ -(1 * I) = -I
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case succ
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))
⊢ HasSum (fun n ↦ ↑((n + (k + 1)).choose (k + 1)) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1 + 1))

Tactic:
| succ k ih =>

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

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

Tactic:
exact h _ H

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 0, ⋯⟩ = ⟨x, ⋯⟩

Tactic:
by 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:
by 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:
by 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 0 = x

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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
⊢ (⇑γ ∘ σ) 0 = y

Tactic:
by 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:
by 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 0 = x

Tactic:
by 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:
by 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:
by 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:
by 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 0 = x

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

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 : Y × X → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (p.1, f p.2)
this : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (p.swap.1, f p.swap.2)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] g

Tactic:
have : Continuous fun p : X₀ × Y => (g ∘ Prod.swap) (f p.1, p.2) := this

Goal state after:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (p.1, f p.2)
this✝ : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (p.swap.1, f p.swap.2)
this : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ (g ∘ Prod.swap) (f p.1, p.2)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] g
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ (γ₁ t).trans (γ₂ t)

Tactic:
have h₂' := Path.continuous_uncurry_extend_of_continuous_family γ₂ h₂

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ (γ₁ t).trans (γ₂ t)
Module: Mathlib.Topology.Instances.Sign

Goal state before:
pp: α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
⊢ ContinuousAt (⇑SignType.sign) a

Tactic:
rcases h.lt_or_gt with (h_neg | h_pos)

Goal state after:
case inl
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_neg : a < 0
⊢ ContinuousAt (⇑SignType.sign) a

case inr
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_pos : 0 < a
⊢ ContinuousAt (⇑SignType.sign) a
Module: Mathlib.Analysis.Normed.Group.AddCircle

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

Tactic:
by 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:
by 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:
by 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:
by 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:
by simp

Goal state after: