mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:

Tactic:
dist x z = dist x.1 z.1 + |1 / infDist x.1 sᶜ - 1 / infDist z.1 sᶜ| := rfl
      _ ≤ dist x.1 y.1 + dist y.1 z.1 + (|1 / infDist x.1 sᶜ - 1 / infDist y.1 sᶜ| +
            |1 / infDist y.1 sᶜ - 1 / infDist z.1 sᶜ|) :=
        add_le_add (dist_triangle _ _ _) (dist_triangle (1 / infDist _ _) _ _)
      _ = dist x y + dist y z := add_add_add_comm ..

Goal state after:
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ Antitone fun n ↦ A (res x n)

Tactic:
refine antitone_nat_of_succ_le ?_

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ ∀ (n : ℕ), A (res x (n + 1)) ⊆ A (res x n)
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol : μ univ < ↑n * μ s
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
by
  have A : ∀ m, NullMeasurableSet (f^[m] ⁻¹' s) μ := fun m ↦
    hs.preimage (hf.iterate m).quasiMeasurePreserving
  have B : ∀ m, μ (f^[m] ⁻¹' s) = μ s := fun m ↦ (hf.iterate m).measure_preimage hs
  have : μ (univ : Set α) < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s) := by simpa [B]
  obtain ⟨i, hi, j, hj, hij, x, hxi : f^[i] x ∈ s, hxj : f^[j] x ∈ s⟩ :
      ∃ i < n, ∃ j < n, i ≠ j ∧ (f^[i] ⁻¹' s ∩ f^[j] ⁻¹' s).Nonempty := by
    simpa using exists_nonempty_inter_of_measure_univ_lt_sum_measure μ (fun m _ ↦ A m) this
  wlog hlt : i < j generalizing i j
  · exact this j hj i hi hij.symm hxj hxi (hij.lt_or_gt.resolve_left hlt)
  refine ⟨f^[i] x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, ?_⟩
  rwa [← iterate_add_apply, tsub_add_cancel_of_le hlt.le]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂Measure.map Subtype.val (Measure.comap Subtype.val μ) = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
map_comap_subtype_coe hs

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (x : α) in s, f x ∂μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
⊢ AnalyticSet (⋂ n, s n)

Tactic:
have : PolishSpace t := t_closed.polishSpace

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
⊢ AnalyticSet (⋂ n, s n)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∈ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * 1

Tactic:
mul_one,

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∈ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∈ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c

Tactic:
rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
b : Set (Set ↑(range f))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable ↑b
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α

Tactic:
have : ∀ s : b, IsClopenable (rangeFactorization f ⁻¹' s) := fun s ↦ by
    apply MeasurableSet.isClopenable
    exact hf.subtype_mk (hb.isOpen s.2).measurableSet

Goal state after:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
b : Set (Set ↑(range f))
b_count : b.Countable
hb : IsTopologicalBasis b
this✝ : Countable ↑b
this : ∀ (s : ↑b), IsClopenable (rangeFactorization f ⁻¹' ↑s)
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [SFinite μ],
    IsFiniteMeasure μ → ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
· choose g hgm hgle hgint using fun n ↦ @this (sfiniteSeq μ n) _ inferInstance
    refine ⟨fun x ↦ ⨆ n, g n x, .iSup hgm, fun x ↦ iSup_le (hgle · x), fun s ↦ ?_⟩
    rw [← sum_sfiniteSeq μ, Measure.restrict_sum_of_countable,
      lintegral_sum_measure, lintegral_sum_measure]
    exact ENNReal.tsum_le_tsum fun n ↦ (hgint n s).trans (lintegral_mono fun x ↦ le_iSup (g · x) _)

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case left
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
⊢ {p | edist p.1 p.2 < ε} ∈ ⨅ i, ⨅ i_1, ⨅ (_ : 0 < i_1), 𝓟 {a | edist (a.1 i) (a.2 i) < i_1}

Tactic:
obtain ⟨K, hK⟩ : ∃ K : Finset ι, ∑' i : {j // j ∉ K}, 2⁻¹ ^ encode (i : ι) < ε / 2 :=
        ((tendsto_order.1 <| ENNReal.tendsto_tsum_compl_atTop_zero
          (tsum_geometric_encode_lt_top ENNReal.one_half_lt_one).ne).2 _
            <| by simpa using hε.ne').exists

Goal state after:
case left
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
⊢ {p | edist p.1 p.2 < ε} ∈ ⨅ i, ⨅ i_1, ⨅ (_ : 0 < i_1), 𝓟 {a | edist (a.1 i) (a.2 i) < i_1}
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
m : MeasurableSpace X
inst✝³ : BorelSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
mZ : MeasurableSpace Z
inst✝¹ : BorelSpace Z
μ : Measure Z
inst✝ : μ.IsOpenPosMeasure
f : X → Z
hf : IsOpenEmbedding f
U : Set X
hU : IsOpen[inst✝⁴] U
Une : U.Nonempty
⊢ (comap f μ) U ≠ 0

Tactic:
by
    rw [hf.measurableEmbedding.comap_apply]
    exact IsOpenPosMeasure.open_pos _ (hf.isOpen_iff_image_isOpen.mp hU) (Une.image f)

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
⊢ ∃ F, IsEmbedding F

Tactic:
by
  let firststep : X ≃ₜ PiNatEmbed X (fun i => I) (distDenseSeq X) := {
    toFun := toPiNat
    invFun := ofPiNat
    left_inv _ := rfl
    right_inv _ := rfl
    continuous_toFun := continuous_toPiNat <| fun i ↦ continuous_distDenseSeq i
    continuous_invFun := continuous_distDenseSeq_inv }
  let secondstep : PiNatEmbed X (fun i => I) (distDenseSeq X) → ℕ → I := embed _ _ _
  let isEmbedding_secondstep : IsEmbedding secondstep :=
      (isUniformEmbedding_embed injective_distDenseSeq).isEmbedding
  exact ⟨_, isEmbedding_secondstep.comp firststep.isEmbedding⟩

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x ↦ ↑x.1 * ↑x.2) y = x * ↑y.2
⊢ x ∈ S

Tactic:
← mul_right_cancel hy

Goal state after:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x ↦ ↑x.1 * ↑x.2) y = x * ↑y.2
⊢ ↑y.1 ∈ S
Module: Mathlib.MeasureTheory.Measure.Prod

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

Tactic:
exact h hs ht

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
⊢ IsComplement S T ↔ ∀ (g : G), ∃! t, g * (↑t)⁻¹ ∈ S

Tactic:
by
  convert! isComplement_iff_existsUnique with g
  constructor <;> rintro ⟨x, hx, hx'⟩
  · exact ⟨(⟨_, hx⟩, x), by simp, by aesop⟩
  · exact ⟨x.2, by simp [← hx], fun y hy ↦ (Prod.ext_iff.1 <| by simpa using hx' (⟨_, hy⟩, y)).2⟩

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

Goal state before:
pp: case refine_3
α : 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₂
⊢ ∀ t ∈ C, μ t = ν t

Tactic:
rintro - ⟨s, hs, -, ⟨t, ht, u, hu, rfl⟩, rfl⟩

Goal state after:
case refine_3
α : 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 : Set α
hs : s ∈ {s | MeasurableSet s}
t : Set β
ht : t ∈ {t | MeasurableSet t}
u : Set γ
hu : u ∈ {u | MeasurableSet u}
⊢ μ ((fun x1 x2 ↦ x1 ×ˢ x2) s ((fun x1 x2 ↦ x1 ×ˢ x2) t u)) = ν ((fun x1 x2 ↦ x1 ×ˢ x2) s ((fun x1 x2 ↦ x1 ×ˢ x2) t u))
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
⊢ ⋃ n, s ∩ B n = s

Tactic:
rw [← inter_iUnion, iUnion_spanningSets, inter_univ]

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 μ
s : Set α
t : Set β
i : ℕ × ℕ
s' : Set α
t' : Set β
hs' : MeasurableSet s'
ht' : MeasurableSet t'
⊢ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)) (s' ×ˢ t' ∩ s ×ˢ t) =
    ((sfiniteSeq μ i.1).restrict s) s' * ((sfiniteSeq ν i.2).restrict t) t'

Tactic:
prod_inter_prod,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
i : ℕ × ℕ
s' : Set α
t' : Set β
hs' : MeasurableSet s'
ht' : MeasurableSet t'
⊢ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)) ((s' ∩ s) ×ˢ (t' ∩ t)) =
    ((sfiniteSeq μ i.1).restrict s) s' * ((sfiniteSeq ν i.2).restrict t) t'
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]

Tactic:
let A : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
  intro U hU r hr
  rcases hU.exists_iUnion_isClosed with ⟨F, F_closed, -, rfl, F_mono⟩
  rw [F_mono.measure_iUnion] at hr
  rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
  exact ⟨F n, subset_iUnion _ _, F_closed n, hn⟩

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
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 ∂μ.prod ν

Tactic:
← (measurePreserving_mul_prod_inv μ ν).map_eq

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 ν)
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
⊢ μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * f x⁻¹ ∂μ

Tactic:
by
  rw [← setLIntegral_one, ← lintegral_indicator sm,
    ← lintegral_lintegral_mul (measurable_const.indicator sm).aemeasurable hf.aemeasurable,
    ← lintegral_lintegral_mul_inv μ ν]
  swap
  · exact (((measurable_const.indicator sm).comp measurable_fst).mul
      (hf.comp measurable_snd)).aemeasurable
  have ms :
    ∀ x : G, Measurable fun y => ((fun z => z * x) ⁻¹' s).indicator (fun _ => (1 : ℝ≥0∞)) y :=
    fun x => measurable_const.indicator (measurable_mul_const _ sm)
  have : ∀ x y, s.indicator (fun _ : G => (1 : ℝ≥0∞)) (y * x) =
      ((fun z => z * x) ⁻¹' s).indicator (fun b : G => 1) y := by
    intro x y; symm; convert! indicator_comp_right (M := ℝ≥0∞) fun y => y * x using 2; ext1; rfl
  simp_rw [this, lintegral_mul_const _ (ms _), lintegral_indicator (measurable_mul_const _ sm),
    setLIntegral_one]

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 * ν univ = ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * 1 ∂μ
⊢ μ s = 0

Tactic:
mul_one,

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 * ν univ = ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) ∂μ
⊢ μ s = 0
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:
simp_rw [Ne, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inr.inl.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + b * ((-c - 1) / b) + c
⊢ b * b - 4 * 0 * c ≤ 0

Tactic:
mul_div_cancel₀ _ hb

Goal state after:
case inr.inl.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + (-c - 1) + c
⊢ b * b - 4 * 0 * c ≤ 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x

pp: case htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x

Tactic:
· have Z := hg.ae_eq_mk
        rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z
        filter_upwards [Z]
        intro x hx
        simp only [g', hx, Pi.mul_apply]

Goal state after:
case htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞

Tactic:
rw [← hasFiniteIntegral_iff_ofReal]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ HasFiniteIntegral bound μ

α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ 0 ≤ᵐ[μ] bound
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 ≠ ∞
⊢ μ.withDensity (f * fun i ↦ (f i)⁻¹) = μ

Tactic:
suffices (f * fun x ↦ (f x)⁻¹) =ᵐ[μ] 1 by
    rw [withDensity_congr_ae this, withDensity_one]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ (f * fun x ↦ (f x)⁻¹) =ᵐ[μ] 1
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
⊢ star B * 1 * B = 1

Tactic:
mul_one,

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
⊢ star B * B = 1
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 * 1 * star U = 1

Tactic:
mul_one,

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 * star U = 1
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
a b : G
⊢ star a * (a * b⁻¹) = star b * 1 ↔ star a * a = star b * b

Tactic:
mul_one,

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
a b : G
⊢ star a * (a * b⁻¹) = star b ↔ star a * a = star b * b
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1⋆ * 1‖ = 1 * ‖1‖

Tactic:
mul_one,

Goal state after:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1⋆‖ = 1 * ‖1‖
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case neg
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

Tactic:
tsum_eq_zero_of_not_summable hf,

Goal state after:
case neg
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
⊢ ∑'[L] (z : ι), e (f z) = y ↔ 0 = e.symm y