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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ (μ.restrict (μ.sigmaFiniteSetWRT' ν)).FiniteSpanningSetsIn (Set.range f)

Tactic:
refine ⟨fun n ↦ f (e n), fun _ ↦ by simp, fun n ↦ ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ (μ.restrict (μ.sigmaFiniteSetWRT' ν)) (f (e n)) < ∞

case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ ⋃ i, f (e i) = Set.univ
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case specialize_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝¹] t →
      IsClosed[inst✝¹] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ U ⊆ {x} ∪ closure[inst✝¹] (U \ {x})

Tactic:
trans {x} ∪ (U \ {x})
    · simp
    apply Set.union_subset_union_right
    exact subset_closure

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

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := fun t ↦ Nat.rec (motive := fun x ↦ α → ℝ≥0∞) (g 0) (fun n I x ↦ max (g (n + 1) x) (I x)) t
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
have M n : Measurable (g' n) := by
    induction n with
    | zero => simp [g', gmeas 0]
    | succ n ih => exact Measurable.max (gmeas (n + 1)) ih

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := fun t ↦ Nat.rec (motive := fun x ↦ α → ℝ≥0∞) (g 0) (fun n I x ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ |b - b| ≤ c - d

pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ |c - d| ≤ c - d

Tactic:
· rwa [sub_self, abs_zero]

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ |c - d| ≤ c - d
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: case h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : IsCompletelyPseudoMetrizableSpace X
inst✝ : T0Space X
this : UpgradedIsCompletelyPseudoMetrizableSpace X := ⋯
⊢ PseudoMetricSpace.toUniformSpace.toTopologicalSpace = inst✝² ∧ CompleteSpace X

Tactic:
exact ⟨rfl, by infer_instance⟩

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

Goal state before:
pp: case mpr.inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
i : ℕ
hi : i < n + 1
h'i : i < n
⊢ y i = update x n (y n) i

pp: case mpr.inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
i : ℕ
H : ∀ i_1 < i, y i_1 = x i_1
hi : i < i + 1
⊢ y i = update x i (y i) i

Tactic:
· simp [H i h'i, h'i.ne]

Goal state after:
case mpr.inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
i : ℕ
H : ∀ i_1 < i, y i_1 = x i_1
hi : i < i + 1
⊢ y i = update x i (y i) i
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : IsCompletelyMetrizableSpace α
this : UpgradedIsCompletelyMetrizableSpace α := upgradeIsCompletelyMetrizable α
⊢ PolishSpace α

Tactic:
have := UniformSpace.secondCountable_of_separable α

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : IsCompletelyMetrizableSpace α
this✝ : UpgradedIsCompletelyMetrizableSpace α := upgradeIsCompletelyMetrizable α
this : SecondCountableTopology α
⊢ PolishSpace α
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e) μc μa
⊢ MeasurePreserving (g ∘ ⇑e) μc μb ↔ MeasurePreserving g μa μb

Tactic:
refine ⟨fun hg => ?_, fun hg => hg.comp h⟩
  convert! hg.comp (MeasurePreserving.symm e h)
  simp [Function.comp_assoc g e e.symm]

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen[inst✝¹] s
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
⊢ AnalyticSet (f '' s)

Tactic:
image_eq_range

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen[inst✝¹] s
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
⊢ AnalyticSet (range fun x ↦ f ↑x)
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: case refine_2
α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ b.2 s

Tactic:
· exact (Measure.measurable_coe hs).comp measurable_snd

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure (Measure α)
⊢ (c • m).join = c • m.join

Tactic:
by
  ext s hs
  simp [hs]

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

Goal state before:
pp: case hfg
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
m : Measure (Measure α)
g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hfg_int : ∫⁻ (a : α), f a ∂m.join = ∫⁻ (a : α), g a ∂m.join
μ : Measure α
x : α
⊢ g x ≤ f x

Tactic:
apply hgf

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

Goal state before:
pp: case h
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)ᶜ
⊢ min (2⁻¹ ^ encode ↑i) (edist (x ↑i) (y ↑i)) ≤ 2⁻¹ ^ encode ↑i

Tactic:
apply min_le_left

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

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
ε : ℝ
hεn : ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
hε : ∀ (x : α), μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * μ (closedBall x ε)
x : α
⊢ μ (closedBall x (2 ^ n * 2 * ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)

Tactic:
mul_assoc,

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
ε : ℝ
hεn : ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
hε : ∀ (x : α), μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * μ (closedBall x ε)
x : α
⊢ μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x ↦ ν (Prod.mk x ⁻¹' f i)
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' ⋃ i, f i)

Tactic:
have (a : α) : ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, ν (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      exacts [hfd.mono fun _ _ ↦ .preimage _, fun i ↦ measurable_prodMk_left (hfm i)]
    simpa only [this] using Measurable.tsum ihf

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
x : M
μ : Measure M
inst✝ : SFinite μ
⊢ map ((fun x ↦ x.1 * x.2) ∘ Prod.mk x) μ = map (fun y ↦ x * y) μ

Tactic:
simp [Function.comp_def]

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✝ : SFinite μ
x : M
⊢ map ((fun x ↦ x.1 * x.2) ∘ fun x_1 ↦ (x_1, x)) μ = map (fun y ↦ y * x) μ

Tactic:
simp [Function.comp_def]

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]

Goal state after:
α : 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
⊢ ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), ν K
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 ↔ MulOpposite.op g₁ • ↑H = MulOpposite.op g₂ • ↑H

Tactic:
rightCoset_eq_iff

Goal state after:
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 ↔ g₂ * g₁⁻¹ ∈ H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ ↑(hHT.equiv g₂).1 * ↑(hHT.equiv g₁).2 * ((↑(hHT.equiv g₁).2)⁻¹ * (↑(hHT.equiv g₁).1)⁻¹) ∈ H

Tactic:
mul_assoc,

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ ↑(hHT.equiv g₂).1 * (↑(hHT.equiv g₁).2 * ((↑(hHT.equiv g₁).2)⁻¹ * (↑(hHT.equiv g₁).1)⁻¹)) ∈ H
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝¹ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this✝ : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
this : Tendsto (fun n ↦ 2 * u n) atTop (𝓝 0)
⊢ CauchySeq y

Tactic:
refine cauchySeq_of_le_tendsto_0' (fun n => 2 * u n) (fun m n hmn => ?_) this

Goal state after:
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝¹ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this✝ : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
this : Tendsto (fun n ↦ 2 * u n) atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
⊢ dist (y m) (y n) ≤ 2 * u m
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝¹ : SMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ μ ((fun x ↦ c • x) ⁻¹' s) = μ s

Tactic:
rw [← measure_toMeasurable s,
    ← SMulInvariantMeasure.measure_preimage_smul c (measurableSet_toMeasurable μ s)]
  exact measure_congr (tendsto_smul_ae μ c hs.toMeasurable_ae_eq) |>.symm

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
r : ℝ≥0∞
hr : r < μ s
h0 : p ∅
⊢ ∃ ε, ε ≠ 0 ∧ ε + ε ≤ μ s ∧ r = μ s - (ε + ε)

Tactic:
use (μ s - r) / 2

Goal state after:
case h
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
r : ℝ≥0∞
hr : r < μ s
h0 : p ∅
⊢ (μ s - r) / 2 ≠ 0 ∧ (μ s - r) / 2 + (μ s - r) / 2 ≤ μ s ∧ r = μ s - ((μ s - r) / 2 + (μ s - r) / 2)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_4
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst✝⁵] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)

Tactic:
image_eq_range

Goal state after:
γ : Type u_3
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_4
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst✝⁵] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (range fun x ↦ f ↑x)
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}
ht' : t'.Countable
x✝ : α
⊢ x✝ ∈ t ↔ x✝ ∈ t \ t' ∪ t'

Tactic:
simp only [sdiff_sep_self, not_not, mem_union, mem_ofPred_eq, t']

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
x✝ : α
⊢ x✝ ∈ t ↔ x✝ ∈ t ∧ ContinuousWithinAt g t x✝ ∨ x✝ ∈ t ∧ ¬ContinuousWithinAt g t x✝
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case hf
α : 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 (map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)))

Tactic:
convert! hf

Goal state after:
α : 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))
⊢ map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)) = (μ.prod ν).restrict (s ×ˢ t)
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 μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ μ s⁻¹ = 0 ↔ μ s = 0

Tactic:
by
  refine ⟨fun hs => ?_, (quasiMeasurePreserving_inv μ).preimage_null⟩
  rw [← inv_inv s]
  exact (quasiMeasurePreserving_inv μ).preimage_null hs

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
⊢ discrim a b c = 0 ↔ ∃! x, a * (x * x) + b * x + c = 0

Tactic:
by
  refine ⟨fun hd => ?_, discrim_eq_zero_of_existsUnique ha⟩
  simp_rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha hd, existsUnique_eq]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, g x ∂μ.withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ

Tactic:
restrict_withDensity hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α), g x ∂(μ.restrict s).withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
⊢ a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0

Tactic:
mul_assoc,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
⊢ a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c = 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ √x < y ↔ x < y ^ 2

Tactic:
rw [← sqrt_lt_sqrt_iff_of_pos (pow_pos hy _), sqrt_sq hy.le]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
restrict_withDensity hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
Module: Mathlib.Analysis.Complex.Norm

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

Tactic:
mul_assoc,

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

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

Tactic:
rw [norm_mul_self_eq_normSq, add_mul_self_eq, norm_mul_self_eq_normSq, norm_mul_self_eq_normSq,
      add_right_comm, normSq_add, mul_assoc, norm_def, norm_def, ← Real.sqrt_mul <| normSq_nonneg z,
      ← normSq_conj w, ← map_mul]
    gcongr
    exact re_le_norm (z * conj w)

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

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

Tactic:
normSq_neg

Goal state after:
z : ℂ
⊢ √(normSq z) = √(normSq z)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
restrict_withDensity hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
hs : MeasurableSet s
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
restrict_withDensity hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
hs : MeasurableSet s
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ