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

Goal state before:
pp: x : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
⊢ cosh x * (cosh x ^ 2 + (cosh x ^ 2 - 1)) + 2 * cosh x * (cosh x ^ 2 - 1) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
ring

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

Goal state before:
pp: x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2

Tactic:
ring

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

Goal state before:
pp: x : ℂ
h1 : x + 2 * x = 3 * x
h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2
⊢ sinh x * (sinh x ^ 2 + 1 + sinh x ^ 2) + 2 * sinh x * (sinh x ^ 2 + 1) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
ring

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

Goal state before:
pp: x y : ℂ
s1 : sin x = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)
s2 : sin y = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)
⊢ sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2) -
      (sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * sin ((x - y) / 2) * cos ((x + y) / 2)

Tactic:
ring

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

Goal state before:
pp: x y : ℂ
s1 : cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : cos y = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) -
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    -2 * sin ((x + y) / 2) * sin ((x - y) / 2)

Tactic:
ring

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

Goal state before:
pp: case calc_3
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Tactic:
ring

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

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

Tactic:
rw [← ofReal_tan_ofReal_re, ofReal_im]

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

Goal state before:
pp: x : ℂ
h : cos x ≠ 0
⊢ (1 + tan x ^ 2) * cos x ^ 2 = (tan x * cos x) ^ 2 + cos x ^ 2

Tactic:
ring

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x‖ ^ 1 * (↑(Nat.succ 1) * (↑(Nat.factorial 1) * ↑1)⁻¹) = 2 * ‖x‖

Tactic:
simp [mul_two, mul_add, mul_comm, Nat.factorial]

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

Goal state before:
pp: x : ℂ
⊢ 2 * (sin x * (1 - sin x ^ 2)) + (2 * (1 - sin x ^ 2) - 1) * sin x = (2 + 1) * sin x - 4 * sin x ^ 3

Tactic:
ring

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

Goal state before:
pp: x y : ℝ
⊢ 2 * sin x * sin y = sin x * sin y + sin x * sin y

Tactic:
ring

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

Goal state before:
pp: x y : ℝ
⊢ 2 * cos x * cos y = cos x * cos y + cos x * cos y

Tactic:
ring

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

Goal state before:
pp: x y : ℝ
⊢ 2 * sin x * cos y = sin x * cos y + sin x * cos y

Tactic:
ring

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

Goal state before:
pp: case inl
x : ℝ
h✝ : x ≤ 0
⊢ cosh |x| = cosh x

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos]

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

Goal state before:
pp: case inr
x : ℝ
h✝ : 0 ≤ x
⊢ cosh |x| = cosh x

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos]

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖(cexp (-(↑x / 2) * I) - cexp (↑x / 2 * I)) * I‖

Tactic:
nth_rw 2 [← one_mul (_ - _), ← exp_zero]

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp 0 * (cexp (-(↑x / 2) * I) - cexp (↑x / 2 * I)) * I‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ =
    ‖cexp (-(↑x / 2 * I)) * (cexp (↑x / 2 * I) * cexp (-(↑x / 2) * I) - cexp (↑x / 2 * I) * cexp (↑x / 2 * I)) * I‖

Tactic:
← exp_add,

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ =
    ‖cexp (-(↑x / 2 * I)) * (cexp (↑x / 2 * I + -(↑x / 2) * I) - cexp (↑x / 2 * I) * cexp (↑x / 2 * I)) * I‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ =
    ‖cexp (-(↑x / 2 * I)) * (cexp (↑x / 2 * I + -(↑x / 2) * I) - cexp (↑x / 2 * I) * cexp (↑x / 2 * I)) * I‖

Tactic:
← exp_add,

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ =
    ‖cexp (-(↑x / 2 * I)) * (cexp (↑x / 2 * I + -(↑x / 2) * I) - cexp (↑x / 2 * I + ↑x / 2 * I)) * I‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < 1
⊢ x ^ 3 = 1 - (1 + x + x ^ 2) * (1 - x)

Tactic:
ring

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

Goal state before:
pp: x : ℝ
⊢ x + 1 ≤ rexp x

Tactic:
obtain rfl | hx := eq_or_ne x 0
  · simp
  · exact (add_one_lt_exp hx).le

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - l • ε + ε

Tactic:
← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0),

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - l.pred.succ • ε + ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

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

Tactic:
ring

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

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

Tactic:
ring

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

Goal state before:
pp: x : ℝ
⊢ rexp x = rexp (x / 2) * rexp (x / 2)

pp: case hx
x : ℝ
⊢ 0 ≤ rexp x

pp: case hy
x : ℝ
⊢ 0 ≤ rexp (x / 2)

Tactic:
← exp_add,

Goal state after:
x : ℝ
⊢ rexp x = rexp (x / 2 + x / 2)

case hx
x : ℝ
⊢ 0 ≤ rexp x

case hy
x : ℝ
⊢ 0 ≤ rexp (x / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
exact absurd h (by norm_num)

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ 1 ≤ ‖S.normedMk‖

Tactic:
refine (le_mul_iff_one_le_left hx).1 ?_

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ ‖↑x‖ ≤ ‖S.normedMk‖ * ‖↑x‖
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
c : 𝕜
hc : c ∈ s
⊢ sphere (c • 0) (‖c‖ * r) = sphere 0 (‖c‖ * r)

Tactic:
smul_zero

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
c : 𝕜
hc : c ∈ s
⊢ sphere 0 (‖c‖ * r) = sphere 0 (‖c‖ * r)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 3 * (π / 3) = π

Tactic:
ring

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

Goal state before:
pp: ⊢ π / 2 - π / 6 = π / 3

Tactic:
ring

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

Goal state before:
pp: case e_a
⊢ π / 2 - π / 3 = π / 6

Tactic:
ring

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

Goal state before:
pp: ⊢ π / 2 - π / 3 = π / 6

Tactic:
ring

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ ε

Tactic:
obtain rfl | hε' := hε.eq_or_lt

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ 0
h : dist x z ≤ 0 + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ 0

case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 1 / 2 / (√3 / 2) = 1 / √3

Tactic:
ring

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

Goal state before:
pp: ⊢ √3 / 2 / (1 / 2) = √3

Tactic:
ring

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
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
this : ‖↑(u n)‖ * ‖r ^ n‖ ≤ ↑(u n) * ‖1‖ * ‖r‖ ^ n
⊢ ↑(u n) * ‖1‖ * ‖r‖ ^ n = ‖1‖ * (↑(u n) * ‖r‖ ^ n)

Tactic:
ring

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

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
rw [cthickening_of_nonpos hδ, infEDist_closure, ofReal_of_nonpos hδ, tsub_zero]

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 < δ
a b : E
⊢ Metric.closedBall a ε + Metric.ball (-b) δ = Metric.ball (a + -b) (ε + δ)

Tactic:
closedBall_add_ball hε hδ

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

Goal state before:
pp: case e'_5
⊢ 2 * ↑π * I = 2 * (↑π * I)

Tactic:
ring

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

Goal state before:
pp: ⊢ Function.Antiperiodic cosh (↑π * I)

Tactic:
simp [Complex.cosh_add, cosh_mul_I, sinh_mul_I]

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, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s

Tactic:
rcases h.mem_iff.mp this with ⟨i, hpi, hi⟩

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
⊢ ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s
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✝ : LocallyCompactPair X Y
f : C(X, Y)
x : X
U : Set Y
hx : f x ∈ U
hU : IsOpen[inst✝³] U
K : Set X
hxK : K ∈ 𝓝 x
hK : IsCompact K
hKU : MapsTo (⇑f) K U
⊢ ∀ᶠ (x : C(X, Y) × X) in 𝓝 (f, x), x.1 x.2 ∈ U

Tactic:
filter_upwards [prod_mem_nhds (eventually_mapsTo hK hU hKU) hxK] using fun _ h ↦ h.1 h.2

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

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

Tactic:
obtain ⟨hp, hx⟩ := hp

Goal state after:
case snoc
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin n → X
x : X
hp : ∀ (i : Fin n), p i ∈ s
hx : x ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin n), p i ∈ range ⇑γ
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a✝ : ℕ
hn : 1 ≤ ‖f (a✝ + 1)‖ / ‖f a✝‖
hc : ‖f a✝‖ = 0
⊢ False

Tactic:
rw [hc, _root_.div_zero] at hn

Goal state after:
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a✝ : ℕ
hn : 1 ≤ 0
hc : ‖f a✝‖ = 0
⊢ False
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ 2 * (1 - ↑t) - 1 = 1 - 2 * ↑t

Tactic:
ring

Goal state after:
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
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
⊢ ContinuousOn (fun x ↦ mkD (f x) g) s

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

Goal state after:
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
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦
    { toFun := (fun t ↦ if t ≤ 1 / 2 then (γ₁ p.1).extend (2 * t) else (γ₂ p.1).extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      p.2

Tactic:
refine Continuous.if_le ?_ ?_ (continuous_subtype_val.comp continuous_snd) continuous_const ?_

Goal state after:
case refine_1
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 p ↦ (γ₁ p.1).extend (2 * ↑p.2)

case refine_2
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 p ↦ (γ₂ p.1).extend (2 * ↑p.2 - 1)

case refine_3
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
⊢ ∀ (x : ι × ↑I), ↑x.2 = 1 / 2 → (γ₁ x.1).extend (2 * ↑x.2) = (γ₂ x.1).extend (2 * ↑x.2 - 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)
hfm : Monotone f
k n : ℕ
⊢ 2 * (n + 1) = 2 * n + 1 + 1

Tactic:
ring

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

Goal state before:
pp: p x : ℝ
hp : p ≠ 0
hx : |x| ≤ |p| / 2
⊢ ‖↑x‖ = |x|

Tactic:
suffices ∀ p : ℝ, 0 < p → |x| ≤ p / 2 → ‖(x : AddCircle p)‖ = |x| by
    rcases hp.symm.lt_or_gt with (hp | hp)
    · rw [abs_eq_self.mpr hp.le] at hx
      exact this p hp hx
    · rw [← norm_neg_period]
      rw [abs_eq_neg_self.mpr hp.le] at hx
      exact this (-p) (neg_pos.mpr hp) hx

Goal state after:
p x : ℝ
hp : p ≠ 0
hx : |x| ≤ |p| / 2
⊢ ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
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 : ℕ
⊢ 2 * (n + 1) = 2 * n + 1 + 1

Tactic:
ring

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

Goal state before:
pp: z : ℂ
⊢ (cexp z).arg = (cexp ↑z.re * cexp (↑z.im * I)).arg

Tactic:
← exp_add,

Goal state after:
z : ℂ
⊢ (cexp z).arg = (cexp (↑z.re + ↑z.im * I)).arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case e'_4.e'_4
z : ℂ
⊢ π = -π + 2 * π

Tactic:
ring

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

Goal state before:
pp: x : ℝ
hx0 : ¬x < 0
this : 1 + 1 ≤ rexp 1
⊢ 2 ≤ rexp 1

Tactic:
one_add_one_eq_two

Goal state after:
x : ℝ
hx0 : ¬x < 0
this : 2 ≤ rexp 1
⊢ 2 ≤ rexp 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ (x + ↑n * (2 * ↑π * I)).im ∈ Ioc (-π) π

Tactic:
simpa [two_mul, mul_add] using hn

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

Goal state before:
pp: case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ = ↑(π / 2) - ↑ψ
⊢ ↑θ = ↑ψ

Tactic:
exact sub_right_inj.1 h

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

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
h₂' : ↑n / ↑d < 1
⊢ Real.log (↑n / ↑d) ≠ 0

Tactic:
exact ne_of_lt <| Real.log_neg h₁' h₂'

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

Goal state before:
pp: x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ (x ^ n) ^ (↑n)⁻¹ = x

Tactic:
← cpow_nat_mul',

Goal state after:
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ x ^ (↑n * (↑n)⁻¹) = x

case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -π < ↑n * x.arg

case hle
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ ↑n * x.arg ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case e'_4.e'_4
θ : ℝ
⊢ π = -π + 2 * π

Tactic:
ring

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

Goal state before:
pp: case e'_4
x✝ : ℝ
⊢ π = -π + 2 * π

Tactic:
ring

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

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑‖x‖ * (↑‖y‖ * cexp (↑y.arg * I) * cexp (↑x.arg * I))

Tactic:
norm_mul_exp_arg_mul_I,

Goal state after:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑‖x‖ * (y * cexp (↑x.arg * I))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
θ : Angle
h : θ = 0 ∨ θ = ↑π
⊢ -↑|θ.toReal| = θ

Tactic:
rcases h with (rfl | rfl) <;> simp [abs_of_pos Real.pi_pos]

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
⊢ (↑(log x) + ↑π * Complex.I) * ↑y = ↑(log x) * ↑y + ↑y * ↑π * Complex.I

Tactic:
ring

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ rexp (log x * y) * cos (y * π) + ((↑(rexp (log x * y) * sin (y * π))).re * 0 - 0 * Complex.I.im) =
    rexp (log x * y) * cos (y * π)

Tactic:
ring

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

Goal state before:
pp: x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0

Tactic:
ring

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

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp (log ↑x * y) = cexp (log (-↑x) * y) * cexp (↑π * I * y)

Tactic:
← exp_add,

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp (log ↑x * y) = cexp (log (-↑x) * y + ↑π * I * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖

Tactic:
calc
    |f x ^ r| ≤ |f x| ^ r := abs_rpow_le_abs_rpow _ _
    _ ≤ (c * |g x|) ^ r := by gcongr; assumption
    _ = c ^ r * |g x ^ r| := by rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]

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

Goal state before:
pp: x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x = y ^ z⁻¹ ↔ x ^ z = y

Tactic:
by
  rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]

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

Goal state before:
pp: x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x ^ z⁻¹ = y ↔ x = y ^ z

Tactic:
by
  rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]

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

Goal state before:
pp: case top
⊢ ∞ ^ 0 = 1

Tactic:
dsimp only [(· ^ ·), Pow.pow, rpow]
      simp [← none_eq_top]

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

Goal state before:
pp: case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 0 = 1

Tactic:
dsimp only [(· ^ ·), Pow.pow, rpow]
      simp [← none_eq_top]

Goal state after: