mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case refine_2
α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∀ a ∈ s,
    (∑ b ∈ univ.sigma fun a ↦ range (f ↑a).natAbs,
        if (fun a ↦ ↑a.fst) b = a then ↑((fun a ↦ sign (f ↑a.fst)) b) else 0) =
      f a

Tactic:
· intro x hx
    simp [sum_sigma, hx, ← Int.sign_eq_sign, Int.sign_mul_abs, mul_comm |f _|,
      sum_attach (s := s) (f := fun y => if y = x then f y else 0)]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (x : ↑(⋃ i ∈ univ, t i)), f ↑x

Tactic:
Set.biUnion_univ

Goal state after:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (x : ↑(⋃ x, t x)), f ↑x
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.zero
x y : EReal
h : ↑(sign y) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = zero
⊢ sign y = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨ sign y = zero ∧ zero = zero ∨ sign y = pos ∧ zero = pos ∧ x.abs ≤ y.abs

Tactic:
hy

Goal state after:
case mp.zero
x y : EReal
h : ↑zero * ↑x.abs ≤ ↑zero * ↑y.abs
hs : sign x = sign y
hy : sign y = zero
⊢ zero = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨ zero = zero ∧ zero = zero ∨ zero = pos ∧ zero = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.neg
x y : EReal
h : ↑(sign y) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ sign y = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ sign y = zero ∧ neg = zero ∨ sign y = pos ∧ neg = pos ∧ x.abs ≤ y.abs

Tactic:
hy

Goal state after:
case mp.neg
x y : EReal
h : ↑neg * ↑x.abs ≤ ↑neg * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ neg = zero ∧ neg = zero ∨ neg = pos ∧ neg = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑ i, ∑' (x : ↑(t i)), f ↑x

Tactic:
rw [← tsum_fintype (L := SummationFilter.unconditional _)]
  exact tsum_iUnion_le_tsum f t

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.pos
x y : EReal
h : ↑(sign y) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ sign y = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ sign y = zero ∧ pos = zero ∨ sign y = pos ∧ pos = pos ∧ x.abs ≤ y.abs

Tactic:
hy

Goal state after:
case mp.pos
x y : EReal
h : ↑pos * ↑x.abs ≤ ↑pos * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ pos = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
⊢ b * (a' / b) = a'

Tactic:
@EReal.mul_div_cancel a' b (ne_bot_of_gt h) h' h.ne'

Goal state after:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
⊢ a' = a'
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
⊢ ∃ a ∈ s, IsMinOn f s a

Tactic:
by
  simp only [isMinOn_iff]
  have _ : Nonempty α := Exists.nonempty ne_s
  have _ : Nonempty s := Nonempty.to_subtype ne_s
  let φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
  let ℱ : Filter α := ⨅ a : s, φ (f a)
  have : ℱ.NeBot := by
    apply iInf_neBot_of_directed _ _
    · change Directed GE.ge (fun x ↦ (φ ∘ (fun (a : s) ↦ f ↑a)) x)
      exact Directed.mono_comp GE.ge (fun x y hxy ↦
        principal_mono.mpr (inter_subset_inter_right _ (preimage_mono <| Iic_subset_Iic.mpr hxy)))
        (Std.Total.directed _)
    · intro x
      have : (pure x : Filter α) ≤ φ (f x) := le_principal_iff.mpr ⟨x.2, le_refl (f x)⟩
      exact neBot_of_le this
  have hℱs : ℱ ≤ 𝓟 s :=
    iInf_le_of_le (Classical.choice inferInstance) (principal_mono.mpr <| inter_subset_left)
  have hℱ (x) (hx : x ∈ s) : ∀ᶠ y in ℱ, f y ≤ f x :=
    mem_iInf_of_mem ⟨x, hx⟩ (by apply inter_subset_right)
  obtain ⟨a, ha, h⟩ := hs hℱs
  refine ⟨a, ha, fun x hx ↦ le_of_not_gt fun hxa ↦ ?_⟩
  let _ : (𝓝 a ⊓ ℱ).NeBot := h
  suffices ∀ᶠ _ in 𝓝 a ⊓ ℱ, False by rwa [eventually_const] at this
  filter_upwards [(hf a ha (f x) hxa).filter_mono (inf_le_inf_left _ hℱs),
    (hℱ x hx).filter_mono (inf_le_right : 𝓝 a ⊓ ℱ ≤ ℱ)] using fun y h₁ h₂ ↦ not_le_of_gt h₁ h₂

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
this : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ (fun i ↦ f i ⁻¹' Iic c) i)
⊢ ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x

Tactic:
simpa [Set.eq_empty_iff_forall_notMem] using
        ks.elim_finite_subfamily_isClosed_subtype _ this H

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: x : EReal
h_top : x = ⊤
n : ℕ
y : EReal
⊢ ↑↑n < y → ↑n < y.toENNReal

Tactic:
hy

Goal state after:
x : EReal
h_top : x = ⊤
n : ℕ
y : EReal
hy : ↑↑n < y
⊢ ↑n < y.toENNReal
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
x : α
a✝ : x ∈ s
y : γ
⊢ y < f x → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x

Tactic:
hy

Goal state after:
case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
x : α
a✝ : x ∈ s
y : γ
hy : y < f x
⊢ ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
⊢ (fun x1 x2 ↦ (g ∘ f) x1 > x2) x y → ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y

Tactic:
hy

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
⊢ (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x y → ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
hy

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case coe.bot
a✝ : ℝ
h : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ ⊥
h' : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, ⊥)

pp: case coe.coe
a✝¹ a✝ : ℝ
h : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h' : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝¹, ↑a✝)

pp: case coe.top
a✝ : ℝ
h : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ ⊥
h' : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, ⊤)

pp: case top.bot
h : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ ⊥
h' : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊥)

pp: case top.coe
a✝ : ℝ
h : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ ⊥
h' : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ↑a✝)

pp: case top.top
h : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ ⊥
h' : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)

Tactic:
· exact continuousAt_add_coe_bot _

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
h : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h' : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝¹, ↑a✝)

case coe.top
a✝ : ℝ
h : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ ⊥
h' : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, ⊤)

case top.bot
h : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ ⊥
h' : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊥)

case top.coe
a✝ : ℝ
h : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ ⊥
h' : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ↑a✝)

case top.top
h : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ ⊥
h' : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
⊢ (fun x1 x2 ↦ (fun x' ↦ ⨆ i, f i x') x1 > x2) x y →
    ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun x' ↦ ⨆ i, f i x') x1 > x2) x' y

Tactic:
hy

Goal state after:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : (fun x' ↦ ⨆ i, f i x') x > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun x' ↦ ⨆ i, f i x') x1 > x2) x' y
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y✝ : δ'
hy : (fun x' ↦ ⨆ i, f i x') x > y✝
i : ι
hi : y✝ < f i x
y : α
⊢ f i y > y✝ → BddAbove (range fun i ↦ f i y) → ⨆ i, f i y > y✝

Tactic:
hy

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y✝ : δ'
hy✝ : (fun x' ↦ ⨆ i, f i x') x > y✝
i : ι
hi : y✝ < f i x
y : α
hy : f i y > y✝
⊢ BddAbove (range fun i ↦ f i y) → ⨆ i, f i y > y✝
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h₁ : P s₁
h₂ : P s₂
⊢ extend m (s₁ ∪ s₂) = extend m s₁ + extend m s₂

Tactic:
rw [union_eq_iUnion,
    extend_iUnion P0 m0 PU mU (pairwise_disjoint_on_bool.2 hd) (Bool.forall_bool.2 ⟨h₂, h₁⟩),
    tsum_fintype]
  simp

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
⊢ s ⊆ hs.choose

pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ s ⊆ h's.choose

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ¬∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ s ⊆ ⋯.choose

Tactic:
exacts [hs.choose_spec.1, h's.choose_spec.1, (exists_measurable_superset μ s).choose_spec.1]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] t ↔ s ∩ t =ᵐ[μ] univ ∩ t

Tactic:
univ_inter

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] t ↔ s ∩ t =ᵐ[μ] t
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ ↔ ∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ

Tactic:
constructor
  · exact AEMeasurable.eval
  · intro h
    use fun x a ↦ (h a).mk _ x, measurable_pi_lambda _ fun a ↦ (h a).measurable_mk
    exact (eventually_countable_forall.mpr fun a ↦ (h a).ae_eq_mk).mono fun _ h ↦ funext h

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f).domRestrict (extend f g g'))

Tactic:
rw [domRestrict_extend_range]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable fun x ↦ g (Exists.choose ⋯)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (g' ∘ Subtype.val)

Tactic:
exact hg'.comp measurable_subtype_coe

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = m.trim s

Tactic:
by
  simp only [trim_eq_iInf]; set ms := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), m t
  by_cases hs : ms = ∞
  · simp only [hs]
    simp only [iInf_eq_top, ms] at hs
    exact ⟨univ, subset_univ s, MeasurableSet.univ, hs _ (subset_univ s) MeasurableSet.univ⟩
  · have : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r := by
      intro r hs
      have : ∃ t, MeasurableSet t ∧ s ⊆ t ∧ m t < r := by simpa [ms, iInf_lt_iff] using hs
      rcases this with ⟨t, hmt, hin, hlt⟩
      exists t
    have : ∀ n : ℕ, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < ms + (n : ℝ≥0∞)⁻¹ := by
      intro n
      refine this _ (ENNReal.lt_add_right hs ?_)
      simp
    choose t hsub hm hm' using this
    refine ⟨⋂ n, t n, subset_iInter hsub, MeasurableSet.iInter hm, ?_⟩
    have : Tendsto (fun n : ℕ => ms + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (ms + 0)) :=
      tendsto_const_nhds.add ENNReal.tendsto_inv_nat_nhds_zero
    rw [add_zero] at this
    refine le_antisymm (ge_of_tendsto' this fun n => ?_) ?_
    · exact le_trans (measure_mono <| iInter_subset t n) (hm' n).le
    · refine iInf_le_of_le (⋂ n, t n) ?_
      refine iInf_le_of_le (subset_iInter hsub) ?_
      exact iInf_le _ (MeasurableSet.iInter hm)

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
⊢ comap f (c • μ) = c • comap f μ

Tactic:
have h' : ¬ (Function.Injective f ∧
        ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)) := by
      simpa [nullMeasurableSet_smul_measure_iff hc] using h
    simp [comap_undef, h, h']

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : μ univ < ∑' (i : ι), μ (s i)
⊢ ∃ i j, i ≠ j ∧ (s i ∩ s j).Nonempty

Tactic:
by
  contrapose! H
  apply tsum_measure_le_measure_univ hs
  intro i j hij
  exact (disjoint_iff_inter_eq_empty.mpr (H i j hij)).aedisjoint

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
⊢ 0 < measureUnivNNReal μ

Tactic:
contrapose! hμ
  simpa [measureUnivNNReal_eq_zero, Nat.le_zero] using hμ

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : μ univ = ν univ
⊢ μ = ν

Tactic:
refine le_antisymm hμν (le_intro fun s hs _ ↦ ?_)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : μ univ = ν univ
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
⊢ ν s ≤ μ s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ μ (s k) - (μ (s k) - μ (⋂ i, s i)) = μ (s k) - ⨆ i, μ (s k) - μ (s i)

Tactic:
←
    measure_sdiff (iInter_subset _ k) (.iInter h) (this _ (iInter_subset _ k)),

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ μ (s k) - μ (s k \ ⋂ i, s i) = μ (s k) - ⨆ i, μ (s k) - μ (s i)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
_m0 : MeasurableSpace α
R : Type u_7
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
μ : Measure α
s : Set α
⊢ (c • μ).restrict s = c • μ.restrict s

Tactic:
by
  simpa only [smul_one_smul] using! (restrictₗ s).map_smul (c • 1) μ

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦ s k \ s i

Tactic:
exact hd.mono_comp _ fun _ _ => sdiff_subset_sdiff_right

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
intro x hx
    rcases (hμ x hx).exists_mem_basis (nhds_basis_opens _) with ⟨U, ⟨hx, hUo⟩, hU⟩
    exact ⟨U, nhdsWithin_le_nhds (hUo.mem_nhds hx), U, Subset.rfl, hUo, hU⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
t : Set α
tT : t ∈ range f
xt : x ∈ t
⊢ x ∈ ⋃ i, f i

Tactic:
obtain ⟨n, rfl⟩ : ∃ n : ℕ, f n = t := by simpa only using! tT

Goal state after:
case inr
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
n : ℕ
tT : f n ∈ range f
xt : x ∈ f n
⊢ x ∈ ⋃ i, f i
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
p : Set α → Prop
t : Set α
⊢ HasCountableSeparatingOn (↑t) (fun u ↦ ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ ↔ HasCountableSeparatingOn α p t

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u_1
p : Set α → Prop
t : Set α
h : HasCountableSeparatingOn (↑t) (fun u ↦ ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ
⊢ HasCountableSeparatingOn α p t

case mpr
α : Type u_1
p : Set α → Prop
t : Set α
h : HasCountableSeparatingOn α p t
⊢ HasCountableSeparatingOn (↑t) (fun u ↦ ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
h : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
by
  simp only [ae_iff] at h ⊢
  simpa [ofPred_and, inter_comm] using measure_inter_eq_zero_of_restrict h

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∑' (n : ℕ), (μ.restrict (t ∩ u)) (disjointed w n) = (μ.restrict (t ∩ u)) (⋃ n, disjointed w n)

Tactic:
rw [measure_iUnion]
        · exact disjoint_disjointed _
        · intro i
          refine MeasurableSet.disjointed (fun n => ?_) i
          exact measurableSet_toMeasurable _ _

Goal state after:
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case refine_2
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x : α
hx : x ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
y : α
⊢ y ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ → x = y

Tactic:
hy

Goal state after:
case refine_2
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x : α
hx : x ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
y : α
hy : y ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
⊢ x = y