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

Goal state before:
pp: case iUnion
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
f : ℕ → Set G
a✝ : Pairwise (Disjoint on f)
hf✝ : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), f i * closure[inst✝³] {1} = f i
⊢ (⋃ i, f i) * closure[inst✝³] {1} = ⋃ i, f i

Tactic:
[

Goal state after:
case iUnion
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
f : ℕ → Set G
a✝ : Pairwise (Disjoint on f)
hf✝ : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), f i * closure[inst✝³] {1} = f i
⊢ (⋃ i, f i) * closure[inst✝³] {1} = ⋃ i, f i
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), ∫⁻ (y : G), s.indicator (fun x ↦ 1) (y * x) * f x⁻¹ ∂ν ∂μ =
    ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * f x⁻¹ ∂μ

Tactic:
[

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
this : ∀ (x y : G), s.indicator (fun x ↦ 1) (y * x) = ((fun z ↦ z * x) ⁻¹' s).indicator (fun b ↦ 1) y
⊢ ∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun x ↦ 1) (y * x) * f x⁻¹ ∂ν ∂μ =
    ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * f x⁻¹ ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)) Sᶜ = 0

Tactic:
· rw [withDensity_apply _ hS.compl, lintegral_eq_zero_iff hf.fun_neg.ennreal_ofReal, EventuallyEq]
    exact
      (ae_restrict_mem hS.compl).mono fun x hx =>
        ENNReal.ofReal_eq_zero.2 (not_lt.1 <| mt neg_pos.1 hx)

Goal state after:
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
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s * ∫⁻ (y : G), 1 y ∂ν = ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * 1 x⁻¹ ∂μ
⊢ μ s = 0

Tactic:
[

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
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s * ∫⁻ (y : G), 1 y ∂ν = ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * 1 x⁻¹ ∂μ
⊢ μ s = 0
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : CommSemigroup G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ Measure.map (fun x ↦ x * g) μ = μ

Tactic:
[

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : CommSemigroup G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ Measure.map (fun x ↦ x * g) μ = μ
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ∫⁻ (a : G) in A⁻¹, 1 a ∂ν' = ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * A⁻¹.indicator 1 x⁻¹ ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞

Tactic:
[

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ∫⁻ (a : G) in A⁻¹, 1 a ∂ν' = ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * A⁻¹.indicator 1 x⁻¹ ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t✝ : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t✝ ∪ {x | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0}
M : MeasurableSet {x | g x = 0}
⊢ ∀ (a : α), g a = 0 → g a = 0 a

Tactic:
simp only [imp_self, Pi.zero_apply, imp_true_iff]

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'

Tactic:
[

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
⊢ (∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0

Tactic:
[

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
⊢ (∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
x : G
hx : ν' ((fun y ↦ y * x) ⁻¹' s) < ∞
⊢ ν' ((fun z ↦ z * x) ⁻¹' s) * (f x / ν' ((fun z ↦ z * x) ⁻¹' s)) = f x

Tactic:
[

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
x : G
hx : ν' ((fun y ↦ y * x) ⁻¹' s) < ∞
⊢ ν' ((fun z ↦ z * x) ⁻¹' s) * (f x / ν' ((fun z ↦ z * x) ⁻¹' s)) = f x
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 : α
⊢ x ∈ notConvergentSeq f g n j ↔ ∃ k ≥ j, (↑n)⁻¹ < edist (f k x) (g x)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : PseudoEMetricSpace β
n : ℕ
j : ι
f : ι → α → β
g : α → β
inst✝ : Preorder ι
x : α
⊢ x ∈ notConvergentSeq f g n j ↔ ∃ k ≥ j, (↑n)⁻¹ < edist (f k x) (g x)
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 ι
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0

Tactic:
[

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 ι
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0
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) ∂ν' =
    ∫⁻ (x : G), t.indicator (fun x ↦ 1) x ∂ν'
h2 :
  μ' s * ∫⁻ (y : G), t.indicator (fun x ↦ 1) y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s) ∂ν' =
    ∫⁻ (x : G), t.indicator (fun x ↦ 1) x ∂μ'
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
lintegral_indicator ht,

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) ∂ν' = ∫⁻ (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
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 ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Tactic:
this

Goal state after:
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)
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✝¹ : μ.IsMulRightInvariant
inst✝ : ν.IsMulRightInvariant
x y : G
⊢ (x * y, x⁻¹) = ((fun z ↦ (z.2, z.1 / z.2)) ∘ fun z ↦ (z.2, z.1 * z.2)) (x, y)

Tactic:
[

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✝¹ : μ.IsMulRightInvariant
inst✝ : ν.IsMulRightInvariant
x y : G
⊢ (x * y, x⁻¹) = ((fun z ↦ (z.2, z.1 / z.2)) ∘ fun z ↦ (z.2, z.1 * z.2)) (x, y)
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✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ QuasiMeasurePreserving (fun h ↦ g / h) μ μ

Tactic:
[

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ QuasiMeasurePreserving (fun h ↦ g / h) μ μ
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✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this✝ : QuasiMeasurePreserving (fun h ↦ h * g⁻¹) μ μ
this : QuasiMeasurePreserving (Inv.inv ∘ (fun h ↦ h * g⁻¹) ∘ Inv.inv) μ μ
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ

Tactic:
[

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this✝ : QuasiMeasurePreserving (fun h ↦ h * g⁻¹) μ μ
this : QuasiMeasurePreserving (Inv.inv ∘ (fun h ↦ h * g⁻¹) ∘ Inv.inv) μ μ
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ
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))
⊢ ∑' (a : ℕ), ENNReal.ofReal (ε / 2 * 2⁻¹ ^ a) ≤ ENNReal.ofReal ε

Tactic:
[

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))
⊢ ∑' (a : ℕ), ENNReal.ofReal (ε / 2 * 2⁻¹ ^ a) ≤ ENNReal.ofReal ε
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : ∃! x, a * (x * x) + b * x + c = 0
⊢ discrim a b c = 0

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : ∃! x, a * (x * x) + b * x + c = 0
⊢ discrim a b c = 0
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
hd : discrim a b c = 0
⊢ ∃! x, a * (x * x) + b * x + c = 0

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
hd : discrim a b c = 0
⊢ ∃! x, a * (x * x) + b * x + c = 0
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

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

Tactic:
[

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
⊢ HasFiniteIntegral (fun x ↦ (f x).toReal) μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

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

Tactic:
this

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f * g) a ∂μ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ map (fun x ↦ ↑(NNReal.sqrt x.toNNReal)) atTop = atTop

Tactic:
[

Goal state after:
⊢ map (fun x ↦ ↑(NNReal.sqrt x.toNNReal)) atTop = atTop
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ comap (fun x ↦ ↑(NNReal.sqrt x.toNNReal)) atTop = atTop

Tactic:
[

Goal state after:
⊢ comap (fun x ↦ ↑(NNReal.sqrt x.toNNReal)) atTop = atTop
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ comap (NNReal.toReal ∘ ⇑NNReal.sqrt ∘ toNNReal) atTop = atTop

Tactic:
simp [← comap_comap]

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

Goal state before:
pp: case inr
x y : ℝ
hx : 0 < x
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
· exact sqrt_le_sqrt_iff hy

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x * y) = √x * √y

Tactic:
[

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x * y) = √x * √y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x / y) = √x / √y

Tactic:
division_def,

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x * y⁻¹) = √x / √y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ √(x / y) = √x / √y

Tactic:
division_def,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ √(x * y⁻¹) = √x / √y
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
hz : ¬z = 0
⊢ |z.re / ‖z‖| ≤ 1

Tactic:
[

Goal state after:
z : ℂ
hz : ¬z = 0
⊢ |z.re / ‖z‖| ≤ 1
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
hz : ¬z = 0
⊢ |z.im / ‖z‖| ≤ 1

Tactic:
[

Goal state after:
z : ℂ
hz : ¬z = 0
⊢ |z.im / ‖z‖| ≤ 1
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun x ↦ ‖x‖) (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ‖(starRingEnd ℂ) (↑f j) - (starRingEnd ℂ) (↑f i)‖ < ε

Tactic:
[

Goal state after:
f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun x ↦ ‖x‖) (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ‖(starRingEnd ℂ) (↑f j) - (starRingEnd ℂ) (↑f i)‖ < ε
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z : ℂ
x : ℝ
⊢ z / ↑x = { re := z.re / x, im := z.im / x }

Tactic:
[

Goal state after:
z : ℂ
x : ℝ
⊢ z / ↑x = { re := z.re / x, im := z.im / x }
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
s : Set (α × β)
hs : MeasurableSet s
A : ∀ (s : Set β), c • ν s = c • 1 * ν s
⊢ (μ.prod (c • ν)) s = (c • μ.prod ν) s

Tactic:
[

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
s : Set (α × β)
hs : MeasurableSet s
A : ∀ (s : Set β), c • ν s = c • 1 * ν s
⊢ (μ.prod (c • ν)) s = (c • μ.prod ν) s
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * (star B * star U) = U * (B * star B) * star U

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * (star B * star U) = U * (B * star B) * star U
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
g : G
hg : g ∈ unitary G
⊢ g⁻¹ ∈ unitary G

Tactic:
[

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
g : G
hg : g ∈ unitary G
⊢ g⁻¹ ∈ unitary G
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‖

Tactic:
rw [← mul_one x]

Goal state after:
𝕜 : 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 * 1)‖
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a • b) = π b
⊢ ∑' (a : α), g (π (a • b)) • f (a • b) = g (π b) • ∑' (a : α), f (a • b)

Tactic:
[

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a • b) = π b
⊢ ∑' (a : α), g (π (a • b)) • f (a • b) = g (π b) • ∑' (a : α), f (a • b)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ (r + s) • x = r • x + s • x

Tactic:
by ext <;> simp [smul_re, smul_im, add_smul]

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

Goal state before:
pp: case «0»
j : Fin 2
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) j = (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case «1»
j : Fin 2
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) j = (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) j

Tactic:
fin_cases j

Goal state after:
case «1».«0»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case «0»
j : Fin 2
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, 0; 0, -1] ((fun i ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)