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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
s : Set β
hs : MeasurableSet s
x✝ : s.Nonempty
⊢ count (f ⁻¹' s) ≤ count s

Tactic:
count_apply (hs.preimage h2f),

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
s : Set β
hs : MeasurableSet s
x✝ : s.Nonempty
⊢ ↑(f ⁻¹' s).encard ≤ count s
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
s : ℕ → Finset ℝ≥0∞
⊢ ∀ (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ) →
        ⨆ n, ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (μ : Measure α), ⨆ n, ∑ r ∈ s n, r * f n r μ ∂m

Tactic:
f

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
⊢ (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
    (Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ) →
      ⨆ n, ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (μ : Measure α), ⨆ n, ∑ r ∈ s n, r * f n r μ ∂m
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∑ b ∈ s n, ∫⁻ (a : Measure α), b * f n b a ∂m

pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∀ b ∈ s n, Measurable fun a ↦ b * f n b a

Tactic:
· simp_rw [lintegral_const_mul _ (hf _ _)]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∀ b ∈ s n, Measurable fun a ↦ b * f n b a
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ (m.bind fun x ↦ dirac (f x)) = map f m

Tactic:
rw [← bind_dirac (m := m.map f), bind, bind, map_map, Function.comp_def]

Goal state after:
case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Measurable dirac

case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Measurable f
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
⊢ ∃ n, C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))

Tactic:
have : Nonempty X := ⟨x⟩

Goal state after:
case inr
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
⊢ ∃ n, C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ μ ∗ₘ (ν + ρ) = μ ∗ₘ ν + μ ∗ₘ ρ

Tactic:
unfold mconv
  rw [prod_add, Measure.map_add]
  fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν
x : α
| ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν

Tactic:
erw [lintegral_add_left (hf.comp m)]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν
x : α
| ∫⁻ (a : β), (f ∘ Prod.mk x) a ∂ν + ∫⁻ (a : β), g (x, a) ∂ν
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(f x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
by
  simp_rw [lintegral_eq_nnreal, lt_iSup_iff] at hL
  rcases hL with ⟨g₀, hg₀, g₀L⟩
  have h'L : L < ∫⁻ x, g₀ x ∂μ := by
    convert! g₀L
    rw [← SimpleFunc.lintegral_eq_lintegral, SimpleFunc.coe_map]
    simp only [Function.comp_apply]
  rcases SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral h'L with ⟨g, hg, gL, gtop⟩
  exact ⟨g, fun x => (hg x).trans (ENNReal.coe_le_coe.1 (hg₀ x)), gL, gtop⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ∞

Tactic:
exact ae_lt_top (measurable_measure_prodMk_left hs) h2s

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

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ map (fun x ↦ DomMulAct.mk.symm (g * g')⁻¹ • x) μ =
    map ((fun x ↦ DomMulAct.mk.symm g⁻¹ • x) ∘ fun x ↦ DomMulAct.mk.symm g'⁻¹ • x) μ

Tactic:
simp [Function.comp_def, mul_smul]

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : PolishSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T0Space Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst✝⁶, inst✝²] f
hsurj : Surjective f
⊢ MeasurableSpace.map f inst✝⁴ = borel Y

Tactic:
borelize Y

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : PolishSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T0Space Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst✝⁶, inst✝²] f
hsurj : Surjective f
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
⊢ MeasurableSpace.map f inst✝⁴ = borel Y
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ ↑(hST.equiv g).2 = ↑⟨1, h1⟩

Tactic:
rw [equiv_snd_eq_inv_mul, equiv_fst_eq_self_of_mem_of_one_mem _ h1 hg, inv_mul_cancel]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
⊢ (x • μ).OuterRegular

Tactic:
rcases eq_or_ne x 0 with (rfl | h0)
  · rw [zero_smul]
    exact OuterRegular.zero
  · refine ⟨fun A _ r hr => ?_⟩
    rw [smul_apply, A.measure_eq_iInf_isOpen, smul_eq_mul] at hr
    simpa only [ENNReal.mul_iInf_of_ne h0 hx, gt_iff_lt, iInf_lt_iff, exists_prop] using! hr

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

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
c : G
⊢ μ (c • s) = 0 ↔ μ s = 0

Tactic:
rw [measure_smul]

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
t : G
p : G → Prop
| ∀ᵐ (x : G) ∂μ, p x

Tactic:
rw [Filter.Eventually, ← map_mul_left_ae μ t]

Goal state after:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
t : G
p : G → Prop
| {x | p x} ∈ Filter.map (fun h ↦ t * h) (ae μ)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
| {x | p x} ∈ ae μ

Tactic:
← map_div_right_ae μ t

Goal state after:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
| {x | p x} ∈ Filter.map (fun t_1 ↦ t_1 / t) (ae μ)
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 μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ ∫⁻ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t) = ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ

Tactic:
lintegral_prod _ (by rwa [Measure.prod_restrict])

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ = ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)
F_mono : Monotone F
hU : IsOpen[inst✝²] (⋃ n, F n)
hr : r < μ (⋃ n, F n)
⊢ ∃ K ⊆ ⋃ n, F n, IsClosed[inst✝²] K ∧ r < μ K

Tactic:
rw [F_mono.measure_iUnion] at hr

Goal state after:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)
F_mono : Monotone F
hU : IsOpen[inst✝²] (⋃ n, F n)
hr : r < ⨆ i, μ (F i)
⊢ ∃ K ⊆ ⋃ n, F n, IsClosed[inst✝²] K ∧ r < μ 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 β
inst✝ : μ.Regular
f : α ≃ₜ β
⊢ (map (⇑f) μ).Regular

Tactic:
have := OuterRegular.map f μ
  have := IsFiniteMeasureOnCompacts.map μ f
  exact
    ⟨Regular.innerRegular.map' f.toMeasurableEquiv
        (fun U hU => hU.preimage f.continuous)
        (fun K hK => hK.image f.continuous)⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : PseudoEMetricSpace β
n : ℕ
j : ι
f : ι → α → β
g : α → β
inst✝ : Preorder ι
x : α
⊢ (∃ i, j ≤ i ∧ x ∈ {x | (↑n)⁻¹ < edist (f i x) (g x)}) ↔ ∃ k ≥ j, (↑n)⁻¹ < edist (f k x) (g x)

Tactic:
mem_ofPred

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
⊢ b * b - 4 * a * c ≤ 0

Tactic:
have : Tendsto (fun x => (a * x + b) * x + c) atTop atBot :=
      tendsto_atBot_add_const_right _ c <|
        (tendsto_atBot_add_const_right _ b (tendsto_id.const_mul_atTop_of_neg ha)).atBot_mul_atTop₀
          tendsto_id
    rcases (this.eventually (eventually_lt_atBot 0)).exists with ⟨x, hx⟩
    exact False.elim ((h x).not_gt <| by rwa [← mul_assoc, ← add_mul])

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

Goal state before:
pp: ⊢ map (fun x ↦ √x) atTop = atTop

Tactic:
unfold sqrt
  simp_rw [← Function.comp_def]
  simp [← map_map]

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

Goal state before:
pp: x y : ℝ
⊢ √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2

Tactic:
rw [← and_iff_right_of_imp fun h => (sqrt_nonneg x).trans h, and_congr_right_iff]

Goal state after:
x y : ℝ
⊢ 0 ≤ y → (√x ≤ y ↔ x ≤ y ^ 2)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: n : ℕ
⊢ ↑‖↑n‖₊ = ↑↑n

Tactic:
simp [norm_natCast]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : SFinite μ
R : Type u_2
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
this : c • μ = c • 1 • μ
⊢ SFinite (c • 1 • μ)

Tactic:
← smul_assoc,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : SFinite μ
R : Type u_2
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
this : c • μ = c • 1 • μ
⊢ SFinite ((c • 1) • μ)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: α : Type u_1
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by ext <;> simp [NNRat.cast_def, div_re, div_im, mul_div_mul_comm]

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

Goal state before:
pp: s s₁ t t₁ : Set ℝ
⊢ ⇑equivRealProd ⁻¹' s ×ˢ t ⊆ ⇑equivRealProd ⁻¹' s₁ ×ˢ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
exact Equiv.preimage_subset equivRealProd _ _

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun z ↦ f z.1 * g z.2

Tactic:
prod_withDensity_left₀ hf,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ ((μ.prod (ν.withDensity g)).withDensity fun z ↦ f z.1) = (μ.prod ν).withDensity fun z ↦ f z.1 * g z.2
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
⊢ 0 < (↑(#s))⁻¹

Tactic:
have : s.Nonempty := ⟨i, hi⟩

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
this : s.Nonempty
⊢ 0 < (↑(#s))⁻¹
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₂
⊢ ∀ (a b : NormedAddGroupHom V₂ V₃),
    AddMonoidHom.mk' (fun f ↦ (a + b).comp f) ⋯ =
      AddMonoidHom.mk' (fun f ↦ a.comp f) ⋯ + AddMonoidHom.mk' (fun f ↦ b.comp f) ⋯

Tactic:
by
      intros
      ext
      simp only [comp_apply, Pi.add_apply, AddMonoidHom.add_apply,
        AddMonoidHom.mk'_apply, coe_add]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖f x‖ ≤ ‖f 1‖ * ‖x‖

Tactic:
conv_lhs => rw [← mul_one x]
    rw [← smul_eq_mul, f.map_smul, mul_comm]; exact norm_smul_le _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : DivisionSemiring γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
⊢ ∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i

Tactic:
rcases eq_or_ne g 0 with rfl | hg
  · simp
  · exact tsum_const_smul' (Units.mk0 g hg)

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝¹ : ℝ
x✝ : 𝕜
⊢ (RCLike.complexRingEquiv h).toFun (x✝¹ • x✝) = (RingHom.id ℝ) x✝¹ • (RCLike.complexRingEquiv h).toFun x✝

Tactic:
simp [RCLike.smul_re, RCLike.smul_im, ofReal_mul]

Goal state after:
z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝¹ : ℝ
x✝ : 𝕜
⊢ ↑x✝¹ * ↑(RCLike.im x✝) * I = ↑x✝¹ * (↑(RCLike.im x✝) * I)
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ ‖x‖ + ‖star x‖ ≤ 2 * ‖x‖

Tactic:
simp [two_mul]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖(starRingEnd K) z‖ₑ = ‖z‖ₑ

Tactic:
simp [enorm]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ LipschitzWith 1 ⇑re

Tactic:
intro x y
  simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]
  calc ‖re x - re y‖ₑ
  _ = ‖re (x - y)‖ₑ := by rw [map_sub re x y]
  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_re_le_norm (x - y)

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r : ℝ),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        ({ toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r) =
      0

Tactic:
subst h''; exact h.ofReal_im_ax

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
simp only [isBigO_iff, eventually_prod_iff]
  exact fun ⟨c, hc⟩ ↦ ⟨c, fun _ ↦ True, eventually_true l', _, hc, fun _ ↦ id⟩

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₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a✝ : α
hx₁ : ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖
hx₂ : ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖
⊢ c₁ * c₂ * ‖g₁ a✝ * g₂ a✝‖ = c₁ * ‖g₁ a✝‖ * (c₂ * ‖g₂ a✝‖)

Tactic:
rw [norm_mul, mul_mul_mul_comm]

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
x : α
hx : 1 x ≤ f x
⊢ ‖(f ^ n) x‖ ≤ 1 * ‖(f ^ m) x‖

Tactic:
by simp [abs_eq_self.mpr (zero_le_one.trans hx), pow_le_pow_right₀ hx h]

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'
B : ι → α → ℝ
i : α → Finset ι
hAB : Function.uncurry A =o[⊤ ×ˢ l] Function.uncurry B
⊢ (fun H ↦ ∑ j ∈ i H, A j H) =o[l] fun H ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
by
  rw [isLittleO_iff_forall_isBigOWith] at *
  intro c hc
  exact (hAB hc).sum_congr'

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

Goal state before:
pp: x : ℂ
⊢ cosh x ^ 2 = sinh x ^ 2 + 1

Tactic:
← cosh_sq_sub_sinh_sq x

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

Goal state before:
pp: x : ℂ
⊢ sinh x ^ 2 = cosh x ^ 2 - 1

Tactic:
← cosh_sq_sub_sinh_sq x

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

Goal state before:
pp: x : ℂ
⊢ tan (x * I) = tanh x * I

Tactic:
rw [tan, sin_mul_I, cos_mul_I, mul_div_right_comm, tanh_eq_sinh_div_cosh]

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

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

Tactic:
by
  rw [← cosh_add_sinh, sinh_mul_I, cosh_mul_I]

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 : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - l.pred.succ • ε + ε

Tactic:
succ_nsmul,

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
hfij : f j ≤ f i
| a - (l.pred • ε + ε) + ε
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:
by
  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.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ ‖1 - r‖ * ‖x - y‖ = (1 - r) * dist y x

Tactic:
rw [Real.norm_eq_abs, abs_eq_self.mpr (sub_nonneg.mpr h.2), dist_eq_norm']

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

Goal state before:
pp: n : ℕ
⊢ sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

Tactic:
by
  rw [sin_sq_pi_over_two_pow, sqrtTwoAddSeries, div_pow, sq_sqrt, add_div, ← sub_sub]
  · congr
    · norm_num
    · norm_num
  · exact add_nonneg two_pos.le (sqrtTwoAddSeries_zero_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
inst✝ : NontrivialTopology E
x : E
r : ℝ
⊢ (sphere x r).Nonempty ↔ 0 ≤ r

Tactic:
refine ⟨fun h => nonempty_closedBall.1 (h.mono sphere_subset_closedBall), fun hr => ?_⟩

Goal state after:
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NontrivialTopology E
x : E
r : ℝ
hr : 0 ≤ r
⊢ (sphere x r).Nonempty