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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
⊢ QuasiMeasurePreserving Prod.fst (μ.prod ν) μ

Tactic:
refine ⟨measurable_fst, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
  rw [map_apply measurable_fst hs, ← prod_univ, ← nonpos_iff_eq_zero]
  refine (prod_prod_le _ _).trans_eq ?_
  rw [h2s, zero_mul]

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

Goal state before:
pp: X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
f : X → Z
inst✝ : CountablySeparated ↑(range f)
hf : Measurable f
s : Set Z
⊢ Measurable (rangeFactorization f)

Tactic:
fun_prop

Goal state after:
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
this : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g
| (hST.equiv (hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩))).1

Tactic:
Equiv.apply_symm_apply

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
this : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g
| (⟨g, hg⟩, ⟨1, h1⟩).1
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 ∈ S
hg : g ∈ T
this : hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g
| (hST.equiv (hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩))).2

Tactic:
Equiv.apply_symm_apply

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
this : hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g
| (⟨1, h1⟩, ⟨g, hg⟩).2
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : ↑↑T
ht1 : (↑t)⁻¹ * f⁻¹ • g ∈ ↑H
ht2 : ∀ (y : ↑↑T), (fun s ↦ (↑s)⁻¹ * f⁻¹ • g ∈ ↑H) y → y = t
t' : G
ht' : t' ∈ ↑T
h : t'⁻¹ * f⁻¹ • g ∈ H
⊢ t' = ↑t

Tactic:
exact Subtype.ext_iff.mp (ht2 ⟨t', ht'⟩ h)

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 μ
ν : Measure ((α × β) × γ)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ Measurable ⇑MeasurableEquiv.prodAssoc

Tactic:
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 α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
⊢ map Prod.swap (μ.prod ν) = ν.prod μ

Tactic:
by
  have : 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))) := by
    ext s hs
    rw [sum_apply _ hs, sum_apply _ hs]
    exact ((Equiv.prodComm ℕ ℕ).tsum_eq _).symm
  rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, prod_sum, prod_sum,
    map_sum measurable_swap.aemeasurable, this]
  congr 1
  ext1 i
  refine (prod_eq ?_).symm
  intro s t hs ht
  simp_rw [map_apply measurable_swap (hs.prod ht), preimage_swap_prod, prod_prod, mul_comm]

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 μ
p : α → β → Prop
h : MeasurableSet {x | p x.1 x.2}
⊢ AEMeasurable Prod.swap (ν.prod μ)

Tactic:
fun_prop

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 α μ
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousConstSMul G α
inst✝ : MulAction.IsMinimal G α
U : Set α
hU : IsOpen[inst✝²] U
hne : U.Nonempty
hμU : μ U ≠ ∞
x : α
g : G
hg : g • x ∈ U
⊢ μ ((fun x ↦ g • x) ⁻¹' U) ≠ ∞

Tactic:
measure_preimage_smul

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
μ : Measure α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousConstSMul G α
inst✝ : MulAction.IsMinimal G α
U : Set α
hU : IsOpen[inst✝²] U
hne : U.Nonempty
hμU : μ U ≠ ∞
x : α
g : G
hg : g • x ∈ U
⊢ μ U ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case compl
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : Set α
hs : MeasurableSet s
H : ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hFs : F ⊆ s
U : Set α
hsU : U ⊇ s
hFc : IsClosed[inst✝²] F
hUo : IsOpen[inst✝²] U
hF : μ s ≤ μ F + ε
hU : μ U ≤ μ s + ε
⊢ ∃ F ⊆ sᶜ, ∃ U ⊇ sᶜ, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ sᶜ ≤ μ F + ε ∧ μ U ≤ μ sᶜ + ε

Tactic:
refine
      ⟨Uᶜ, compl_subset_compl.2 hsU, Fᶜ, compl_subset_compl.2 hFs, hUo.isClosed_compl,
        hFc.isOpen_compl, ?_⟩

Goal state after:
case compl
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : Set α
hs : MeasurableSet s
H : ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hFs : F ⊆ s
U : Set α
hsU : U ⊇ s
hFc : IsClosed[inst✝²] F
hUo : IsOpen[inst✝²] U
hF : μ s ≤ μ F + ε
hU : μ U ≤ μ s + ε
⊢ μ sᶜ ≤ μ Uᶜ + ε ∧ μ Fᶜ ≤ μ sᶜ + ε
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst✝² : SFinite μ
inst✝¹ : SFinite τ
inst✝ : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ Measurable (Prod.map f g)

Tactic:
fun_prop

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 γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst✝² : SFinite μ
inst✝¹ : SFinite τ
inst✝ : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ Measurable f

Tactic:
fun_prop

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 γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst✝² : SFinite μ
inst✝¹ : SFinite τ
inst✝ : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ Measurable g

Tactic:
fun_prop

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 : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
⊢ ↑H.index * μ ↑H = μ univ

Tactic:
obtain ⟨s, hs, -⟩ := H.exists_isComplement_left 1

Goal state after:
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul G
H : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s ↑H
⊢ ↑H.index * μ ↑H = μ univ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
f g : α × β → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ.prod ν] g
⊢ Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν

Tactic:
fun_prop

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
⊢ Measurable fun x ↦ g * x

Tactic:
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 α
ν : Measure β
inst✝ : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.bind fun x ↦ map (Prod.mk x) ν)
a : α
ha : AEMeasurable f (map (Prod.mk a) ν)
⊢ AEMeasurable (Prod.mk a) ν

Tactic:
fun_prop

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
this : ⇑f '' (fun x ↦ g * x) ⁻¹' s = (fun x ↦ f g * x) ⁻¹' ⇑f '' s
⊢ Measurable fun x ↦ f g * x

Tactic:
fun_prop

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
⊢ Measurable fun x ↦ x * g

Tactic:
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 α
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ AEMeasurable (fun z ↦ f z.1 * g z.2) (μ.prod ν)

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u_6
E✝ : Type u_7
ι : Type u_8
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : CommMonoid E✝
inst✝⁸ : TopologicalSpace E✝
inst✝⁷ : IsCompletelyPseudoMetrizableSpace E✝
inst✝⁶ : SecondCountableTopology E✝
inst✝⁵ : MeasurableSpace E✝
inst✝⁴ : BorelSpace E✝
inst✝³ : MeasurableMul₂ E✝
inst✝² : Countable ι
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E✝
h : ∀ (i : ι), Measurable (f i)
E : Set X := {x | Multipliable (fun x_1 ↦ f x_1 x) L}
⊢ ∀ (i : Finset ι), Measurable fun x ↦ ∏ b ∈ i, (fun x_1 ↦ f x_1 x) b

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u_6
E✝ : Type u_7
ι : Type u_8
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : CommMonoid E✝
inst✝⁸ : TopologicalSpace E✝
inst✝⁷ : IsCompletelyPseudoMetrizableSpace E✝
inst✝⁶ : SecondCountableTopology E✝
inst✝⁵ : MeasurableSpace E✝
inst✝⁴ : BorelSpace E✝
inst✝³ : MeasurableMul₂ E✝
inst✝² : Countable ι
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E✝
h : ∀ (i : ι), Measurable (f i)
E : Set X := {x | Multipliable (fun x_1 ↦ f x_1 x) L}
hE : MeasurableSet E
h0 : (Eᶜ.domRestrict fun x ↦ ∏'[L] (i : ι), f i x) = fun x ↦ 1
⊢ ∀ (i : Finset ι), Measurable fun e ↦ ∏ b ∈ i, (fun x ↦ f x ↑e) b

Tactic:
fun_prop

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
this : ⇑f '' (fun x ↦ x * g) ⁻¹' s = (fun x ↦ x * f g) ⁻¹' ⇑f '' s
⊢ Measurable fun x ↦ x * f g

Tactic:
fun_prop

Goal state after:
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)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∈ L.support
⊢ Measurable ↿fun a ↦ f x✝¹.down

Tactic:
fun_prop

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

Goal state before:
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✝¹ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∉ L.support
⊢ Measurable ↿fun a ↦ 1

Tactic:
fun_prop

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

Goal state before:
pp: 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
⊢ ∀ (i : Finset ι), Measurable (∏ b ∈ i, (fun i ↦ f i) b)

Tactic:
fun_prop

Goal state after:
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
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (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)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∈ L.support
⊢ AEMeasurable (f x✝¹.down) μ

Tactic:
fun_prop

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

Goal state before:
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
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (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)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∉ L.support
⊢ AEMeasurable 1 μ

Tactic:
fun_prop

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

Goal state before:
pp: case neg.hf
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
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (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
⊢ ∀ (n : Finset ι), AEMeasurable (∏ i ∈ n, f i) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : Inv G
f : G → ℝ≥0∞
μ : Measure G
⊢ 0 ⋆ₘₗ[μ] f = 0

Tactic:
by
  ext; simp [mlconvolution]

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : Inv G
f : G → ℝ≥0∞
μ : Measure G
⊢ f ⋆ₘₗ[μ] 0 = 0

Tactic:
by
  ext; simp [mlconvolution]

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Mul G
inst✝³ : Inv G
inst✝² : MeasurableMul₂ G
inst✝¹ : MeasurableInv G
f g : G → ℝ≥0∞
μ : Measure G
inst✝ : SFinite μ
hf : Measurable f
hg : Measurable g
⊢ Measurable fun x ↦ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
⊢ AEMeasurable (fun y_1 ↦ g y_1 * k (y_1⁻¹ * (y⁻¹ * x))) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
⊢ AEMeasurable (fun y_1 ↦ f y_1 * g (y_1⁻¹ * y)) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ AEMeasurable (Function.uncurry fun y x_1 ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)

Tactic:
fun_prop

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

Goal state before:
pp: case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := ⋯
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

Tactic:
have A : μ.withDensity f t = 0 := by rw [measure_toMeasurable, hs]

Goal state after:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : (μ.withDensity f) t = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0
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 α
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
U : Set α
hUo : IsOpen[inst✝⁴] U
hμU : μ U < ∞
hUs : μ (U ∆ t) < ε
⊢ μ (U ∆ s) < ε

Tactic:
rwa [measure_congr <| (ae_eq_refl _).symmDiff hst]

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

Goal state before:
pp: case inr
G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ✝ : Measure G
inst✝⁶ : μ✝.IsHaarMeasure
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : T1Space G
inst✝² : WeaklyLocallyCompactSpace G
inst✝¹ : (𝓝[≠] 1).NeBot
μ : Measure G
inst✝ : μ.IsHaarMeasure
h : μ 1 ≠ 0
⊢ NullSingletonClass μ

Tactic:
| inr h =>

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
this : ↑(f a) ≠ 0
⊢ ↑(f a) * g a = ↑(f a) * g' a

Tactic:
ha this

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
this : ↑(f a) ≠ 0
⊢ ↑(f a) * g' a = ↑(f a) * g' a
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ count.withDensity f = sum fun a ↦ f a • dirac a

Tactic:
by
  simp [count, withDensity_sum, dirac_withDensity' hf _]

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

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

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

Goal state before:
pp: x : ℝ
⊢ √x ^ 2 = max x 0

Tactic:
rcases lt_trichotomy x 0 with _ | _ | _

Goal state after:
case inl
x : ℝ
h✝ : x < 0
⊢ √x ^ 2 = max x 0

case inr.inl
x : ℝ
h✝ : x = 0
⊢ √x ^ 2 = max x 0

case inr.inr
x : ℝ
h✝ : 0 < x
⊢ √x ^ 2 = max x 0
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ normSq (z + w) ≤ normSq z + 2 * ‖z‖ * ‖w‖ + normSq w

Tactic:
add_right_comm,

Goal state after:
z w : ℂ
⊢ normSq (z + w) ≤ normSq z + normSq w + 2 * ‖z‖ * ‖w‖
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x : ℂ
⊢ 1 < normSq x ↔ 1 < ‖x‖

Tactic:
rw [← one_lt_sq_iff₀ (norm_nonneg _), normSq_eq_norm_sq]

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

Goal state before:
pp: z : ℂ
⊢ normSq z - z.re ^ 2 = z.im ^ 2

Tactic:
normSq_apply,

Goal state after:
z : ℂ
⊢ z.re * z.re + z.im * z.im - z.re ^ 2 = z.im ^ 2