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

Goal state before:
pp: case refine_2
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∞
hr : r < μ s
K : Set G
Ks : K ⊆ s
K_comp : IsCompact K
hK : r < μ K
⊢ r < μ (closure[inst✝³] K)

Tactic:
rwa [K_comp.measure_closure]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : NullMeasurableSet s μ
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ U, IsOpen[inst✝⁴] U ∧ μ U < ∞ ∧ μ (U ∆ s) < ε

Tactic:
rcases hs with ⟨t, htm, hst⟩

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ ∃ U, IsOpen[inst✝⁴] U ∧ μ U < ∞ ∧ μ (U ∆ s) < ε
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this✝ : QuasiMeasurePreserving (fun h ↦ h * g⁻¹) μ μ
this : QuasiMeasurePreserving (Inv.inv ∘ (fun h ↦ h * g⁻¹) ∘ Inv.inv) μ μ
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ

Tactic:
simp_rw [Function.comp_def, mul_inv_rev, inv_inv] at this

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this✝ : QuasiMeasurePreserving (fun h ↦ h * g⁻¹) μ μ
this : QuasiMeasurePreserving (fun x ↦ g * x) μ μ
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
bound_hasFiniteIntegral : HasFiniteIntegral bound' μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F' n a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
⊢ HasFiniteIntegral f' μ

Tactic:
hasFiniteIntegral_iff_enorm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
bound_hasFiniteIntegral : HasFiniteIntegral bound' μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F' n a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∫⁻ (a : α), ‖f' a‖ₑ ∂μ < ∞
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ ‖z / w‖ = ‖z‖ / ‖w‖

Tactic:
rw [norm_def, norm_def, norm_def, normSq_div, Real.sqrt_div (normSq_nonneg _)]

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

Goal state before:
pp: x y : ℝ
⊢ normSq (↑x + ↑y * I) = x ^ 2 + y ^ 2

Tactic:
rw [← mk_eq_add_mul_I, normSq_mk, sq, sq]

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₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
⊢ f.SurjectiveOnWith K C'

Tactic:
by
  intro k k_in
  rcases h k k_in with ⟨g, rfl, hg⟩
  use g, rfl
  by_cases Hg : ‖f g‖ = 0
  · simpa [Hg] using hg
  · exact hg.trans (by gcongr)

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:
by gcongr; apply hb

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₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖z‖ * ‖f v‖ ≤ ‖z‖ * (b * ‖v‖)

Tactic:
by gcongr; apply hb

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₂
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖g‖ * ‖f v‖ ≤ ‖g‖ * (‖f‖ * ‖v‖)

Tactic:
gcongr; apply le_opNorm

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: f : ℂ →ₐ[ℝ] ℂ
⊢ f = AlgHom.id ℝ ℂ ∨ f = ↑conjAe

Tactic:
refine
      (eq_or_eq_neg_of_sq_eq_sq (f I) I <| by rw [← map_pow, I_sq, map_neg, map_one]).imp ?_ ?_ <;>
    refine fun h => algHom_ext ?_
  exacts [h, conj_I.symm ▸ h]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
x✝ : im z = 0
h : im z = 0 := x✝
⊢ ↑(re z) = z

Tactic:
conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
F : ℂ →ₐ[ℝ] A
⊢ F I * F I = -1

Tactic:
by rw [← map_mul, I_mul_I, map_neg, map_one]

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

Goal state before:
pp: z : ℂ
hz : z ∈ Metric.ball 1 1
⊢ z ∈ slitPlane

Tactic:
apply Or.inl

Goal state after:
z : ℂ
hz : z ∈ Metric.ball 1 1
⊢ 0 < z.re
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace X'
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Y'
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace Z'
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
⊢ IsHomeomorph ⇑(InjOn.toPartialEquiv f univ ⋯).toEquiv

Tactic:
isHomeomorph_iff_isEmbedding_surjective

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace X'
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Y'
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace Z'
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
⊢ IsEmbedding ⇑(InjOn.toPartialEquiv f univ ⋯).toEquiv ∧ Surjective ⇑(InjOn.toPartialEquiv f univ ⋯).toEquiv
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
f : Y → Z
x : Y
h : x ∈ e.target
⊢ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' univ) (↑e.symm x) ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)

Tactic:
preimage_univ,

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
f : Y → Z
x : Y
h : x ∈ e.target
⊢ ContinuousWithinAt (f ∘ ↑e) univ (↑e.symm x) ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (z : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        ((starRingEnd 𝕜) z) =
      (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        z

Tactic:
exact h.conj_re_ax

Goal state after:
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
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g → ∀ᶠ (a : α) in l, (fun x ↦ f (a, x)) =O[l'] fun x ↦ g (a, x)

Tactic:
simp only [isBigO_iff, eventually_iff, mem_prod_iff]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ (∃ c, ∃ t₁ ∈ l, ∃ t₂ ∈ l', t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}) → {a | ∃ c, {x | ‖f (a, x)‖ ≤ c * ‖g (a, x)‖} ∈ l'} ∈ l
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
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g → ∀ᶠ (b : β) in l', (fun x ↦ f (x, b)) =O[l] fun x ↦ g (x, b)

Tactic:
simp only [isBigO_iff, eventually_iff, mem_prod_iff]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ (∃ c, ∃ t₁ ∈ l, ∃ t₂ ∈ l', t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}) → {b | ∃ c, {x | ‖f (x, b)‖ ≤ c * ‖g (x, b)‖} ∈ l} ∈ l'
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : f₂ =o[l] g
hc : c₁ < c₂
⊢ IsBigOWith c₂ l (fun x ↦ f₁ x - f₂ x) g

Tactic:
by
  simpa only [sub_eq_add_neg] using h₁.add_isLittleO h₂.neg_left hc

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

Goal state before:
pp: x y : ℂ
⊢ cexp (x + y) - cexp (-(x + y)) = 2 * (sinh x * cosh y + cosh x * sinh y)

Tactic:
exp_add,

Goal state after:
x y : ℂ
⊢ cexp x * cexp y - cexp (-(x + y)) = 2 * (sinh x * cosh y + cosh x * sinh y)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cexp x * cexp y - cexp (-x + -y) = 2 * (sinh x * cosh y + cosh x * sinh y)

Tactic:
exp_add,

Goal state after:
x y : ℂ
⊢ cexp x * cexp y - cexp (-x) * cexp (-y) = 2 * (sinh x * cosh y + cosh x * sinh y)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
⊢ cexp (↑n * x + 1 * x) = cexp x ^ n * cexp x

Tactic:
exp_add,

Goal state after:
x : ℂ
n : ℕ
⊢ cexp (↑n * x) * cexp (1 * x) = cexp x ^ n * cexp x
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
h : cexp x = 0
⊢ x + -x = cexp (x + -x)

Tactic:
exp_add,

Goal state after:
x : ℂ
h : cexp x = 0
⊢ x + -x = cexp x * cexp (-x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cexp (x + y) + cexp (-(x + y)) = 2 * (cosh x * cosh y + sinh x * sinh y)

Tactic:
exp_add,

Goal state after:
x y : ℂ
⊢ cexp x * cexp y + cexp (-(x + y)) = 2 * (cosh x * cosh y + sinh x * sinh y)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cexp x * cexp y + cexp (-x + -y) = 2 * (cosh x * cosh y + sinh x * sinh y)

Tactic:
exp_add,

Goal state after:
x y : ℂ
⊢ cexp x * cexp y + cexp (-x) * cexp (-y) = 2 * (cosh x * cosh y + sinh x * sinh y)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖

Tactic:
apply (((continuous_norm.tendsto _).comp h).eventually_const_le ha).mono

Goal state after:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
⊢ ∀ (x : α), C⁻¹ ≤ ((fun a ↦ ‖a‖) ∘ fun x ↦ g x / f x) x → ‖f x‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (tan ↑x) = tan ↑x

Tactic:
by rw [← tan_conj, conj_ofReal]

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

Goal state before:
pp: x y : ℂ
⊢ cexp (x + y * I) = cexp x * (cos y + sin y * I)

Tactic:
exp_add,

Goal state after:
x y : ℂ
⊢ cexp x * cexp (y * I) = cexp x * (cos y + sin y * I)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖Real.exp x - 1 - x‖ = ‖↑(Real.exp x) - 1 - ↑x‖

Tactic:
exact_mod_cast Complex.norm_real _

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

Goal state before:
pp: x : ℂ
⊢ cexp x = cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)

Tactic:
by
  rw [← exp_add_mul_I, re_add_im]

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

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

Tactic:
rw [← nnnorm_norm, norm_exp_ofReal_mul_I, ← NNReal.coe_eq_one]

Goal state after:
x : ℝ
⊢ ↑‖1‖₊ = 1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖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) * (cexp (-(↑x / 2) * I) - cexp (↑x / 2 * I)) * I‖
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''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
⊢ C₁ ∈ ubounds

Tactic:
Set.mem_ofPred

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
⊢ ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C₁ * ‖g m‖
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝¹ : Field α
inst✝ : LinearOrder α
p : ℤ
hp : Even p
a : α
⊢ |a| ^ p = a ^ p

Tactic:
rcases abs_choice a with h | h <;> simp only [h, hp.neg_zpow _]

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

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x < 1
⊢ rexp x ≤ 1 / (1 - x)

Tactic:
rcases eq_or_lt_of_le h1 with (rfl | h1)

Goal state after:
case inl
h1 : 0 ≤ 0
h2 : 0 < 1
⊢ rexp 0 ≤ 1 / (1 - 0)

case inr
x : ℝ
h1✝ : 0 ≤ x
h2 : x < 1
h1 : 0 < x
⊢ rexp x ≤ 1 / (1 - x)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ rexp (1 + x) / (rexp 1 * C) = rexp x / C

Tactic:
exp_add,

Goal state after:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ rexp 1 * rexp x / (rexp 1 * C) = rexp x / C
Module: Mathlib.Analysis.Normed.Group.Pointwise

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

Tactic:
rw [mul_comm, singleton_mul_ball, mul_comm y]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝ : M ⧸ S
m : M
r✝ ε : ℝ
h : S ≤ T
x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T
r : ℝ
⊢ r ≤ ‖(quotientQuotientEquivQuotient S T h) x‖ ↔ r ≤ ‖x‖

Tactic:
simp only [le_norm_iff]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝ : M ⧸ S
m : M
r✝ ε : ℝ
h : S ≤ T
x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T
r : ℝ
⊢ (∀ (m : M), ↑m = (quotientQuotientEquivQuotient S T h) x → r ≤ ‖m‖) ↔
    ∀ (m : M ⧸ S), ↑m = x → ∀ (m_1 : M), ↑m_1 = m → r ≤ ‖m_1‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ √((2 + sqrtTwoAddSeries 0 n) / 2 / 2) = √(2 + sqrtTwoAddSeries 0 n) / 2

pp: case hc
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ 2 ≠ 0

pp: case hl
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ -π ≤ π / 2 ^ (n + 1)

pp: case hr
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ π / 2 ^ (n + 1) ≤ π

Tactic:
← div_mul_eq_div_div,

Goal state after:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ √((2 + sqrtTwoAddSeries 0 n) / (2 * 2)) = √(2 + sqrtTwoAddSeries 0 n) / 2

case hc
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ 2 ≠ 0

case hl
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ -π ≤ π / 2 ^ (n + 1)

case hr
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ π / 2 ^ (n + 1) ≤ π
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r

Tactic:
by
  rcases hr.lt_or_gt with hr | hr
  · rw [closedBall_eq_empty.2 hr, ball_eq_empty.2 hr.le, interior_empty]
  refine Subset.antisymm ?_ ball_subset_interior_closedBall
  intro y hy
  rcases (mem_closedBall.1 <| interior_subset hy).lt_or_eq with (hr | rfl)
  · exact hr
  set f : ℝ → E := fun c : ℝ => c • (y - x) + x
  suffices f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1 by
    have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) :=
      interior_mono this (preimage_interior_subset_interior_preimage (by fun_prop) (by simpa [f]))
    simp at h1
  intro c hc
  rw [mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← mul_le_mul_iff_left₀ hr]
  simpa [f, dist_eq_norm, norm_smul] using hc

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

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

pp: ⊢ 2 ≠ 0

pp: case hl
⊢ -π ≤ π / 3

pp: case hr
⊢ π / 3 ≤ π

Tactic:
← div_mul_eq_div_div,

Goal state after:
⊢ √((2 + 1) / (2 * 2)) = √3 / 2

⊢ 2 ≠ 0

case hl
⊢ -π ≤ π / 3

case hr
⊢ π / 3 ≤ π
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y < ε
⊢ False

Tactic:
exact h.le_bot ⟨hxz, hzy⟩

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

Goal state before:
pp: ⊢ tan (π / 4) = 1

Tactic:
by
  rw [tan_eq_sin_div_cos, cos_pi_div_four, sin_pi_div_four]
  have h : √2 / 2 > 0 := by positivity
  exact div_self (ne_of_gt h)

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 y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
exact h.le_bot ⟨hxz, hzy⟩

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 y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ ε + δ
z : E
hxz : dist z x ≤ δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
exact h.le_bot ⟨hxz, hzy⟩

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (cthickening δ s)

Tactic:
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ, infEDist_cthickening]
    exact tsub_le_iff_right.2

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

Goal state before:
pp: case e'_5
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
n : ℕ
⊢ ↑n * x ^ n = (↑n + 1) * x ^ n - x ^ n

Tactic:
simp [add_mul]

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

Goal state before:
pp: case neg
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f

Tactic:
refine .of_norm_bounded_eventually_nat summable_zero ?_

Goal state after:
case neg
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ 0
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
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝³] U
hf : MapsTo (⇑f) K U
V : Set Y
hVo : IsOpen[inst✝³] V
hKV : ⇑f '' K ⊆ V
hVU : closure[inst✝³] V ⊆ U
g : C(X, Y)
hg : g ∈ closure {x | MapsTo (⇑x) K V}
⊢ MapsTo (⇑(id g)) K U

Tactic:
refine ((isClosed_setOfPred_mapsTo isClosed_closure K).closure_subset ?_).mono_right hVU

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
hU : IsOpen[inst✝³] U
hf : MapsTo (⇑f) K U
V : Set Y
hVo : IsOpen[inst✝³] V
hKV : ⇑f '' K ⊆ V
hVU : closure[inst✝³] V ⊆ U
g : C(X, Y)
hg : g ∈ closure {x | MapsTo (⇑x) K V}
⊢ id g ∈ closure {f | MapsTo (⇑f) K (closure[inst✝³] V)}
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ∀ {γ₁ γ₂ : Path x y}, ⇑γ₁ = ⇑γ₂ → γ₁ = γ₂

Tactic:
by
  rintro ⟨⟨x, h11⟩, h12, h13⟩ ⟨⟨x, h21⟩, h22, h23⟩ rfl
  rfl

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

Goal state before:
pp: case convert_2
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ N : ℕ
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n ↦ f (n + N)) atTop (𝓝 0)
h'' : 0 = ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) 0
⊢ False

Tactic:
simp only [comp_apply, zero_add] at h''

Goal state after:
case convert_2
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ N : ℕ
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n ↦ f (n + N)) atTop (𝓝 0)
h'' : 0 = ‖f N‖
⊢ False
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
⊢ (γ₁.trans γ₂).extend t = γ₁.extend (2 * t)

Tactic:
obtain _ | ht₀ := le_total t 0

Goal state after:
case inl
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
h✝ : t ≤ 0
⊢ (γ₁.trans γ₂).extend t = γ₁.extend (2 * t)

case inr
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ (γ₁.trans γ₂).extend t = γ₁.extend (2 * t)