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

Goal state before:
pp: case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
this : dist x ct ≤ max rs rt
⊢ ENNReal.ofReal (dist x ct) ≤ ENNReal.ofReal (max rs rt)

Tactic:
ENNReal.ofReal_le_ofReal_iff

Goal state after:
case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
this : dist x ct ≤ max rs rt
⊢ dist x ct ≤ max rs rt

case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
this : dist x ct ≤ max rs rt
⊢ 0 ≤ max rs rt
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
this : dist x cs ≤ max rs rt
⊢ ENNReal.ofReal (dist x cs) ≤ ENNReal.ofReal (max rs rt)

Tactic:
ENNReal.ofReal_le_ofReal_iff

Goal state after:
case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
this : dist x cs ≤ max rs rt
⊢ dist x cs ≤ max rs rt

case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
this : dist x cs ≤ max rs rt
⊢ 0 ≤ max rs rt
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ diam (s ∪ t)

Tactic:
· exact fun z hz => ⟨x, xs, dist_le_diam_of_mem (bs.union bt) (subset_union_right hz)
      (subset_union_left xs)⟩

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

Goal state before:
pp: case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ x ∈ thickening ε (thickening δ s) → x ∈ thickening (ε + δ) s

Tactic:
mem_thickening_iff_exists_edist_lt,

Goal state after:
case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ (∃ z, (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) →
    ∃ z ∈ s, edist x z < ENNReal.ofReal (ε + δ)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ x ∈ thickening ε (cthickening δ s) → x ∈ thickening (ε + δ) s

Tactic:
mem_thickening_iff_exists_edist_lt,

Goal state after:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ (∃ z ∈ cthickening δ s, edist x z < ENNReal.ofReal ε) → ∃ z ∈ s, edist x z < ENNReal.ofReal (ε + δ)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: β : Type u_2
δ : Type u_4
inst✝⁶ : TopologicalSpace β
mβ : MeasurableSpace β
inst✝⁵ : BorelSpace β
mδ : MeasurableSpace δ
inst✝⁴ : CompleteLinearOrder β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous fun x_1 ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
⊢ MeasurableSet ((⨆ i, f i) ⁻¹' Ioi c)

Tactic:
suffices (⨆ i, f i) ⁻¹' Ioi c = ⋃ j ∈ J, {x | c < f j x} by
    rw [this]
    exact .biUnion cJ fun j _ ↦ by measurability

Goal state after:
β : Type u_2
δ : Type u_4
inst✝⁶ : TopologicalSpace β
mβ : MeasurableSpace β
inst✝⁵ : BorelSpace β
mδ : MeasurableSpace δ
inst✝⁴ : CompleteLinearOrder β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous fun x_1 ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
⊢ (⨆ i, f i) ⁻¹' Ioi c = ⋃ j ∈ J, {x | c < f j x}
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet (s ×ˢ t)

Tactic:
rw [prod_eq]

Goal state after:
case a
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
this : Measurable fun _b ↦ sSup ∅
b : δ
hb : b ∈ {b | BddAbove (range fun i ↦ f i b)}
⊢ IsLUB {a | ∃ i, f i b = a} (⨆ i, f i b)

Tactic:
apply isLUB_ciSup

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
this : Measurable fun _b ↦ sSup ∅
b : δ
hb : b ∈ {b | BddAbove (range fun i ↦ f i b)}
⊢ BddAbove (range fun y ↦ f y b)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_2
q : ℚ
⊢ MeasurableSet (Ici ↑q)

Tactic:
← compl_Iio

Goal state after:
case refine_2
q : ℚ
⊢ MeasurableSet (Iio ↑q)ᶜ
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k N : ℕ
hk : k ≤ N
⊢ edist ((nearestPt e N) x) x ≤ edist (e k) x

Tactic:
by
  induction N generalizing k with
  | zero => simp [nonpos_iff_eq_zero.1 hk]
  | succ N ihN =>
    simp only [nearestPt, nearestPtInd_succ, map_apply]
    split_ifs with h
    · rcases hk.eq_or_lt with (rfl | hk)
      exacts [le_rfl, (h k (Nat.lt_succ_iff.1 hk)).le]
    · push Not at h
      rcases h with ⟨l, hlN, hxl⟩
      rcases hk.eq_or_lt with (rfl | hk)
      exacts [(ihN hlN).trans hxl, ihN (Nat.lt_succ_iff.1 hk)]

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

Goal state before:
pp: α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n ↦ (hf.approxBounded c n) x) atTop (𝓝 (f x))

Tactic:
simp only [StronglyMeasurable.approxBounded, SimpleFunc.coe_map, Function.comp_apply]

Goal state after:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n ↦ min 1 (c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
⊢ ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}

Tactic:
intro p

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
p : ℝ≥0∞
⊢ ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
⊢ ‖(hf.approxBounded c n) x‖ ≤ c

Tactic:
simp only [StronglyMeasurable.approxBounded, SimpleFunc.coe_map, Function.comp_apply]

Goal state after:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
⊢ ‖min 1 (c / ‖(hf.approx n) x‖) • (hf.approx n) x‖ ≤ c
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n ↦ (f_approx n) x) atTop (𝓝 (f x))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t

Tactic:
by
        rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
        · exact ⟨n, fun m hnm => Set.mem_inter (hn m hnm) hxt⟩
        rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S n
        · exact ⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩
        rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict t)]
        trivial

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
⊢ aeSeq hf p b₁ ≤ aeSeq hf p z

Tactic:
intro x
        by_cases hx : x ∈ aeSeqSet hf p
        · repeat rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
          apply_rules [hz₁, hz₂]
        · simp only [aeSeq, hx, if_false]
          exact le_rfl

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
⊢ aeSeq hf p b₂ ≤ aeSeq hf p z

Tactic:
intro x
        by_cases hx : x ∈ aeSeqSet hf p
        · repeat rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
          apply_rules [hz₁, hz₂]
        · simp only [aeSeq, hx, if_false]
          exact le_rfl

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f : β → α → ℝ≥0∞
a : β
s : Finset β
has : a ∉ s
ih : (∀ b ∈ s, AEMeasurable (f b) μ) → ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
hf : ∀ b ∈ insert a s, AEMeasurable (f b) μ
⊢ ∫⁻ (a_1 : α), f a a_1 + ∑ b ∈ s, f b a_1 ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

Tactic:
Finset.forall_mem_insert

Goal state after:
case insert
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f : β → α → ℝ≥0∞
a : β
s : Finset β
has : a ∉ s
ih : (∀ b ∈ s, AEMeasurable (f b) μ) → ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
hf : AEMeasurable (f a) μ ∧ ∀ x ∈ s, AEMeasurable (f x) μ
⊢ ∫⁻ (a_1 : α), f a a_1 + ∑ b ∈ s, f b a_1 ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f : β → α → ℝ≥0∞
a : β
s : Finset β
has : a ∉ s
ih : (∀ b ∈ s, AEMeasurable (f b) μ) → ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
hf : AEMeasurable (f a) μ ∧ ∀ x ∈ s, AEMeasurable (f x) μ
⊢ ∫⁻ (a_1 : α), f a a_1 + ∑ b ∈ s, f b a_1 ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

Tactic:
lintegral_add_left' hf.1,

Goal state after:
case insert
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f : β → α → ℝ≥0∞
a : β
s : Finset β
has : a ∉ s
ih : (∀ b ∈ s, AEMeasurable (f b) μ) → ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
hf : AEMeasurable (f a) μ ∧ ∀ x ∈ s, AEMeasurable (f x) μ
⊢ ∫⁻ (a_1 : α), f a a_1 ∂μ + ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
⊢ Tendsto (fun n ↦ ∫⁻ (a : α), F n a ∂μ) l (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
rw [tendsto_iff_seq_tendsto]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
⊢ ∀ (x : ℕ → ι), Tendsto x atTop l → Tendsto ((fun n ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
⊢ StronglyMeasurable f

Tactic:
have h's : MeasurableSet s := by simpa using hs.measurableSet.compl

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
h's : MeasurableSet s
⊢ StronglyMeasurable f
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ (b : ℕ), a ≤ b → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), k ≤ b → x b ∈ {x | (fun n ↦ AEMeasurable (F n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto ((fun n ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
← tendsto_add_atTop_iff_nat k

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ (b : ℕ), a ≤ b → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), k ≤ b → x b ∈ {x | (fun n ↦ AEMeasurable (F n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto (fun n ↦ ((fun n ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
⊢ σ i ≤ σ j ↔ j ≤ i

Tactic:
simp only [symm, Subtype.mk_le_mk, sub_le_sub_iff, add_le_add_iff_left, Subtype.coe_le_coe]

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
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
⊢ dist x z ≤ dist z (Φ q) + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))

Tactic:
dist_comm z

Goal state after:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
⊢ dist x z ≤ dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

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

Tactic:
by_cases y = z

Goal state after:
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : x = y
h✝¹ : x = z
h✝ : y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : x = y
h✝¹ : x = z
h✝ : ¬y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝¹ : x = y
h✝ : ¬x = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
by_cases y = z

Goal state after:
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : x = y
h✝¹ : ¬x = z
h✝ : y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : x = y
h✝¹ : ¬x = z
h✝ : ¬y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝¹ : ¬x = y
h✝ : x = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
by_cases y = z

Goal state after:
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : ¬x = y
h✝¹ : x = z
h✝ : y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : ¬x = y
h✝¹ : x = z
h✝ : ¬y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝¹ : ¬x = y
h✝ : ¬x = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
by_cases y = z

Goal state after:
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : ¬x = y
h✝¹ : ¬x = z
h✝ : y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : ¬x = y
h✝¹ : ¬x = z
h✝ : ¬y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
non1 : D₁.Nonempty
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ ediam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ ediam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Tactic:
obtain ⟨x₁, hx₁⟩ := non1

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ ediam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ ediam C₁ ≤ ε) ∧ Disjoint C₀ C₁
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)
x y : (n : ℕ) × X n
⊢ inductiveLimitDist f x y = inductiveLimitDist f y x

Tactic:
let m := max x.1 y.1

Goal state after:
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 : ℕ := max x.fst y.fst
⊢ inductiveLimitDist f x y = inductiveLimitDist f y x
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff x y ≤ shortestPrefixDiff x s - 1

Tactic:
le_tsub_iff_right

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff x y + 1 ≤ shortestPrefixDiff x s

E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff x s