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

Goal state before:
pp: case mp.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
y : E i
hy : dist x y < ε ∧ dist x y < 1
⊢ ⟨i, y⟩ ∈ s

Tactic:
exact hε (mem_ball'.2 hy.1)

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)
this : Antitone fun n ↦ A (res x n)
n m : ℕ
hnm : n ≤ m
⊢ u m ∈ A (res x n)

Tactic:
exact this hnm (hu _)

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
⊢ (inducedMap A).fst = univ

Tactic:
rw [eq_univ_iff_forall]
  intro x
  choose u hu using fun n => hnonempty (res x n)
  have umem : ∀ n m : ℕ, n ≤ m → u m ∈ A (res x n) := by
    have : Antitone fun n : ℕ => A (res x n) := by
      refine antitone_nat_of_succ_le ?_
      intro n
      apply hanti.antitone
    intro n m hnm
    exact this hnm (hu _)
  have : CauchySeq u := by
    rw [Metric.cauchySeq_iff]
    intro ε ε_pos
    obtain ⟨n, hn⟩ := hdiam.dist_lt _ ε_pos x
    use n
    intro m₀ hm₀ m₁ hm₁
    apply hn <;> apply umem <;> assumption
  obtain ⟨y, hy⟩ := cauchySeq_tendsto_of_complete this
  use y
  rw [mem_iInter]
  intro n
  apply hanti _ (x n)
  apply mem_closure_of_tendsto hy
  rw [eventually_atTop]
  exact ⟨n.succ, umem _⟩

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

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ dist ⟨n.succ, f n x⟩.snd (f n ⟨n, x⟩.snd) = 0

pp: case h1
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n, x⟩.fst ≤ n

pp: case hx
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n.succ, f n x⟩.fst ≤ n.succ

pp: case hy
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n, x⟩.fst ≤ n.succ

Tactic:
dist_self

Goal state after:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ 0 = 0

case h1
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n, x⟩.fst ≤ n

case hx
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n.succ, f n x⟩.fst ≤ n.succ

case hy
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n, x⟩.fst ≤ n.succ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ ∫⁻ (a : β), AEMeasurable.mk f hf a ∂Measure.map g μ =
    ∫⁻ (a : β), AEMeasurable.mk f hf a ∂Measure.map (AEMeasurable.mk g hg) μ

Tactic:
by
      congr 1
      exact Measure.map_congr hg.ae_eq_mk

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : ν₁ s = 0
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : μ t = 0
htν₂ : ν₂ tᶜ = 0
this : μ s = μ (s ∩ tᶜ)
⊢ ν₁ (s ∩ tᶜ) = 0 ∧ ν₂ (s ∩ tᶜ) = 0

Tactic:
exact ⟨measure_inter_null_of_null_left _ hs_zero, measure_inter_null_of_null_right _ htν₂⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ (map (fun x ↦ c) μ) s = μ univ * s.indicator 1 c

Tactic:
classical
  rw [Measure.map_apply measurable_const hs, Set.preimage_const]
  by_cases hsc : c ∈ s
  · rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]
  · rw [if_neg hsc, (Set.indicator_eq_zero_iff_notMem _).mpr hsc, measure_empty, mul_zero]

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

Goal state before:
pp: case iUnion
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable (⋃ i, f i)

Tactic:
· exact fun f _ _ hf => IsClopenable.iUnion hf

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
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α

Tactic:
by
  obtain ⟨b, b_count, -, hb⟩ :
      ∃ b : Set (Set (range f)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b :=
    exists_countable_basis (range f)
  have : Countable b := b_count.to_subtype
  have : ∀ s : b, IsClopenable (rangeFactorization f ⁻¹' s) := fun s ↦ by
    apply MeasurableSet.isClopenable
    exact hf.subtype_mk (hb.isOpen s.2).measurableSet
  choose T Tt Tpolish _ Topen using this
  obtain ⟨t', t'T, t't, t'_polish⟩ :
      ∃ t' : TopologicalSpace α, (∀ i, t' ≤ T i) ∧ t' ≤ t ∧ @PolishSpace α t' :=
    exists_polishSpace_forall_le (t := t) T Tt Tpolish
  refine ⟨t', t't, ?_, t'_polish⟩
  have : Continuous[t', _] (rangeFactorization f) :=
    hb.continuous_iff.2 fun s hs => t'T ⟨s, hs⟩ _ (Topen ⟨s, hs⟩)
  exact continuous_subtype_val.comp this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ Measurable fun μ ↦ map f μ

Tactic:
refine measurable_of_measurable_coe _ fun s hs => ?_
  simp_rw [map_apply hf hs]
  exact measurable_coe (hf hs)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
⊢ ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * ∫⁻ (μ : Measure α), μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m =
    ∫⁻ (μ : Measure α), ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m

Tactic:
suffices
    ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞), (∀ n r, Measurable (f n r)) →
      Monotone (fun n μ => ∑ r ∈ s n, r * f n r μ) →
      ⨆ n, ∑ r ∈ s n, r * ∫⁻ μ, f n r μ ∂m = ∫⁻ μ, ⨆ n, ∑ r ∈ s n, r * f n r μ ∂m by
    refine
      this (fun n => SimpleFunc.range (SimpleFunc.eapprox f n))
        (fun n r μ => μ (SimpleFunc.eapprox f n ⁻¹' {r})) ?_ ?_
    · exact fun n r => measurable_coe (SimpleFunc.measurableSet_preimage _ _)
    · exact fun n m h μ => SimpleFunc.lintegral_mono (SimpleFunc.monotone_eapprox _ h) le_rfl

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
⊢ ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ) →
        ⨆ n, ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (μ : Measure α), ⨆ n, ∑ r ∈ s n, r * f n r μ ∂m
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
⊢ Measurable fun x ↦ map (Prod.mk x) ν

Tactic:
apply measurable_of_measurable_coe; intro s hs
  simp_rw [map_apply measurable_prodMk_left hs]
  exact measurable_measure_prodMk_left hs

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
x y : M
| s.indicator 1 (x * y)

Tactic:
change s.indicator 1 ((fun y ↦ x * y) y)

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
x y : M
| s.indicator 1 ((fun y ↦ x * y) y)
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
⊢ map (⇑L) (μ ∗ₘ ν) = map (⇑L) μ ∗ₘ map (⇑L) ν

Tactic:
unfold mconv
  rw [map_map (by fun_prop) (by fun_prop)]
  have : (L ∘ fun p : M × M ↦ p.1 * p.2) = (fun p : M' × M' ↦ p.1 * p.2) ∘ (Prod.map L L) := by
    ext; simp
  rw [this, ← map_map (by fun_prop) (by fun_prop), ← map_prod_map _ _ (by fun_prop) (by 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 α μ
c : G
s : Set α
⊢ μ (c • s) = μ s

Tactic:
simpa only [preimage_smul_inv] using measure_preimage_smul μ c⁻¹ s

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

Goal state before:
pp: M : Type uM
α : Type uα
β : Type uβ
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableConstSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ (f ⁻¹' (fun x ↦ m • x) ⁻¹' S) = μ ((fun x ↦ m • f x) ⁻¹' S)

Tactic:
preimage_preimage

Goal state after:
M : Type uM
α : Type uα
β : Type uβ
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableConstSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ ((fun x ↦ m • f x) ⁻¹' S) = μ ((fun x ↦ m • f x) ⁻¹' 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 γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
a : α
ha : map (g a) μc = μd
⊢ μc ((fun x ↦ (f (a, x).1, g (a, x).1 (a, x).2)) ⁻¹' s) = μc (g a ⁻¹' Prod.mk (f a) ⁻¹' s)

Tactic:
preimage_preimage

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
a : α
ha : map (g a) μc = μd
⊢ μc ((fun x ↦ (f (a, x).1, g (a, x).1 (a, x).2)) ⁻¹' s) = μc ((fun x ↦ (f a, g a x)) ⁻¹' 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 γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun y ↦ f (x, y)) ν τ
s : Set γ
hs : MeasurableSet s
h2s : τ s = 0
⊢ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' f ⁻¹' s) ∂μ = 0

Tactic:
preimage_preimage

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun y ↦ f (x, y)) ν τ
s : Set γ
hs : MeasurableSet s
h2s : τ s = 0
⊢ ∫⁻ (x : α), ν ((fun x_1 ↦ f (x, x_1)) ⁻¹' s) ∂μ = 0
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : BorelSpace α
inst✝⁸ : LinearOrder α
inst✝⁷ : OrderTopology α
inst✝⁶ : PolishSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : LinearOrder β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x | x ∈ t ∧ ¬ContinuousWithinAt g t x}
⊢ MeasurableSet (g '' t)

Tactic:
have ht' : Set.Countable t' := hg.countable_not_continuousWithinAt

Goal state after:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : BorelSpace α
inst✝⁸ : LinearOrder α
inst✝⁷ : OrderTopology α
inst✝⁶ : PolishSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : LinearOrder β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
⊢ MeasurableSet (g '' t)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ AEMeasurable f ((μ.restrict s).prod (ν.restrict t))

Tactic:
rwa [Measure.prod_restrict]

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)
⊢ AEMeasurable (∏ i ∈ Finite.toFinset h✝, L.support.mulIndicator (fun i ↦ f i) i.down) μ

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✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ AEMeasurable (Exists.choose hm) μ

Tactic:
· refine Finset.aemeasurable_prod _ (fun _ _ ↦ ?_)
    rw [Set.mulIndicator]
    split_ifs <;> fun_prop

Goal state after:
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✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ AEMeasurable (Exists.choose hm) μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ.withDensity f = 0 ↔ f =ᵐ[μ] 0

Tactic:
by
  rw [← measure_univ_eq_zero, withDensity_apply _ .univ, restrict_univ, lintegral_eq_zero_iff' hf]

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 α := toMeasurable (μ.withDensity f) s
A : μ {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0 a)} = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

Tactic:
simp only [Pi.zero_apply] at A

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 : μ {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 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✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun h ↦ g / h) μ μ

Tactic:
rw [← μ.inv_inv]
  exact
    (quasiMeasurePreserving_div_left μ.inv g).mono (inv_absolutelyContinuous μ.inv)
      (absolutelyContinuous_inv μ.inv)

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

Goal state before:
pp: case refine_1.hs
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ μ (spanningSets μ n ∩ f ⁻¹' Iic ↑n) ≠ ∞

Tactic:
exact ((measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ n)).ne

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

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
h : HasFiniteIntegral f μ
s : Set α
⊢ HasFiniteIntegral f (μ.restrict s)

Tactic:
refine lt_of_le_of_lt ?_ h
  simpa [Measure.restrict_univ] using lintegral_mono_set (subset_univ s)

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

Goal state before:
pp: ⊢ normSq I = 1

Tactic:
by simp [normSq]

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

Goal state before:
pp: z : ℂ
⊢ normSq (-z) = normSq z

Tactic:
by simp [normSq]

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

Goal state before:
pp: z : ℂ
⊢ normSq ((starRingEnd ℂ) z) = normSq z

Tactic:
by simp [normSq]

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

Goal state before:
pp: case zero
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x ^ 2 ^ 0‖₊ = ‖x‖₊ ^ 2 ^ 0

Tactic:
simp only [pow_zero, pow_one]

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

Goal state before:
pp: z : ℂ
R : Type u_1
inst✝¹ : NormedField R
inst✝ : NormedAlgebra R ℝ
r : R
x : ℂ
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
← algebraMap_smul ℝ r x,

Goal state after:
z : ℂ
R : Type u_1
inst✝¹ : NormedField R
inst✝ : NormedAlgebra R ℝ
r : R
x : ℂ
⊢ ‖(algebraMap R ℝ) r • x‖ ≤ ‖r‖ * ‖x‖
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ ^ n = 1 ^ n

Tactic:
by rw [← nnnorm_pow, h, nnnorm_one, one_pow]

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

Goal state before:
pp: case inr
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.im RCLike.I = 1
⊢ ‖↑(RCLike.re a) + ↑(RCLike.im a) * I‖ = ‖a‖

Tactic:
exact (RCLike.complexLinearIsometryEquiv h).norm_map a

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

Goal state before:
pp: ⊢ ∀ (x y : ℤ), dist ↑x ↑y = dist x y

Tactic:
by simp_rw [← Complex.ofReal_intCast,
    Complex.isometry_ofReal.dist_eq, Int.dist_cast_real, implies_true]

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

Goal state before:
pp: z : ℂ
hz : z ∈ Metric.ball 1 1
⊢ 0 < z.re

Tactic:
simpa using (re_le_norm _).trans_lt (mem_ball_iff_norm'.1 hz)

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ re ↑(‖x‖ ^ 2) = ‖↑(‖x‖ ^ 2)‖

Tactic:
simp [-map_pow]

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ Continuous[instTopologicalSpaceSubtype, inst✝⁵] (f.target.domRestrict f.invFun)

Tactic:
← continuous_codRestrict_iff (s := f.source) (by simp)

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype]
    (codRestrict (f.target.domRestrict f.invFun) f.source ⋯)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ tanh (-x) = -tanh x

Tactic:
by simp [tanh, neg_div]

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

Goal state before:
pp: x : ℂ
⊢ cos (x * I) = cosh x

Tactic:
rw [← cosh_mul_I]

Goal state after:
x : ℂ
⊢ cosh (x * I * I) = cosh x
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x‖ ^ 1 * (↑(Nat.succ 1) * (↑(Nat.factorial 1) * ↑1)⁻¹) = 2 * ‖x‖

Tactic:
by simp [mul_two, mul_add, mul_comm, Nat.factorial]

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

Goal state before:
pp: x : ℝ
⊢ ↑(sinh x ^ 2) = ↑(cosh x ^ 2 - 1)

Tactic:
simp [sinh_sq]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
k : ℕ
hk : m = k + n.succ
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
induction k generalizing m n with

Goal state after: