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

Goal state before:
pp: case iUnion
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Function.onFun Disjoint f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ) (ε : ℝ≥0∞),
            ε ≠ 0 →
              ∃ F ⊆ f i, ∃ U ⊇ f i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (f i) ≤ μ F + ε ∧ μ U ≤ μ (f i) + ε) →
          ∀ (ε : ℝ≥0∞),
            ε ≠ 0 →
              ∃ F ⊆ ⋃ i, f i,
                ∃ U ⊇ ⋃ i, f i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (⋃ i, f i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, f i) + ε

Tactic:
intro s

Goal state after:
case iUnion
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
⊢ Pairwise (Function.onFun Disjoint s) →
    (∀ (i : ℕ), MeasurableSet (s i)) →
      (∀ (i : ℕ) (ε : ℝ≥0∞),
          ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε) →
        ∀ (ε : ℝ≥0∞),
          ε ≠ 0 →
            ∃ F ⊆ ⋃ i, s i,
              ∃ U ⊇ ⋃ i, s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (⋃ i, s i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, s i) + ε
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
μ' : Measure α
inst✝ : SFinite μ'
⊢ (μ + μ').prod ν = μ.prod ν + μ'.prod ν

Tactic:
by
  simp_rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq μ', sum_add_sum, ← sum_sfiniteSeq ν, prod_sum,
    sum_add_sum]
  congr
  ext1 i
  refine prod_eq fun s t _ _ => ?_
  simp_rw [add_apply, prod_prod, right_distrib]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
⊢ borel γ ≤ borel γ

Tactic:
intro s

Goal state after:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
⊢ MeasurableSet s → MeasurableSet s
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul G
H : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s ↑H
hs' : Finite ↑s
⊢ ∑' (a : ↑s), μ (↑a • ↑H) = μ univ

Tactic:
by
      rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]
      · simp [hs.mul_eq]
      · exact fun a b hab ↦ hs.pairwiseDisjoint_smul a.2 b.2 (Subtype.val_injective.ne hab)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
⊢ (μ + ν).InnerRegularWRT IsCompact MeasurableSet

Tactic:
intro s

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
⊢ (μ + ν).InnerRegular

Tactic:
constructor
  intro s hs r hr
  simp only [Measure.coe_add, Pi.add_apply] at hr
  rcases eq_or_ne (μ s) 0 with h | h
  · simp only [h, zero_add] at hr
    rcases MeasurableSet.exists_lt_isCompact hs hr with ⟨K, Ks, hK, h'K⟩
    exact ⟨K, Ks, hK, h'K.trans_le (by simp)⟩
  rcases eq_or_ne (ν s) 0 with h' | h'
  · simp only [h', add_zero] at hr
    rcases MeasurableSet.exists_lt_isCompact hs hr with ⟨K, Ks, hK, h'K⟩
    exact ⟨K, Ks, hK, h'K.trans_le (by simp)⟩
  rcases ENNReal.exists_lt_add_of_lt_add hr h h' with ⟨u, hu, v, hv, huv⟩
  rcases MeasurableSet.exists_lt_isCompact hs hu with ⟨K, Ks, hK, h'K⟩
  rcases MeasurableSet.exists_lt_isCompact hs hv with ⟨K', K's, hK', h'K'⟩
  refine ⟨K ∪ K', union_subset Ks K's, hK.union hK', huv.trans_le ?_⟩
  apply (add_le_add h'K.le h'K'.le).trans
  simp only [Measure.coe_add, Pi.add_apply]
  gcongr <;> simp

Goal state after:
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
⊢ (sum μ).InnerRegularWRT IsCompact MeasurableSet

Tactic:
intro s

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ) s
⊢ Tendsto (fun a ↦ ∑ i ∈ a, (μ i) s) atTop (𝓝 ((sum μ) s))

Tactic:
simp only [hs, Measure.sum_apply]

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
⊢ Tendsto (fun a ↦ ∑ i ∈ a, (μ i) s) atTop (𝓝 (∑' (i : ι), (μ i) s))
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 : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
⊢ ∃ U, IsOpen[inst✝⁴] U ∧ μ U < ∞ ∧ μ (U ∆ s) < ε

Tactic:
rcases hKco.exists_isOpen_lt_add (μ := μ) this with ⟨U, hKU, hUo, hμU⟩

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ ∃ U, IsOpen[inst✝⁴] U ∧ μ U < ∞ ∧ μ (U ∆ s) < ε
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ ((μ.withDensity f).restrict s) t = ((μ.restrict s).withDensity f) t

Tactic:
rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply' _ (t ∩ s),
    restrict_restrict ht]

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
μ : Measure G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h : μ.InnerRegularCompactLTTop
⊢ μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed[inst✝³] s) fun s ↦ MeasurableSet s ∧ μ s ≠ ∞

Tactic:
intro s

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ.withDensity f = 0 ↔ f =ᵐ[μ] 0

Tactic:
rw [← measure_univ_eq_zero, withDensity_apply _ .univ, restrict_univ, lintegral_eq_zero_iff' hf]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
⊢ (c • μ).InnerRegularWRT IsCompact fun s ↦ MeasurableSet s ∧ (c • μ) s ≠ ∞

Tactic:
intro s

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous[inst✝⁴, inst✝¹] f
⊢ (map f μ).InnerRegularCompactLTTop

Tactic:
constructor
  refine InnerRegularWRT.map h.innerRegular hf.aemeasurable ?_ (fun K hK ↦ hK.image hf) ?_
  · rintro s ⟨hs, h's⟩
    exact ⟨hf.measurable hs, by rwa [map_apply hf.measurable hs] at h's⟩
  · rintro s ⟨hs, -⟩
    exact hs

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝¹ : MeasurableSpace β
f : β → α → ℝ≥0∞
inst✝ : SFinite μ
hf : Measurable (Function.uncurry f)
⊢ ∀ (s : Set α), MeasurableSet s → Measurable fun b ↦ (μ.withDensity (f b)) s

Tactic:
intro s

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝¹ : MeasurableSpace β
f : β → α → ℝ≥0∞
inst✝ : SFinite μ
hf : Measurable (Function.uncurry f)
s : Set α
⊢ MeasurableSet s → Measurable fun b ↦ (μ.withDensity (f b)) s
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))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N)⁻¹ < δ
⊢ ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg, edist (g x) (f n x) < δ

Tactic:
rw [eventually_atTop]

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 : ℕ
hN : (↑N)⁻¹ < δ
⊢ ∃ a, ∀ (b : ι), a ≤ b → ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg, edist (g x) (f b x) < δ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x < y ↔ √x < √(y ^ 2)

Tactic:
sqrt_sq hy

Goal state after:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x < y ↔ √x < y
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
h : z.re = w.re
⊢ edist z w = edist z.im w.im

Tactic:
rw [edist_nndist, edist_nndist, nndist_of_re_eq h]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
⊢ μ.withDensity f = μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f)

Tactic:
by
      simp (disch := measurability) [withDensity_indicator, ← restrict_withDensity]

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

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

Tactic:
← @preimage_equivRealProd_prod s t,

Goal state after:
s s₁ t t₁ : Set ℝ
⊢ ⇑equivRealProd ⁻¹' s ×ˢ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g = ∫⁻ (y : β), ((fun z ↦ g z.2) * φ) (x, y) ∂ν

Tactic:
rw [lintegral_withDensity_eq_lintegral_mul₀ hg (by fun_prop)]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ ∫⁻ (a : β), (g * fun y ↦ φ (x, y)) a ∂ν = ∫⁻ (y : β), ((fun z ↦ g z.2) * φ) (x, y) ∂ν
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: M : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
μ ν : Measure M
inst✝ : SFinite ν
s : ℝ≥0∞
⊢ map (fun x ↦ x.1 * x.2) (μ.prod (s • ν)) = s • map (fun x ↦ x.1 * x.2) (μ.prod ν)

Tactic:
Measure.prod_smul_right,

Goal state after:
M : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
μ ν : Measure M
inst✝ : SFinite ν
s : ℝ≥0∞
⊢ map (fun x ↦ x.1 * x.2) (s • μ.prod ν) = s • map (fun x ↦ x.1 * x.2) (μ.prod ν)
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₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : dist (r • f x) (r • f 0) ≤ dist r 0 * dist (f x) (f 0)
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * b * ‖x‖

Tactic:
rw [map_zero, smul_zero, dist_zero_right, dist_zero_right] at this

Goal state after:
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₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : ‖r • f x‖ ≤ dist r 0 * ‖f x‖
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * b * ‖x‖
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:
by
  have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero
  rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : ℝ
n : ℕ
⊢ im (↑a ^ n) = 0

Tactic:
by
  rw [← @ofReal_pow, @ofReal_im_ax]

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

Goal state before:
pp: z : ℂ
⊢ ‖equivRealProd z‖ ≤ 1 * ‖z‖

Tactic:
by
  simpa using equivRealProd_apply_le z

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

Goal state before:

Tactic:
‖im x - im y‖ₑ
  _ = ‖im (x - y)‖ₑ := by rw [map_sub im x y]
  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_im_le_norm (x - y)

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ 1 * ‖g x‖

Tactic:
rw [one_mul]
    exact hfg x

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

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
hn : 0 < n.succ
⊢ (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ

Tactic:
clear hn

Goal state after:
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
⊢ (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case inl
α : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Norm E
inst✝³ : Norm F
f : α → E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
c : ℝ
b : α
hc : ∀ᶠ (a : α) in 𝓝[≠] b, ‖f a‖ ≤ c
hb : b ∈ {b}ᶜ → ‖f b‖ ≤ c
⊢ ‖f b‖ ≤ max c ‖f b‖

Tactic:
apply le_max_right

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

Goal state before:
pp: case inr
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x ≠ 0
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖

Tactic:
have hc : 0 < c := pos_of_mul_pos_left ((norm_pos_iff.2 hx).trans_le hle) (norm_nonneg _)
    replace hle := inv_anti₀ (norm_pos_iff.2 hx) hle
    simpa only [norm_inv, mul_inv, ← div_eq_inv_mul, div_le_iff₀ hc] using! hle

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

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

Tactic:
by
  have hj : ∀ j : ℕ, (∑ m ∈ range j, (x + y) ^ m / m.factorial) =
        ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / k.factorial *
          (y ^ (i - k) / (i - k).factorial) := by
    intro j
    refine Finset.sum_congr rfl fun m _ => ?_
    rw [add_pow, div_eq_mul_inv, sum_mul]
    refine Finset.sum_congr rfl fun I hi => ?_
    have h₁ : (m.choose I : ℂ) ≠ 0 :=
      Nat.cast_ne_zero.2 (pos_iff_ne_zero.1 (Nat.choose_pos (Nat.le_of_lt_succ (mem_range.1 hi))))
    have h₂ := Nat.choose_mul_factorial_mul_factorial (Nat.le_of_lt_succ <| Finset.mem_range.1 hi)
    rw [← h₂, Nat.cast_mul, Nat.cast_mul, mul_inv, mul_inv]
    simp only [mul_left_comm (m.choose I : ℂ), mul_assoc, mul_left_comm (m.choose I : ℂ)⁻¹,
      mul_comm (m.choose I : ℂ)]
    rw [inv_mul_cancel₀ h₁]
    simp [div_eq_mul_inv, mul_assoc, mul_left_comm]
  simp_rw [exp, exp', lim_mul_lim]
  apply (lim_eq_lim_of_equiv _).symm
  simp only [hj]
  exact cauchy_product (isCauSeq_norm_exp x) (isCauSeq_exp y)

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

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

Tactic:
have s2 := sin_sub ((x + y) / 2) ((x - y) / 2)

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

Goal state before:
pp: x : ℂ
⊢ sin x ^ 2 + cos x ^ 2 = cosh (x * I) ^ 2 - sinh (x * I) ^ 2

Tactic:
rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm]

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

Goal state before:
pp: x : ℂ
⊢ cos (2 * x) = 2 * cos x ^ 2 - 1

Tactic:
by
  rw [cos_two_mul', eq_sub_iff_add_eq.2 (sin_sq_add_cos_sq x), ← sub_add, sub_add_eq_add_sub,
    two_mul]

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

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

Tactic:
norm_I,

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-↑(x / 2) * I) * (1 - cexp (↑x * I))‖ * 1
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case ha
x : ℝ
hx : 0 < x
hx' : x < 2
⊢ 0 ≤ rexp (x / 2)

Tactic:
apply Real.exp_nonneg

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

Goal state before:
pp: case refine_2
α : 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
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)

Tactic:
← one_mul (abv x ^ n),

Goal state after:
case refine_2
α : 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
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ (1 - 1 * abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)
Module: Mathlib.Analysis.SpecificLimits.Normed

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

Tactic:
rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ (abs_nonneg _).trans (H n) with (rfl | ⟨hC₀, ha₀⟩)
    · obtain rfl : f = 0 := by
        ext n
        simpa using H n
      simp only [lt_irrefl, false_or] at h₀
      exact ⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, isBigO_zero _ _⟩
    exact ⟨a, A ⟨ha₀, ha⟩,
      isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩

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

Goal state before:
pp: ⊢ comap cexp (𝓝[≠] 0) = comap re atBot

Tactic:
have : (exp ⁻¹' {0})ᶜ = Set.univ := eq_univ_of_forall exp_ne_zero

Goal state after:
this : (cexp ⁻¹' {0})ᶜ = Set.univ
⊢ comap cexp (𝓝[≠] 0) = comap re atBot
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: case h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m m' : M
⊢ 0 ≤ (fun m_1 ↦ ‖m + m_1‖) m'

Tactic:
apply norm_nonneg

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
ht : 0 ≤ t
x : E
⊢ ‖t • x‖ = t * ‖x‖

Tactic:
by
  rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

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

Tactic:
refine Subset.antisymm ?_ ball_subset_interior_closedBall

Goal state after:
case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) ⊆ ball x r