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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
h✝ : b ∈ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
h✝ : b ∉ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
p : Prop
h✝ : p
⊢ MeasurableSet {_a | p}

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
p : Prop
h✝ : ¬p
⊢ MeasurableSet {_a | p}

Tactic:
simp [*]

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

Goal state before:
pp: case inr
𝕜 : 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
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ ↑⟨k • e, hx⟩ ∈ ball 0 ‖e‖ ↔ ⟨k • e, hx⟩ ∈ {0}

Tactic:
mem_ball_zero_iff,

Goal state after:
case inr
𝕜 : 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
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ ‖↑⟨k • e, hx⟩‖ < ‖e‖ ↔ ⟨k • e, hx⟩ ∈ {0}
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x : 𝕜
⊢ ‖x • 1‖ = ‖x‖

Tactic:
by
  simp [norm_smul]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
hs : μ s = 0
ht : μ t = 0
⊢ μ (s ∪ t) = 0

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
⊢ Measurable fun x ↦ Nat.find ⋯

Tactic:
refine measurable_to_nat fun x => ?_

Goal state after:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet ((fun x ↦ Nat.find ⋯) ⁻¹' {Nat.find ⋯})
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C : ℝ
hC : ⇑f '' ball 0 δ ⊆ ball 0 C
ε : ℝ
hε : 0 < ε
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, dist x 0 < δ → dist (f x) (f 0) < ε

Tactic:
simp only [dist_zero_right, map_zero]

Goal state after:
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C : ℝ
hC : ⇑f '' ball 0 δ ⊆ ball 0 C
ε : ℝ
hε : 0 < ε
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → ‖f x‖ < ε
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
⊢ ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)

Tactic:
by simp +contextual

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α × β → γ
hf : ∀ (x : α), Measurable fun y ↦ f (x, y)
⊢ ∀ (x x' : α) (y : β), x' ∈ measurableAtom x → f (x', y) = f (x, y)

Tactic:
by simp +contextual

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

Goal state before:
pp: ι : Type u_4
s : Finset ι
f : ι → ℝ≥0∞
⊢ ∑' (x : ι), (↑s).indicator f x + ∑' (x : ι), (↑s)ᶜ.indicator f x = ∑' (i : ι), f i

Tactic:
simp [← ENNReal.tsum_add]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
⊢ ∑' (a : α), ↑(f a) ≠ ∞ ↔ Summable fun a ↦ ↑(f a)

Tactic:
by
  rw [NNReal.summable_coe]
  exact tsum_coe_ne_top_iff_summable

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

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

Tactic:
rcases lt_trichotomy a 0 with a0 | rfl | a0
    · obtain ⟨a', aa', a0'⟩ := exists_between a0
      rw [mul_top_of_neg a0] at hc
      refine ⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt a0'⟩, mul_top_of_neg a0' ▸ hc⟩
    · rw [ne_self_iff_false, ne_self_iff_false, false_or] at h₁; exact h₁.rec
    · rw [mul_top_of_pos a0] at hc; exact (not_top_lt hc).rec

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ↑(f x)) l (𝓝 ⊤) ↔ Tendsto f l atTop

Tactic:
tendsto_nhds_top_iff_real,

Goal state after:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ Tendsto f l atTop
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : 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
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
H : f x < f z
⊢ min (f z) (f x) ∈ u

Tactic:
· simpa [H.le]

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

Goal state before:
pp: case neg
α : 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
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
A1 : min (f z) (f x) ∈ u
H : g x < g z
⊢ min (g z) (g x) ∈ v

Tactic:
· simpa [H.le]

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

Goal state before:
pp: r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ↑n = ↑(#(Finset.range n))

Tactic:
card_range

Goal state after:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ↑n = ↑n
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : 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
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : f z > z₁
H : f x < f z
⊢ min (f z) (f x) ∈ u

Tactic:
· simpa [H.le]

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

Goal state before:
pp: case inl
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
⊢ (c • fun s ↦ ⨆ (_ : s.Nonempty), m s) ∅ = ⨆ (_ : ∅.Nonempty), (c • m) ∅

Tactic:
simp [*]

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

Goal state before:
pp: case inr
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
hs : s.Nonempty
⊢ (c • fun s ↦ ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s

Tactic:
simp [*]

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

Goal state before:
pp: case inr
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
ht : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t

Tactic:
· simp [ht, sInfGen_def]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ UpperSemicontinuous f ↔ ∀ (y : γ), IsClosed[inst✝¹] (f ⁻¹' Ici y)

Tactic:
upperSemicontinuous_iff_isOpen_preimage

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen[inst✝¹] (f ⁻¹' Iio y)) ↔ ∀ (y : γ), IsClosed[inst✝¹] (f ⁻¹' Ici y)
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
n m : ℕ
hm : s m ⊆ dissipate s n
k : ℕ
hk : (fun x1 x2 ↦ x1 ⊇ x2) (s m) (s k) ∧ (fun x1 x2 ↦ x1 ⊇ x2) (s (n + 1)) (s k)
⊢ s k ⊆ dissipate s (n + 1)

Tactic:
by simp; grind

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x

Tactic:
by
  simp_rw [← continuousWithinAt_univ, ← lowerSemicontinuousWithinAt_univ_iff, ←
    upperSemicontinuousWithinAt_univ_iff, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ m.IsCaratheodory (⋃ i, s i)

Tactic:
apply (isCaratheodory_iff_le' m).mpr
  intro t
  have hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i < n, s i) := by
    convert! measure_iUnion_le (μ := m) fun i => t ∩ s i using 1
    · simp [inter_iUnion]
    · simp [ENNReal.tsum_eq_iSup_nat, isCaratheodory_sum m h hd]
  grw [hp, ENNReal.iSup_add]
  refine iSup_le fun n => ?_
  rw [isCaratheodory_iUnion_lt _ (fun i _ => h i) t (n := n)]
  gcongr with i
  exact iUnion_subset fun _ => .rfl

Goal state after:
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 (⋃ b, bif b then s₁ else s₂) = extend m s₁ + extend m s₂

Tactic:
extend_iUnion P0 m0 PU mU (pairwise_disjoint_on_bool.2 hd) (Bool.forall_bool.2 ⟨h₂, h₁⟩),

Goal state after:
α : 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₂
⊢ ∑' (i : Bool), extend m (bif i then s₁ else s₂) = extend m s₁ + extend m s₂
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
hs : a ∈ s
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
hs : a ∉ s
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mp
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
⊢ a ∈ ⋂ b ∈ T, f b → a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b

Tactic:
· simp -proj only
          [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
        intro h1 b h_b h_b_in_T
        have h2 := h1 b h_b h_b_in_T
        revert h2
        rw [Subtype.val_injective.extend_apply]
        apply id

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
⊢ a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b → a ∈ ⋂ b ∈ T, f b

Tactic:
· simp -proj only
          [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
        intro h1 b h_b h_b_in_T
        have h2 := h1 b h_b h_b_in_T
        revert h2
        rw [Subtype.val_injective.extend_apply]
        apply id

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

Goal state before:
pp: case e_f
α : 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)
n : ℕ
⊢ m (f n) ⋯ = (inducedOuterMeasure m ⋯ m0) (f n)

Tactic:
inducedOuterMeasure_eq m0 mU

Goal state after:
case e_f
α : 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)
n : ℕ
⊢ m (f n) ⋯ = m (f n) ?e_f✝

case e_f
α : 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)
n : ℕ
⊢ MeasurableSet (f n)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
t₁ t₂ : Set α
ht₁ : (generate s).Has t₁
ht₂ : (generate s).Has t₂
s₁ : Set α
hs₁ : s₁ ∈ s
this✝¹ : (generate s).Has s₁
this✝ : generate s ≤ (generate s).restrictOn this✝¹
this : (generate s).Has (t₂ ∩ s₁)
⊢ (generate s).Has (s₁ ∩ t₂)

Tactic:
inter_comm

Goal state after:
α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
t₁ t₂ : Set α
ht₁ : (generate s).Has t₁
ht₂ : (generate s).Has t₂
s₁ : Set α
hs₁ : s₁ ∈ s
this✝¹ : (generate s).Has s₁
this✝ : generate s ≤ (generate s).restrictOn this✝¹
this : (generate s).Has (t₂ ∩ s₁)
⊢ (generate s).Has (t₂ ∩ s₁)
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 ≤ᵐ[μ] t
⊢ μ t + μ (s \ t) = μ t

Tactic:
rw [ae_le_set.1 H, add_zero]

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
h's : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ h's.choose = μ s

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)
⊢ μ ⋯.choose = μ s

Tactic:
· simpa only [inter_univ] using h's.choose_spec.2.2 univ MeasurableSet.univ

Goal state after:
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)
⊢ μ ⋯.choose = μ s
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set α
⊢ ⇑e ⁻¹' ⇑e '' s = s

Tactic:
by
  rw [← coe_toEquiv, Equiv.preimage_image]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝² : (x : δ') → MeasurableSpace (π x)
inst✝¹ : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ Measurable ⇑(Equiv.sumPiEquivProdPi α).symm

Tactic:
by
    rw [measurable_pi_iff]; rintro (i | i)
    · exact measurable_pi_iff.1 measurable_fst _
    · exact measurable_pi_iff.1 measurable_snd _

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

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ μ (t ∩ s) = 0

Tactic:
inter_comm

Goal state after:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ μ (s ∩ t) = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
⊢ F (iInter X) = iInter X

Tactic:
apply subset_antisymm

Goal state after:
case refine_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := ⋯
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := ⋯
⊢ F (iInter X) ⊆ iInter X

case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := ⋯
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := ⋯
⊢ iInter X ⊆ F (iInter X)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
n : ℕ
⊢ y ∈ f '' F^[n] univ

Tactic:
specialize hx n.succ

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F^[n.succ] univ
⊢ y ∈ f '' F^[n] univ
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : ν s = 0
⊢ (c • μ) s = 0

Tactic:
by
  simp only [h hνs, smul_apply, smul_zero, ← smul_one_smul ℝ≥0∞ c (0 : ℝ≥0∞)]

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

Goal state before:
pp: case hf
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet ((fun x ↦ x) '' s)

Tactic:
simp [*]

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

Goal state before:
pp: case hs
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise Disjoint
h : ∀ s ∈ S, MeasurableSet s
⊢ μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s

Tactic:
by
  rw [sUnion_eq_biUnion, measure_biUnion hs hd h]

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

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

Tactic:
ENNReal.sub_eq_top_iff.2 ⟨hμu, hμv⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ∞
u v : Set α
hμuv : μ (u ∆ v) ≠ ∞
hμu : μ u = ∞
hμv : μ v ≠ ∞
⊢ ∞ = ∞
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
hsne : s.Nonempty
this✝ : Nonempty ↑s
hsub : ¬s ⊆ Iio b
this : ¬Tendsto Subtype.val atTop (𝓝[<] b)
⊢ comap Subtype.val (𝓝[<] b) = atTop ↔ s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty

Tactic:
contrapose this
      simp_all [tendsto_iff_comap]

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
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
⊢ ∀ a' < toDual a, ∃ a_2 < toDual a, Ioo a_2 (toDual a) ⊆ ⇑ofDual ⁻¹' s

Tactic:
intro b'

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
b' : Xᵒᵈ
⊢ b' < toDual a → ∃ a_2 < toDual a, Ioo a_2 (toDual a) ⊆ ⇑ofDual ⁻¹' s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ t + μ s
⊢ (s ∩ t).Nonempty

Tactic:
inter_comm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ t + μ s
⊢ (t ∩ s).Nonempty