mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b : α
x : ↑(Iic b)
⊢ projIic b ↑x = x

Tactic:
cases x; apply projIic_of_mem

Goal state after:
Module: Mathlib.Topology.Algebra.UniformMulAction

Goal state before:
pp: M : Type v
X : Type x
inst✝³ : UniformSpace X
inst✝² : Monoid M
inst✝¹ : MulAction M X
inst✝ : UniformContinuousConstSMul M X
c : M
hc : IsUnit c
d : M
hcd : c * d = 1
cU : c • 𝓤 X ≤ 𝓤 X
dU : d • 𝓤 X ≤ 𝓤 X
⊢ 𝓤 X ≤ c • 𝓤 X

Tactic:
by simpa [smul_smul, hcd] using Filter.smul_filter_le_smul_filter (a := c) dU

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)

Tactic:
filter_upwards [Metric.closedEBall_mem_nhds x (ENNReal.coe_pos.2 δ0)] with y hy

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f y ∈ Icc (f x - ε) (f x + ε)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a b : ℝ
⊢ ediam (Ioo a b) = ENNReal.ofReal (b - a)

Tactic:
rcases le_or_gt b a with (h | h)
  · simp [h]
  · rw [Real.ediam_eq (isBounded_Ioo _ _), csSup_Ioo h, csInf_Ioo h]

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞
h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0
a : ℝ≥0∞
a_u : a > limsup u f
b : ℝ≥0∞
b_v : b > limsup v f
c : ℝ≥0∞
c_ab : c > a * b
x : ι
a_x : u x < a
⊢ v x < b → (u * v) x < c

Tactic:
b_x

Goal state after:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞
h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0
a : ℝ≥0∞
a_u : a > limsup u f
b : ℝ≥0∞
b_v : b > limsup v f
c : ℝ≥0∞
c_ab : c > a * b
x : ι
a_x : u x < a
b_x : v x < b
⊢ (u * v) x < c
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
c_ab : c < a * b
x : ι
a_x : a < u x
⊢ b < v x → c < (u * v) x

Tactic:
b_x

Goal state after:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
c_ab : c < a * b
x : ι
a_x : a < u x
b_x : b < v x
⊢ c < (u * v) x
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 * dist b y + dist a x * dist y 0 ≤ ε

Tactic:
hxy.2,

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)
⊢ C * dist b y + dist a x * C ≤ ε
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₂ : y ∈ Prod.snd ⁻¹' U
this : r ≤ ‖f y.2‖
hy₁ : ‖f y.2 - F y.1 y.2‖ < r / 2
⊢ r / 2 < ‖F y.1 y.2‖

Tactic:
linarith [hy₁, norm_sub_norm_le (f y.2) (F y.1 y.2)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
g : α → β
f : β → γ
hg : Function.Surjective g
⊢ mγ ≤ MeasurableSpace.map f mβ ↔ mγ ≤ MeasurableSpace.map f (MeasurableSpace.map g (MeasurableSpace.comap g mβ))

Tactic:
map_comap_eq_of_surjective hg

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
g : α → β
f : β → γ
hg : Function.Surjective g
⊢ mγ ≤ MeasurableSpace.map f mβ ↔ mγ ≤ MeasurableSpace.map f mβ
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : 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
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples e)

Tactic:
by
  have : IsAddTorsionFree E := .of_module_rat E
  rcases eq_or_ne e 0 with (rfl | he)
  · rw [AddSubgroup.zmultiples_zero_eq_bot]
    exact Subsingleton.discreteTopology (α := ↑(⊥ : Subspace ℚ E))
  · rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]
    refine ⟨Metric.ball 0 ‖e‖, Metric.isOpen_ball, ?_⟩
    ext ⟨x, hx⟩
    obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
    rw [mem_preimage, mem_ball_zero_iff, AddSubgroup.coe_mk, mem_singleton_iff, Subtype.ext_iff,
      AddSubgroup.coe_mk, AddSubgroup.coe_zero, norm_zsmul ℚ k e, Int.norm_cast_rat,
      Int.norm_eq_abs, mul_lt_iff_lt_one_left (norm_pos_iff.mpr he), ← @Int.cast_one ℝ _,
      ← Int.cast_abs, Int.cast_lt, Int.abs_lt_one_iff, smul_eq_zero, or_iff_left he]

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 α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
h0 : Tendsto (fun k ↦ μ ((⋃ n, s n) \ s k)) l (𝓝 0)
⊢ μ (⋃ n, s n) = ⨆ n, μ (s n)

Tactic:
refine le_antisymm ?_ <| iSup_le fun n ↦ measure_mono <| subset_iUnion _ _

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
h0 : Tendsto (fun k ↦ μ ((⋃ n, s n) \ s k)) l (𝓝 0)
⊢ μ (⋃ n, s n) ≤ ⨆ n, μ (s n)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
h : y ∈ measurableAtom x
s : Set β
hs : MeasurableSet s
hxs : x ∈ s
⊢ y ∈ s

Tactic:
simp only [measurableAtom, mem_iInter] at h
  exact h s hxs 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:
refine one_div_lt_one_div_of_lt ?_ ?_

Goal state after:
case refine_1
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n < m
⊢ 0 < ↑n + 1

case refine_2
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n < m
⊢ ↑n + 1 < ↑m + 1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ sign (-a) = -sign a

Tactic:
simp_rw [sign_apply, Right.neg_pos_iff, Right.neg_neg_iff]

Goal state after:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ (if a < 0 then 1 else if 0 < a then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : EReal
⊢ ↑x.abs * ↑(sign x) = x

Tactic:
rw [EReal.mul_comm, EReal.sign_mul_abs]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ update f i 0 i' ≤ f i'

Tactic:
Function.update_apply

Goal state after:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ (if i' = i then 0 else f i') ≤ f i'
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ (𝓝 ⊥).HasBasis (fun x ↦ True) fun x ↦ Iio ↑x

Tactic:
by
  refine (_root_.nhds_bot_basis (α := EReal)).to_hasBasis (fun x hx => ?_)
    fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩
  rcases exists_rat_btwn_of_lt hx with ⟨y, -, hxy⟩
  exact ⟨_, trivial, Iio_subset_Iio hxy.le⟩

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_x : a < u x
⊢ b < v x → c < (u + v) x

Tactic:
b_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_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 : α
a_x : u x < a
⊢ v x < b → (u + v) x < c

Tactic:
b_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
b_x : v x < b
⊢ (u + v) x < c
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
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₁
⊢ g z > z₂ → f z + g z > y

Tactic:
h₂z

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
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₂
⊢ f z + g z > y
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)
⊢ ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)

Tactic:
· simp [_root_.pow_succ', mul_assoc]

Goal state after:
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
⊢ ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0

Tactic:
· simp [_root_.pow_succ', mul_assoc]

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 = ∑ i ∈ Finset.range n, 1

Tactic:
rw [sum_const, nsmul_one, card_range]

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

Goal state before:
pp: case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ n, (range f)ᶜ ∪ f '' t n

pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ∑' (n : ℕ), m (f ⁻¹' (fun n ↦ (range f)ᶜ ∪ f '' t n) n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
· rw [← union_iUnion, ← inter_subset, ← image_preimage_eq_inter_range, ← image_iUnion]
    exact image_mono ht

Goal state after:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ∑' (n : ℕ), m (f ⁻¹' (fun n ↦ (range f)ᶜ ∪ f '' t n) n) ≤ ∑' (n : ℕ), m (t n)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
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₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
⊢ g z > z₂ → f z + g z > y

Tactic:
h₂z

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
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₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
⊢ f z + g z > y
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ μ ≤ OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : s.Nonempty), m s) ⋯ ↔ ∀ (s : Set α), μ s ≤ m s

Tactic:
le_ofFunction,

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ (∀ (s : Set α), μ s ≤ ⨆ (_ : s.Nonempty), m s) ↔ ∀ (s : Set α), μ s ≤ m s
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr
a : ℝ
h : a ≠ 0
a_pos : 0 < a
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)

Tactic:
· exact continuousAt_mul_top_pos a_pos

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h₁ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h₂ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
h₃ : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
h₄ : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝¹, ↑a✝)

Tactic:
exact continuousAt_mul_coe_coe _ _

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + (m (t \ s₁ ∩ s₂) + m ((t \ s₁) \ s₂)) =
    m (t ∩ s₁) + m (t ∩ (s₂ \ s₁)) + m (t \ (s₁ ∪ s₂))

Tactic:
h₂ (t ∩ s₁)

Goal state after:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + (m (t \ s₁ ∩ s₂) + m ((t \ s₁) \ s₂)) =
    m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + m (t ∩ (s₂ \ s₁)) + m (t \ (s₁ ∪ s₂))
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ∈ ⨅ i, f i

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ MeasurableSet (⋂ i, U i)

pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ⊆ ⋂ i, V i

Tactic:
· rw [← Equiv.plift.surjective.iInf_comp, mem_iInf]
    exact ⟨t, ht, U, hUf, rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ MeasurableSet (⋂ i, U i)

case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ⊆ ⋂ i, V i
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ m.trim s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t

Tactic:
simp +singlePass only [iInf_comm]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ m.trim s = ⨅ t, ⨅ (_ : MeasurableSet t), ⨅ (_ : s ⊆ t), m t
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Injective toEquiv

Tactic:
rintro ⟨e₁, _, _⟩ ⟨e₂, _, _⟩ (rfl : e₁ = e₂)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e₁ : α ≃ β
measurable_toFun✝¹ : Measurable ⇑e₁
measurable_invFun✝¹ : Measurable ⇑e₁.symm
measurable_toFun✝ : Measurable ⇑e₁
measurable_invFun✝ : Measurable ⇑e₁.symm
⊢ { toEquiv := e₁, measurable_toFun := measurable_toFun✝¹, measurable_invFun := measurable_invFun✝¹ } =
    { toEquiv := e₁, measurable_toFun := measurable_toFun✝, measurable_invFun := measurable_invFun✝ }
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 : (c • ν) s = 0
⊢ (c • μ) s = 0

Tactic:
smul_apply,

Goal state after:
α : 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 : c • ν s = 0
⊢ c • μ s = 0
Module: Mathlib.MeasureTheory.Measure.Comap

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

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)

Tactic:
smul_apply,

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

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)
Module: Mathlib.MeasureTheory.Measure.Comap

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

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)

Tactic:
smul_apply,

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

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

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

Tactic:
by
  rw [← Set.not_disjoint_iff_nonempty_inter]
  contrapose! h
  calc
    μ s + μ t = μ (s ∪ t) := (measure_union h ht).symm
    _ ≤ μ u := measure_mono (union_subset h's h't)

Goal state after:
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ₗ_apply,

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

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
rcases exists_seq_monotone_tendsto_atTop_atTop ι with ⟨x, hxm, hx⟩

Goal state after:
case inr
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
⊢ (sInf (toOuterMeasure '' m)) (s ∩ t) = (sInf (toOuterMeasure '' (fun μ ↦ μ.restrict t) '' m)) s

Tactic:
Set.image_image,

Goal state after:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
⊢ (sInf (toOuterMeasure '' m)) (s ∩ t) = (sInf ((fun x ↦ (x.restrict t).toOuterMeasure) '' m)) s