mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: q : ℚ
⊢ (Ioi ↑q).Nontrivial

Tactic:
exact ⟨q + 1, show (q : ℝ) < _ by linarith, q + 2, show (q : ℝ) < _ by linarith, by simp⟩

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

Goal state before:
pp: case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
⊢ Measurable fun b ↦ ⨆ i ∈ s, f i b

Tactic:
· have : ∀ b, ⨆ i ∈ s, f i b = (⨆ (i : s), f i b) ⊔ sSup ∅ :=
      fun b ↦ cbiSup_eq_of_not_forall (f := fun i ↦ f i b) H
    simp only [this]
    apply Measurable.sup _ measurable_const
    exact .iSup (fun (i : s) ↦ hf i i.2)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MulZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (f * g).FinMeasSupp μ

Tactic:
rw [mul_eq_map₂]
  exact hf.map₂ hg (zero_mul 0)

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)
x : α
⊢ (∑' (i : ι), f i) x = ∑' (i : ι), f i x

Tactic:
exact tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : PseudoMetricSpace β
inst✝ : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : ℕ → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
x : α
hx : ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
⊢ Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))

Tactic:
rw [tendsto_iff_dist_tendsto_zero]

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : PseudoMetricSpace β
inst✝ : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : ℕ → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
x : α
hx : ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
⊢ Tendsto (fun b ↦ dist (f b x) (g x)) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: X : Type u_3
Y : Type u_4
α : Type u_5
inst✝¹⁰ : Zero α
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : OpensMeasurableSpace Y
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetrizableSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : ℕ → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n) x) < u n
x : X × Y
⊢ Tendsto (fun n ↦ (g n) x) atTop (𝓝 (f x))

Tactic:
rw [tendsto_iff_dist_tendsto_zero]

Goal state after:
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝¹⁰ : Zero α
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : OpensMeasurableSpace Y
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetrizableSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : ℕ → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n) x) < u n
x : X × Y
⊢ Tendsto (fun b ↦ dist ((g b) x) (f x)) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : c ≤ ‖(hf.approx n) x‖
⊢ ‖(hf.approx n) x‖ * ‖c‖ / ‖(hf.approx n) x‖ ≤ c

Tactic:
div_eq_mul_inv,

Goal state after:
case neg.inr
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : c ≤ ‖(hf.approx n) x‖
⊢ ‖(hf.approx n) x‖ * ‖c‖ * ‖(hf.approx n) x‖⁻¹ ≤ c
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
rw [lintegral_congr_ae]
  rw [EventuallyEq]
  rwa [ae_restrict_iff' hs]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ι : Type u_4
f : α → ℝ≥0∞
μ : ι → Measure α
⊢ ∫⁻ (a : α), f a ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i

Tactic:
by
  simp_rw [ENNReal.tsum_eq_iSup_sum, ← lintegral_finsetSum_measure,
    lintegral, SimpleFunc.lintegral_sum, ENNReal.tsum_eq_iSup_sum,
    SimpleFunc.lintegral_finsetSum, iSup_comm (ι := Finset ι)]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ∞
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ

Tactic:
hfi,

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ∞
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
hsσ : SigmaFinite (μ.restrict s)
⊢ ν (μ.sigmaFiniteSetWRT' ν) < ν (μ.sigmaFiniteSetWRT' ν ∪ s)

Tactic:
measure_union _ hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
hsσ : SigmaFinite (μ.restrict s)
⊢ ν (μ.sigmaFiniteSetWRT' ν) < ν (μ.sigmaFiniteSetWRT' ν) + ν s

α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
hsσ : SigmaFinite (μ.restrict s)
⊢ Disjoint (μ.sigmaFiniteSetWRT' ν) s
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : AddZeroClass β
inst✝ : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
ind : ∀ (c : β) ⦃s : Set α⦄ (hs : MeasurableSet s), P (s.indicator fun x ↦ c) ⋯
add :
  ∀ ⦃f g : α → β⦄ (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hfg : StronglyMeasurable (f + g)),
    Disjoint (support f) (support g) → P f hf → P g hg → P (f + g) hfg
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun x_1 ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
n : ℕ
⊢ P ⇑(s n) ⋯

Tactic:
induction s n using SimpleFunc.induction with
  | const c hs => exact ind c hs
  | @add f g h_supp hf hg =>
    exact add f.stronglyMeasurable g.stronglyMeasurable (f + g).stronglyMeasurable h_supp hf hg

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pcw
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Nonempty β
inst✝ : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun x ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun x_1 ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f✝ : α → β
hf : StronglyMeasurable f✝
s✝ : ℕ → α →ₛ β := hf.approx
n : ℕ
f g : α →ₛ β
s : Set α
hs : MeasurableSet s
Pf : P ⇑f ⋯
Pg : P ⇑g ⋯
⊢ P ⇑(SimpleFunc.piecewise s hs f g) ⋯

Tactic:
simp_rw [SimpleFunc.coe_piecewise]
    exact pcw f.stronglyMeasurable g.stronglyMeasurable hs Pf Pg

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case h.right.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ (Perfect (closure[inst✝¹] (V ∩ C)) ∧ (closure[inst✝¹] (V ∩ C)).Nonempty) ∧ closure[inst✝¹] (V ∩ C) ⊆ C

pp: case h.right.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ Disjoint (closure[inst✝¹] (U ∩ C)) (closure[inst✝¹] (V ∩ C))

Tactic:
· refine ⟨hC.closure_nhds_inter y yC yV Vop, ?_⟩
    rw [hC.closed.closure_subset_iff]
    exact inter_subset_right

Goal state after:
case h.right.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ Disjoint (closure[inst✝¹] (U ∩ C)) (closure[inst✝¹] (V ∩ C))
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
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun i ↦ ∫⁻ (x : α), f i x ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))

Tactic:
exact hf_tendsto

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
h : 0 < i ∧ ↑j < 1
⊢ j * i < i

Tactic:
← coe_pos

Goal state after:
i j : ↑I
h : 0 < ↑i ∧ ↑j < 1
⊢ j * i < i
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case inl
α : 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 ∂μ ≠ ∞
a : α
h_mono : Antitone fun i ↦ f i a
h : Tendsto (fun i ↦ f i a) atTop atBot
⊢ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)

pp: case inr
α : 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 ∂μ ≠ ∞
a : α
h_mono : Antitone fun i ↦ f i a
h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)

Tactic:
· refine ⟨0, h.mono_right ?_⟩
      rw [OrderBot.atBot_eq]
      exact pure_le_nhds _

Goal state after:
case inr
α : 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 ∂μ ≠ ∞
a : α
h_mono : Antitone fun i ↦ f i a
h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: a b : ℝ
x : ↑(Icc a b)
t : ↑unitInterval
⊢ convexComb x x t = x

Tactic:
simp [convexComb, sub_mul]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
⊢ TopologicalSpace.IsCompletelyMetrizableSpace X

Tactic:
let : MetricSpace X := hf.isEmbedding.comapMetricSpace f

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this✝ : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
this : MetricSpace X := IsEmbedding.comapMetricSpace f ⋯
⊢ TopologicalSpace.IsCompletelyMetrizableSpace X
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ι : Sort u_1
a b : ℝ
h : a ≤ b
c : ι → Set ↑(Icc a b)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
δ : ℝ
δ_pos : δ > 0
ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
n : ℕ
⊢ ∃ i, Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ c i

Tactic:
obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ / 2) n) trivial

Goal state after:
ι : Sort u_1
a b : ℝ
h : a ≤ b
c : ι → Set ↑(Icc a b)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
δ : ℝ
δ_pos : δ > 0
ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
n : ℕ
i : ι
hsub : Metric.ball (addNSMul h (δ / 2) n) δ ⊆ c i
⊢ ∃ i, Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ c i
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: case e'_4
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ ε = ε / 2 * 2

Tactic:
ENNReal.div_mul_cancel

Goal state after:
case e'_4
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ ε = ε

case e'_4.ha₀
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ 2 ≠ 0

case e'_4.ha
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ 2 ≠ ∞
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case a
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε} ≤ ⨅ i, 𝓟 {a | a.1 i = a.2 i}

Tactic:
· simp only [le_iInf_iff, le_principal_iff]
        intro n
        refine mem_iInf_of_mem ((1 / 2) ^ n : ℝ) ?_
        refine mem_iInf_of_mem (by positivity) ?_
        simp only [mem_principal, ofPred_subset_ofPred, Prod.forall]
        intro x y hxy
        exact apply_eq_of_dist_lt hxy le_rfl

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
⊢ μ (s ∆ (f^[n + 1] ⁻¹' s)) ≤ (n + 1) • μ (s ∆ (f ⁻¹' s))

Tactic:
simp only [add_smul, one_smul]

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
⊢ μ (s ∆ (f^[n + 1] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s)) + μ (s ∆ (f ⁻¹' s))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

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

Tactic:
by
  rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs]

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

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

Tactic:
← mem_ae_iff

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
⊢ s ∈ ae (dirac a) ↔ a ∈ s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
⊢ μ = ∑ a ∈ s, μ {a} • dirac a

Tactic:
by
    ext t ht
    rw [← measure_sdiff_null (s := t) hμ]
    dsimp
    rw [Set.sdiff_compl, ← (s : Set α).biUnion_of_singleton]
    simp_rw [Finset.mem_coe, Set.inter_iUnion]
    rw [measure_biUnion_finset (fun i hi j hj hij ↦ .inter_left' _ <| .inter_right' _ ?_)
      (by measurability)]
    · simp only [coe_finsetSum, Finset.sum_apply, smul_apply]
      congr with a
      by_cases ha : a ∈ t <;> simp [*]
    simpa

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

Goal state before:

Tactic:
edist x y = ∑' i : ι, min (2⁻¹ ^ encode i) (edist (x i) (y i)) := rfl
          _ = ∑ i ∈ K, min (2⁻¹ ^ encode i) (edist (x i) (y i)) +
                ∑' i : ↑(K : Set ι)ᶜ, min (2⁻¹ ^ encode (i : ι)) (edist (x i) (y i)) :=
            (ENNReal.sum_add_tsum_compl ..).symm
          _ ≤ ∑ i ∈ K, edist (x i) (y i) + ∑' i : ↑(K : Set ι)ᶜ, 2⁻¹ ^ encode (i : ι) := by
            gcongr
            · apply min_le_right
            · apply min_le_left
          _ < ∑ _i ∈ K, δ + ε / 2 := by
            refine ENNReal.add_lt_add_of_le_of_lt (by simpa using fun i hi ↦ (hxy i hi).ne_top) ?_
              hK
            gcongr with i hi
            exact (hxy i hi).le
          _ ≤ ε / 2 + ε / 2 := by gcongr; simpa [mul_comm] using hδ.le
          _ = ε := ENNReal.add_halves _

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure α
⊢ m.bind dirac = m

Tactic:
by
  ext1 s hs
  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.Topology.MetricSpace.PiNat

Goal state before:
pp: X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
⊢ ∃ n, C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))

Tactic:
obtain hC | hC := (closure Cᶜ).eq_empty_or_nonempty

Goal state after:
case inl
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ = ∅
⊢ ∃ n, C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))

case inr
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
⊢ ∃ n, C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.bind fun x ↦ map (Prod.mk x) ν) s ≤ ∫⁻ (x : α), (map (Prod.mk x) ν) s ∂μ

Tactic:
exact bind_apply_le _ hs

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
h : IsComplement S T
x : G
⊢ x ∈ S * T

Tactic:
simpa [mem_mul] using (h.existsUnique x).exists

Goal state after:
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
⊢ (hHT.equiv g₁).2 = (hHT.equiv g₂).2 → g₂ * g₁⁻¹ ∈ H

pp: case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
⊢ g₂ * g₁⁻¹ ∈ H → (hHT.equiv g₁).2 = (hHT.equiv g₂).2

Tactic:
· 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 _

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
⊢ g₂ * g₁⁻¹ ∈ H → (hHT.equiv g₁).2 = (hHT.equiv g₂).2
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 t : Set α
⊢ μ (c⁻¹ • s ∪ t) = μ (s ∪ c • t)

Tactic:
simpa [inv_inv] using (measure_union_inv_smul _ c⁻¹ _ _).symm

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 γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ ∑' (i : ℕ × ℕ × ℕ), ((sfiniteSeq μ i.1).prod ((sfiniteSeq ν i.2.1).prod (sfiniteSeq τ i.2.2))) s =
    ∑' (i : (ℕ × ℕ) × ℕ), ((sfiniteSeq μ i.1.1).prod ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2))) s

Tactic:
← (Equiv.prodAssoc _ _ _).tsum_eq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ ∑' (c : (ℕ × ℕ) × ℕ),
      ((sfiniteSeq μ ((Equiv.prodAssoc ℕ ℕ ℕ) c).1).prod
          ((sfiniteSeq ν ((Equiv.prodAssoc ℕ ℕ ℕ) c).2.1).prod (sfiniteSeq τ ((Equiv.prodAssoc ℕ ℕ ℕ) c).2.2)))
        s =
    ∑' (i : (ℕ × ℕ) × ℕ), ((sfiniteSeq μ i.1.1).prod ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2))) s