mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝
⊢ AEMeasurable (L.support.mulIndicator (fun i ↦ f i) x✝¹.down) μ

Tactic:
rw [Set.mulIndicator]

Goal state after:
case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝
⊢ AEMeasurable (if x✝¹.down ∈ L.support then f x✝¹.down else 1) μ
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
h : Nonempty ι
⊢ Tendsto (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 (μ (⋂ i, s ∩ notConvergentSeq f g n i)))

Tactic:
refine tendsto_measure_iInter_atTop
    (fun n ↦ (hsm.inter <| notConvergentSeq_measurableSet hf).nullMeasurableSet)
    (fun k l hkl => Set.inter_subset_inter_right _ <| notConvergentSeq_antitone hkl)
    ⟨h.some, ne_top_of_le_ne_top hs (measure_mono Set.inter_subset_left)⟩

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 g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ

Tactic:
← lintegral_add_left' (hf.edist hh)

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (a : α), f_1 a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1) a ∂μ →
            ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
              ∫⁻ (a : α), (f_1 + g) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ

Tactic:
intro g h _ h_mea_g _ h_ind_g h_ind_h

Goal state after:
case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
a✝¹ : Disjoint (Function.support g) (Function.support h)
h_mea_g : Measurable g
a✝ : Measurable h
h_ind_g : ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
h_ind_h : ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ
⊢ ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ENNReal.ofReal (ε / 2 * 2) ≤ ENNReal.ofReal ε

pp: case hf_nonneg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ (n : ℕ), 0 ≤ 2⁻¹ ^ n

pp: case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow 2⁻¹)

Tactic:
div_mul_cancel₀ ε two_ne_zero

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ENNReal.ofReal ε ≤ ENNReal.ofReal ε

case hf_nonneg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ (n : ℕ), 0 ≤ 2⁻¹ ^ n

case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow 2⁻¹)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ √(y * x) = √x * √y

Tactic:
sqrt_mul hy,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ √y * √x = √x * √y
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: r : ℝ
⊢ ‖↑r‖₊ = ‖r‖₊

Tactic:
ext; exact norm_real _

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

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ s, p (f i)
hs_nonempty : s.Nonempty
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Tactic:
· exact le_expect_nonempty_of_subadditive_on_pred h_add hp_add h_div hs_nonempty hs

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

Goal state before:
pp: E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
⊢ ‖1‖ = 1

Tactic:
have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero

Goal state after:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1‖ = 1
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
⊢ ‖↑U * A‖ = ‖A‖

Tactic:
by
  rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)]
  simp [sq, ← CStarRing.norm_star_mul_self, mul_assoc, ← mul_assoc (U : E)⋆]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ re ↑1 = 1

Tactic:
ofReal_re

Goal state after:
K : Type u_1
inst✝ : RCLike K
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: f : ℂ →ₐ[ℝ] ℂ
⊢ f I ^ 2 = I ^ 2

Tactic:
← map_pow,

Goal state after:
f : ℂ →ₐ[ℝ] ℂ
⊢ f (I ^ 2) = I ^ 2
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
⊢ (starRingEnd K) ↑r = ↑r

Tactic:
rw [ext_iff]

Goal state after:
K : Type u_1
inst✝ : RCLike K
r : ℝ
⊢ re ((starRingEnd K) ↑r) = re ↑r ∧ im ((starRingEnd K) ↑r) = im ↑r
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) + ↑(im z) * I - (↑(re z) - ↑(im z) * I) = 2 * ↑(im z) * I

Tactic:
rw [add_sub_sub_cancel, ← two_mul, mul_assoc]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ re ↑↑n = ↑n

Tactic:
ofReal_re

Goal state after:
K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ re ↑↑n = ↑n

Tactic:
ofReal_re

Goal state after:
K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ ↑n = ↑n
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
ofReal_re

Goal state after:
K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ↑q = ↑q
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
ofReal_re

Goal state after:
K : Type u_1
inst✝ : RCLike K
q : ℚ
⊢ ↑q = ↑q
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ re ↑(ofScientific m s e) = ofScientific m s e

Tactic:
ofReal_re

Goal state after:
K : Type u_1
inst✝ : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ ofScientific m s e = ofScientific m s e
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ (2 * re x) ^ 2 = re ↑(2 * re x) ^ 2

Tactic:
ofReal_re

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ (2 * re x) ^ 2 = (2 * re 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
t : Set Y
hs : t ⊆ e.target
⊢ IsOpen[inst✝¹] (↑e.symm '' t) ↔ IsOpen[inst✝] t

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ e.symm.isOpen_image_of_subset_source h hs⟩

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst✝¹] (↑e.symm '' t)
⊢ IsOpen[inst✝] t
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case mp.zero
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
⊢ ∀ᶠ (x : α) in l, ↑0 * ‖f x‖ ≤ ‖g x‖

pp: case mp.succ
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
n : ℕ
⊢ ∀ᶠ (x : α) in l, ↑(n + 1) * ‖f x‖ ≤ ‖g x‖

Tactic:
· refine (H.def one_pos).mono fun x h₀' => ?_
      rw [Nat.cast_zero, zero_mul]
      refine h₀.elim (fun hf => (hf x).trans ?_) fun hg => hg x
      rwa [one_mul] at h₀'

Goal state after:
case mp.succ
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
n : ℕ
⊢ ∀ᶠ (x : α) in l, ↑(n + 1) * ‖f x‖ ≤ ‖g x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1 + 1), 0 ^ m / ↑m.factorial - 1‖ = 0

Tactic:
rw [← ih (by simp)]
      simp only [sum_range_succ, pow_succ]
      simp

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

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (x : ℝ) in map (fun x ↦ ‖f x / g x‖) l, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ f =O[l] g

Tactic:
simp only [eventually_map, norm_div] at hc

Goal state after:
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
⊢ f =O[l] g
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℝ
h : x < y
⊢ rexp x < rexp y

Tactic:
← sub_add_cancel y x,

Goal state after:
x y : ℝ
h : x < y
⊢ rexp x < rexp (y - x + x)
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'' → F''
x₀ : E''
n : ℕ
h : f =O[𝓝 x₀] fun x ↦ ‖x - x₀‖ ^ n
hn : n ≠ 0
⊢ f x₀ = 0

Tactic:
rw [← nhdsWithin_univ] at h
  exact h.eq_zero_of_norm_pow_within (mem_univ _) hn

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

Goal state before:
pp: ⊢ tan 0 = 0

Tactic:
by simp [tan]

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

Goal state before:
pp: x : ℝ
⊢ tan (-x) = -tan x

Tactic:
by simp [tan]

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

Goal state before:
pp: n : ℕ
x r₁ r₂ : ℝ
⊢ expNear n x r₁ - expNear n x r₂ = x ^ n / ↑n.factorial * (r₁ - r₂)

Tactic:
by
  simp [expNear, mul_sub]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
a x : α
hx1 : |x| < 1
⊢ IsCauSeq abs fun m ↦ ∑ n ∈ range m, a * x ^ n

Tactic:
simpa [mul_sum, Pi.mul_def] using (const a).mul (geo_series x hx1)

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ (rexp ∘ f) x) l atTop ↔ Tendsto f l atTop

Tactic:
← tendsto_comap_iff,

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto f l (comap rexp atTop) ↔ Tendsto f l atTop
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ (rexp ∘ f) x) l (𝓝 0) ↔ Tendsto f l atBot

Tactic:
← tendsto_comap_iff,

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto f l (comap rexp (𝓝 0)) ↔ Tendsto f l atBot
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ sin (x - π / 2) = -cos x

Tactic:
by simp [sub_eq_add_neg, sin_add]

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

Goal state before:
pp: x : ℝ
⊢ sin (π / 2 - x) = cos x

Tactic:
by simp [sub_eq_add_neg, sin_add]

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

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

Tactic:
rw [← comap_norm_nhds_zero, comap_comap, Function.comp_def]

Goal state after:
⊢ comap (fun x ↦ ‖cexp x‖) (𝓝 0) = comap re (comap Real.exp (𝓝 0))
Module: Mathlib.Analysis.SpecialFunctions.Exp

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

Tactic:
rw [← comap_norm_nhds_zero, comap_comap, Function.comp_def]
      simp_rw [norm_exp, comap_comap, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (fun x ↦ (cexp ∘ f) x) l (𝓝 0) ↔ Tendsto (fun x ↦ (f x).re) l atBot

Tactic:
← tendsto_comap_iff,

Goal state after:
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto f l (comap cexp (𝓝 0)) ↔ Tendsto (fun x ↦ (f x).re) l atBot
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:
ball_mul_singleton

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
hker : x ∈ S.normedMk.ker.topologicalClosure
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖

Tactic:
rw [ker_normedMk] at hker

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
hker : x ∈ S.topologicalClosure
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
⊢ g = lift S f hf

Tactic:
ext x
  rcases AddSubgroup.surjective_normedMk _ x with ⟨x, rfl⟩
  change g.comp S.normedMk x = _
  simp only [h]
  rfl

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 z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ∃ y, dist x y < δ ∧ dist y z < ε

Tactic:
refine (exists_dist_eq x z (div_nonneg hε.le <| add_nonneg hε.le hδ.le)
    (div_nonneg hδ.le <| add_nonneg hε.le hδ.le) <| by
      rw [← add_div, div_self (add_pos hε hδ).ne']).imp
    fun y hy => ?_

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y < δ ∧ dist y z < ε
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n ↦ ↑(n ^ k) * ‖r‖ ^ n) =O[atTop] fun n ↦ r' ^ n

Tactic:
simp only [cast_pow]
      exact (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO

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

Goal state before:
pp: case inr.top
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
h : edist x z < ∞
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < ∞

Tactic:
| top =>

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

Goal state before:
pp: case h1
⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝 0)

Tactic:
convert! continuous_cos.continuousWithinAt.tendsto

Goal state after:
case e'_5
⊢ 0 = cos (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case h1
⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 0)

Tactic:
convert! continuous_cos.continuousWithinAt.tendsto

Goal state after:
case e'_5
⊢ 0 = cos (-(π / 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℂ
⊢ sin (x - ↑π / 2) = -cos x

Tactic:
by simp [sub_eq_add_neg, sin_add]

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

Goal state before:
pp: x : ℂ
⊢ sin (↑π / 2 - x) = cos x

Tactic:
by simp [sub_eq_add_neg, sin_add]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
x : E
⊢ thickening (ε + δ) {x} = Metric.ball x (ε + δ)

Tactic:
thickening_singleton

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
x : E
⊢ Metric.ball x (ε + δ) = Metric.ball x (ε + δ)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
x : E
⊢ thickening (ε + δ) {x} = Metric.ball x (ε + δ)

Tactic:
thickening_singleton

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
x : E
⊢ Metric.ball x (ε + δ) = Metric.ball x (ε + δ)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
⊢ Summable f

Tactic:
refine summable_of_ratio_norm_eventually_le hr₁ ?_

Goal state after:
α : Type u_4
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
⊢ ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: a : ℝ
ha : a ≠ 0
⊢ Tendsto (⇑((zmultiplesHom ℝ) a)) Filter.cofinite (cocompact ℝ)

Tactic:
apply (zmultiplesHom ℝ a).tendsto_coe_cofinite_of_discrete <| smul_left_injective ℤ ha
  rw [AddSubgroup.range_zmultiplesHom, SetLike.isDiscrete_iff_discreteTopology]
  infer_instance

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
f : Y → Path x y
g : Y → Path y z
hf : Continuous[inst✝, _] f
hg : Continuous[inst✝, _] g
⊢ Continuous[inst✝, _] fun t ↦ (f t).trans (g t)

Tactic:
apply continuous_uncurry_iff.mp

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
f : Y → Path x y
g : Y → Path y z
hf : Continuous[inst✝, _] f
hg : Continuous[inst✝, _] g
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ (f t).trans (g t)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
x : ℂ
hx : x ≠ 0
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x

Tactic:
have : ‖x‖ ≠ 0 := norm_ne_zero_iff.mpr hx

Goal state after:
case inr
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

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

Tactic:
add_assoc

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ |log x * x| < 1

Tactic:
have : 0 < 1 / x := by simpa only [one_div, inv_pos] using h1
  replace := log_le_sub_one_of_pos this
  replace : log (1 / x) < 1 / x := by linarith
  rw [log_div one_ne_zero h1.ne', log_one, zero_sub, lt_div_iff₀ h1] at this
  have aux : 0 ≤ -log x * x := by
    refine mul_nonneg ?_ h1.le
    rw [← log_inv]
    apply log_nonneg
    rw [← le_inv_comm₀ h1 zero_lt_one, inv_one]
    exact h2
  rw [← abs_of_nonneg aux, neg_mul, abs_neg] at this
  exact this

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

Goal state before:
pp: case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π = (θ + ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

Tactic:
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]

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

Goal state before:
pp: case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ

Tactic:
rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), eq_sub_iff_add_eq] at hn

Goal state after:
case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 + ψ = θ
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log e

Tactic:
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have : 1 < (n : ℝ) / d := by
      simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h)
    exact Real.log_pos this

Goal state after: