mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
x y : α
h : y = x
⊢ x = y

Tactic:
exact h.symm

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
⊢ AEMeasurable (g ∘ f) μ ↔ AEMeasurable f μ

Tactic:
refine ⟨fun H => ?_, hg.measurable.comp_aemeasurable⟩
  suffices AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ by
    rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
  exact hg.measurable_rangeSplitting.comp_aemeasurable H.subtype_mk

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NeZero μ
h : IsEmpty α
⊢ False

Tactic:
simpa [eq_empty_of_isEmpty] using NeZero.ne (μ univ)

Goal state after:
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₂
⊢ M • (μ.restrict (⋃ C ∈ Cs, P C)) t ≤ M • (μ.restrict (⋃ i, s i)) t

Tactic:
exact nsmul_le_nsmul_right (μ.restrict_mono_set iUnion_P t) M

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

Goal state before:
pp: α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁴ : MeasurableSpace M✝
inst✝³ : MeasurableSMul M✝ X
M : Type u_6
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
⊢ Measurable (Function.uncurry fun x1 x2 ↦ x1 • x2)

Tactic:
by
    suffices Measurable fun p : M × ℕ => p.2 • p.1 by apply this.comp measurable_swap
    refine measurable_from_prod_countable_left fun n => ?_
    induction n with
    | zero => simp only [zero_smul, ← Pi.zero_def, measurable_zero]
    | succ n ih =>
      simp only [succ_nsmul]
      exact ih.add measurable_id

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

Goal state before:
pp: α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁵ : MeasurableSpace M✝
inst✝⁴ : MeasurableSMul M✝ X
M : Type u_6
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
⊢ Measurable (Function.uncurry fun x1 x2 ↦ x1 • x2)

Tactic:
suffices Measurable fun p : M × ℤ => p.2 • p.1 by apply this.comp measurable_swap
    refine measurable_from_prod_countable_left fun n => ?_
    cases n with
    | ofNat n =>
      simp only [Int.ofNat_eq_natCast, natCast_zsmul]
      exact measurable_const_smul _
    | negSucc n =>
      simp only [negSucc_zsmul]
      exact (measurable_const_smul _).neg

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace β
inst✝ : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
this : MeasurableSpace.comap e (borel β) = inst✝³
⊢ inst✝³ = borel α

Tactic:
← this,

Goal state after:
α : Type u_6
β : Type u_7
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace β
inst✝ : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
this : MeasurableSpace.comap e (borel β) = inst✝³
⊢ MeasurableSpace.comap e (borel β) = borel α
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
x : α
xu : x ∈ u
⊢ hausdorffEDist u t + hausdorffEDist t s = hausdorffEDist s t + hausdorffEDist t u

Tactic:
by simp [hausdorffEDist_comm, add_comm]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickening δ (thickening δ E)ᶜ ⊆ Eᶜ

Tactic:
apply compl_subset_compl.mp

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ Eᶜᶜ ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : SecondCountableTopology α
inst✝ : OrderClosedTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ Measurable fun a ↦ Max.max (f a) (g a)

Tactic:
by
  simpa only [max_def'] using! hf.piecewise (measurableSet_le hg hf) hg

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, μ (thickening R s) ≠ ∞
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun r ↦ μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ s))

Tactic:
by
  convert! tendsto_measure_thickening 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
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : SemilatticeSup β
inst✝⁶ : OrderBot β
inst✝⁵ : Zero β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderClosedTopology β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
inst✝ : MeasurableSpace γ
i : ℕ → β
f : γ → β
g : α → γ
n : ℕ
a : α
hf : Measurable f
hg : Measurable g
⊢ (approx i (f ∘ g) n) a = (Finset.range n).sup fun k ↦ if i k ≤ f (g a) then i k else 0

Tactic:
approx_apply _ (hf.comp hg),

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : SemilatticeSup β
inst✝⁶ : OrderBot β
inst✝⁵ : Zero β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderClosedTopology β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
inst✝ : MeasurableSpace γ
i : ℕ → β
f : γ → β
g : α → γ
n : ℕ
a : α
hf : Measurable f
hg : Measurable g
⊢ ((Finset.range n).sup fun k ↦ if i k ≤ (f ∘ g) a then i k else 0) =
    (Finset.range n).sup fun k ↦ if i k ≤ f (g a) then i k else 0
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f n) a + ↑((eapprox f (n + 1) - eapprox f n) a).toNNReal = (eapprox f (n + 1)) a

Tactic:
coe_sub,

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f n) a + ↑((⇑(eapprox f (n + 1)) - ⇑(eapprox f n)) a).toNNReal = (eapprox f (n + 1)) a
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ IsLUB (f '' Ici k) x

Tactic:
by
  rw [tendsto_nhds_unique h_tto
    (Real.tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici h_mon h_bdd)]
  exact isLUB_csSup (image_nonempty.mpr nonempty_Ici) h_bdd

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

Tactic:
by
  refine ⟨range (hf.mk f), hf.stronglyMeasurable_mk.isSeparable_range, ?_⟩
  filter_upwards [hf.ae_eq_mk] with x hx
  simp [hx]

Goal state after:
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
⊢ ∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
set F := fun a : α => ⨆ n, f n a

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
⊢ lintegral μ F = ⨆ n, ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun n ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
have : Monotone fun n => ∫⁻ x, f n x ∂μ := fun i j hij =>
    lintegral_mono_ae (h_mono.mono fun x hx => hx hij)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Monotone fun n ↦ ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun n ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hμf : μ {x | f x = ∞} ≠ 0
⊢ ∞ = ∞ * μ {x | ∞ ≤ f x}

Tactic:
simp [hμf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable f⁻¹

Tactic:
refine ⟨fun n => ((hf.approx n).restrict {x | f x ≠ 0})⁻¹, fun x => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ ((hf.approx n).restrict {x | f x ≠ 0})⁻¹) n) x) atTop (𝓝 (f⁻¹ x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∫⁻ (x : α) in {x | f x ≤ g x}, max (f x) (g x) ∂μ + ∫⁻ (x : α) in {x | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ =
    ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {a | f a ≤ g a}ᶜ, f x ∂μ

Tactic:
refine congr_arg₂ (· + ·) (setLIntegral_congr_fun hm ?_) (setLIntegral_congr_fun hm.compl ?_)

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ EqOn (fun x ↦ max (f x) (g x)) g {x | f x ≤ g x}

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ EqOn (fun x ↦ max (f x) (g x)) f {x | f x ≤ g x}ᶜ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : StronglyMeasurable fun x ↦ g (f x)
G : β → ↑(range g) := rangeFactorization g
⊢ Measurable f

Tactic:
have hG : IsClosedEmbedding G :=
      { hg.codRestrict _ _ with
        isClosed_range := by
          rw [rangeFactorization_surjective.range_eq]
          exact isClosed_univ }

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : StronglyMeasurable fun x ↦ g (f x)
G : β → ↑(range g) := rangeFactorization g
hG : IsClosedEmbedding G
⊢ Measurable f
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ Measurable g

pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (range g)

Tactic:
· exact measurable_of_tendsto_metrizable' u (fun i => (hf i).measurable) lim

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (range g)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ • (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) s

Tactic:
smul_eq_mul,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ * (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) s
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
⊢ ∃ D, Perfect D ∧ D.Nonempty ∧ D ⊆ C

Tactic:
by
  rcases exists_countable_union_perfect_of_isClosed hclosed with ⟨V, D, Vct, Dperf, VD⟩
  refine ⟨D, ⟨Dperf, ?_⟩⟩
  constructor
  · rw [nonempty_iff_ne_empty]
    by_contra h
    rw [h, union_empty] at VD
    rw [VD] at hunc
    contradiction
  rw [VD]
  exact subset_union_right

Goal state after:
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
this : ∃ a, ∀ (b : Finset ι), a ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Tactic:
obtain ⟨t, ht⟩ := this

Goal state after:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
⊢ Summable fun n ↦ ‖f n x‖

Tactic:
apply Summable.add_compl (s := hN.toFinset) Summable.of_finite

Goal state after:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
⊢ Summable ((fun n ↦ ‖f n x‖) ∘ Subtype.val)
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ∀ (i : { x // x ∉ n }), ((fun n ↦ ‖f n x‖) ∘ Subtype.val) i ≤ (u ∘ Subtype.val) i

Tactic:
simp only [comp_apply, Subtype.forall]

Goal state after:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ∀ a ∉ n, ‖f a x‖ ≤ u a
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → x ∈ s → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑(K' x hx) * edist x y
t : Finset ↑s
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x) (ε ↑x ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : ↑s
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z) (ε ↑z ⋯ / 2)
⊢ edist (f x) (f y) ≤ ↑(t.sup fun i ↦ K ↑i ⋯ + 2 * K' ↑i ⋯) * edist x y

Tactic:
by_cases hy' : y ∈ ball z.1 (ε _ z.2)

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → x ∈ s → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑(K' x hx) * edist x y
t : Finset ↑s
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x) (ε ↑x ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : ↑s
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z) (ε ↑z ⋯ / 2)
hy' : y ∈ ball (↑z) (ε ↑z ⋯)
⊢ edist (f x) (f y) ≤ ↑(t.sup fun i ↦ K ↑i ⋯ + 2 * K' ↑i ⋯) * edist x y

case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → x ∈ s → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑(K' x hx) * edist x y
t : Finset ↑s
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x) (ε ↑x ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : ↑s
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z) (ε ↑z ⋯ / 2)
hy' : y ∉ ball (↑z) (ε ↑z ⋯)
⊢ edist (f x) (f y) ≤ ↑(t.sup fun i ↦ K ↑i ⋯ + 2 * K' ↑i ⋯) * edist x y
Module: Mathlib.Topology.UnitInterval

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

Tactic:
by
  rw [← symm_le_symm, symm_symm]

Goal state after:
Module: Mathlib.Topology.UnitInterval

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

Tactic:
by
  rw [← symm_le_symm, symm_symm]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case inr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
this : ∀ {c d : α}, d ≤ c → |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|
hdc : ¬d ≤ c
⊢ |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|

Tactic:
rw [abs_sub_comm, abs_sub_comm c]

Goal state after:
case inr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
this : ∀ {c d : α}, d ≤ c → |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|
hdc : ¬d ≤ c
⊢ |↑(projIcc a b h d) - ↑(projIcc a b h c)| ≤ |d - c|
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
⊢ min (firstDiff x y) (firstDiff y z) ≤ firstDiff x z

Tactic:
by_contra! H

Goal state after:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < min (firstDiff x y) (firstDiff y z)
⊢ False
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ¬↑z - ↑x = 0
⊢ 0 ≤ (↑y - ↑x) / (↑z - ↑x)

Tactic:
replace hxy : (x : ℝ) ≤ (y : ℝ) := hxy
    replace hyz : (y : ℝ) ≤ (z : ℝ) := hyz
    apply div_nonneg <;> grind

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

Goal state before:
pp: case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ i < n, y i = x i
⊢ n ≤ firstDiff y x

Tactic:
by_contra! H

Goal state after:
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ i < n, y i = x i
H : firstDiff y x < n
⊢ False
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x y + dist y ⋯.some + 1 + dist ⋯.some z

Tactic:
by
          apply_rules [add_le_add, le_rfl, dist_triangle]

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
⊢ res (↑x) (n + 1) = res (↑y) (n + 1)

Tactic:
simp only [res_succ, cons.injEq]
    refine ⟨?_, ih⟩
    contrapose hA
    simp only [CantorScheme.Disjoint, _root_.Pairwise, Ne, not_forall, exists_prop]
    refine ⟨res x n, _, _, hA, ?_⟩
    rw [not_disjoint_iff]
    refine ⟨(inducedMap A).2 x, ?_, ?_⟩
    · rw [← res_succ]
      apply map_mem
    rw [hxy, ih, ← res_succ]
    apply map_mem

Goal state after: