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

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : Group G
inst✝⁸ : TopologicalSpace G
μ : Measure G
inst✝⁷ : μ.IsHaarMeasure
inst✝⁶ : BorelSpace G
inst✝⁵ : ContinuousMul G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : MeasurableSpace H
inst✝¹ : BorelSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁸, inst✝³] ⇑f
h_surj : Surjective ⇑f
h_prop : Tendsto (⇑f) (cocompact G) (cocompact H)
K : Set H
⊢ IsCompact K → (map (⇑f) μ) K < ∞

Tactic:
hK

Goal state after:
G : Type u_1
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : Group G
inst✝⁸ : TopologicalSpace G
μ : Measure G
inst✝⁷ : μ.IsHaarMeasure
inst✝⁶ : BorelSpace G
inst✝⁵ : ContinuousMul G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : MeasurableSpace H
inst✝¹ : BorelSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁸, inst✝³] ⇑f
h_surj : Surjective ⇑f
h_prop : Tendsto (⇑f) (cocompact G) (cocompact H)
K : Set H
hK : IsCompact K
⊢ (map (⇑f) μ) K < ∞
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
s : Set α
this : (c • μ) s ≠ ∞ ↔ μ s ≠ ∞
⊢ MeasurableSet s ∧ (c • μ) s ≠ ∞ ↔ MeasurableSet s ∧ μ s ≠ ∞

Tactic:
simp only [this]

Goal state after:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : PseudoEMetricSpace β
n : ℕ
j : ι
f : ι → α → β
g : α → β
inst✝ : Preorder ι
x : α
⊢ x ∈ ⋃ k, ⋃ (_ : j ≤ k), {x | (↑n)⁻¹ < edist (f k x) (g x)} ↔ ∃ k ≥ j, (↑n)⁻¹ < edist (f k x) (g x)

Tactic:
Set.mem_iUnion,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : PseudoEMetricSpace β
n : ℕ
j : ι
f : ι → α → β
g : α → β
inst✝ : Preorder ι
x : α
⊢ (∃ i, ∃ (_ : j ≤ i), x ∈ {x | (↑n)⁻¹ < edist (f i x) (g x)}) ↔ ∃ k ≥ j, (↑n)⁻¹ < edist (f k x) (g x)
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ HasFiniteIntegral X μ

Tactic:
apply (hasFiniteIntegral_const (max ‖a‖ ‖b‖)).mono'
  filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω using abs_le_max_abs_abs

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
apply F_le_bound.mp ((ae_tendsto_ofReal_norm h_lim).mono _)

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
⊢ ∀ (x : α),
    Tendsto (fun n ↦ ENNReal.ofReal ‖F n x‖) atTop (𝓝 (ENNReal.ofReal ‖f x‖)) →
      (∀ (i : ℕ), ENNReal.ofReal ‖F i x‖ ≤ ENNReal.ofReal (bound x)) → ENNReal.ofReal ‖f x‖ ≤ ENNReal.ofReal (bound x)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
h : -1 ≤ x
⊢ 1 + x ≤ (1 + x / 2) ^ 2

Tactic:
calc 1 + x
    _ ≤ 1 + x + (x / 2) ^ 2 := le_add_of_nonneg_right <| sq_nonneg _
    _ = _ := by ring

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

Goal state before:
pp: z w : ℂ
⊢ normSq z + normSq (-w) + 2 * (z * (starRingEnd ℂ) (-w)).re = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re

Tactic:
simp only [map_neg, mul_neg, neg_re, normSq_neg]

Goal state after:
z w : ℂ
⊢ normSq z + normSq w + -(2 * (z * (starRingEnd ℂ) w).re) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z : ℂ
n : ℕ
⊢ (z / ↑n).re = z.re / ↑n

Tactic:
by rw [div_natCast]

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

Goal state before:
pp: z : ℂ
n : ℕ
⊢ (z / ↑n).im = z.im / ↑n

Tactic:
by rw [div_natCast]

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

Goal state before:
pp: case e'_1
s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
exact reProdIm_subset_iff

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
⊢ ‖f‖ * ‖x‖ ≤ ‖f‖ * c

Tactic:
by gcongr; exact f.opNorm_nonneg

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

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖n • f v‖ ≤ ↑n * (b * ‖v‖)

Tactic:
exact norm_nsmul_le.trans (by gcongr; apply hb)

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

Goal state before:
pp: case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖0‖ = c * 0

pp: case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x

Tactic:
· exact ⟨1, by simp⟩

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖0‖ = 0

pp: case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x

Tactic:
· exact ⟨1, by simp⟩

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ Injective (↑e ∘ Subtype.val)

Tactic:
e.injOn.injective_iff e.source (by simp)

Goal state after:
case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ Injective Subtype.val
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : X
⊢ ↑(toPartialHomeomorph f h).symm (f x) = x

Tactic:
by
  rw [← congr_fun (h.toPartialHomeomorph_apply f), PartialHomeomorph.left_inv]
  exact Set.mem_univ _

Goal state after:
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
s : Set X
hs : IsOpen[inst✝¹] s
hse : s ⊆ e.source
⊢ IsOpen[inst✝] (e.target ∩ ↑e.symm ⁻¹' s)

Tactic:
exact e.continuousOn_invFun.isOpen_inter_preimage e.open_target hs

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ z ↔ ∃ x ≥ 0, ↑x = z

Tactic:
simp_rw [nonneg_iff (K := K), ext_iff (K := K)]; aesop

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)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e.symm (↑e y) ∈ s → ↑e.symm (↑e y) ∈ f ⁻¹' t

Tactic:
e.left_inv hy,

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)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ y ∈ s → y ∈ f ⁻¹' t
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case e'_1.e'_3
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
this : I ≠ 0
⊢ ‖z‖ = ‖-I * z‖

pp: case e'_1.e'_4
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
this : I ≠ 0
⊢ im z = re (-I * z)

pp: case e'_2
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
this : I ≠ 0
⊢ -I * (I * ↑‖z‖) = ↑‖-I * z‖

Tactic:
all_goals simp [neg_mul, ← mul_assoc, I_mul_I_of_nonzero this, norm_I_of_ne_zero this]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c⁻¹ * ‖f x‖ ≤ ‖g x‖

Tactic:
inv_mul_le_iff₀ (by positivity)

Goal state after:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
x : α
hx : c⁻¹⁻¹ * ‖f x‖ ≤ ‖g x‖
⊢ ‖f x‖ ≤ c⁻¹ * ‖g x‖

Tactic:
inv_mul_le_iff₀ (by positivity)

Goal state after:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
x : α
hx : ‖f x‖ ≤ c⁻¹ * ‖g x‖
⊢ ‖f x‖ ≤ c⁻¹ * ‖g x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x ^ (n + i) / ↑(n + i).factorial‖ ≤ ∑ i ∈ range k, ‖x‖ ^ (n + i) / ↑(n + i).factorial

Tactic:
simp [norm_natCast, Complex.norm_pow]

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

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j, ‖x‖ ^ m / ↑m.factorial - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
gcongr
    exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
⊢ f =O[l] g

Tactic:
by
  obtain ⟨C, hC_pos, hC⟩ := bound_of_isBigO_nat_atTop hfg
  refine isBigO_iff.mpr ⟨C, ?_⟩
  filter_upwards [h] with x h
  by_cases hf : f x = 0
  · simp [hf, hC_pos]
  exact hC fun a ↦ hf (h a)

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

Goal state before:
pp: x : ℝ
⊢ ↑(cos (2 * x)) = ↑(cos x ^ 2 - sin x ^ 2)

Tactic:
simp [cos_two_mul']

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (fun x ↦ f x * g x) =o[l] h ↔ g =o[l] fun x ↦ h x / f x

Tactic:
rw [isLittleO_iff_forall_isBigOWith, isLittleO_iff_forall_isBigOWith]

Goal state after:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ f x * g x) h) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g fun x ↦ h x / f x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝² : NormedRing α
inst✝¹ : NormSMulClass ℤ α
inst✝ : Nontrivial α
⊢ Tendsto Nat.cast atTop (Bornology.cobounded α)

Tactic:
rw [← tendsto_norm_atTop_iff_cobounded]
  simpa [norm_natCast_eq_mul_norm_one] using tendsto_natCast_atTop_atTop
    |>.atTop_mul_const (norm_pos_iff.mpr one_ne_zero)

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ 0 < x + π / 2

Tactic:
linarith [hx.1]

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

Goal state before:
pp: x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ 0 ≤ x + π / 2

Tactic:
linarith [hx.1]

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

Goal state before:
pp: ⊢ comap cexp (comap norm (𝓝 0)) = comap re (comap Real.exp (𝓝 0))

Tactic:
comap_comap,

Goal state after:
⊢ comap (norm ∘ cexp) (𝓝 0) = comap re (comap Real.exp (𝓝 0))
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ comap (fun x ↦ Real.exp x.re) (𝓝 0) = comap re (comap Real.exp (𝓝 0))

Tactic:
comap_comap,

Goal state after:
⊢ comap (fun x ↦ Real.exp x.re) (𝓝 0) = comap (Real.exp ∘ re) (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn0 : n % 2 = 0
⊢ ↑(n / 2) * 2 * π = x

Tactic:
← @Int.cast_two ℝ,

Goal state after:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn0 : n % 2 = 0
⊢ ↑(n / 2) * ↑2 * π = x
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
⊢ IsBounded (s * t)

Tactic:
obtain ⟨Rt, hRt⟩ : ∃ R, ∀ x ∈ t, ‖x‖ ≤ R := ht.exists_norm_le'

Goal state after:
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
⊢ IsBounded (s * t)
Module: Mathlib.Analysis.Normed.Group.Pointwise

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

Tactic:
by
  simp_rw [singleton_mul, ← smul_eq_mul, image_smul, smul_closedBall]

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
S : AddSubgroup M
m : M
⊢ ‖(↑(mk' S)).toFun m‖ ≤ 1 * ‖m‖

Tactic:
by simpa [one_mul] using norm_mk_le_norm

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
f : C(X, Y)
g : C(Y, Z)
K : Set X
⊢ IsCompact K →
    ∀ (U : Set Z),
      IsOpen[inst✝¹] U →
        MapsTo (⇑((f, g).2.comp (f, g).1)) K U → ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U

Tactic:
hK

Goal state after:
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
f : C(X, Y)
g : C(Y, Z)
K : Set X
hK : IsCompact K
⊢ ∀ (U : Set Z),
    IsOpen[inst✝¹] U →
      MapsTo (⇑((f, g).2.comp (f, g).1)) K U → ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
g : G
hg : g ∈ (Submonoid.pathComponentOne G).carrier
⊢ g⁻¹ ∈ (Submonoid.pathComponentOne G).carrier

Tactic:
simpa using! hg.inv

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
x✝¹ : X
x✝ : x✝¹ ∈ pathComponentIn F x
γ : Path x x✝¹
hγ : ∀ (t : ↑I), γ t ∈ F
t t' : ↑I
⊢ min (max (↑t') 0) ↑t ∈ Icc 0 1

Tactic:
simp [t.2.1, t.2.2]

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
⊢ IsCompact K →
    ∀ (U : Set Y), IsOpen[inst✝³] U → MapsTo (⇑f) K U → ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a)) K U

Tactic:
hK

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), IsOpen[inst✝³] U → MapsTo (⇑f) K U → ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a)) K U
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
a : X
b : Y
⊢ Joined (x, y) (a, b) ↔ Joined x a ∧ Joined y b

Tactic:
exact ⟨fun h ↦ ⟨h.map continuous_fst, h.map continuous_snd⟩, fun ⟨h₁, h₂⟩ ↦ h₁.prod h₂⟩

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Function.LeftInverse uncurry ContinuousMap.curry

Tactic:
intro; ext; rfl

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Function.RightInverse uncurry ContinuousMap.curry

Tactic:
intro; ext; rfl

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

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

Tactic:
rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]

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

Goal state before:
pp: z : ℂ
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

Tactic:
by
  by_cases h₀ : z = 0
  · simp [h₀, Real.pi_ne_zero.symm]
  constructor
  · intro h
    rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [h₀]
  · obtain ⟨x, y⟩ := z
    rintro ⟨h : x < 0, rfl : y = 0⟩
    rw [← arg_neg_one, ← arg_real_mul (-1) (neg_pos.2 h)]
    simp [← ofReal_def]

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

Goal state before:
pp: x : ℝ
hx : x < -1
⊢ 0 < log (-x)

Tactic:
have : 1 < -x := by linarith

Goal state after:
x : ℝ
hx : x < -1
this : 1 < -x
⊢ 0 < log (-x)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

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

Tactic:
· simp [h₀, Real.pi_ne_zero]

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

Goal state before:
pp: x y : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
hy₁ : -π < y.im
hy₂ : y.im ≤ π
hxy : cexp x = cexp y
⊢ x = y

Tactic:
rw [← log_exp hx₁ hx₂, ← log_exp hy₁ hy₂, hxy]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ log (↑r * x) = ↑(Real.log r) + log x

Tactic:
replace hx := norm_ne_zero_iff.mpr hx
  simp_rw [log, norm_mul, norm_real, arg_real_mul _ hr, Real.norm_of_nonneg hr.le,
    Real.log_mul hr.ne' hx, ofReal_add, add_assoc]

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

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

Tactic:
by
  obtain rfl | hx := hx.eq_or_lt
  · simp
  · exact (log_le_sub_one_of_pos hx).trans (by linarith)

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

Goal state before:
pp: case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then log x else (starRingEnd ℂ) (log x)) - ↑(Real.log (normSq x)) =
    if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

Tactic:
simp_rw [log, map_add, map_mul, conj_ofReal, conj_I, normSq_eq_norm_sq, Real.log_pow,
      Nat.cast_two, ofReal_mul, neg_add, mul_neg, neg_neg]
    norm_num
    grind

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
⊢ ↑n / ↑d < 1

Tactic:
simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h₂)

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

Goal state before:
pp: x : ℂ
⊢ x = x ^ 2⁻¹ * x ^ 2⁻¹

Tactic:
simp [← sq]

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
⊢ z.arg ≤ π / 2 ↔ z.im < 0

pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Tactic:
· simp only [him.not_gt]
    rw [iff_false, not_le, arg_of_re_neg_of_im_nonneg hre him, ← sub_lt_iff_lt_add, half_sub,
      Real.neg_pi_div_two_lt_arcsin, neg_im, neg_div, neg_lt_neg_iff, div_lt_one, ←
      abs_of_nonneg him, abs_im_lt_norm]
    exacts [hre.ne, norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne]

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
x✝ : ℝ
⊢ (↑x✝ + ↑π).sin = -(↑x✝).sin

Tactic:
exact Real.sin_antiperiodic _

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

Goal state before:
pp: case inl
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : (θ + ψ).toReal ≤ 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
obtain rfl : k = -1 := IsStrictOrderedRing.int_eq_of_mul_mem_Ioo two_pi_pos <| by
      grind [toReal_mem_Ioc]

Goal state after:
case inl
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
h : (θ + ψ).toReal ≤ 0
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑(-1)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: r : ℝ
hr : r < 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ∈ {x | (fun x ↦ (fun x ↦ -|log x| ^ 1) x = log x) x}

Tactic:
simp [abs_of_nonpos (log_nonpos hx.1 hx.2)]

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
by
  simpa using rpow_sub_natCast hx y 1

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

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
by
  simpa using rpow_sub_natCast hx y 1

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

Goal state before:
pp: case inl
ε : ℝ
hε : 0 < ε
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ^ ε / ε

Tactic:
rw [log_zero, zero_rpow hε.ne', zero_div]

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

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 < x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx2 le_top)

Goal state after:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < ↑x
hx2 : ↑x < 1
⊢ 1 < ↑x ^ z
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
s : Set E
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ openSegment 𝕜 x y ⊆ s ↔ [x -[𝕜] y] ⊆ s

Tactic:
by
  simp only [← insert_endpoints_openSegment, insert_subset_iff, *, true_and]

Goal state after: