mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: case inl
α : 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 : IsEmpty ι
⊢ Tendsto (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

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 (𝓝 0)

Tactic:
· have : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0 := by
      simp only [eq_iff_true_of_subsingleton]
    rw [this]
    exact tendsto_const_nhds

Goal state after:
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 (𝓝 0)
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✝ : 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 : ℕ
⊢ Tendsto (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Tactic:
by
  rcases isEmpty_or_nonempty ι with h | h
  · have : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0 := by
      simp only [eq_iff_true_of_subsingleton]
    rw [this]
    exact tendsto_const_nhds
  rw [← measure_inter_notConvergentSeq_eq_zero hfg n, Set.inter_iInter]
  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.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ count.withDensity f = sum fun a ↦ f a • dirac a

Tactic:
simp [count, withDensity_sum, dirac_withDensity' hf _]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : ¬f x = ∞
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Tactic:
lift f x to ℝ≥0 using hfx with fx h
    simp

Goal state after:
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))
⊢ ∀ ε_1 > 0, ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg, edist (g x) (f n x) < ε_1

Tactic:
intro δ hδ

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))
δ : ℝ≥0∞
hδ : δ > 0
⊢ ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg, edist (g x) (f n x) < δ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ Continuous fun x ↦ √x

Tactic:
by unfold sqrt; fun_prop

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n ↦ (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n ↦ (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |↑(⟨fun n ↦ (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).re, ⋯⟩)) j| < ε / 2
H₂ : |↑(⟨fun n ↦ (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).im, ⋯⟩)) j| < ε / 2
⊢ (fun x ↦ ‖x‖) (↑(f - CauSeq.const (fun x ↦ ‖x‖) (limAux f)) j) < ε

Tactic:
apply lt_of_le_of_lt (norm_le_abs_re_add_abs_im _)

Goal state after:
f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n ↦ (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n ↦ (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |↑(⟨fun n ↦ (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).re, ⋯⟩)) j| < ε / 2
H₂ : |↑(⟨fun n ↦ (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).im, ⋯⟩)) j| < ε / 2
⊢ |(↑(f - CauSeq.const (fun x ↦ ‖x‖) (limAux f)) j).re| + |(↑(f - CauSeq.const (fun x ↦ ‖x‖) (limAux f)) j).im| < ε
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z w : ℂ
⊢ z.re < w.re ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)

Tactic:
rw [lt_iff_le_not_ge]
    tauto

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f g : ι → α
h : 𝔼 i ∈ s, g i < 𝔼 i ∈ s, f i
⊢ ∃ x ∈ s, g x < f x

Tactic:
contrapose! h; exact expect_le_expect h

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

Goal state before:
pp: case right
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'
g : V₁
k_in : f g ∈ K
hg : ‖g‖ ≤ C * ‖f g‖
⊢ ‖g‖ ≤ C' * ‖f g‖

Tactic:
by_cases Hg : ‖f g‖ = 0

Goal state after:
case pos
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'
g : V₁
k_in : f g ∈ K
hg : ‖g‖ ≤ C * ‖f g‖
Hg : ‖f g‖ = 0
⊢ ‖g‖ ≤ C' * ‖f g‖

case neg
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'
g : V₁
k_in : f g ∈ K
hg : ‖g‖ ≤ C * ‖f g‖
Hg : ¬‖f g‖ = 0
⊢ ‖g‖ ≤ C' * ‖f g‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₂ V₃
⊢ f.comp 0 = 0

Tactic:
ext
  exact map_zero f

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : R
hu : IsUnit u
⊢ star u ∈ unitary R ↔ u * star u = 1

Tactic:
hu.star.mem_unitary_iff_star_mul_self,

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : R
hu : IsUnit u
⊢ star (star u) * star u = 1 ↔ u * star u = 1
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a b : Rˣ
⊢ ↑a * ↑b⁻¹ ∈ unitary R ↔ star a * a = star b * b

Tactic:
by
  simp [← mul_inv_mem_iff, Units.unitary_eq]

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

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Star E
inst✝¹ : Module ℂ E
inst✝ : StarModule ℂ E
r : ℝ
a : E
⊢ (star r • 1) • star a = star r • star a

Tactic:
smul_one_smul

Goal state after:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Star E
inst✝¹ : Module ℂ E
inst✝ : StarModule ℂ E
r : ℝ
a : E
⊢ star r • star a = star r • star a
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝⁴ : RCLike K
inst✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ K E
r : ℝ
x : E
⊢ r • x = (r • 1) • x

Tactic:
smul_one_smul

Goal state after:
K : Type u_1
E : Type u_2
inst✝⁴ : RCLike K
inst✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ K E
r : ℝ
x : E
⊢ r • x = r • x
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsEmbedding (e.source.domRestrict ↑e.toPartialEquiv)

Tactic:
by
  rw [isEmbedding_iff]
  constructor
  · apply Topology.IsInducing.of_codRestrict (t := e.target) (by simp)
    rw [← PartialEquiv.toEquiv_eq_codRestrict_restrict]
    exact e.toHomeomorphSourceTarget.isInducing
  · rw [domRestrict_eq, toFun_eq_coe e, e.injOn.injective_iff e.source (by simp)]
    exact Subtype.val_injective

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ z ↔ 0 ≤ re z ∧ im z = 0

Tactic:
simpa only [map_zero, eq_comm] using le_iff_re_im (z := 0) (w := z)

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e y ∈ ↑e.symm ⁻¹' s ↔ ↑e y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
simp_rw [mem_inter_iff, mem_preimage, mem_inter_iff, e.mapsTo hy, true_and, iff_self_and,
    e.left_inv hy, iff_true_intro hyu]

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

Goal state before:
pp: case mpr
α : 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‖
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖) → f =o[l] g

Tactic:
· refine fun H => isLittleO_iff.2 fun ε ε0 => ?_
    rcases exists_nat_gt ε⁻¹ with ⟨n, hn⟩
    have hn₀ : (0 : ℝ) < n := (inv_pos.2 ε0).trans hn
    refine ((isBigOWith_inv hn₀).2 (H n)).bound.mono fun x hfg => ?_
    refine hfg.trans (mul_le_mul_of_nonneg_right (inv_le_of_inv_le₀ ε0 hn.le) ?_)
    refine h₀.elim (fun hf => nonneg_of_mul_nonneg_right ((hf x).trans hfg) ?_) fun h => h x
    exact inv_pos.2 hn₀

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ c₁ * ‖g₁ x‖ + c₂ * ‖g₂ x‖ ≤ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖

Tactic:
gcongr <;> simp [le_max_left _ _, le_max_right _ _]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁵ : Semiring R
inst✝³⁴ : Semiring R₂
inst✝³³ : Semiring R₃
inst✝³² : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁹ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁸ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁷ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁶ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁵ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁴ : RingHomInvPair σ₄₁ σ₁₄
inst✝²³ : RingHomInvPair σ₂₄ σ₄₂
inst✝²² : RingHomInvPair σ₄₂ σ₂₄
inst✝²¹ : RingHomInvPair σ₃₄ σ₄₃
inst✝²⁰ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁶ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁴ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹² : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup E₂
inst✝⁹ : SeminormedAddCommGroup E₃
inst✝⁸ : SeminormedAddCommGroup E₄
inst✝⁷ : Module R E
inst✝⁶ : Module R₂ E₂
inst✝⁵ : Module R₃ E₃
inst✝⁴ : Module R₄ E₄
inst✝³ : NormedAddCommGroup F
inst✝² : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝¹ : TopologicalSpace α
inst✝ : Module R E₂
⊢ ∀ (x : E × E₂), ‖(LinearEquiv.prodComm R E E₂) x‖ = ‖x‖

Tactic:
intro; simp [norm, sup_comm]

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

Goal state before:
pp: x y : ℂ
⊢ ∀ (x y : Multiplicative ℂ),
    cexp (Multiplicative.toAdd (x * y)) = cexp (Multiplicative.toAdd x) * cexp (Multiplicative.toAdd y)

Tactic:
by simp [exp_add]

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

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

Tactic:
by rw [← exp_conj, conj_ofReal]

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

Goal state before:
pp: x y : ℝ
⊢ ∀ (x y : Multiplicative ℝ),
    rexp (Multiplicative.toAdd (x * y)) = rexp (Multiplicative.toAdd x) * rexp (Multiplicative.toAdd y)

Tactic:
by simp [exp_add]

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

Goal state before:
pp: x : ℂ
⊢ cosh x - sinh x = cexp (-x)

Tactic:
by
  rw [← mul_right_inj' (two_ne_zero' ℂ), mul_sub, two_cosh, two_sinh, add_sub_sub_cancel, two_mul]

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

Goal state before:
pp: case hba
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ range (j - n)
⊢ n.factorial * n.succ ^ x ≤ (n + x).factorial

Tactic:
exact Nat.factorial_mul_pow_le_factorial

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

Goal state before:
pp: ⊢ cos 0 = 1

Tactic:
simp [cos]

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

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

Tactic:
rw [← cosh_mul_I, add_mul, cosh_add, cosh_mul_I, cosh_mul_I, sinh_mul_I, sinh_mul_I,
    mul_mul_mul_comm, I_mul_I, mul_neg_one, sub_eq_add_neg]

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

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

Tactic:
by
  have s1 := sin_add ((x + y) / 2) ((x - y) / 2)
  have s2 := sin_sub ((x + y) / 2) ((x - y) / 2)
  rw [← add_div, add_sub, add_right_comm, add_sub_cancel_right, add_self_div_two] at s1
  rw [div_sub_div_same, ← sub_add, add_sub_cancel_left, add_self_div_two] at s2
  rw [s1, s2]
  ring

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

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

Tactic:
simp [cos]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ (∑ m ∈ range 3, (x / 2) ^ m / ↑m.factorial + (x / 2) ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3)) ^ 2 <
    (2 + x) / (2 - x)

Tactic:
rw [lt_div_iff₀ (by linarith), ← sub_pos]
    simp only [Finset.sum_range_succ]
    ring_nf
    positivity

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

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
⊢ cexp x - cexp y = cexp y * (cexp (x - y) - 1)

Tactic:
rw [mul_sub_one, ← exp_add]

Goal state after:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
⊢ cexp x - cexp y = cexp (y + (x - y)) - cexp y
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
⊢ IsCauSeq abv fun n ↦ ∑ m ∈ range n, x ^ m

Tactic:
by
  have hx1' : abv x ≠ 1 := fun h ↦ by simp [h] at hx1
  refine of_abv ?_
  simp only [abv_pow abv, geom_sum_eq hx1']
  conv in _ / _ => rw [← neg_div_neg_eq, neg_sub, neg_sub]
  have : 0 < 1 - abv x := sub_pos.2 hx1
  refine of_mono_bounded _ (a := (1 : α) / (1 - abv x)) (m := 0) ?_ ?_
  · intro n _
    rw [abs_of_nonneg]
    · gcongr
      exact sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _)
    refine div_nonneg (sub_nonneg.2 ?_) (sub_nonneg.2 <| le_of_lt hx1)
    exact pow_le_one₀ (by positivity) hx1.le
  · intro n _
    rw [← one_mul (abv x ^ n), pow_succ']
    gcongr

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ closedBall 1 δ * s = cthickening δ s

Tactic:
by rw [mul_comm, hs.mul_closedBall_one hδ]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ (infEDist (c • x) (c • s)).toReal = ‖c‖ * (infEDist x s).toReal

Tactic:
infEDist_smul₀ hc s,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ (‖c‖₊ • infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ hc]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ hc]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ StrictMonoOn tan (Ioo (-(π / 2)) (π / 2))

Tactic:
rintro x hx y hy hlt
  rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos,
    div_lt_div_iff₀ (cos_pos_of_mem_Ioo hx) (cos_pos_of_mem_Ioo hy), mul_comm, ← sub_pos, ← sin_sub]
  exact sin_pos_of_pos_of_lt_pi (sub_pos.2 hlt) <| by linarith [hx.1, hy.2]

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

Goal state before:
pp: ⊢ tan π = 0

Tactic:
rw [tan_periodic.eq, tan_zero]

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
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
n : ℕ
⊢ ↑((n + (k + 1)).choose (k + 1)) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), ↑((k_1 + k).choose k) * r ^ k_1 * r ^ (n - k_1)

Tactic:
have : ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) =
            ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n := by
          apply Finset.sum_congr rfl (fun i hi ↦ ?_)
          simp only [Finset.mem_range] at hi
          rw [mul_assoc, ← pow_add, show i + (n - i) = n by lia]
        simp [this, ← sum_mul, ← Nat.cast_sum, sum_range_add_choose n k, add_assoc]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
⊢ ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s

Tactic:
rcases ContinuousMap.mem_nhds_iff.mp hs with ⟨S, hSf, hS, hSsub⟩
    choose hScompact hSopen hSmaps using hS
    have : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c := by
      simp only [biInter_mem hSf, Prod.forall, iInter_mem]
      rintro K U hKU ⟨x, hx⟩
      exact (hSopen K U hKU).mem_nhds <| hSmaps K U hKU hx
    rcases h.mem_iff.mp this with ⟨i, hpi, hi⟩
    refine ⟨(⋃ KU ∈ S, KU.1, i), ⟨hSf.isCompact_biUnion <| Prod.forall.2 hScompact, hpi⟩,
      Subset.trans ?_ hSsub⟩
    intro f hf K V hKV
    rcases K.eq_empty_or_nonempty with rfl | hKne
    · exact mapsTo_empty _ _
    · refine hf.out.mono (subset_biUnion_of_mem (u := Prod.fst) hKV) (hi.trans ?_)
      exact (biInter_subset_of_mem hKV).trans <| iInter_subset _ hKne

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ compactOpen = ⨅ K, ⨅ (_ : IsCompact K), induced (restrict K) compactOpen

Tactic:
refine le_antisymm (le_iInf₂ fun s _ ↦ compactOpen_le_induced s) ?_

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ ⨅ K, ⨅ (_ : IsCompact K), induced (restrict K) compactOpen ≤ compactOpen
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p (last n))
hγ : range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
rcases hγ with ⟨h₁, h₂⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p (last n))
h₁ : range ⇑γ ⊆ s
h₂ : ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
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
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst✝¹, inst✝] f
t : ↑I
⊢ ((γ.trans γ').map h) t = if h_1 : ↑t ≤ 1 / 2 then (γ.map h) ⟨2 * ↑t, ⋯⟩ else (γ'.map h) ⟨2 * ↑t - 1, ⋯⟩

Tactic:
map_coe,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst✝¹, inst✝] f
t : ↑I
⊢ (f ∘ ⇑(γ.trans γ')) t = if h_1 : ↑t ≤ 1 / 2 then (γ.map h) ⟨2 * ↑t, ⋯⟩ else (γ'.map h) ⟨2 * ↑t - 1, ⋯⟩