mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.UniformMulAction

Goal state before:
pp: R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ m • n • x = n • m • x

Tactic:
hmn,

Goal state after:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x = n • m • x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
⊢ ↑r ≤ ↑(limsup u f) ↔ ↑r ≤ limsup (fun i ↦ ↑(u i)) f

Tactic:
rw [coe_le_coe, le_limsup_iff, le_limsup_iff]

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
⊢ (∀ y < r, ∃ᶠ (a : ι) in f, y < u a) ↔ ∀ y < ↑r, ∃ᶠ (a : ι) in f, y < ↑(u a)
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
x : α
hx : x ∈ s
⊢ g x ≤ f x

Tactic:
simpa only [add_zero, Subtype.coe_mk, mul_zero, dist_self] using ciInf_le (B x) ⟨x, hx⟩

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

Goal state before:
pp: α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i => by
    have : LipschitzOnWith K (fun x : α => f x i) s :=
      LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
        (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
    exact this.extend_real
  choose g hg using this
  refine ⟨fun x i => g i x, LipschitzWith.of_dist_le_mul fun x y => ?_, fun x hx ↦ ?_⟩
  · exact (dist_pi_le_iff (mul_nonneg K.2 dist_nonneg)).2 fun i => (hg i).1.dist_le_mul x y
  · ext1 i
    exact (hg i).2 hx

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

Goal state before:
pp: case cons
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s✝ : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : ∀ i ∈ cons a s ha, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))

Tactic:
rw [forall_mem_cons] at hs

Goal state after:
case cons
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s✝ : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))
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 : (a, b) ∈ s
x : α
y : β
hxy : (x, y) ∈ s
h : dist (a, b) (x, y) ≤ ε / (2 * C)
⊢ dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) (a, b)) (Function.uncurry (fun x1 x2 ↦ x1 • x2) (x, y)) ≤ ε

Tactic:
grw [hC, Metric.mem_ball, Prod.dist_eq, max_lt_iff] at hab hxy

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, b).1 0.1 < C ∧ dist (a, b).2 0.2 < C
x : α
y : β
hxy : dist (x, y).1 0.1 < C ∧ dist (x, y).2 0.2 < C
h : dist (a, b) (x, y) ≤ ε / (2 * C)
⊢ dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) (a, b)) (Function.uncurry (fun x1 x2 ↦ x1 • x2) (x, y)) ≤ ε
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
x y : α
h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖

Tactic:
simpa only [inf_idem, sub_zero] using h

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

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
⊢ Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖

Tactic:
simp only [isometry_iff_dist_eq, dist_eq_norm_inv_mul, ← map_inv, ← map_mul]
  refine ⟨fun h x => ?_, fun h x y => h _⟩
  simpa using h x 1

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

Goal state before:
pp: 𝕜✝ : Type u_5
inst✝² : NormedDivisionRing 𝕜✝
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
⊢ ‖x‖ = 1

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℕ, ‖x‖ ^ k < ε := exists_pow_lt_of_lt_one εpos h

Goal state after:
𝕜✝ : Type u_5
inst✝² : NormedDivisionRing 𝕜✝
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
k : ℕ
hk : ‖x‖ ^ k < ε
⊢ ‖x‖ = 1
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π ↑i_1
j : ι
hj : ¬j = i
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j

Tactic:
simp [hj, updateFinset]

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : ¬j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

Tactic:
simp [hj, updateFinset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Tactic:
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
  · simp [h, prod_eq_empty_iff.mp h]
  · simp [← not_nonempty_iff_eq_empty, prod_nonempty_iff.mp h, measurableSet_prod_of_nonempty h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
⊢ Measurable fun x ↦ a = f x

Tactic:
by
  conv => enter [1, x]; rw [eq_comm]
  exact .eq_const hf a

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ∀ (a : SignType), -1 ≤ a

Tactic:
by exact LE.of_neg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
a : α
ha : a ∈ s
b : β
x✝ : s.domRestrict r ⟨a, ha⟩ b
⊢ (∀ᶠ (x' : ↑s) in 𝓝 ⟨a, ha⟩, s.domRestrict r x' b) ↔ ∀ᶠ (x' : α) in 𝓝[s] a, r x' b

Tactic:
simp only [nhdsWithin_eq_map_subtype_coe ha, eventually_map, domRestrict]

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

Goal state before:
pp: a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ a⁻¹⁻¹ = a

Tactic:
← coe_toReal h' h,

Goal state after:
a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ (↑a.toReal)⁻¹⁻¹ = ↑a.toReal
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
β : Type u_4
f : α → ℝ
hf : Summable f
hn : ∀ (a : α), 0 ≤ f a
i : β → α
hi : Injective i
⊢ tsum (f ∘ i) ≤ tsum f

Tactic:
by
  lift f to α → ℝ≥0 using hn
  rw [NNReal.summable_coe] at hf
  simpa only [Function.comp_def, ← NNReal.coe_tsum] using! NNReal.tsum_comp_le_tsum_of_inj hf hi

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

Goal state before:
pp: a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : a ≠ 0
⊢ a / a = 1

Tactic:
← coe_toReal h₂ h₁

Goal state after:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : ↑a.toReal ≠ 0
⊢ ↑a.toReal / ↑a.toReal = 1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a < c / b ↔ a * b < c

Tactic:
nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' h.ne']
  rw [EReal.mul_div b a b, mul_comm a b]
  exact (strictMono_div_right_of_pos h h').lt_iff_lt

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

Goal state before:
pp: case inl
α : Type u_4
s : Set α
hfin : s.Finite
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Tactic:
lift s to Finset α using hfin

Goal state after:
case inl
α : Type u_4
s : Finset α
⊢ ∑' (x : ↑↑s), 1 = ↑(↑s).encard
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
⊢ C / ↑n = ↑(C.toReal / ↑n)

Tactic:
← coe_toReal h' h,

Goal state after:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
⊢ ↑C.toReal / ↑n = ↑(C.toReal / ↑n)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val) ((comap Subtype.val) (OuterMeasure.ofFunction m m_empty)) =
    OuterMeasure.ofFunction (fun t ↦ m (s ∩ t)) ⋯

Tactic:
comap_ofFunction _ (Or.inl hm)

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val) (OuterMeasure.ofFunction (fun s_1 ↦ m (Subtype.val '' s_1)) ⋯) =
    OuterMeasure.ofFunction (fun t ↦ m (s ∩ t)) ⋯
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ ↑⌊a * b⌋₊ / b

Tactic:
refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Goal state after:
case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : 1 ≤ x
⊢ a - x⁻¹ ≤ ↑⌊a * x⌋₊ / x
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a

Tactic:
refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Goal state after:
case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : 1 ≤ x
⊢ ↑⌊a * x⌋₊ / x ≤ a
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a ≤ ↑⌈a * b⌉₊ / b

Tactic:
refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Goal state after:
case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
x : R
hx : 1 ≤ x
⊢ a ≤ ↑⌈a * x⌉₊ / x
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌈a * b⌉₊ / b ≤ a + b⁻¹

Tactic:
refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Goal state after:
case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
x : R
hx : 1 ≤ x
⊢ ↑⌈a * x⌉₊ / x ≤ a + x⁻¹
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case insert
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
i : ι
t : Finset ι
hi : i ∉ t
IH : (∀ i ∈ ↑t, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i ∈ ↑t, s i)
h : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ t → m.IsCaratheodory (s i_1)
⊢ m.IsCaratheodory (s i ∪ ⋃ x ∈ t, s x)

Tactic:
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_6
β : Type u_7
inst✝ : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)
x : β
⊢ C x ∅ →
    (∀ t ∈ s, C x t) →
      (∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ) →
        (∀ (f : ℕ → Set α),
            Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)) →
          ∀ ⦃t : Set α⦄, MeasurableSet t → C x t

Tactic:
hx_empty

Goal state after:
α : Type u_6
β : Type u_7
inst✝ : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)
x : β
hx_empty : C x ∅
⊢ (∀ t ∈ s, C x t) →
    (∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ) →
      (∀ (f : ℕ → Set α),
          Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)) →
        ∀ ⦃t : Set α⦄, MeasurableSet t → C x t
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ᶜ ∪ s₂)

Tactic:
exact d.has_union (d.has_compl h₁) h₂ (disjoint_compl_left.mono_right h)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
this : extend m s₂ = extend m s₁ + extend m (s₂ \ s₁)
⊢ extend m s₁ ≤ extend m s₂

Tactic:
exact le_iff_exists_add.2 ⟨_, this⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s (map f μ)
⊢ (map f μ) s = μ (f ⁻¹' s)

Tactic:
by
  rw [map, dif_pos hf, mapₗ, dif_pos hf.measurable_mk] at hs ⊢
  rw [liftLinear_apply₀ _ hs, measure_congr (hf.ae_eq_mk.preimage s)]
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ Injective (map f)

Tactic:
intro μ ν h
  ext s hs
  rw [← Set.preimage_image_eq s hf.injective, ← hf.map_apply, ← hf.map_apply]
  congr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measure.map (⇑e.symm ∘ ⇑e) μ ≪ μ

pp: case hg
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measurable ⇑e.symm

pp: case hf
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measurable ⇑e

Tactic:
e.symm_comp_self,

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measure.map id μ ≪ μ

case hg
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measurable ⇑e.symm

case hf
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measurable ⇑e
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ∞
u : Set α
⊢ ∀ (v : Set α), μ (u ∆ v) ≠ ∞ → μ u = ∞ → μ v = ∞

Tactic:
v

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ∞
u v : Set α
⊢ μ (u ∆ v) ≠ ∞ → μ u = ∞ → μ v = ∞
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case pos.mpr.refine_1
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
⊢ ∀ i < b, ∃ i', True ∧ Ici i' ⊆ Subtype.val ⁻¹' Ioo i b

Tactic:
intro a hab
        rcases h a hab with ⟨c, hcs, hc⟩
        use ⟨c, hcs⟩
        simp_all [subset_def, hc.1.trans_le]

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

Goal state before:
pp: X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
decr : Antitone fun n ↦ ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left✝ : j ≥ 0
x_in_Es_j : x ∈ Es j
⊢ x ∈ ∅

Tactic:
obtain ⟨k, k_gt_j, x_in_Es_k⟩ := hx (j + 1)

Goal state after:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
decr : Antitone fun n ↦ ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left✝ : j ≥ 0
x_in_Es_j : x ∈ Es j
k : ℕ
k_gt_j : k ≥ j + 1
x_in_Es_k : x ∈ Es k
⊢ x ∈ ∅
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : m = ⊥
⊢ ∃ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D) = m

Tactic:
exact ⟨∅, by simp, by simp [hm]⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))

Tactic:
refine .of_neBot_imp fun h ↦ ?_

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
h : atTop.NeBot
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Tactic:
refine .of_neBot_imp fun h ↦ ?_

Goal state after:
α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ∞
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))

Tactic:
refine .of_neBot_imp fun h ↦ ?_

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ∞
h : atTop.NeBot
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case basic
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
this : IsFiniteMeasure ν
t : Set α
ht : t ∈ C
⊢ μ t = ν t

Tactic:
| basic t ht =>

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
u : Set α
⊢ ∀ {v : Set α}, u ∈ memPartition f 0 → v ∈ memPartition f 0 → u ≠ v → Disjoint u v

Tactic:
v

Goal state after:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
⊢ u ∈ memPartition f 0 → v ∈ memPartition f 0 → u ≠ v → Disjoint u v
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u : Set α
⊢ ∀ {v : Set α}, u ∈ memPartition f (n + 1) → v ∈ memPartition f (n + 1) → u ≠ v → Disjoint u v

Tactic:
v

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
⊢ u ∈ memPartition f (n + 1) → v ∈ memPartition f (n + 1) → u ≠ v → Disjoint u v
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
n : ℕ
hn : r < μ (s ∩ spanningSets μ n)
⊢ μ (s ∩ spanningSets μ n) < ∞

Tactic:
exact (measure_mono inter_subset_right).trans_lt (measure_spanningSets_lt_top _ _)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∀ (x : ℕ), (if x = 1 then 0 else if x = 0 then 0 else min (μ (t' x)) (ν (t' x))) = 0

Tactic:
simp only [ite_eq_left_iff]
        intro n hn₁ hn₀
        simp only [ht', if_neg hn₀, if_neg hn₁, measure_empty, le_refl, inf_of_le_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : SeparatesPoints α
b : Set (Set α)
hbc : b.Countable
hb : inst✝¹ = generateFrom b
⊢ ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y

Tactic:
rw [hb] at ‹SeparatesPoints _›

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
b : Set (Set α)
inst✝ : SeparatesPoints α
hbc : b.Countable
hb : inst✝¹ = generateFrom b
⊢ ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y