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 α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ) s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ) K

Tactic:
have : Tendsto (fun (a : Finset ι) ↦ ∑ i ∈ a, μ i s) atTop (𝓝 (Measure.sum μ s)) := by
    simp only [hs, Measure.sum_apply]
    exact ENNReal.summable.hasSum

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∞
hr : r < (sum μ) s
this : Tendsto (fun a ↦ ∑ i ∈ a, (μ i) s) atTop (𝓝 ((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✝⁴ : Group G
inst✝³ : TopologicalSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : ContinuousMul G
inst✝ : BorelSpace G
g : G
⊢ μ {g} = μ {1}

Tactic:
convert! measure_preimage_mul μ g⁻¹ _
  simp only [mul_one, preimage_mul_left_singleton, inv_inv]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → p x

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ NullMeasurableSet {x | f x ≠ 0} μ

Tactic:
· simp only [mem_ofPred]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ NullMeasurableSet {x | f x ≠ 0} μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp.htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f' x ≠ 0}ᶜ → (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

Tactic:
filter_upwards [hf'_ae] with a ha ha_null

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = f' a
ha_null : a ∈ {x | f' x ≠ 0}ᶜ
⊢ ↑(f a) * g a = ↑(f' a) * g' a
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‖ₑ‖ₑ ≠ ∞
ω : α
h₁ : a ≤ X ω
h₂ : X ω ≤ b
⊢ ‖X ω‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ

Tactic:
simp [h₂]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ x ≤ √x ↔ x ≤ 1

Tactic:
obtain hx | hx := le_or_gt x 0
  · simp [hx.trans]
  · rw [le_sqrt' hx, sq, mul_le_iff_le_one_left hx]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∀ (a : α), f a < ∞ → f a = AEMeasurable.mk f hf a → AEMeasurable.mk f hf a < ∞

Tactic:
intro x hx h'x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
x : α
hx : f x < ∞
h'x : f x = AEMeasurable.mk f hf x
⊢ AEMeasurable.mk f hf x < ∞
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
⊢ SFinite μ

Tactic:
obtain ⟨s, h⟩ := exists_sum_smul_dirac μ

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
s : Set α
h : μ = sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x
⊢ SFinite μ
Module: Mathlib.Data.Complex.Basic

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

Tactic:
rw [← @preimage_equivRealProd_prod s t, ← @preimage_equivRealProd_prod s₁ t₁]
  exact Equiv.preimage_subset equivRealProd _ _

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : μ U < ∞
hUf : U ⊆ {x_1 | (fun a ↦ f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ (μ.withDensity fun x ↦ ↑(f x)) U < ∞

Tactic:
rw [withDensity_apply _ hUo.measurableSet]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : μ U < ∞
hUf : U ⊆ {x_1 | (fun a ↦ f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ ∫⁻ (a : α) in U, ↑(f a) ∂μ < ∞
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
f₁ : NormedAddGroupHom V₁ W₁
f₂ : NormedAddGroupHom V₂ W₂
f₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
⊢ (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)

Tactic:
rw [comp_assoc, hf, ← comp_assoc, hf', comp_assoc]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ e (∑'[L] (z : ι), f z) = ∑'[L] (z : ι), e (f z)

Tactic:
refine symm (e.tsum_eq_iff.mpr ?_)
  rw [e.symm_apply_apply _]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
c : ℝ
f : α → E
g' : α → F'
l : Filter α
⊢ (IsBigOWith c l f fun x ↦ ‖g' x‖) ↔ IsBigOWith c l f g'

Tactic:
by
  simp only [IsBigOWith_def, norm_norm]

Goal state after:
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 : ℝ
g : α → F
f' : α → E'
l : Filter α
⊢ IsBigOWith c l (fun x ↦ ‖f' x‖) g ↔ IsBigOWith c l f' g

Tactic:
by
  simp only [IsBigOWith_def, norm_norm]

Goal state after:
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : x = z + y
a : ℕ
p : (z + 1).ascFactorial y = a
⊢ IsNat (n.descFactorial l) a

Tactic:
by
  constructor
  simpa [h₁.out, h₂.out, ← p, h₃] using Nat.add_descFactorial_eq_ascFactorial _ _

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ ∀ i ∈ s, C i * ‖B i x‖ ≤ sSup (C '' ↑s) * ‖B i x‖

Tactic:
intro j hj

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
⊢ C j * ‖B j x‖ ≤ sSup (C '' ↑s) * ‖B j x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case nil
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
hf : ∀ i ∈ [], f i =O[l] g i
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) []).prod) =O[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) []).prod

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
h₁ : ∀ i ∈ [], f i =O[l] g i
h₂ : ∃ i ∈ [], f i =o[l] g i
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) []).prod) =o[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) []).prod

Tactic:
| nil =>

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

Goal state before:
pp: case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ IsBigOWith c l u v → ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Tactic:
intro h
    use fun x => u x / v x
    refine ⟨Eventually.mono h.bound fun y hy => ?_, h.eventually_mul_div_cancel.symm⟩
    simpa using div_le_of_le_mul₀ (norm_nonneg _) hc hy

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedDivisionRing 𝕜
u : α → E'
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
⊢ Tendsto u l (𝓝 0)

Tactic:
suffices h : u =o[l] fun _x => (1 : 𝕜) by
    rwa [isLittleO_one_iff] at h
  exact huv.trans_isBigO (hv.isBigO_one 𝕜)

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ {m ∈ range j | n ≤ m}
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)

Tactic:
rw [mem_filter, mem_range] at hm

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
by rw [← ofReal_sin_ofReal_re, ofReal_im]

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

Goal state before:
pp: x : ℝ
⊢ (cexp (↑x * I)).re = Real.cos x

Tactic:
by
  simp [exp_mul_I, cos_ofReal_re]

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

Goal state before:
pp: n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
rm : ℝ
er : ↑m = rm
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / rm * ((rm + 1) / rm)
⊢ |rexp x - expNear n x a| ≤ |x| ^ n / ↑n.factorial * b

Tactic:
subst er

Goal state after:
n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)
⊢ |rexp x - expNear n x a| ≤ |x| ^ n / ↑n.factorial * b
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
rm : ℝ
er : ↑m = rm
h : |rexp 1 - expNear m 1 ((a₁ - 1) * rm)| ≤ |1| ^ m / ↑m.factorial * (b₁ * rm)
⊢ |rexp 1 - expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁

Tactic:
subst er

Goal state after:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ |rexp 1 - expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ rexp x = rexp (x / 2) ^ 2

Tactic:
grind [Real.exp_nat_mul (x / 2) 2]

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

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

Tactic:
intro j hj

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
⊢ (𝓝 1).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {x | ‖x‖ < ε}

Tactic:
have : ∀ ε : ℝ, mk '' ball (1 : M) ε = {x : M ⧸ S | ‖x‖ < ε} := by
    refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_
    rw [ball_one_eq, mem_ofPred_eq, norm_lt_iff, mem_image]
    exact exists_congr fun _ ↦ and_comm

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), mk '' ball 1 ε = {x | ‖x‖ < ε}
⊢ (𝓝 1).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {x | ‖x‖ < ε}
Module: Mathlib.Analysis.Normed.Group.Pointwise

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

Tactic:
by
  simp [mul_comm _ {y}, mul_comm y]

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

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

Tactic:
by
  simp [mul_comm _ {y}, mul_comm y]

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

Goal state before:
pp: ⊢ tan = fun x ↦ cos⁻¹ x * sin x

Tactic:
simp only [Pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]

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
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x (thickening δ s) ≤ ENNReal.ofReal ε

Tactic:
infEDist_thickening hδ

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos ↑π = -1

Tactic:
by rw [← ofReal_cos, Real.cos_pi]; simp

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

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

Tactic:
infEDist_thickening hδ

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEDist x s - ENNReal.ofReal δ = infEDist x s - ENNReal.ofReal δ
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case nil
M : Type u_4
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l l' : List M
⊢ Joined [].prod [].prod

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: 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)

Tactic:
repeat rw [extend_of_le_zero _ (by linarith)]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ mk ⁻¹' {mk x} = pathComponent x

Tactic:
by
  ext y
  rw [mem_preimage, mem_singleton_iff, eq_comm, mem_pathComponent_iff]
  exact Quotient.eq

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend ⋯ f)
this : Icc (IccExtend ⋯ f 0) (IccExtend ⋯ f 1) ⊆ IccExtend ⋯ f '' Icc 0 1
⊢ ∃ a, f a = t

Tactic:
IccExtend_left,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend ⋯ f)
this : Icc (f ⟨0, ⋯⟩) (IccExtend ⋯ f 1) ⊆ IccExtend ⋯ f '' Icc 0 1
⊢ ∃ a, f a = t
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
⊢ ∀ (x_1 : ℝ), x_1 ∉ Icc (x + ↑z * p - ε) (x + ↑z * p + ε) ∩ s

Tactic:
rintro y ⟨⟨hy₁, hy₂⟩, hy₀⟩

Goal state after:
case 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 + ε
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ (x ∈ range fun x ↦ cexp (↑x * I)) ↔ x ∈ sphere 0 1

Tactic:
simp only [mem_sphere_zero_iff_norm, norm_eq_one_iff, Set.mem_range]

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

Goal state before:
pp: case inl
x y : ℝ
h : log x < y
hx : x ≤ 0
⊢ x < rexp y

pp: case inr
x y : ℝ
h : log x < y
hx : 0 < x
⊢ x < rexp y

Tactic:
· exact hx.trans_lt <| exp_pos y

Goal state after:
case inr
x y : ℝ
h : log x < y
hx : 0 < x
⊢ x < rexp y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case nil
h : ∀ x ∈ [], x ≠ 0
⊢ log [].prod = (List.map (fun x ↦ log x) []).sum

Tactic:
| nil =>

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

Goal state before:
pp: case pos
s : Set ℂ
hs : s.Countable
w : ℂ
hz : cexp w ∈ s
⊢ (⋃ i, {x | x = w + ↑i * (2 * ↑π * I)}).Countable

Tactic:
exact Set.countable_iUnion fun m => Set.countable_singleton _

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

Goal state before:
pp: z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt log {z | 0 ≤ z.im} z

Tactic:
convert!
    (continuous_ofReal.continuousAt.comp_continuousWithinAt
          (continuous_norm.continuousWithinAt.log _)).tendsto.add
      ((continuous_ofReal.continuousAt.comp_continuousWithinAt <|
            continuousWithinAt_arg_of_re_neg_of_im_zero hre him).mul
        tendsto_const_nhds) using 1

Goal state after:
case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
by
  simp only [cpow_def]
  split_ifs <;> simp [*, exp_ne_zero]

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

Goal state before:
pp: θ ψ : ℝ
⊢ cos θ = cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

Tactic:
constructor
  · intro Hcos
    rw [← sub_eq_zero, cos_sub_cos, mul_eq_zero, mul_eq_zero, neg_eq_zero,
      eq_false (two_ne_zero' ℝ), false_or, sin_eq_zero_iff, sin_eq_zero_iff] at Hcos
    rcases Hcos with (⟨n, hn⟩ | ⟨n, hn⟩)
    · right
      rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), ← sub_eq_iff_eq_add] at hn
      rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul,
        mul_comm, coe_two_pi, zsmul_zero]
    · left
      rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), eq_sub_iff_add_eq] at hn
      rw [← hn, coe_add, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero,
        zero_add]
  · rw [angle_eq_iff_two_pi_dvd_sub, ← coe_neg, angle_eq_iff_two_pi_dvd_sub]
    rintro (⟨k, H⟩ | ⟨k, H⟩)
    · rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]
    rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]

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

Goal state before:
pp: θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
⊢ θ + ψ = 2 * ↑k * π + π

Tactic:
rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
        mul_assoc] at H

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

Goal state before:
pp: case h
ψ x✝ : ℝ
⊢ (↑x✝).cos = Real.cos ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ = -↑ψ

Tactic:
exact cos_eq_iff_coe_eq_or_eq_neg

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

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

Tactic:
Real.Angle.sin_coe,

Goal state after:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(‖x‖ * ‖y‖) * (↑(↑(x.arg + y.arg)).cos + ↑(Real.sin (x.arg + y.arg)) * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
n : ℤ
⊢ ↑(x ^ n).arg = n • ↑x.arg

Tactic:
match n with
  | Int.ofNat m => simp [arg_pow_coe_angle]
  | Int.negSucc m => simp [arg_pow_coe_angle]

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

Goal state before:
pp: θ : Angle
⊢ Real.tan θ.toReal = θ.tan

Tactic:
conv_rhs => rw [← coe_toReal θ, tan_coe]

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

Goal state before:
pp: θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ).sign

Tactic:
by
  rw [sign, sign_nonneg_iff]
  exact sin_nonneg_of_nonneg_of_le_pi h0 hpi

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

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ Tendsto (fun x ↦ x ^ y) atTop atTop

Tactic:
(atTop_basis' 0).tendsto_right_iff

Goal state after:
y : ℝ
hy : 0 < y
⊢ ∀ (i : ℝ), 0 ≤ i → ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici i
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: ⊢ Tendsto (fun x ↦ x ^ (1 / x)) atTop (𝓝 1)

Tactic:
convert! tendsto_rpow_div_mul_add (1 : ℝ) _ (0 : ℝ) zero_ne_one

Goal state after:
x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hy : 0 < y
b : ℝ≥0
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y

Tactic:
obtain ⟨c, hc⟩ := tendsto_atTop_atTop.mp (tendsto_rpow_atTop hy) b

Goal state after:
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
θ ψ : 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| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
· simp_all only [sign_coe_pi, ne_eq, zero_ne_one, not_false_eq_true, toReal_pi, coe_add,
      coe_toReal, pi_pos, abs_of_pos]
    obtain rfl : k = 0 := IsStrictOrderedRing.int_eq_of_mul_mem_Ioo two_pi_pos (by grind)
    grind

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℤ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
by
  rw [rpow_mul hx, rpow_intCast]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
by
  rw [rpow_mul hx, rpow_intCast]

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

Goal state before:
pp: a b✝ : ℂ
ha : a ≠ 0
b : ℂ
⊢ a ^ b = cexp (Complex.log a * b)

Tactic:
cpow_def_of_ne_zero ha

Goal state after:
a b✝ : ℂ
ha : a ≠ 0
b : ℂ
⊢ cexp (Complex.log a * b) = cexp (Complex.log a * b)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: z : ℂ
hz : 0 < z.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (0, z)

Tactic:
have hz₀ : z ≠ 0 := ne_of_apply_ne re hz.ne'

Goal state after:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (0, z)