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

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
⊢ Disjoint (measurableAtom x) (measurableAtom y)

Tactic:
rw [Set.disjoint_iff_inter_eq_empty]
  ext z
  simp only [mem_inter_iff, mem_empty_iff_false, iff_false, not_and]
  intro hzx hzy
  have h1 := measurableAtom_eq_of_mem hzx
  have h2 := measurableAtom_eq_of_mem hzy
  rw [← h2, h1] at hx
  exact hx (mem_measurableAtom_self x)

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
t : (i : δ) → Set (X i)
ht : ∀ (i : δ), MeasurableSet (t i)
⊢ univ.pi t = {f | ∀ (i : δ), f i ∈ t i}

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inl)

Tactic:
← image_univ

Goal state after:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inl '' univ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inr)

Tactic:
← image_univ

Goal state after:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inr '' univ)
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inl
z : ℤ
hz : Odd z
⊢ 0 ^ z = 0

Tactic:
rw [zero_zpow]

Goal state after:
case inl.a
z : ℤ
hz : Odd z
⊢ z ≠ 0
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: s : SignType
n : ℕ
hn : Even n
hs : s ≠ 0
⊢ s ^ n = 1

Tactic:
cases s <;> simp_all

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

Goal state before:
pp: case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = pos
⊢ sign (∑ i ∈ s, f i) = pos

Tactic:
simp_rw [pos_eq_one, sign_eq_one_iff] at h ⊢
    exact Finset.sum_pos h hs

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ 1 / (↑m + 1) ≤ 1 / (↑n + 1)

Tactic:
by
  refine one_div_le_one_div_of_le ?_ ?_
  · exact Nat.cast_add_one_pos _
  · simpa

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
⊢ sign a = 1 ↔ 0 < a

Tactic:
by
  refine ⟨fun h => ?_, fun h => sign_pos h⟩
  by_contra hn
  rw [sign_apply, if_neg hn] at h
  split_ifs at h

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

Goal state before:
pp: case bot
⊢ ⊥.abs = 0 ↔ ⊥ = 0

pp: case coe
a✝ : ℝ
⊢ (↑a✝).abs = 0 ↔ ↑a✝ = 0

pp: case top
⊢ ⊤.abs = 0 ↔ ⊤ = 0

Tactic:
· simp

Goal state after:
case coe
a✝ : ℝ
⊢ (↑a✝).abs = 0 ↔ ↑a✝ = 0

case top
⊢ ⊤.abs = 0 ↔ ⊤ = 0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

pp: case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
· simp

Goal state after:
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
· simp

Goal state after:
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
· simp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

pp: case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
· simp

Goal state after:
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
· simp

Goal state after:
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
· simp

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

Goal state before:
pp: 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

pp: 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

pp: 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

Tactic:
· simp

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

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: case coe.inr.inl
⊢ ↑(sign ↑0) * (↑(↑0).abs)⁻¹ = (↑0)⁻¹

pp: case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(sign ↑a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Tactic:
· simp

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(sign ↑a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inr.inl
⊢ ↑(sign ↑0) * ↑(↑0).abs⁻¹ = (↑0)⁻¹

pp: case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(sign ↑a) * ↑(↑a).abs⁻¹ = (↑a)⁻¹

Tactic:
· simp

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(sign ↑a) * ↑(↑a).abs⁻¹ = (↑a)⁻¹
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ UpperHemicontinuousWithinAt f s x ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
rw [UpperHemicontinuousWithinAt, semicontinuousWithinAt_iff_frequently, compl_surjective.forall]
  simp [← subset_interior_iff_mem_nhdsSet, not_subset, forall_isClosed_iff, inter_nonempty]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
h : SemicontinuousWithinAt (fun x1 x2 ↦ f x1 > x2) s x
hf : liminf f (𝓝[s] x) < f x
z : γ
ltz : z > liminf f (𝓝[s] x)
y : γ
ylt : y < f x
h₁ : ∀ x < z, ∀ y_1 > y, x < y_1
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝[s] x) f

Tactic:
by isBoundedDefault

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
a_u : a < liminf u f
b : EReal
b_v : b < liminf v f
c : EReal
c_ab : c < a + b
x : α
⊢ a < u x → b < v x → c < (u + v) x

Tactic:
a_x

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
a_u : a < liminf u f
b : EReal
b_v : b < liminf v f
c : EReal
c_ab : c < a + b
x : α
a_x : a < u x
⊢ b < v x → c < (u + v) x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a + b
x : α
⊢ u x < a → v x < b → (u + v) x < c

Tactic:
a_x

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a + b
x : α
a_x : u x < a
⊢ v x < b → (u + v) x < c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
h₁ : 0 ≤ 0
h₂ : 0 ≠ ⊤
⊢ limsup (fun x ↦ 0 * u x) f = 0 * limsup u f

pp: case inr
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun x ↦ c * u x) f = c * limsup u f

Tactic:
· simp

Goal state after:
case inr
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun x ↦ c * u x) f = c * limsup u f
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case pos
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto (fun n ↦ |r| ^ n) atTop (𝓝 0)
⊢ False

Tactic:
simp only [hr.symm, one_pow] at h

Goal state after:
case pos
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto (fun n ↦ 1) atTop (𝓝 0)
⊢ False
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 ^ 0 * u 0 ≤ u 0

pp: 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)

Tactic:
· simp

Goal state after:
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.OfFunction

Goal state before:
pp: case zero
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i ↦ Nat.casesOn i s fun x ↦ ∅
⊢ 0 ≠ 0 → m (f 0) = 0

pp: case succ
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i ↦ Nat.casesOn i s fun x ↦ ∅
i : ℕ
⊢ i + 1 ≠ 0 → m (f (i + 1)) = 0

Tactic:
· simp

Goal state after:
case succ
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i ↦ Nat.casesOn i s fun x ↦ ∅
i : ℕ
⊢ i + 1 ≠ 0 → m (f (i + 1)) = 0
Module: Mathlib.Analysis.SpecificLimits.Basic

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

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

Tactic:
· simp

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

Goal state before:
pp: a : ℝ
⊢ HasSum (fun n ↦ a / 2 / 2 ^ n) a

Tactic:
by
  convert!
    HasSum.mul_left (a / 2)
      (hasSum_geometric_of_lt_one (le_of_lt one_half_pos) one_half_lt_one) using 1
  · funext n
    simp only [one_div, inv_pow]
    rfl
  · norm_num

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

Goal state before:
pp: ⊢ ∑' (m : ℕ), 2 ^ (-1 - ↑m) = 1

Tactic:
neg_sub_left,

Goal state after:
⊢ ∑' (m : ℕ), 2 ^ (-(↑m + 1)) = 1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a b : ℝ
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a, ↑b)

Tactic:
by
  simp [ContinuousAt, EReal.nhds_coe_coe, ← EReal.coe_mul, Filter.tendsto_map'_iff,
    Function.comp_def, EReal.tendsto_coe, tendsto_mul]

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

Goal state before:
pp: case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (max (↑x) 0)

pp: case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1

Tactic:
· simp

Goal state after:
case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * max (x + 1) 0 / a)

pp: case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)

Tactic:
· simp

Goal state after:
case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε

Tactic:
rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
  refine ⟨ε', hpos, fun t ht ↦ ?_⟩
  rw [← sum_subtype_of_mem _ ht]
  refine (sum_le_hasSum _ ?_ hε'c).trans hcε
  exact fun _ _ ↦ (hpos _).le

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ ↑n ! / ↑n ^ n ≤ 1 / ↑n

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩

Goal state after:
k : ℕ
hn : 0 < k.succ
⊢ ↑k.succ ! / ↑k.succ ^ k.succ ≤ 1 / ↑k.succ
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
⊢ t ∈ {S} → (s ∩ t).Nonempty → s ∩ t ∈ {S}

Tactic:
h_t

Goal state after:
α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
⊢ (s ∩ t).Nonempty → s ∩ t ∈ {S}
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)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ m (t ∩ ⋃ i, s i) + m (t \ ⋃ i, s i) ≤ m t

Tactic:
hp,

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ (⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)) + m (t \ ⋃ i, s i) ≤ m t
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)
⊢ ∑' (i : ℕ), m (s i) ≤ m (⋃ i, s i)

Tactic:
rw [ENNReal.tsum_eq_iSup_nat]

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ ⨆ i, ∑ a ∈ Finset.range i, m (s a) ≤ m (⋃ i, s i)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inl.refine_3
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ x ∈ {i}, (fun x ↦ s) x

Tactic:
simp only [Finset.mem_singleton, iInter_iInter_eq_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s

Tactic:
simpa only [← measure_eq_trim] using! μ.toOuterMeasure.exists_measurable_superset_eq_trim s

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ ¬μ (s ∪ t) = ∞ ↔ ¬(μ s = ∞ ∨ μ t = ∞)

Tactic:
simp only [← lt_top_iff_ne_top, ← Ne.eq_def, not_or, measure_union_lt_top_iff]

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 : t =ᵐ[μ] ∅
⊢ s ∩ t =ᵐ[μ] ∅

Tactic:
by
  convert! ae_eq_set_inter (ae_eq_refl s) h
  rw [inter_empty]

Goal state after:
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
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ (toMeasurable μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n ↦ f n x}ᶜ)ᶜ ⊆
    {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}

Tactic:
← compl_compl { x | ∀ i, f i x = (hf i).mk (f i) x },

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ (toMeasurable μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n ↦ f n x}ᶜ)ᶜ ⊆
    {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}ᶜᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
this : x = univ
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
this : x ⊆ ∅
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
by grind

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

Goal state before:
pp: case mpr.inr.inr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = sᶜ

Tactic:
(Tactic.tacticSeq
 (Tactic.tacticSeq1Indented
  [(Mathlib.Tactic.useSyntax
    "use"
    []
    (group)
    [(choice
      («term{_}» "{" [`False] "}")
      (Term.structInst
       "{"
       []
       (Term.structInstFields [(Term.structInstField (Term.structInstLVal `False []) [])])
       (Term.optEllipsis [])
       []
       "}"))])]))

Goal state after:
case h
α : Type u_1
s : Set α
⊢ (fun x ↦ x ∈ s) ⁻¹' {False} = sᶜ
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
s : Set α
hs : MeasurableSet s
⊢ m.trim s ≤ m s

Tactic:
trim_eq _ (h s hs)

Goal state after:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
s : Set α
hs : MeasurableSet s
⊢ m s ≤ m s
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ MeasurableSet (range f)

Tactic:
← image_univ

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ MeasurableSet (f '' univ)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs✝ : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r

Tactic:
have : ∃ t, MeasurableSet t ∧ s ⊆ t ∧ m t < r := by simpa [ms, iInf_lt_iff] using hs

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs✝ : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
this : ∃ t, MeasurableSet t ∧ s ⊆ t ∧ m t < r
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
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)
⊢ ∀ (a : δ ⊕ δ'), Measurable fun x ↦ (Equiv.sumPiEquivProdPi α).symm x a

Tactic:
rintro (i | i)

Goal state after:
case inl
α✝ : 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)
i : δ
⊢ Measurable fun x ↦ (Equiv.sumPiEquivProdPi α).symm x (Sum.inl i)

case inr
α✝ : 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)
i : δ'
⊢ Measurable fun x ↦ (Equiv.sumPiEquivProdPi α).symm x (Sum.inr i)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_2.a.zero
α : 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) ⊆ F^[0] univ

pp: case refine_2.a.succ
α : 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
n✝ : ℕ
⊢ F (iInter X) ⊆ F^[n✝ + 1] univ

Tactic:
· exact subset_univ _

Goal state after:
case refine_2.a.succ
α : 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
n✝ : ℕ
⊢ F (iInter X) ⊆ F^[n✝ + 1] univ
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ (mapₗ (AEMeasurable.mk f hf)) μ = map f μ

Tactic:
by simp [map, hf]

Goal state after: