mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
a : α
ha : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 ha.choose)

Tactic:
exact ha.choose_spec

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case ha
α : Type ?u.3
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : ↑unitInterval
⊢ 0 ≤ ↑s * (1 - ↑t)

Tactic:
nlinarith [s.2.1, t.2.2]

Goal state after:
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y : X
⊢ (if x = y then 0 else 1) = if y = x then 0 else 1

Tactic:
by
        obtain h | h := eq_or_ne x y
        · simp [h]
        · simp [h, h.symm]

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

Goal state before:
pp: α : Type u_2
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ y ∈ cylinder x n ↔ y ∈ {y | res y n = res x n}

Tactic:
dsimp [cylinder]

Goal state after:
α : Type u_2
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ (∀ i < n, y i = x i) ↔ res y n = res x n
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
⊢ ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε

Tactic:
intro y hy z hz

Goal state after:
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ dist y z < ε
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
hA : VanishingDiam A
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
⊢ ∃ n, ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε

Tactic:
specialize hA x
  rw [ENNReal.tendsto_atTop_zero] at hA
  obtain ⟨n, hn⟩ := hA (ENNReal.ofReal (ε / 2)) (by
    simp only [gt_iff_lt, ENNReal.ofReal_pos]; linarith)
  use n
  intro y hy z hz
  rw [← ENNReal.ofReal_lt_ofReal_iff ε_pos, ← edist_dist]
  apply lt_of_le_of_lt (Metric.edist_le_ediam_of_mem hy hz)
  apply lt_of_le_of_lt (hn _ (le_refl _))
  rw [ENNReal.ofReal_lt_ofReal_iff ε_pos]
  linarith

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

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (inducedMap A).snd

Tactic:
by
  rw [Metric.continuous_iff']
  rintro x ε ε_pos
  obtain ⟨n, hn⟩ := hA.dist_lt _ ε_pos x
  rw [_root_.eventually_nhds_iff]
  refine ⟨(↑)⁻¹' cylinder x.1 n, ?_, ?_, by simp⟩
  · rintro y hyx
    rw [mem_preimage, Subtype.coe_mk, cylinder_eq_res, mem_ofPred] at hyx
    apply hn
    · rw [← hyx]
      apply map_mem
    apply map_mem
  apply continuous_subtype_val.isOpen_preimage
  apply isOpen_cylinder

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopenable s
⊢ IsClopenable sᶜ

Tactic:
rcases hs with ⟨t, t_le, t_polish, h, h'⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t : TopologicalSpace α
t_le : t ≤ inst✝
t_polish : PolishSpace α
h : IsClosed[t] s
h' : IsOpen[t] s
⊢ IsClopenable sᶜ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : StandardBorelSpace α
⊢ MeasurableEq α

Tactic:
let := upgradeStandardBorel α

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : StandardBorelSpace α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ MeasurableEq α
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ AnalyticSet ∅

Tactic:
rw [AnalyticSet]
  exact Or.inl rfl

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
⊢ μ (s ∪ sᶜ) = 0

Tactic:
measure_union disjoint_compl_right hs.compl,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
⊢ μ s + μ sᶜ = 0
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ ∀ (b' : ↑(range points)),
    b' ≠ ⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩ → μ (measurableAtom ↑b') * (measurableAtom x).indicator 1 ↑b' = 0

Tactic:
· simp only [ne_eq, mul_eq_zero, indicator_apply_eq_zero, Pi.one_apply, one_ne_zero, imp_false,
      Subtype.forall, Set.mem_range, Subtype.exists, Subtype.mk.injEq, forall_exists_index]
    refine fun y s hs hsy hyx ↦ .inr fun hyx' ↦ hyx ?_
    rw [← hsy]
    congr
    have h1 : measurableAtom y = measurableAtom x := measurableAtom_eq_of_mem hyx'
    have h2 : measurableAtom y = s := by
      specialize h_points_mem ⟨s, hs⟩
      obtain ⟨z, _, hz⟩ := hs
      simp only at h_points_mem
      rw [← hz, ← hsy]
      refine measurableAtom_eq_of_mem ?_
      convert! h_points_mem
    rw [← h2, h1]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
⊢ s ∈ ae (dirac a) ↔ a ∈ s

Tactic:
by_cases a ∈ s

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
h✝ : a ∈ s
⊢ s ∈ ae (dirac a) ↔ a ∈ s

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
h✝ : a ∉ s
⊢ s ∈ ae (dirac a) ↔ a ∈ s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ ∫⁻ (x : α) in s, f x ∂dirac a = if a ∈ s then f a else 0

Tactic:
rw [restrict_dirac' hs]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
t : Set α
hst : sᶜ ⊆ t
htm : MeasurableSet t
ht : (fun μ ↦ μ t) =ᵐ[m] 0
⊢ {a | s ∈ ae a} ∈ ae m

Tactic:
exact ht.mono fun _ ↦ measure_mono_null hst

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure α
s : Set α
hs : MeasurableSet s
⊢ (m.bind dirac) s = m s

Tactic:
simp only [bind_apply hs measurable_dirac.aemeasurable, dirac_apply' _ hs, lintegral_indicator hs,
    Pi.one_apply, lintegral_one, restrict_apply, MeasurableSet.univ, univ_inter]

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

Goal state before:
pp: case const
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
simp only [hs, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero, univ_inter,
      piecewise_eq_indicator, lintegral_indicator, lintegral_const, Measure.restrict_apply',
      ENNReal.coe_indicator, Function.const_apply] at hL
    have c_ne_zero : c ≠ 0 := by
      intro hc
      simp only [hc, ENNReal.coe_zero, zero_mul, not_lt_zero] at hL
    have : L / c < μ s := by
      rwa [ENNReal.div_lt_iff, mul_comm]
      · simp only [c_ne_zero, Ne, ENNReal.coe_eq_zero, not_false_iff, true_or]
      · simp only [Ne, coe_ne_top, not_false_iff, true_or]
    obtain ⟨t, ht, ts, mlt, t_top⟩ :
      ∃ t : Set α, MeasurableSet t ∧ t ⊆ s ∧ L / ↑c < μ t ∧ μ t < ∞ :=
      Measure.exists_subset_measure_lt_top hs this
    refine ⟨piecewise t ht (const α c) (const α 0), fun x => ?_, ?_, ?_⟩
    · refine indicator_le_indicator_of_subset ts (fun x => ?_) x
      exact zero_le
    · simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero, univ_inter,
        piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
        lintegral_const, Measure.restrict_apply', ENNReal.mul_lt_top ENNReal.coe_lt_top t_top]
    · simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero,
        piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
        lintegral_const, Measure.restrict_apply', univ_inter]
      rwa [mul_comm, ← ENNReal.div_lt_iff]
      · simp only [c_ne_zero, Ne, ENNReal.coe_eq_zero, not_false_iff, true_or]
      · simp only [Ne, coe_ne_top, not_false_iff, true_or]

Goal state after:
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:
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
firststep : X ≃ₜ PiNatEmbed X (fun i ↦ ↑I) (distDenseSeq X) :=
  { toFun := toPiNat, invFun := ofPiNat, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
secondstep : PiNatEmbed X (fun i ↦ ↑I) (distDenseSeq X) → ℕ → ↑I := embed X (fun i ↦ ↑I) (distDenseSeq X)
isEmbedding_secondstep : IsEmbedding secondstep :=
  IsUniformEmbedding.isEmbedding (isUniformEmbedding_embed injective_distDenseSeq)
⊢ ∃ F, IsEmbedding F

Tactic:
exact ⟨_, isEmbedding_secondstep.comp firststep.isEmbedding⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' S ×ˢ T) ∂μ = μ S * ν T

Tactic:
classical
      simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, mul_comm]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
ϕ : ↥H × ↥K ≃ ↥K × ↥H :=
  { toFun := fun x ↦ (x.2⁻¹, x.1⁻¹), invFun := fun x ↦ (x.2⁻¹, x.1⁻¹), left_inv := ⋯, right_inv := ⋯ }
ψ : G ≃ G := { toFun := fun g ↦ g⁻¹, invFun := fun g ↦ g⁻¹, left_inv := ⋯, right_inv := ⋯ }
⊢ (⇑ψ ∘ fun x ↦ ↑x.1 * ↑x.2) = (fun x ↦ ↑x.1 * ↑x.2) ∘ ⇑ϕ

Tactic:
exact funext fun x => mul_inv_rev _ _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
ν : Measure α
hμ : μ.InnerRegularWRT p q
hν : ν.InnerRegularWRT p q
hμν : ∀ (U : Set α), p U → μ U = ν U
U : Set α
hU : q U
⊢ μ U = ν U

Tactic:
rw [hμ.measure_eq_iSup hU, hν.measure_eq_iSup hU]
  congr! 4 with t _ ht2
  exact hμν t ht2

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
⊢ S.Nonempty

Tactic:
by
  contrapose! hst; simp [hst]

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
⊢ T.Nonempty

Tactic:
by
  contrapose! hst; simp [hst]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
⊢ Nat.card ↥(map H.subtype H'') * Nat.card ↑(⇑H.subtype '' S) = Nat.card ↥H

Tactic:
· have : Nat.card H'' * Nat.card S = Nat.card H := cmem.card_mul_card
    rw [← this]
    refine congr_arg₂ (· * ·) ?_ ?_ <;>
      exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
⊢ (hSK.equiv g₁).1 = (hSK.equiv g₂).1 → g₁⁻¹ * g₂ ∈ K

pp: case mpr
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
⊢ g₁⁻¹ * g₂ ∈ K → (hSK.equiv g₁).1 = (hSK.equiv g₂).1

Tactic:
· intro h
    rw [← hSK.equiv_fst_mul_equiv_snd g₂, ← hSK.equiv_fst_mul_equiv_snd g₁, ← h,
      mul_inv_rev, ← mul_assoc, inv_mul_cancel_right, ← coe_inv, ← coe_mul]
    exact Subtype.property _

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
⊢ g₁⁻¹ * g₂ ∈ K → (hSK.equiv g₁).1 = (hSK.equiv g₂).1
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > (x • μ) A
⊢ ∃ U ⊇ A, IsOpen[inst✝¹] U ∧ (x • μ) U < r

Tactic:
rw [smul_apply, A.measure_eq_iInf_isOpen, smul_eq_mul] at hr

Goal state after:
case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > x * ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst✝¹] U), μ U
⊢ ∃ U ⊇ A, IsOpen[inst✝¹] U ∧ (x • μ) U < r
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
⊢ H.IsComplement' (MulAction.stabilizer G a)

Tactic:
refine isComplement_iff_existsUnique.mpr fun g => ?_
  obtain ⟨h, hh⟩ := h2 g
  have hh' : (↑h * g) • a = a := by rwa [mul_smul]
  refine ⟨⟨h⁻¹, h * g, hh'⟩, inv_mul_cancel_left ↑h g, ?_⟩
  rintro ⟨h', g, hg : g • a = a⟩ rfl
  specialize h1 (h * h') (by rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg])
  refine Prod.ext (eq_inv_of_mul_eq_one_right h1) (Subtype.ext ?_)
  rwa [Subtype.ext_iff, coe_one, coe_mul, ← right_eq_mul, mul_assoc (↑h) (↑h') g] at h1

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 μ
μ' : Measure α
inst✝ : SFinite μ'
⊢ (μ + μ').prod ν = μ.prod ν + μ'.prod ν

Tactic:
simp_rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq μ', sum_add_sum, ← sum_sfiniteSeq ν, prod_sum,
    sum_add_sum]
  congr
  ext1 i
  refine prod_eq fun s t _ _ => ?_
  simp_rw [add_apply, prod_prod, right_distrib]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Mul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
c : ℝ≥0∞
g : G
⊢ Measure.map (fun x ↦ g * x) (c • μ) = c • μ

Tactic:
by rw [Measure.map_smul, map_mul_left_eq_self]

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

Goal state before:
pp: case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
⊢ MeasurableSet {x | Cauchy (map (fun n ↦ f n x) l)}

Tactic:
change MeasurableSet { x | _ ∧ _ }

Goal state after:
case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
⊢ MeasurableSet {x | (map (fun n ↦ f n x) l).NeBot ∧ map (fun n ↦ f n x) l ×ˢ map (fun n ↦ f n x) l ≤ uniformity γ}
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✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ Measurable (Exists.choose hm)

Tactic:
exact measurable_of_tendsto_metrizable' L.filter (by fun_prop) hm.choose_spec

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)
⊢ Measurable (∏'[L] (i : ι), f i)

Tactic:
rw [tprod_def, finprod_def']
  split_ifs with hm
  any_goals exact measurable_one
  · refine Finset.measurable_prod_apply (fun _ _ ↦ ?_) measurable_id
    rw [Set.mulIndicator]
    split_ifs <;> fun_prop
  · exact measurable_of_tendsto_metrizable' L.filter (by fun_prop) hm.choose_spec

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

Goal state before:
pp: α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
⊢ ∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s

Tactic:
let := upgradeStandardBorel α

Goal state after:
α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ ∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
h : ¬Countable α
⊢ Nonempty (α ≃ᵐ (ℕ → Bool))

Tactic:
let := upgradeStandardBorel α

Goal state after:
α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
h : ¬Countable α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ Nonempty (α ≃ᵐ (ℕ → Bool))
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
x y : G
⊢ (y * x, x⁻¹) = (y * x, x⁻¹ * y⁻¹ * y)

Tactic:
inv_mul_cancel_right

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

Goal state before:
pp: case succ
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
n : ℕ
IH : IsCompact (L n)
⊢ IsCompact (L (n + 1))

Tactic:
simp_rw [L, iterate_succ']

Goal state after:
case succ
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
n : ℕ
IH : IsCompact (L n)
⊢ IsCompact (((fun T ↦ T ∪ g T • K) ∘ (fun T ↦ T ∪ g T • K)^[n]) K)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s = 0
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K

Tactic:
simp only [h, zero_add] at hr

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
h : μ s = 0
hr : r < ν s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K