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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
⊢ ↑K * edist (f x) (f y) ≤ ↑K * ediam s

Tactic:
edist_le_ediam_of_mem (mem_preimage.1 hx) hy

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
⊢ ↑K * ediam s ≤ ↑K * ediam s
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ (x :: lxy).length = (lxy ++ [y]).length

Tactic:
rw [length_cons, length_append, length_singleton]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
j a c : ℕ
hc : ∀ (b : ℕ), c ≤ b → ∀ i ≤ a, y b ∉ closure[inst✝¹] {x i}
b : ℕ
hb : y (c + j) ∈ closure[inst✝¹] {x b}
hab : b < a
⊢ False

Tactic:
simp_all [hc (c + j) (c.le_add_right j) b hab.le]

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

Goal state before:
pp: case refine_1.succ
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M < l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
⊢ d x (x :: l)[M + 1] ≤ L.sum

Tactic:
have hMl' : length (take M l) = M := length_take.trans (min_eq_left hMl.le)

Goal state after:
case refine_1.succ
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M < l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
hMl' : (take M l).length = M
⊢ d x (x :: l)[M + 1] ≤ L.sum
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: n : ℕ
⊢ Continuous fun a ↦ a ^ n

Tactic:
by
  induction n with
  | zero => simp [continuous_const]
  | succ n IH =>
    simp_rw [pow_add, pow_one, continuous_iff_continuousAt]
    intro x
    refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_ <;> by_cases H : x = 0
    · simp only [H, zero_ne_top, Ne, or_true, not_false_iff]
    · exact Or.inl fun h => H (eq_zero_of_pow_eq_zero h)
    · simp only [H, pow_eq_top_iff, zero_ne_top, false_or, not_true, Ne,
        not_false_iff, false_and]
    · simp only [H, true_or, Ne, not_false_iff]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case refine_1
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝ : Completion (SeparationQuotient α)
a : α
⊢ Completion.map SeparationQuotient.mk ↑a = ↑(SeparationQuotient.mk a)

Tactic:
map_coe uniformContinuous_mk

Goal state after:
case refine_1
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝ : Completion (SeparationQuotient α)
a : α
⊢ ↑(SeparationQuotient.mk a) = ↑(SeparationQuotient.mk a)
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a x : α
⊢ projIci a x = ⟨a, ⋯⟩ ↔ x ≤ a

Tactic:
simp [projIci, Subtype.ext_iff]

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

Goal state before:
pp: case e'_4
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs'✝ : (drop (M + 1) L).sum ≤ (take (M + 1) L).sum
hMs' : 2 * (drop (M + 1) L).sum ≤ L.sum
⊢ zipWith d (drop M l) (drop (M + 1) l ++ [y]) = drop (M + 1) L

Tactic:
rwa [drop_zipWith, drop, drop_append_of_le_length]

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

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∈ {p | dist p.1 p.2 < ↑(1 / 2) ^ (n + 1)}
⊢ x ∈ U n

Tactic:
rw [mem_ofPred_eq] at hx

Goal state after:
case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : dist x.1 x.2 < ↑(1 / 2) ^ (n + 1)
⊢ x ∈ U n
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x✝¹ x✝ : α × β
a : α
b : β
hab : dist a 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
⊢ C * (ε / (2 * C)) + ε / (2 * C) * C ≤ ε

Tactic:
field_simp

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x✝¹ x✝ : α × β
a : α
b : β
hab : dist a 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
⊢ 1 + 1 ≤ 2
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ y.toNNReal * ‖x‖₊ = ‖y * x‖₊

Tactic:
toNNReal_mul_nnnorm x hy

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ ‖y * x‖₊ = ‖y * x‖₊
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
h✝ : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ 1 ≠ 0

pp: case neg
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
h✝ : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ ⋯.choose ≠ 0

Tactic:
· exact one_ne_zero

Goal state after:
case neg
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
h✝ : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ ⋯.choose ≠ 0
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNormedRing α
inst✝ : NormMulClass α
a : α
ha : a ≠ 0
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ ≤ ↑‖a‖₊⁻¹ * dist (x✝¹ * a) (x✝ * a)

Tactic:
simp [dist_eq_norm, ← sub_mul, mul_comm, ha]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ r⁻¹ * (ε * r ^ 2) * r⁻¹ = ε

Tactic:
field_simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
this : IsAddTorsionFree E
⊢ DiscreteTopology ↥⊥

Tactic:
exact Subsingleton.discreteTopology (α := ↑(⊥ : Subspace ℚ E))

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ diam (ball x r) = 2 * r

Tactic:
refine le_antisymm (diam_ball hr) <|
    mul_le_of_forall_lt_of_nonneg (by positivity) diam_nonneg fun a ha ha' r' hr' hr'' ↦ ?_

Goal state after:
E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
⊢ a * r' ≤ diam (ball x r)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
have f_ne_top : ∀ n, f n ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top hf
  have h_f_coe : f = fun n => ((f n).toNNReal : ENNReal) :=
    funext fun n => (coe_toNNReal (f_ne_top n)).symm
  rw [h_f_coe, ← @coe_zero, tendsto_coe]
  exact NNReal.tendsto_cofinite_zero_of_summable (summable_toNNReal_of_tsum_ne_top hf)

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

Goal state before:
pp: a : EReal
h : 0 ≤ a
⊢ 0 ≤ a⁻¹

Tactic:
cases a with

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

Goal state before:
pp: a : EReal
h : a ≤ 0
⊢ a⁻¹ ≤ 0

Tactic:
cases a with

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

Goal state before:
pp: case inl
a c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤

Tactic:
rcases eq_or_lt_of_le ha with rfl | ha
    · rw [zero_mul] at h
      exact (not_le_of_gt h hc).rec
    · obtain ⟨a', a0', aa'⟩ := exists_between ha
      use a', mem_Ioo.2 ⟨a0', aa'⟩
      rw [mul_top_of_pos ha] at h
      rwa [mul_top_of_pos a0']

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

Goal state before:
pp: case inr.inr.inr
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
b_top : b < ⊤
a' : EReal
aa' : a < a'
hc' : a' < c / b
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
exact ⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt hc'⟩, (lt_div_iff b0 b_top.ne).1 hc'⟩

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
⊢ liminf u f * liminf v f ≤ liminf (u * v) f

Tactic:
apply mul_le_of_forall_lt_of_nonneg ((le_liminf_of_le) hu)
    <| (le_liminf_of_le) ((hu.and hv).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0)
  refine fun a ha b hb ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_lt_liminf (mem_Ioo.1 ha).2,
    eventually_lt_of_lt_liminf (mem_Ioo.1 hb).2] with x xa xb
  exact c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ioo.1 hb).1.le ((mem_Ioo.1 ha).1.le.trans xa.le))

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ c ^ n * u 0 < u n

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_le_of_lt hn _ _ h

Goal state after:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ c ^ 0 * u 0 ≤ u 0

u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
h : ∀ i ∈ t, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ t, s i)

Tactic:
by
  classical
  lift t to Finset ι using ht
  induction t using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢
    exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ m (⋃ b, f b) ⋯ = ∑' (i : ℕ), (inducedOuterMeasure m ⋯ m0) (f i)

Tactic:
mU hf hd

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ ∑' (i : ℕ), m (f i) ⋯ = ∑' (i : ℕ), (inducedOuterMeasure m ⋯ m0) (f i)
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : SupSet β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
⊢ ⨆ n, aeSeq hf p n =ᵐ[μ] ⨆ n, f n

Tactic:
filter_upwards [aeSeq_eq_fun_ae hf hp] with x hx

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : SupSet β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
x : α
hx : ∀ (i : ι), aeSeq hf p i x = f i x
⊢ (⨆ n, aeSeq hf p n) x = (⨆ n, f n) x
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ : OuterMeasure α
s : Set α
hs : MeasurableSet s
⊢ m₁.trim s ≤ m₂ s ↔ m₁ s ≤ m₂ s

Tactic:
trim_eq _ hs

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ : OuterMeasure α
s : Set α
hs : MeasurableSet s
⊢ m₁ s ≤ m₂ s ↔ m₁ s ≤ m₂ s
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

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

Tactic:
exact ⟨t, hst, ht, h ▸ hm⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ((restrict s) μ).trim t ≤ μ.trim (t ∩ s)

Tactic:
rcases μ.exists_measurable_superset_eq_trim (t ∩ s) with ⟨t', htt', ht', hμt'⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ ((restrict s) μ).trim t ≤ μ.trim (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ Exists.choose ?hc =ᵐ[μ] s

pp: case hc
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s

Tactic:
exact (exists_measurable_superset_ae_eq h).choose_spec.2.2

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ μ (s ∪ t) = μ (s ∪ t) + μ (s ∩ t)

Tactic:
hd,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ μ (s ∪ t) = μ (s ∪ t) + 0
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
⊢ s ⊆ t

Tactic:
rw [subset_union_compl_iff_inter_subset, ← image_preimage_eq_inter_range]

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
⊢ f '' f ⁻¹' s ⊆ f '' toMeasurable μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ((OuterMeasure.comap f) μ.toOuterMeasure) t =
    ((OuterMeasure.comap f) μ.toOuterMeasure) (t ∩ s) + ((OuterMeasure.comap f) μ.toOuterMeasure) (t \ s)

Tactic:
by
      simp only [OuterMeasure.comap_apply, image_inter hf.1, image_sdiff hf.1]
      apply le_toOuterMeasure_caratheodory
      exact hf.2 s hs

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
⊢ comap Subtype.val (𝓝[>] b) = atBot ↔ s ⊆ Ioi b ∧ (s.Nonempty → ∀ a > b, (s ∩ Ioo b a).Nonempty)

Tactic:
refine comap_coe_nhdsLT_eq_atTop_iff (s := OrderDual.ofDual ⁻¹' s) (b := OrderDual.toDual b)
    |>.trans ?_
  simp [← preimage_inter, ofDual.surjective]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
⊢ ((restrictₗ s) μ).toOuterMeasure = (OuterMeasure.restrict s) μ.toOuterMeasure

Tactic:
restrictₗ,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
⊢ ((liftLinear (OuterMeasure.restrict s) ⋯) μ).toOuterMeasure = (OuterMeasure.restrict s) μ.toOuterMeasure
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯) μ)
⊢ ((restrictₗ s) μ) t = μ (t ∩ s)

Tactic:
restrictₗ,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯) μ)
⊢ ((liftLinear (OuterMeasure.restrict s) ⋯) μ) t = μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ μ univ < ∞ ∧ ν univ < ∞

Tactic:
exact ⟨measure_lt_top _ _, measure_lt_top _ _⟩

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s

Tactic:
ext1 u hu
  simp only [add_apply, restrict_apply hu, ← inter_assoc, sdiff_eq]
  exact measure_inter_add_sdiff₀ (u ∩ s) ht

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 : α
hx✝ : x ∈ s
U : Set α
hU : μ U < ∞
hx : x ∈ U
hUo : IsOpen[inst✝¹] U
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
exact ⟨U, nhdsWithin_le_nhds (hUo.mem_nhds hx), U, Subset.rfl, hUo, hU⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
x : α
hx : x ∈ t
⊢ s x ≤ (t ∩ s) x

Tactic:
h'x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
x : α
hx : x ∈ t
h'x : s x
⊢ (t ∩ s) x
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
hμ : μ.toMeasure h = 0
s : Set α
⊢ μ s = 0 s

Tactic:
exact le_bot_iff.1 <| (le_toMeasure_apply _ _ _).trans_eq congr($hμ s)

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

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ CountablyGenerated α

Tactic:
use b

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

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
⊢ MeasurableSet s ↔ ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨S, hS_subset, hS_eq⟩ ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
h : MeasurableSet s
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S

case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ AEMeasurable (s.indicator fun x ↦ b) μ ↔ NullMeasurableSet s μ

Tactic:
classical
  constructor <;> intro h
  · convert! h.nullMeasurable (MeasurableSet.singleton (0 : β)).compl
    rw [indicator_const_preimage_eq_union s {0}ᶜ b]
    simp [NeZero.ne b]
  · exact (aemeasurable_indicator_iff₀ h).mpr aemeasurable_const

Goal state after: