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

Goal state before:
pp: α : Type u_3
inst✝² : PseudoMetricSpace α
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.OuterRegular
inst✝ : ν.OuterRegular
hμν : ∀ (U : Set α), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U → Bornology.IsBounded U → μ U = ν U
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
f : ℕ → Set α
hm : Monotone f
hu : ⋃ i, f i = U
hf : ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ μ (⋃ i, f i) = ν (⋃ i, f i)

Tactic:
hm.measure_iUnion,

Goal state after:
α : Type u_3
inst✝² : PseudoMetricSpace α
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.OuterRegular
inst✝ : ν.OuterRegular
hμν : ∀ (U : Set α), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U → Bornology.IsBounded U → μ U = ν U
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
f : ℕ → Set α
hm : Monotone f
hu : ⋃ i, f i = U
hf : ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ ⨆ i, μ (f i) = ν (⋃ i, f i)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < μ F
hBU : ⋃ n, F ∩ s n = F
⊢ μ F = ⨆ n, μ (F ∩ s n)

Tactic:
rw [← (monotone_const.inter hmono).measure_iUnion, hBU]

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 ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
⊢ map Prod.swap (sum fun p ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)) =
    sum fun p ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2)

Tactic:
map_sum measurable_swap.aemeasurable,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
⊢ (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun p ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2)
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
f : ι → X → E
h : ∀ (i : ι), Measurable (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)
⊢ Measurable (∏ i ∈ Finite.toFinset h✝, L.support.mulIndicator (fun i ↦ f i) i.down)

pp: case neg
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
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ Measurable (Exists.choose hm)

Tactic:
· refine Finset.measurable_prod_apply (fun _ _ ↦ ?_) measurable_id
    rw [Set.mulIndicator]
    split_ifs <;> fun_prop

Goal state after:
case neg
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
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ Measurable (Exists.choose hm)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case inr
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
s : Set G
hs : IsOpen[inst✝⁵] s
hμ : NeZero μ
⊢ μ s = 0 ↔ s = ∅ ∨ μ = 0

Tactic:
simp only [or_false, hs.measure_eq_zero_iff μ, NeZero.ne μ]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᵐ[μ] g
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity f) s = (μ.withDensity g) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᵐ[μ] g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ = (μ.withDensity g) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity f) s ≤ (μ.withDensity g) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ (μ.withDensity g) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (f + g)) s = (μ.withDensity f + μ.withDensity g) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f + g) a ∂μ = (μ.withDensity f + μ.withDensity g) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f + g) a ∂μ = (μ.withDensity f) s + (μ.withDensity g) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f + g) a ∂μ = ∫⁻ (a : α) in s, f a ∂μ + (μ.withDensity g) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f + g) a ∂μ = ∫⁻ (a : α) in s, f a ∂μ + (μ.withDensity g) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f + g) a ∂μ = ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in s, g a ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (r • f)) s = (r • μ.withDensity f) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = (r • μ.withDensity f) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = r • (μ.withDensity f) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = r • ∫⁻ (a : α) in s, f a ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (r • f)) s = (r • μ.withDensity f) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = (r • μ.withDensity f) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = r • (μ.withDensity f) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = r • ∫⁻ (a : α) in s, f a ∂μ
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y ↦ ((fun z ↦ z * x) ⁻¹' s).indicator (fun x ↦ 1) y
this : ∀ (x y : G), s.indicator (fun x ↦ 1) (y * x) = ((fun z ↦ z * x) ⁻¹' s).indicator (fun b ↦ 1) y
⊢ ∫⁻ (x : G), (∫⁻ (x : G) in (fun z ↦ z * x) ⁻¹' s, 1 ∂ν) * f x⁻¹ ∂μ = ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * f x⁻¹ ∂μ

Tactic:
setLIntegral_one

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ((μ.withDensity f).trim hm) s = ((μ.trim hm).withDensity f) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ((μ.withDensity f).trim hm) s = ∫⁻ (a : α) in s, f a ∂μ.trim hm
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
h1 : ν' s * ∫⁻ (y : G), t.indicator (fun x ↦ 1) y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s) ∂ν' = ∫⁻ (a : G) in t, 1 ∂ν'
h2 : μ' s * ∫⁻ (y : G), t.indicator (fun x ↦ 1) y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s) ∂ν' = ∫⁻ (a : G) in t, 1 ∂μ'
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
setLIntegral_one

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
h1 : ν' s * ∫⁻ (y : G), t.indicator (fun x ↦ 1) y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s) ∂ν' = ν' t
h2 : μ' s * ∫⁻ (y : G), t.indicator (fun x ↦ 1) y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s) ∂ν' = μ' t
⊢ μ' s * ν' t = ν' s * μ' t
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
⊢ 0 ≤ f a → f a ≤ g a → ‖f a‖ ≤ ‖g a‖

Tactic:
hn

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
hn : 0 ≤ f a
⊢ f a ≤ g a → ‖f a‖ ≤ ‖g a‖
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : HasFiniteIntegral f μ
x : α
⊢ ENNReal.ofReal (f x) ≤ ‖f x‖ₑ

Tactic:
exact Real.ofReal_le_enorm (f x)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (f * g)) s = ((μ.withDensity f).withDensity g) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f * g) a ∂μ = ((μ.withDensity f).withDensity g) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f * g) a ∂μ = ((μ.withDensity f).withDensity g) s

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, g a ∂μ.withDensity f
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : (f * fun x ↦ (f x)⁻¹) =ᵐ[μ] 1
⊢ μ.withDensity (f * fun i ↦ (f i)⁻¹) = μ

Tactic:
rw [withDensity_congr_ae this, withDensity_one]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : (μ.withDensity f) s = 0
⊢ μ s = 0

Tactic:
withDensity_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : ∫⁻ (a : α) in s, f a ∂μ = 0
⊢ μ s = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ I ^ 4 = 1

Tactic:
rw [(by simp : 4 = 2 * 2), pow_mul, I_sq, neg_one_sq]

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

Goal state before:
pp: α : Type u_1
n : ℕ
h : ↑n = 0
⊢ n = 0

Tactic:
← ofReal_natCast,

Goal state after:
α : Type u_1
n : ℕ
h : ↑↑n = 0
⊢ n = 0
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 : ι → α
a : α
hs : s.Nonempty
h : a < 𝔼 i ∈ s, f i
⊢ ∃ x ∈ s, a < f x

Tactic:
contrapose! h; exact expect_le hs h

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : 0 < ‖x⋆‖
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
· refine le_of_mul_le_mul_right ?_ hx
      simpa using norm_mul_self_le (x := x⋆) |>.trans <| norm_mul_le _ _

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

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
hx : IsSelfAdjoint x
⊢ skewAdjoint.negISMul ((skewAdjointPart ℝ) x) = 0

Tactic:
hx.skewAdjointPart_apply _,

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
hx : IsSelfAdjoint x
⊢ skewAdjoint.negISMul 0 = 0
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
← ofReal_natCast,

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

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

Tactic:
← ofReal_natCast,

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
⊢ 0 < ↑x * z ↔ x < 0 ∧ z < 0 ∨ 0 < x ∧ 0 < z

Tactic:
simp only [pos_iff (K := K), neg_iff (K := K), re_ofReal_mul, im_ofReal_mul]

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
ι : Sort u_18
p : ι → Prop
s : ι → Set α
h✝ : f =O[l] g'
hb : l.HasBasis p s
c : ℝ
h : c > 0 ∧ IsBigOWith c l f g'
⊢ c > 0 ∧ ∃ i, p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖

Tactic:
simpa only [isBigOWith_iff, hb.eventually_iff, exists_prop] using h

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

Goal state before:
pp: α : 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 α
a : α
h : f =O[𝓝[≠] a] fun x ↦ 1
⊢ f =O[𝓝 a] fun x ↦ 1

Tactic:
simp only [isBigO_one_iff, IsBoundedUnder, IsBounded, eventually_map] at h ⊢

Goal state after:
α : 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 α
a : α
h : ∃ b, ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ b
⊢ ∃ b, ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: F : Type u_4
inst✝⁴ : Norm F
α : Type u_17
E : Type u_18
inst✝³ : NormedRing E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
f : α → E
x : α
⊢ ContinuousAt f x ↔ (fun x_1 ↦ f x_1 - f x) =o[𝓝 x] fun x ↦ 1

Tactic:
by
  simp [ContinuousAt, ← tendsto_sub_nhds_zero_iff]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ (f =o[l] fun x ↦ c • f' x) ↔ f =o[l] f'

Tactic:
by
  have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
  rw [← isLittleO_norm_right]
  simp only [norm_smul]
  rw [isLittleO_const_mul_right_iff cne0, isLittleO_norm_right]

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

Goal state before:
pp: x : ℂ
x✝¹ n : ℕ
x✝ : n ∈ range x✝¹
⊢ (starRingEnd ℂ) x ^ n / ↑n.factorial = (starRingEnd ℂ) x ^ n / (starRingEnd ℂ) ↑n.factorial

Tactic:
← ofReal_natCast,

Goal state after:
x : ℂ
x✝¹ n : ℕ
x✝ : n ∈ range x✝¹
⊢ (starRingEnd ℂ) x ^ n / ↑↑n.factorial = (starRingEnd ℂ) x ^ n / (starRingEnd ℂ) ↑↑n.factorial
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
⊢ ↑(rexp (-x)) = ↑(rexp x)⁻¹

Tactic:
by simp [exp_neg]

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

Goal state before:
pp: x : ℝ
⊢ ↑(tan x) = ↑(sin x / cos x)

Tactic:
simp only [ofReal_tan, tan_eq_sin_div_cos, ofReal_div, ofReal_sin,
    ofReal_cos]

Goal state after:
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''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
⊢ n₁ ≤ n → ‖f n‖ ≤ max C₀ C₁ * ‖g n‖

Tactic:
hn

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
hn : n₁ ≤ n
⊢ ‖f n‖ ≤ max C₀ C₁ * ‖g n‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ x + 1 < rexp x

Tactic:
by
  obtain hx | hx := hx.symm.lt_or_gt
  · exact add_one_lt_exp_of_pos hx
  obtain h' | h' := le_or_gt 1 (-x)
  · linarith [x.exp_pos]
  have hx' : 0 < x + 1 := by linarith
  simpa [add_comm, exp_neg, inv_lt_inv₀ (exp_pos _) hx']
    using exp_bound_div_one_sub_of_interval' (neg_pos.2 hx) h'

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

Goal state before:
pp: n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ rexp (-(t / ↑n)) ^ n = rexp (-t)

Tactic:
rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity

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

Goal state before:
pp: x z : ℂ
hz : ‖z‖ ≤ 1
⊢ cexp (x + z) - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)

Tactic:
rw [exp_add]

Goal state after:
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ cexp x * cexp z - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖y - x‖ ^ 2 ≤ r * ‖y - x‖

Tactic:
rw [pow_two]

Goal state after:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖y - x‖ * ‖y - x‖ ≤ r * ‖y - x‖
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 • ε + ε < f j + ε

Tactic:
by gcongr; exact hl _ <| hi.1.trans hj

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

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn0 : n % 2 = 0
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
by
          rwa [← mul_assoc, ← @Int.cast_two ℝ, ← Int.cast_mul,
            Int.ediv_mul_cancel (Int.dvd_iff_emod_eq_zero.2 hn0)]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ infDist m ↑S = sInf ((fun x ↦ ‖m + x‖) '' ↑S)

Tactic:
sInf_image',

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ infDist m ↑S = ⨅ a, ‖m + ↑a‖
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
hx : x ∈ (↑S.topologicalClosure)ᶜ
⊢ 0 < ‖↑x‖

Tactic:
exact (norm_nonneg _).lt_of_ne' <| mt norm_mk_eq_zero_iff_mem_closure.1 hx

Goal state after: