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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst✝³] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : μ {a | a ∈ U ∧ ¬f a = g a} = 0
a : X
ha : a ∈ U ∩ {a | f a ≠ g a}
⊢ {a | f a ≠ g a} ∈ 𝓝 a

Tactic:
rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst✝³] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : μ {a | a ∈ U ∧ ¬f a = g a} = 0
a : X
ha : a ∈ U
ha' : (f a, g a) ∈ (diagonal Y)ᶜ
⊢ {a | f a ≠ g a} ∈ 𝓝 a
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
⊢ (map f μ).InnerRegularWRT pb qb

Tactic:
by
  intro U hU r hr
  rw [map_apply_of_aemeasurable hf (hB₂ _ hU)] at hr
  rcases H (hAB U hU) r hr with ⟨K, hKU, hKc, hK⟩
  refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩
  exact hK.trans_le (le_map_apply_image hf _)

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

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
⊢ μ s = ν s

Tactic:
let C := image2 (· ×ˢ ·) { s : Set α | MeasurableSet s } C₂

Goal state after:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
⊢ μ s = ν s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A✝ : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A✝ → Set β
hq1 : ∀ (p : A✝), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A✝), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A✝), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
m n : ℕ
h : Disjoint ↑(s m) ↑(s n)
A : x ∈ q ⟨(s m, s n), h⟩ \ q ⟨(s n, s m), ⋯⟩
B : x ∈ q ⟨(s n, s m), ⋯⟩ \ q ⟨(s m, s n), h⟩
⊢ False

Tactic:
exact A.2 B.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (map f μa).prod (map g μc) = map (Prod.map f g) (μa.prod μc)

Tactic:
simp_rw [← sum_sfiniteSeq μa, ← sum_sfiniteSeq μc, map_sum hf.aemeasurable,
    map_sum hg.aemeasurable, prod_sum, map_sum (hf.prodMap hg).aemeasurable]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (sum fun p ↦ (map f (sfiniteSeq μa p.1)).prod (map g (sfiniteSeq μc p.2))) =
    sum fun i ↦ map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2))
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₁
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t'))

Tactic:
apply (ht.diff ht').image_of_continuousOn_injOn (h'g.mono sdiff_subset)
    intro x hx y hy hxy
    contrapose! hxy
    wlog! H : x < y generalizing x y with h
    · have : y < x := lt_of_le_of_ne H hxy.symm
      exact (h hy hx hxy.symm this).symm
    intro h
    exact hx.2 ⟨hx.1, x, y, hx.1, hy.1, H, rfl, h.symm⟩

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
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ (comap (⇑f) μ) ((fun x ↦ g * x) ⁻¹' s) = (comap (⇑f) μ) s

Tactic:
rw [hf.comap_apply]

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ g * x) ⁻¹' s) = (comap (⇑f) μ) s
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ g * x) ⁻¹' s) = (comap (⇑f) μ) s

Tactic:
rw [hf.comap_apply]

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ g * x) ⁻¹' s) = μ (⇑f '' s)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ g * x) ⁻¹' s) = μ (⇑f '' s)

Tactic:
rw [hf.comap_apply]

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ g * x) ⁻¹' s) = μ (⇑f '' s)
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 : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν

Tactic:
rw [← Measure.prod_restrict, ← lintegral_prod_swap, Measure.prod_restrict,
    setLIntegral_prod]
  · rfl
  · refine AEMeasurable.comp_measurable ?_ measurable_swap
    convert! hf
    rw [← Measure.prod_restrict, Measure.prod_swap, Measure.prod_restrict]

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
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ (comap (⇑f) μ) ((fun x ↦ x * g) ⁻¹' s) = (comap (⇑f) μ) s

Tactic:
rw [hf.comap_apply]

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ x * g) ⁻¹' s) = (comap (⇑f) μ) s
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ x * g) ⁻¹' s) = (comap (⇑f) μ) s

Tactic:
rw [hf.comap_apply]

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ x * g) ⁻¹' s) = μ (⇑f '' s)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ x * g) ⁻¹' s) = μ (⇑f '' s)

Tactic:
rw [hf.comap_apply]

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ μ (⇑f '' (fun x ↦ x * g) ⁻¹' s) = μ (⇑f '' s)
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 μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (uncurry fun x y ↦ f (y * x) x⁻¹) (μ.prod ν)
⊢ ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν = ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun z ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν)

Tactic:
symm

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (uncurry fun x y ↦ f (y * x) x⁻¹) (μ.prod ν)
⊢ ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun z ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν) = ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν
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
x y : G
⊢ s.indicator (fun x ↦ 1) (y * x) = ((fun z ↦ z * x) ⁻¹' s).indicator (fun b ↦ 1) y

Tactic:
symm

Goal state after:
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
x y : G
⊢ ((fun z ↦ z * x) ⁻¹' s).indicator (fun b ↦ 1) y = s.indicator (fun x ↦ 1) (y * x)
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 : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ K ≠ ∞

Tactic:
exact ne_top_of_le_ne_top hμs (by gcongr)

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

Goal state before:
pp: case inr
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
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
this : ∀ (t : Set G), MeasurableSet t → μ' s * ν' t = ν' s * μ' t
ht : ¬MeasurableSet t
t' : Set G
hm : MeasurableSet t'
hμ : μ' t' = μ' t
hν : ν' t' = ν' t
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
rw [← hμ, ← hν, this _ hm]

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

Tactic:
exact tendsto_const_nhds

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ∞

Tactic:
by
  simp only [hasFiniteIntegral_iff_enorm, ofReal_norm]

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

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x = 0
⊢ i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
⊢ i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x

Tactic:
· have := hi x
    simp only [hx, zero_mul, Pi.mul_apply, nonpos_iff_eq_zero] at this
    simp [this]

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
⊢ i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ |z.re| ≤ ‖z‖

Tactic:
mul_self_le_mul_self_iff (abs_nonneg z.re) (Complex.norm_nonneg _),

Goal state after:
z : ℂ
⊢ |z.re| * |z.re| ≤ ‖z‖ * ‖z‖
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f' * g) a ∂μ

Tactic:
by
      apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk
      filter_upwards [h'f, hf.ae_eq_mk]
      intro x hx h'x
      rwa [← h'x]

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

Goal state before:
pp: ⊢ ∀ (n : ℕ) (x : ℂ), (n + 1) • x = n • x + x

Tactic:
intros; ext <;> simp [smul_re, smul_im] <;> ring

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

Goal state before:
pp: ⊢ ∀ (n : ℕ) (a : ℂ), ↑n.succ • a = ↑n • a + a

Tactic:
intros; ext <;> simp [smul_re, smul_im] <;> ring

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

Goal state before:
pp: ⊢ ∀ (n : ℕ) (a : ℂ), Int.negSucc n • a = -(↑n.succ • a)

Tactic:
intros; ext <;> simp [smul_re, smul_im] <;> ring

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, f i ≤ 0
⊢ 𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
simp +contextual [expect, sum_eq_zero_iff_of_nonpos hf]

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
⊢ u ∈ unitary R ↔ u * star u = 1

Tactic:
by
  rw [← star_mem_iff, hu.star.mem_unitary_iff_star_mul_self, star_star]

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

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
e : E
he : IsStarProjection e
⊢ ‖e‖ * (‖e‖ - 1) = 0

Tactic:
simp [mul_sub, ← CStarRing.norm_star_mul_self, he.isSelfAdjoint.star_eq, he.isIdempotentElem.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 • a) = star r • star a

Tactic:
by rw [← smul_one_smul ℂ r a, star_smul, star_smul, star_one, smul_one_smul]

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

Goal state before:

Tactic:
‖imaginaryPart x‖ = ‖realPart (Complex.I • (-x))‖ := by simp
    _ ≤ ‖x‖ := by simpa only [smul_neg, map_neg, realPart_I_smul, neg_neg,
        AddSubgroupClass.coe_norm, norm_neg, norm_smul, Complex.norm_I, one_mul] using
        realPart.norm_le (Complex.I • (-x))

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ normSq (z - w) = normSq z + normSq w - 2 * re (z * (starRingEnd K) w)

Tactic:
simp only [normSq_add, sub_eq_add_neg, map_neg, mul_neg, normSq_neg, map_neg]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z⁻¹ = re z / normSq z

Tactic:
by
  rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : 0 ≤ x
⊢ ↑‖x‖ = x

Tactic:
rw [eq_comm, ← norm_le_re_iff_eq_norm, ← sqrt_normSq_eq_norm, normSq_apply]
  simp [nonneg_iff.mp hx]

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

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

Tactic:
by
  simpa only [mul_neg, neg_pos, neg_neg_iff_pos] using ofReal_mul_pos_iff x (-z)

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 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ (algebraMap ℝ 𝕜) 1 = 1

Tactic:
exact h.algebraMap.map_one'

Goal state after:
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n l m a b : ℕ
h₁ : n.ascFactorial l = a
h₂ : (n + l).ascFactorial m = b
⊢ n.ascFactorial (l + m) = n.ascFactorial l * (n + l).ascFactorial m

Tactic:
symm

Goal state after:
n l m a b : ℕ
h₁ : n.ascFactorial l = a
h₂ : (n + l).ascFactorial m = b
⊢ n.ascFactorial l * (n + l).ascFactorial m = n.ascFactorial (l + m)
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
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
hi₂ : |(fun n ↦ ∑ i ∈ range n, a i) (max n i) - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
sub_le :
  |∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k| ≤
    |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (max n i), a k|
this :
  |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| +
      |(fun n ↦ ∑ i ∈ range n, a i) i - ∑ k ∈ range (max n i), a k| <
    ε
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) ≤
    ∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k

Tactic:
generalize hk : j - max n i = k

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
hi₂ : |(fun n ↦ ∑ i ∈ range n, a i) (max n i) - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
sub_le :
  |∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k| ≤
    |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (max n i), a k|
this :
  |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| +
      |(fun n ↦ ∑ i ∈ range n, a i) i - ∑ k ∈ range (max n i), a k| <
    ε
k : ℕ
hk : j - max n i = k
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) ≤
    ∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case inl
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
c : E''
l : Filter α
inst✝ : l.NeBot
⊢ ((fun _x ↦ c) =O[l] fun _x ↦ 0) ↔ 0 = 0 → c = 0

Tactic:
simp [EventuallyEq]

Goal state after: