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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ ∀ r < μ s, ∃ K ⊆ s, (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) K ∧ r < μ K

Tactic:
r

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
⊢ r < μ s → ∃ K ⊆ s, (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst✝² : SFinite μ
inst✝¹ : SFinite τ
inst✝ : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ map (Prod.map f g) (μ.prod τ) ≪ ν.prod υ

Tactic:
← map_prod_map _ _ (by fun_prop) (by fun_prop)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst✝² : SFinite μ
inst✝¹ : SFinite τ
inst✝ : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ (map f μ).prod (map g τ) ≪ ν.prod υ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 ↦ f x_1 x) l ×ˢ map (fun x_1 ↦ f x_1 x) l).HasAntitoneBasis fun n ↦
      ((fun x_1 ↦ f x_1 x) '' u n) ×ˢ ((fun x_1 ↦ f x_1 x) '' u n)
⊢ MeasurableSet {x | (map (fun n ↦ f n x) l).NeBot ∧ map (fun n ↦ f n x) l ×ˢ map (fun n ↦ f n x) l ≤ uniformity γ}

Tactic:
and_iff_right (hl.map _),

Goal state after:
case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 ↦ f x_1 x) l ×ˢ map (fun x_1 ↦ f x_1 x) l).HasAntitoneBasis fun n ↦
      ((fun x_1 ↦ f x_1 x) '' u n) ×ˢ ((fun x_1 ↦ f x_1 x) '' u n)
⊢ MeasurableSet {x | map (fun n ↦ f n x) l ×ˢ map (fun n ↦ f n x) l ≤ uniformity γ}
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
U : Set X
hU : IsOpen[inst✝²] U
⊢ ∀ r < μ U, ∃ K ⊆ U, IsClosed[inst✝²] K ∧ r < μ K

Tactic:
r

Goal state after:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
U : Set X
hU : IsOpen[inst✝²] U
r : ℝ≥0∞
⊢ r < μ U → ∃ K ⊆ U, IsClosed[inst✝²] K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
⊢ ∀ r < μ F, ∃ K ⊆ F, IsCompact K ∧ r < μ K

Tactic:
r

Goal state after:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
⊢ r < μ F → ∃ K ⊆ F, IsCompact K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : OpensMeasurableSpace α
h : μ.InnerRegular
U : Set α
hU : IsOpen[inst✝²] U
⊢ ∀ r < μ U, ∃ K ⊆ U, IsClosed[inst✝²] K ∧ r < μ K

Tactic:
r

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : OpensMeasurableSpace α
h : μ.InnerRegular
U : Set α
hU : IsOpen[inst✝²] U
r : ℝ≥0∞
⊢ r < μ U → ∃ K ⊆ U, IsClosed[inst✝²] K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
⊢ ∀ r < (μ + ν) s, ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K

Tactic:
r

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
⊢ r < (μ + ν) s → ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
⊢ ∀ r < (sum μ) s, ∃ K ⊆ s, IsCompact K ∧ r < (sum μ) K

Tactic:
r

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
⊢ r < (sum μ) s → ∃ K ⊆ s, IsCompact K ∧ r < (sum μ) K
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
μ : Measure G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h : μ.InnerRegularCompactLTTop
s : Set G
s_meas : MeasurableSet s
μs : μ s ≠ ∞
⊢ ∀ r < μ s, ∃ K ⊆ s, (fun s ↦ IsCompact s ∧ IsClosed[inst✝³] s) K ∧ r < μ K

Tactic:
r

Goal state after:
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
μ : Measure G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h : μ.InnerRegularCompactLTTop
s : Set G
s_meas : MeasurableSet s
μs : μ s ≠ ∞
r : ℝ≥0∞
⊢ r < μ s → ∃ K ⊆ s, (fun s ↦ IsCompact s ∧ IsClosed[inst✝³] s) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : c = 0
⊢ (c • μ).InnerRegularCompactLTTop

Tactic:
simp only [hc, zero_smul]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : c = 0
⊢ InnerRegularCompactLTTop 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
s : Set α
hs : MeasurableSet s ∧ (c • μ) s ≠ ∞
⊢ ∀ r < (c • μ) s, ∃ K ⊆ s, IsCompact K ∧ r < (c • μ) K

Tactic:
r

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
s : Set α
hs : MeasurableSet s ∧ (c • μ) s ≠ ∞
r : ℝ≥0∞
⊢ r < (c • μ) s → ∃ K ⊆ s, IsCompact K ∧ r < (c • μ) K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst✝³] V
⊢ ∀ r < (μ.restrict A) V, ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K

Tactic:
r

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst✝³] V
r : ℝ≥0∞
⊢ r < (μ.restrict A) V → ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
this : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞
⊢ HasFiniteIntegral X μ

Tactic:
apply (hasFiniteIntegral_const_enorm this (μ := μ)).mono'_enorm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
this : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : ExistsAddOfLE R
inst✝¹ : Module ℚ≥0 R
inst✝ : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ (𝔼 i ∈ s, f i * g i) ^ 2 ≤ (𝔼 i ∈ s, f i ^ 2) * 𝔼 i ∈ s, g i ^ 2

Tactic:
simp only [expect, smul_pow, inv_pow, smul_mul_smul_comm, ← sq]
  gcongr
  exact sum_mul_sq_le_sq_mul_sq ..

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * star (U * B) = U * B * (star B * star U)

Tactic:
star_mul

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * (star B * star U) = U * B * (star B * star U)
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x y : ↥(unitary R)
⊢ star (↑x * ↑y) = star ↑y * star ↑x

Tactic:
star_mul

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x y : ↥(unitary R)
⊢ star ↑y * star ↑x = star ↑y * star ↑x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ
⊢ im ↑q = 0

Tactic:
rw [← ofReal_ratCast, ofReal_im]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ ‖x + (starRingEnd K) x‖ ^ 2 = re (x + (starRingEnd K) x) ^ 2

Tactic:
norm_sq_re_add_conj

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ re (x + (starRingEnd K) x) ^ 2 = re (x + (starRingEnd K) x) ^ 2
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
x : X
hx : x ∈ e.source
⊢ 𝓝 x = comap (↑e) (𝓝 (↑e x)) ⊓ 𝓟 e.source

Tactic:
by
  lift x to e.source using hx
  rw [← e.open_source.nhdsWithin_eq x.2, ← map_nhds_subtype_val, ← map_comap_setCoe_val,
    e.toHomeomorphSourceTarget.nhds_eq_comap, nhds_subtype_eq_comap]
  simp only [Function.comp_def, toHomeomorphSourceTarget_apply_coe, comap_comap]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
h : 0 ≤ re x ∧ im x = 0
⊢ x = star ↑√(re x) * ↑√(re x)

Tactic:
by simp [ext_iff (K := K), h.1, h.2]

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ ‖0‖ ≤ c * ‖g' x‖

Tactic:
norm_zero

Goal state after:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ 0 ≤ c * ‖g' x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
simp only [isBigO_iff, eventually_prod_iff]
  exact fun ⟨c, hc⟩ ↦ ⟨c, _, hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : f₁ =O[l] g₁
h₂ : f₂ =O[l] g₂
⊢ (fun x ↦ f₁ x + f₂ x) =O[l] fun x ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
by
  obtain ⟨c₁, hc₁⟩ := h₁.isBigOWith
  obtain ⟨c₂, hc₂⟩ := h₂.isBigOWith
  exact (hc₁.add_add hc₂).isBigO

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

Goal state before:
pp: case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x‖ < ε
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
⊢ IsBigOWith c l u v

Tactic:
exact isBigOWith_of_eq_mul _ ((hφ c hpos).mono fun x => le_of_lt) huvφ

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

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

Tactic:
have s1 := cos_add ((x + y) / 2) ((x - y) / 2)

Goal state after:
x y : ℂ
s1 : cos ((x + y) / 2 + (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
gcongr; norm_num [Nat.factorial]

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

Goal state before:
pp: x : ℝ
⊢ ↑(cosh (3 * x)) = ↑(4 * cosh x ^ 3 - 3 * cosh x)

Tactic:
simp [cosh_three_mul]

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ 0 < sin x

Tactic:
by
  calc 0 < x - x ^ 3 / 6 - |x| ^ 5 / 100 := by grind [pow_le_of_le_one]
    _ ≤ sin x :=
      sub_le_comm.1 (abs_sub_le_iff.1 (sin_bound (by rwa [abs_of_nonneg (le_of_lt hx0)]))).2

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

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =O[atTop] fun x ↦ a ^ x
C : ℝ
hC₀ : C > 0
hC : ∀ ⦃x : ℕ⦄, a ^ x ≠ 0 → ‖f x‖ ≤ C * ‖a ^ x‖
⊢ ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n

Tactic:
refine ⟨a, ha, C, hC₀, fun n ↦ ?_⟩

Goal state after:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =O[atTop] fun x ↦ a ^ x
C : ℝ
hC₀ : C > 0
hC : ∀ ⦃x : ℕ⦄, a ^ x ≠ 0 → ‖f x‖ ≤ C * ‖a ^ x‖
n : ℕ
⊢ |f n| ≤ C * a ^ n
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ UniformContinuousOn cexp {x | x.re ≤ a}

Tactic:
by
  have : Continuous (cexp - 1) := Continuous.sub (by fun_prop) continuous_one
  rw [Metric.uniformContinuousOn_iff, Metric.continuous_iff'] at *
  intro ε hε
  simp only [gt_iff_lt, Pi.sub_apply, Pi.one_apply, dist_sub_eq_dist_add_right,
    sub_add_cancel] at this
  have ha : 0 < ε / (2 * Real.exp a) := by positivity
  have H := this 0 (ε / (2 * Real.exp a)) ha
  rw [Metric.eventually_nhds_iff] at H
  obtain ⟨δ, hδ⟩ := H
  refine ⟨δ, hδ.1, ?_⟩
  intro x _ y hy hxy
  have h3 := hδ.2 (y := x - y) (by simpa only [dist_eq_norm, sub_zero] using hxy)
  rw [dist_eq_norm, exp_zero] at *
  have : cexp x - cexp y = cexp y * (cexp (x - y) - 1) := by
    rw [mul_sub_one, ← exp_add]
    ring_nf
  rw [this, mul_comm]
  have hya : ‖cexp y‖ ≤ Real.exp a := by simpa only [norm_exp, Real.exp_le_exp]
  simp only [gt_iff_lt, dist_zero_right, Set.mem_ofPred_eq, norm_mul, Complex.norm_exp] at *
  apply lt_of_le_of_lt (mul_le_mul h3.le hya (Real.exp_nonneg y.re) ha.le)
  simp [field]

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.nat_mul n).add_antiperiod_eq cos_antiperiodic

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
⊢ x ∈ S.normedMk.ker.topologicalClosure

Tactic:
S.ker_normedMk,

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ S.topologicalClosure
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ 2 + sqrtTwoAddSeries 0 n < 2 ^ 2

pp: n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
← lt_sub_iff_add_lt'

Goal state after:
n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2 ^ 2 - 2

n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
by
  have h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0 := by
    have : cos (3 * (π / 3)) = cos π := by
      congr 1
      ring
    linarith [cos_pi, cos_three_mul (π / 3)]
  rcases mul_eq_zero.mp h₁ with h | h
  · linarith [eq_zero_of_pow_eq_zero h]
  · have : cos π < cos (π / 3) := by
      refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_ <;> linarith [pi_pos]
    linarith [cos_pi]

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

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

Tactic:
rw [cos_pi_div_six, div_pow, sq_sqrt]

Goal state after:
⊢ 3 / 2 ^ 2 = 3 / 4

⊢ 0 ≤ 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ ↑(Real.sin π) = 0

Tactic:
Real.sin_pi

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

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

Tactic:
by
  simpa only [cos_zero] using (cos_periodic.nat_mul n).add_antiperiod_eq cos_antiperiodic

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

Goal state before:
pp: case pos
α : 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
⊢ ‖0‖ ≤ C * r ^ n

Tactic:
norm_zero

Goal state after:
case pos
α : 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
⊢ 0 ≤ C * r ^ n
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
motive : ZerothHomotopy X → Prop
mk : ∀ (x : X), motive (ZerothHomotopy.mk x)
x : ZerothHomotopy X
⊢ motive x

Tactic:
obtain ⟨x, rfl⟩ := mk_surjective x

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
motive : ZerothHomotopy X → Prop
mk : ∀ (x : X), motive (ZerothHomotopy.mk x)
x : X
⊢ motive (ZerothHomotopy.mk x)
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
⊢ Continuous[instTopologicalSpaceProd, _] fun p ↦ (const Y p.1).prodMk p.2

Tactic:
by
  simp_rw [continuous_iff_continuousAt, ContinuousAt, ContinuousMap.tendsto_nhds_compactOpen]
  rintro ⟨r, f⟩ K hK U hU H
  obtain ⟨V, W, hV, hW, hrV, hKW, hVW⟩ := generalized_tube_lemma (isCompact_singleton (x := r))
    (hK.image f.continuous) hU (by simpa [Set.subset_def, forall_comm (α := X)])
  refine Filter.eventually_of_mem (prod_mem_nhds (hV.mem_nhds (by simpa using hrV))
    (ContinuousMap.eventually_mapsTo hK hW (Set.mapsTo_iff_image_subset.mpr hKW))) ?_
  rintro ⟨r', f'⟩ ⟨hr'V, hf'⟩ x hxK
  exact hVW (Set.mk_mem_prod hr'V (hf' hxK))

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
⊢ JoinedIn F x y

Tactic:
refine ⟨⟨⟨Set.piecewise {1} (const I y) (const I x), ?_⟩, by simp, by simp⟩, fun t ↦ ?_⟩
  · exact isClosed_singleton.continuous_piecewise_of_specializes continuous_const continuous_const
      fun _ ↦ h
  · simp only [Path.coe_mk_mk, piecewise]
    split_ifs <;> assumption

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
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst✝¹] (Function.uncurry f)
⊢ Continuous[inst✝, _] fun x ↦ mkD (f x) g

Tactic:
have (x : _) : Continuous (f x) := f_cont.comp (Continuous.prodMk_right x)
  refine continuous_of_continuous_uncurry _ ?_
  conv in mkD _ _ => rw [mkD_of_continuous (this x)]
  exact f_cont

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

Goal state before:
pp: case inr.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
⊢ False

Tactic:
· rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'
      · have : -p ≤ ↑z * p := by nlinarith
        linarith [abs_eq_neg_self.mpr hp.le]
      · have : ↑z * p ≤ p := by nlinarith
        linarith [abs_eq_neg_self.mpr hp.le]

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

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
⊢ p ≤ addOrderOf u • ‖u‖

Tactic:
obtain ⟨n, hn⟩ := exists_norm_eq_of_isOfFinAddOrder hu
  replace hu : (addOrderOf u : ℝ) ≠ 0 := by
    norm_cast
    exact (addOrderOf_pos_iff.mpr hu).ne'
  conv_lhs => rw [← mul_one p]
  rw [hn, nsmul_eq_mul, ← mul_assoc, mul_comm _ p, mul_assoc, mul_div_cancel₀ _ hu,
    mul_le_mul_iff_right₀ hp.out, Nat.one_le_cast, Nat.one_le_iff_ne_zero]
  contrapose hu'
  simpa only [hu', Nat.cast_zero, zero_div, mul_zero, norm_eq_zero] using hn

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

Goal state before:
pp: x : ℝ
⊢ -(π / 2) = arcsin x ↔ x ≤ -1

Tactic:
neg_pi_div_two_eq_arcsin

Goal state after:
x : ℝ
⊢ x ≤ -1 ↔ x ≤ -1
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:

Tactic:
‖x ^ (n + 1) / (n + 1)!‖ = ‖x‖ / (n + 1) * ‖x ^ n / (n !)‖ := by
      rw [_root_.pow_succ', Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul,
        norm_div, Real.norm_natCast, Nat.cast_succ]
    _ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / (n !)‖ := by gcongr

Goal state after: