mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ.InnerRegular

Tactic:
convert! h.map f.symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ = map (⇑f.symm) (map (⇑f) μ)
Module: Mathlib.MeasureTheory.Group.LIntegral

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
convert! (lintegral_map_equiv f <| MeasurableEquiv.mulRight g).symm using 1

Goal state after:
case e'_3
G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f x ∂μ = ∫⁻ (a : G), f a ∂map (⇑(MeasurableEquiv.mulRight g)) μ
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: case hf
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (uncurry fun x y ↦ s.indicator (fun x ↦ 1) x * f y) (μ.prod ν)

pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun x ↦ 1) (y * x) * f x⁻¹ ∂ν ∂μ =
    ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * f x⁻¹ ∂μ

Tactic:
· exact (((measurable_const.indicator sm).comp measurable_fst).mul
      (hf.comp measurable_snd)).aemeasurable

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun x ↦ 1) (y * x) * f x⁻¹ ∂ν ∂μ =
    ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * f x⁻¹ ∂μ
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
μ : Measure G
t : Set G
kt : s ⊆ t
⊢ MeasurableSet t → μ (s * closure[inst✝³] {1}) ≤ μ t

Tactic:
t_meas

Goal state after:
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
μ : Measure G
t : Set G
kt : s ⊆ t
t_meas : MeasurableSet t
⊢ μ (s * closure[inst✝³] {1}) ≤ μ t
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ.Regular

Tactic:
convert! h.map f.symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ = map (⇑f.symm) (map (⇑f) μ)
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s * s = (2 * a * x + b) * (2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)

Tactic:
mul_self_eq_mul_self_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
this : discrim a b c = 0 * 0
⊢ x = -b / (2 * a) ∨ x = -b / (2 * a) ↔ x = -b / (2 * a)

Tactic:
or_self_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
this : discrim a b c = 0 * 0
⊢ x = -b / (2 * a) ↔ x = -b / (2 * a)
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
⊢ HasFiniteIntegral (fun x ↦ (f x).toReal) μ

Tactic:
simp_rw [hasFiniteIntegral_iff_enorm, h]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a).toReal ∂μ < ∞
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x / y) = √x / √y

Tactic:
by
  rw [division_def, sqrt_mul hx, sqrt_inv, division_def]

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

Goal state before:
pp: z w : ℂ
h : z.re = w.re
⊢ √(0 + (z.im - w.im) ^ 2) = dist z.im w.im

Tactic:
zero_add,

Goal state after:
z w : ℂ
h : z.re = w.re
⊢ √((z.im - w.im) ^ 2) = dist z.im w.im
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
h : z.re = w.re
⊢ dist z w = dist z.im w.im

Tactic:
by
  rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, zero_add, Real.sqrt_sq_eq_abs, Real.dist_eq]

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

Goal state before:
pp: z : ℂ
⊢ dist ((starRingEnd ℂ) z) z = ↑(2 * Real.nnabs z.im)

Tactic:
NNReal.coe_mul,

Goal state after:
z : ℂ
⊢ dist ((starRingEnd ℂ) z) z = ↑2 * ↑(Real.nnabs z.im)
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
E : Type u_2
α : Type u_3
𝕜 : Type u_4
A : Type u_5
inst✝⁵ : NormedField 𝕜
inst✝⁴ : StarRing 𝕜
inst✝³ : SeminormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : StarModule 𝕜 A
S : StarSubalgebra 𝕜 A
⊢ NormedAlgebra 𝕜 ↥S

Tactic:
by infer_instance

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ ‖reLm x‖ ≤ 1 * ‖x‖

Tactic:
by simp [abs_re_le_norm]

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

Tactic:
rcases eq_or_ne z 0 with (rfl | h₀)

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ 0⁻¹ = (starRingEnd K) 0 * ↑(‖0‖ ^ 2)⁻¹

case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ 2 • I • (↑(ℜ x) * ↑(ℑ x) - ↑(ℑ x) * ↑(ℜ x)) = 0 ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
two_smul ℕ,

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ I • (↑(ℜ x) * ↑(ℑ x) - ↑(ℑ x) * ↑(ℜ x)) + I • (↑(ℜ x) * ↑(ℑ x) - ↑(ℑ x) * ↑(ℜ x)) = 0 ↔ Commute ↑(ℜ x) ↑(ℑ x)
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst✝¹] (↑e.symm '' t)
⊢ e.source ∩ ↑e ⁻¹' t ⊆ e.source

Tactic:
apply Set.inter_subset_left

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ↑e.symm ⁻¹' s =ᶠ[𝓝 (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
eventuallyEq_set,

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : Y) in 𝓝 (↑e x), x ∈ ↑e.symm ⁻¹' s ↔ x ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * ((↑(m.choose I))⁻¹ * (↑I.factorial)⁻¹ * (↑(m - I).factorial)⁻¹) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
simp only [mul_left_comm (m.choose I : ℂ), mul_assoc, mul_left_comm (m.choose I : ℂ)⁻¹,
      mul_comm (m.choose I : ℂ)]

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * ((↑(m.choose I))⁻¹ * ↑(m.choose I))))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
⊢ ∃ φ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
rcases h.exists_nonneg with ⟨c, hnnc, hc⟩

Goal state after:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : c ≥ 0
hc : IsBigOWith c l u v
⊢ ∃ φ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case hab
x✝ : ℂ
hx : ‖x✝‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
x : ℕ
a✝ : x ∈ {m ∈ range j | n ≤ m}
⊢ ‖x✝ ^ (x - n)‖ ≤ 1

Tactic:
rw [Complex.norm_pow]

Goal state after:
case hab
x✝ : ℂ
hx : ‖x✝‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
x : ℕ
a✝ : x ∈ {m ∈ range j | n ≤ m}
⊢ ‖x✝‖ ^ (x - n) ≤ 1
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case hac
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
hi : i ∈ Ico n j
⊢ ‖x ^ (i - n)‖ ≤ ‖x‖ ^ (i - n)

Tactic:
rw [Complex.norm_pow]

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

Goal state before:
pp: y : ℝ
h_le : y ≤ rexp (y - 1)
⊢ y * rexp (-y) ≤ rexp (-1)

Tactic:
have h_mul_le : y * rexp (-y) ≤ rexp (y - 1) * rexp (-y) := by gcongr

Goal state after:
y : ℝ
h_le : y ≤ rexp (y - 1)
h_mul_le : y * rexp (-y) ≤ rexp (y - 1) * rexp (-y)
⊢ y * rexp (-y) ≤ rexp (-1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℤ
⊢ cos (↑n * (2 * π) - π) = -1

Tactic:
by
  simpa only [cos_zero] using (cos_periodic.int_mul n).sub_antiperiod_eq cos_antiperiodic

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
r : ℝ
⊢ ‖x‖ < r ↔ ∃ m, ↑m = x ∧ ‖m‖ < r

Tactic:
simp [norm_eq_infDist, infDist_lt_iff (norm_aux _)]

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:
ball_div_singleton,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball (1 / x) δ = ball x⁻¹ δ
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior {x} = ball x 0

Tactic:
ball_zero,

Goal state after:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior {x} = ∅
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝¹ : SeminormedRing R
inst✝ : NormMulClass R
x : R
⊢ Tendsto (fun n ↦ x ^ n) atTop (𝓝 0) ↔ ‖x‖ < 1

Tactic:
by
  -- this proof is slightly fiddly since `‖x ^ n‖ = ‖x‖ ^ n` might not hold for `n = 0`
  refine ⟨?_, tendsto_pow_atTop_nhds_zero_of_norm_lt_one⟩
  rw [← abs_of_nonneg (norm_nonneg _), ← tendsto_pow_atTop_nhds_zero_iff,
    tendsto_zero_iff_norm_tendsto_zero]
  apply Tendsto.congr'
  filter_upwards [eventually_ge_atTop 1] with n hn
  induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hn IH => simp [pow_succ, IH]

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

Goal state before:
pp: n : ℤ
⊢ cos (↑n * (2 * ↑π) - ↑π) = -1

Tactic:
by
  simpa only [cos_zero] using (cos_periodic.int_mul n).sub_antiperiod_eq cos_antiperiodic

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 ≤ δ
x : E
⊢ cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)

Tactic:
rw [← cthickening_singleton _ hδ, cthickening_cthickening hε hδ,
      cthickening_singleton _ (add_nonneg hε hδ)]

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

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

Tactic:
zero_add,

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
| (n + k).descFactorial k

Tactic:
A,

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
| Polynomial.eval n P
Module: Mathlib.Topology.Connected.PathConnected

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

Tactic:
use γ₀.trans γ₁

Goal state after:
case h
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc p y 0) y
hγ₀s : range ⇑γ₀ ⊆ s
hγ₀p : ∀ (i : Fin n), p i ∈ range ⇑γ₀
γ₁ : Path y x
hγ₁ : range ⇑γ₁ ⊆ s
⊢ range ⇑(γ₀.trans γ₁) ⊆ s ∧ (∀ (i : Fin n), p i ∈ range ⇑(γ₀.trans γ₁)) ∧ y ∈ range ⇑(γ₀.trans γ₁)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ PathConnectedSpace X

Tactic:
by infer_instance

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 : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + (-1) ^ (2 * n) * f (2 * n) + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i

Tactic:
_root_.pow_succ',

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 n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + (-1) ^ (2 * n) * f (2 * n) + -1 * (-1) ^ (2 * n) * f (2 * n + 1) ≤
    ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f 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)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) +
      (-1) ^ (2 * n + 1 + 1) * f (2 * n + 1 + 1)

Tactic:
_root_.pow_succ',

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 n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + -1 * (-1) ^ (2 * n) * f (2 * n + 1) +
      -1 * (-1 * (-1) ^ (2 * n)) * f (2 * n + 1 + 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 n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤
    ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + (-1) ^ (2 * n) * f (2 * n) + (-1) ^ (2 * n + 1) * f (2 * n + 1)

Tactic:
_root_.pow_succ',

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 n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + (-1) ^ (2 * n) * f (2 * n) + -1 * (-1) ^ (2 * n) * f (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 n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) +
      (-1) ^ (2 * n + 2) * f (2 * n + 2) ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i

Tactic:
_root_.pow_succ',

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 n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + -1 * (-1) ^ (2 * n) * f (2 * n + 1) +
      -1 * (-1 * (-1) ^ (2 * n)) * f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
m n : ℕ
this : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n
⊢ p * |↑m / ↑n - ↑(round (↑m / ↑n))| = p * (↑(min (m % n) (n - m % n)) / ↑n)

Tactic:
abs_sub_round_div_natCast_eq

Goal state after:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
this : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n
⊢ p * (↑(min (m % n) (n - m % n)) / ↑n) = p * (↑(min (m % n) (n - m % n)) / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
rw [arcsin_of_le_neg_one hx₁.le, cos_neg, cos_pi_div_two, sqrt_eq_zero_of_nonpos]

Goal state after:
case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) + π) = x.re / ‖x‖

pp: case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) - π) = x.re / ‖x‖

Tactic:
· rw [Real.cos_add_pi, Real.cos_arcsin]
    field_simp
    simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]
    field

Goal state after:
case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) - π) = x.re / ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
sqrt_mul_self (cos_arcsin_nonneg _)

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = ↑‖z‖ * cexp (↑z.arg * I)

Tactic:
rw [hz, ofReal_one, one_mul]

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

Goal state before:
pp: x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖

Tactic:
_root_.pow_succ',

Goal state after:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x * x ^ n / ↑(n + 1)!‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x * x ^ n / (↑(n + 1) * ↑n !)‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖

Tactic:
← _root_.div_mul_div_comm,

Goal state after:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x / ↑(n + 1) * (x ^ n / ↑n !)‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im

Tactic:
rcases eq_or_ne z 0 with (rfl | h₀)

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 refine_2
x y : ℝ
⊢ 0 ≤ { re := x, im := y }.re ∧ { re := x, im := y }.im = 0 → { re := x, im := y }.arg = 0

Tactic:
rintro ⟨h, rfl : y = 0⟩

Goal state after:
case refine_2
x : ℝ
h : 0 ≤ { re := x, im := 0 }.re
⊢ { re := x, im := 0 }.arg = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ 2 • ↑π = 0

Tactic:
two_nsmul_coe_pi

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

Goal state before:
pp: case inr.hg
n : ℕ
hn : n ≠ 0
p : ℕ
hp : ↑(p ^ n.factorization p) = 0
⊢ n.factorization p = 0

Tactic:
eq_zero_of_pow_eq_zero (Nat.cast_eq_zero.1 hp),

Goal state after:
case inr.hg
n : ℕ
hn : n ≠ 0
p : ℕ
hp : ↑(p ^ n.factorization p) = 0
⊢ n.factorization 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
exact_mod_cast of_decide_eq_true h₁

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

Goal state before:
pp: x : ℂ
hi : 0 < x.im
⊢ (-x).arg = x.arg - π

Tactic:
rw [arg_of_im_pos hi, arg_of_im_neg (show (-x).im < 0 from Left.neg_neg_iff.2 hi)]

Goal state after:
x : ℂ
hi : 0 < x.im
⊢ -Real.arccos ((-x).re / ‖-x‖) = Real.arccos (x.re / ‖x‖) - π