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

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
⊢ ∑' (C : Finset ι), ∑ i ∈ F, (G i).indicator (fun C ↦ (μ.restrict (P C)) t) C =
    ∑ C ∈ Cs, ∑ i ∈ F, (↑C).indicator (fun x ↦ (μ.restrict (P C)) t) i

Tactic:
rw [sum_eq_tsum_indicator]

Goal state after:
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
⊢ ∑' (C : Finset ι), ∑ i ∈ F, (G i).indicator (fun C ↦ (μ.restrict (P C)) t) C =
    ∑' (x : Finset ι), (↑Cs).indicator (fun C ↦ ∑ i ∈ F, (↑C).indicator (fun x ↦ (μ.restrict (P C)) t) i) x
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:

Tactic:
sum f s = sum f t := measure_congr ht.symm
  _ = ∑' i, f i t := sum_apply _ t_meas
  _ ≤ ∑' i, f i s := ENNReal.tsum_le_tsum fun i ↦ measure_mono ts

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι✝ : Sort y
s t u : Set α
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : MeasurableSpace α
inst✝¹⁴ : OpensMeasurableSpace α
inst✝¹³ : TopologicalSpace β
inst✝¹² : MeasurableSpace β
inst✝¹¹ : OpensMeasurableSpace β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : MeasurableSpace γ
inst✝⁸ : BorelSpace γ
inst✝⁷ : TopologicalSpace γ₂
inst✝⁶ : MeasurableSpace γ₂
inst✝⁵ : BorelSpace γ₂
inst✝⁴ : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Subsingleton ι
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
h : Nonempty ι
this : Unique ι
⊢ borel ((i : ι) → X i) ≤ MeasurableSpace.pi

Tactic:
borel,

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι✝ : Sort y
s t u : Set α
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : MeasurableSpace α
inst✝¹⁴ : OpensMeasurableSpace α
inst✝¹³ : TopologicalSpace β
inst✝¹² : MeasurableSpace β
inst✝¹¹ : OpensMeasurableSpace β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : MeasurableSpace γ
inst✝⁸ : BorelSpace γ
inst✝⁷ : TopologicalSpace γ₂
inst✝⁶ : MeasurableSpace γ₂
inst✝⁵ : BorelSpace γ₂
inst✝⁴ : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Subsingleton ι
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
h : Nonempty ι
this : Unique ι
⊢ MeasurableSpace.generateFrom {s | IsOpen[topologicalSpace] s} ≤ MeasurableSpace.pi
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ∃ F,
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Tactic:
obtain ⟨a, a_pos, a_lt_one⟩ : ∃ a : ℝ≥0∞, 0 < a ∧ a < 1 := exists_between zero_lt_one
  let F := fun n : ℕ => (fun x => infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
  have F_subset : ∀ n, F n ⊆ U := fun n x hx ↦ by
    by_contra h
    have : infEDist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
    exact this (infEDist_zero_of_mem h)
  refine ⟨F, fun n => IsClosed.preimage continuous_infEDist isClosed_Ici, F_subset, ?_, ?_⟩
  · show ⋃ n, F n = U
    refine Subset.antisymm (by simp only [iUnion_subset_iff, F_subset, forall_const]) fun x hx => ?_
    have : x ∉ Uᶜ := by simpa using hx
    rw [mem_iff_infEDist_zero_of_closed hU.isClosed_compl] at this
    have B : 0 < infEDist x Uᶜ := by simpa [pos_iff_ne_zero] using this
    have : Filter.Tendsto (fun n => a ^ n) atTop (𝓝 0) :=
      ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one a_lt_one
    rcases ((tendsto_order.1 this).2 _ B).exists with ⟨n, hn⟩
    simp only [mem_iUnion]
    exact ⟨n, hn.le⟩
  show Monotone F
  intro m n hmn x hx
  simp only [F, mem_Ici, mem_preimage] at hx ⊢
  apply le_trans (pow_le_pow_right_of_le_one' a_lt_one.le hmn) hx

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
s : Set α
t : Set β
⊢ ⨅ i, ⨅ j, ⨅ (_ : (i, j).1 ∈ s ∧ (i, j).2 ∈ t), max (edist x.1 i) (edist x.2 j) =
    max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y)

Tactic:
iInf_and,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
s : Set α
t : Set β
⊢ ⨅ i, ⨅ j, ⨅ (_ : i ∈ s), ⨅ (_ : j ∈ t), max (edist x.1 i) (edist x.2 j) =
    max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hE : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Tactic:
rw [cthickening_eq_biUnion_closedBall E hδ, hE.closure_eq]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ∞
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun r ↦ μ (cthickening r s)) (𝓝 0) (𝓝 (μ s))

Tactic:
convert! tendsto_measure_cthickening hs
  exact h's.closure_eq.symm

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (support ⇑f)

Tactic:
f.support_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (⋃ y ∈ {y ∈ f.range | y ≠ 0}, ⇑f ⁻¹' {y})
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x ↦ ∑' (i : ι), f i x

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_sum]
  exact .iSup fun s ↦ s.measurable_fun_sum fun i _ => h i

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x ↦ ∑' (i : ι), f i x

Tactic:
NNReal.tsum_eq_toNNReal_tsum

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x ↦ (∑' (b : ι), ↑(f b x)).toNNReal
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_5
x✝ : MeasurableSpace α
ι : Type u_6
inst✝ : Countable ι
f : ι → α → ℝ≥0
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x ↦ ∑' (i : ι), f i x) μ

Tactic:
NNReal.tsum_eq_toNNReal_tsum

Goal state after:
α : Type u_5
x✝ : MeasurableSpace α
ι : Type u_6
inst✝ : Countable ι
f : ι → α → ℝ≥0
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x ↦ (∑' (b : ι), ↑(f b x)).toNNReal) μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n ↦ {x | f x ≤ ↑n}
x : α
⊢ x ∈ ⋃ n, norm_sets n ↔ x ∈ univ

Tactic:
simp only [Set.mem_iUnion, Set.mem_univ, iff_true]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n ↦ {x | f x ≤ ↑n}
x : α
⊢ ∃ i, x ∈ norm_sets i
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
inst✝ : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : μ sᶜ = 0
a✝ : Nontrivial α
a : α
⊢ AEStronglyMeasurable id μ

Tactic:
refine ⟨(closure s).piecewise id (fun _ ↦ a), ?_,
    Filter.mem_of_superset h2 (fun x hx ↦ by simp [subset_closure hx])⟩

Goal state after:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
inst✝ : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : μ sᶜ = 0
a✝ : Nontrivial α
a : α
⊢ StronglyMeasurable ((closure[inst✝²] s).piecewise id fun x ↦ a)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ⨆ x, ((↑x).restrict s).lintegral μ ≤ ⨆ x, (↑x).lintegral μ

Tactic:
refine iSup_mono' (Subtype.forall.2 fun φ hφ => ?_)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a ↦ f a
⊢ ∃ i', ((↑⟨φ, hφ⟩).restrict s).lintegral μ ≤ (↑i').lintegral μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
this : ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ, s ⊆ t → MeasurableSet t → μ t = ∞
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
⊢ μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ∞

Tactic:
have hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ := Set.subset_inter hts hs_subset

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
this : ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ, s ⊆ t → MeasurableSet t → μ t = ∞
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ
⊢ μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ⨆ i, (μ.restrict (spanningSets μ i)) (μ.sigmaFiniteSetWRT ν)ᶜ = 0

Tactic:
simp_rw [Measure.restrict_apply' (measurableSet_spanningSets μ _), ENNReal.iSup_eq_zero]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ∀ (i : ℕ), μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst✝¹] C
⊢ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C

Tactic:
have : ∀ y, y ≠ x ∧ y ∈ closure C → ∃ᶠ z in 𝓝 y, z ≠ x ∧ z ∈ C := by
    rintro y ⟨hyx, yC⟩
    simp only [← mem_compl_singleton_iff, and_comm, ← frequently_nhdsWithin_iff,
      hyx.nhdsWithin_compl_singleton, ← mem_closure_iff_frequently]
    exact yC

Goal state after:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst✝¹] C
this : ∀ (y : α), y ≠ x ∧ y ∈ closure[inst✝¹] C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C
⊢ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
⊢ (μ.restrict μ.sigmaFiniteSetᶜ) s = 0 ∨ (μ.restrict μ.sigmaFiniteSetᶜ) s = ∞

Tactic:
Measure.restrict_apply' measurableSet_sigmaFiniteSet.compl

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
⊢ μ (s ∩ μ.sigmaFiniteSetᶜ) = 0 ∨ μ (s ∩ μ.sigmaFiniteSetᶜ) = ∞
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
⊢ IsClosed[inst✝¹] D

Tactic:
refine hclosed.sdiff (isOpen_biUnion fun _ ↦ ?_)
    exact fun ⟨Ub, _⟩ ↦ IsTopologicalBasis.isOpen bbasis Ub

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X ⊕ Y
⊢ Sum.dist x x = 0

Tactic:
cases x <;> simp only [Sum.dist, dist_self]

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

Goal state before:
pp: case succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
ih : res (↑x) n = res (↑y) n
⊢ ↑x n = ↑y n ∧ res (↑x) n = res (↑y) n

Tactic:
refine ⟨?_, ih⟩

Goal state after:
case succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
ih : res (↑x) n = res (↑y) n
⊢ ↑x n = ↑y n
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
⊢ P

Tactic:
exact ⟨C, ⟨hC, hnonempty⟩⟩

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

Goal state before:
pp: case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd)

Tactic:
· have : max x.1 y.1 ≤ succ m := by simp [hx, hy]
      have : max x.1 y.1 ≤ m := by simpa [h] using of_le_succ this
      have xm : x.1 ≤ m := le_trans (le_max_left _ _) this
      have ym : y.1 ≤ m := le_trans (le_max_right _ _) this
      rw [leRecOn_succ xm, leRecOn_succ ym, (I m).dist_eq]
      exact inductiveLimitDist_eq_dist I x y m xm ym

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
s : Finset α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, f x * μ {x}

Tactic:
simp only [lintegral_countable _ s.countable_toSet, ← Finset.tsum_subtype']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : AEMeasurable f m
⊢ ∫⁻ (μ : Measure β), μ s ∂map f m = ∫⁻ (a : α), (f a) s ∂m

Tactic:
lintegral_map' (measurable_coe hs).aemeasurable hf

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : AEMeasurable f m
⊢ ∫⁻ (a : α), (f a) s ∂m = ∫⁻ (a : α), (f a) s ∂m
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: 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
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * ↑K.card < ε / 2
x y : (i : ι) → F i
hxy : ∀ (x_1 : ι) (h : x_1 ∈ K), edist (x x_1) (y x_1) < δ
⊢ ∑ _i ∈ K, δ + ε / 2 ≤ ε / 2 + ε / 2

Tactic:
by gcongr; simpa [mul_comm] using hδ.le

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

Goal state before:
pp: E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → EMetricSpace (F i)
⊢ ∀ {x y : (i : ι) → F i}, edist x y = 0 → x = y

Tactic:
simp [edist_eq_tsum, funext_iff]

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

Goal state before:
pp: ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
⊢ Summable fun i ↦ min (2⁻¹ ^ encode i) (dist (x i) (y i))

Tactic:
refine .of_nonneg_of_le (fun i => ?_) (fun i => min_le_left _ _) <| by
    simpa [one_div] using summable_geometric_two_encode

Goal state after:
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
i : ι
⊢ 0 ≤ min (2⁻¹ ^ encode i) (dist (x i) (y i))
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
⊢ (hHT.equiv g₁).2 = (hHT.equiv g₂).2 ↔ RightCosetEquivalence (↑H) g₁ g₂

Tactic:
rw [RightCosetEquivalence, rightCoset_eq_iff]
  constructor
  · intro h
    rw [← hHT.equiv_fst_mul_equiv_snd g₂, ← hHT.equiv_fst_mul_equiv_snd g₁, ← h,
      mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← coe_inv, ← coe_mul]
    exact Subtype.property _
  · intro h
    apply (isComplement_iff_existsUnique_mul_inv_mem.1 hHT g₁).unique
    · -- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
      rw [equiv_snd_eq_inv_mul]; simp
    · rw [SetLike.mem_coe, ← mul_mem_cancel_left h]
      -- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
      rw [equiv_snd_eq_inv_mul, mul_assoc]; simp

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
⊢ IsCompl H K

Tactic:
refine
    ⟨disjoint_iff_inf_le.mpr fun g ⟨p, q⟩ =>
        let x : H × K := ⟨⟨g, p⟩, 1⟩
        let y : H × K := ⟨1, g, q⟩
        Subtype.ext_iff.mp
          (Prod.ext_iff.mp (show x = y from h.1 ((mul_one g).trans (one_mul g).symm))).1,
      codisjoint_iff_le_sup.mpr fun g _ => ?_⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
g : G
x✝ : g ∈ ⊤
⊢ g ∈ H ⊔ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s ↦ MeasurableSet s ∧ μ s ≠ ∞
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ∞
r : ℝ≥0∞
hr : r < (μ.restrict A) s
⊢ ∃ K ⊆ toMeasurable μ (s ∩ A) ∩ s, p K ∧ r < μ K

Tactic:
by
    have : r < μ ((toMeasurable μ (s ∩ A)) ∩ s) := by
      apply hr.trans_le
      rw [restrict_apply s_meas]
      exact measure_mono <| subset_inter (subset_toMeasurable μ (s ∩ A)) inter_subset_left
    refine h ⟨(measurableSet_toMeasurable _ _).inter s_meas, ?_⟩ _ this
    apply (lt_of_le_of_lt _ hs.lt_top).ne
    rw [← measure_toMeasurable (s ∩ A)]
    exact measure_mono inter_subset_left

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

Goal state before:
pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : DivInvMonoid G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ Measure.map (fun x ↦ x / g) μ = μ

Tactic:
by simp_rw [div_eq_mul_inv, map_mul_right_eq_self μ g⁻¹]

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 γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
⊢ (map (fun a ↦ (X a, Y a)) μ).fst = map X μ

Tactic:
by
  by_cases hX : AEMeasurable X μ
  · ext1 s hs
    rw [Measure.fst_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_fst hs),
      Measure.map_apply_of_aemeasurable hX hs, ← prod_univ, mk_preimage_prod, preimage_univ,
      inter_univ]
  · have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by
      contrapose hX
      exact measurable_fst.comp_aemeasurable hX
    simp [map_of_not_aemeasurable, hX, this]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ μ.withDensity (s.indicator f) = (μ.restrict s).withDensity f

Tactic:
by
  ext1 t ht
  rw [withDensity_apply _ ht, lintegral_indicator hs, restrict_comm hs, ←
    withDensity_apply _ ht]

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s * s = (2 * a * x + b) ^ 2 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)

Tactic:
sq,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s * s = (2 * a * x + b) * (2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
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 μ
c : ℝ≥0∞
hc : c ≠ ∞
⊢ HasFiniteIntegral f (c • μ)

Tactic:
by
  simp only [HasFiniteIntegral, lintegral_smul_measure] at *
  exact mul_lt_top hc.lt_top h

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

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

Tactic:
sq,

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ √x * √x = x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ √(x ^ 2) = x

Tactic:
sq,

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x = y ↔ x = y ^ 2

Tactic:
sq,

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

Goal state before:
pp: x : ℝ
⊢ √(x ^ 2) = |x|

Tactic:
sq,

Goal state after:
x : ℝ
⊢ √(x * x) = |x|
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ x.toNNReal ≤ y.toNNReal ^ 2 ↔ x ≤ y ^ 2

Tactic:
sq,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ x.toNNReal ≤ y.toNNReal * y.toNNReal ↔ x ≤ y ^ 2