mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, x i < ↑(q - 1)

pp: case inr.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, ↑q < x i

Tactic:
· simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd
      refine fun hcon => hbdd ↑(q - 1) ?_
      filter_upwards [hcon] with x hx using not_lt.1 hx

Goal state after:
case inr.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, ↑q < x i
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a : α
f : ↑(Ici a) → β
⊢ range (IciExtend f) = range f

Tactic:
by
  simp only [IciExtend, range_comp f, range_projIci, image_univ]

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

Goal state before:
pp: case pos
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
x y : X
h : ∃ n, (x, y) ∉ U n
⊢ (1 / 2) ^ Nat.find h = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i

pp: case neg
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
x y : X
h : ¬∃ n, (x, y) ∉ U n
⊢ 0 = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i

Tactic:
· simp [h, pow_eq_zero_iff']

Goal state after:
case neg
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
x y : X
h : ¬∃ n, (x, y) ∉ U n
⊢ 0 = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' closedBall b r = closedBall (b / a) r

Tactic:
rw [div_eq_mul_inv]
  exact preimage_smul_closedBall (MulOpposite.op a) b r

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

Goal state before:
pp: case mpr.inr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜},
    x ≠ 0 → (∀ (y : 𝕜), ‖y‖ < ε → y = 0) → ‖x‖ < 1 → ‖x‖ = 1
h : 1 ≤ ‖x‖
⊢ ‖x‖ = 1

Tactic:
rcases h.eq_or_lt with h | h

Goal state after:
case mpr.inr.inl
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜},
    x ≠ 0 → (∀ (y : 𝕜), ‖y‖ < ε → y = 0) → ‖x‖ < 1 → ‖x‖ = 1
h✝ : 1 ≤ ‖x‖
h : 1 = ‖x‖
⊢ ‖x‖ = 1

case mpr.inr.inr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜},
    x ≠ 0 → (∀ (y : 𝕜), ‖y‖ < ε → y = 0) → ‖x‖ < 1 → ‖x‖ = 1
h✝ : 1 ≤ ‖x‖
h : 1 < ‖x‖
⊢ ‖x‖ = 1
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r

Tactic:
rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x ↦ ‖f x‖) l atTop ↔ Tendsto f l (cobounded E)

Tactic:
rw [← comap_norm_atTop', tendsto_comap_iff]; rfl

Goal state after:
Module: Mathlib.Algebra.Order.AddTorsor

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
hbdc : b • d ≤ b • c
h : d ≤ c
⊢ False

Tactic:
@lt_iff_le_not_ge

Goal state after:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c ≤ d ∧ ¬d ≤ c
hbdc : b • d ≤ b • c
h : d ≤ c
⊢ False
Module: Mathlib.Algebra.Order.AddTorsor

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
⊢ False

Tactic:
@lt_iff_le_not_ge

Goal state after:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b ∧ ¬b ≤ a
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
⊢ False
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ ‖s‖ * dist (s⁻¹ • p) x < ‖s‖ * ε

Tactic:
← dist_smul₀

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ dist (s • s⁻¹ • p) (s • x) < ‖s‖ * ε
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) ≤ ‖s‖ * ε
⊢ ‖s‖ * dist (s⁻¹ • p) x ≤ ‖s‖ * ε

Tactic:
← dist_smul₀

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) ≤ ‖s‖ * ε
⊢ dist (s • s⁻¹ • p) (s • x) ≤ ‖s‖ * ε
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: 𝕜 : Type u_4
inst✝ : NormedField 𝕜
h : BddAbove (Set.range fun k ↦ ‖k‖)
⊢ DiscreteTopology 𝕜

Tactic:
refine (NormedField.discreteTopology_or_nontriviallyNormedField _).resolve_right ?_

Goal state after:
𝕜 : Type u_4
inst✝ : NormedField 𝕜
h : BddAbove (Set.range fun k ↦ ‖k‖)
⊢ ¬Nonempty { h' // h'.toNormedField = inst✝ }
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case top
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
⊢ MeasurableSet (f ⁻¹' {⊤})

Tactic:
rw [← WithTop.none_eq_top, ← compl_range_some, preimage_compl, ← iUnion_singleton_eq_range,
      preimage_iUnion]

Goal state after:
case top
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
⊢ MeasurableSet (⋃ i, f ⁻¹' {some i})ᶜ
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 ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ (C / ε)⁻¹ * C = ε

Tactic:
by simp [hC₀.ne']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ c • 1 * m (⋃ i, s i) ≤ ∑' (i : ℕ), c • 1 * m (s i)

Tactic:
ENNReal.tsum_mul_left

Goal state after:
α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ c • 1 * m (⋃ i, s i) ≤ c • 1 * ∑' (i : ℕ), m (s i)
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ ∑ i ∈ Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)

Tactic:
sum_Ico_eq_sum_range

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ ∑ k ∈ range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.zero
⊢ Decidable (zero ≤ zero)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case zero.neg
⊢ Decidable (zero ≤ neg)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case zero.pos
⊢ Decidable (zero ≤ pos)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case neg.zero
⊢ Decidable (neg ≤ zero)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case neg.neg
⊢ Decidable (neg ≤ neg)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case neg.pos
⊢ Decidable (neg ≤ pos)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case pos.zero
⊢ Decidable (pos ≤ zero)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case pos.neg
⊢ Decidable (pos ≤ neg)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case pos.pos
⊢ Decidable (pos ≤ pos)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case inl.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : y < 0
⊢ sign (x * y) = sign x * sign y

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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

Goal state before:
pp: case inl.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : y = 0
⊢ sign (x * y) = sign x * sign y

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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

Goal state before:
pp: case inl.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : 0 < y
⊢ sign (x * y) = sign x * sign y

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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

Goal state before:
pp: case inr.inl.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : y < 0
⊢ sign (x * y) = sign x * sign y

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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

Goal state before:
pp: case inr.inl.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : y = 0
⊢ sign (x * y) = sign x * sign y

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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

Goal state before:
pp: case inr.inl.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : 0 < y
⊢ sign (x * y) = sign x * sign y

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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

Goal state before:
pp: case inr.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : y < 0
⊢ sign (x * y) = sign x * sign y

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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

Goal state before:
pp: case inr.inr.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : y = 0
⊢ sign (x * y) = sign x * sign y

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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

Goal state before:
pp: case inr.inr.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : 0 < y
⊢ sign (x * y) = sign x * sign y

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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

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

Tactic:
by rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]

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

Goal state before:
pp: a : EReal
h : 0 < a
h' : a ≠ ⊤
⊢ 0 < a⁻¹

Tactic:
by
  lift a to ℝ using ⟨h', ne_bot_of_gt h⟩
  rw [← coe_inv a]; norm_cast at *; exact inv_pos_of_pos h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun x ↦ f (M x) x) x > b
⊢ ∀ᶠ (x_1 : α) in 𝓝[s] x, (fun x1 x2 ↦ f (M x) x1 > x2) x_1 b → (fun x1 x2 ↦ (fun x ↦ f (M x) x) x1 > x2) x_1 b

Tactic:
apply eventually_nhdsWithin_of_forall

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun x ↦ f (M x) x) x > b
⊢ ∀ x_1 ∈ s, (fun x1 x2 ↦ f (M x) x1 > x2) x_1 b → (fun x1 x2 ↦ (fun x ↦ f (M x) x) x1 > x2) x_1 b
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 0) ↔ r < 1

Tactic:
refine ⟨fun h ↦ ?_, tendsto_pow_atTop_nhds_zero_of_lt_one⟩

Goal state after:
r : ℝ≥0∞
h : Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)
⊢ r < 1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
r : ℝ≥0∞
⊢ r ≤ 1 → ¬Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)

Tactic:
intro r_le_one

Goal state after:
case refine_1
r : ℝ≥0∞
r_le_one : r ≤ 1
⊢ ¬Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: β : Type u_2
s : ℕ → Set β
n : ℕ
⊢ dissipate s n = ⋂ k, ⋂ (_ : k ≤ n), s k

Tactic:
dissipate

Goal state after:
Module: Mathlib.Order.SetDissipate

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

Tactic:
obtain ⟨k, hk⟩ := hd m (n + 1)

Goal state after:
case succ
α : 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)
⊢ ∃ m, s m ⊆ dissipate s (n + 1)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
⊢ m.IsCaratheodory ∅

Tactic:
by simp [IsCaratheodory, sdiff_empty]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.refine_3
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ x ∈ {k}, s x

Tactic:
· simp only [Finset.mem_singleton, Set.iInter_iInter_eq_left]

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
simp_rw +instances [MeasurableSpace.generateFrom_singleton]

Goal state after:
α : Type u_1
s t : Set α
⊢ MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ 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:
· grind

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

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

pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ 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:
· grind

Goal state after:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
⊢ (sum fun i ↦ (m i).trim) s ≤ (sum m).trim s

Tactic:
simp only [sum_apply, trim_eq_iInf, le_iInf_iff]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
⊢ ∀ (i : Set α),
    s ⊆ i → MeasurableSet i → ∑' (i : ι), ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m i) t ≤ ∑' (i_3 : ι), (m i_3) i
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
⊢ Measurable (g ∘ f) ↔ Measurable f

Tactic:
by
  refine ⟨fun H => ?_, hg.measurable.comp⟩
  suffices Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) by
    rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
  exact hg.measurable_rangeSplitting.comp H.subtype_mk

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

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

Tactic:
union_inter_cancel_right,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ t + μ ((s ∪ t) \ t) + μ (s ∩ t) = μ s + μ t
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℕ
hs : ⇑e ⁻¹' s =ᵐ[μ] s
⊢ ⇑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s

Tactic:
replace he : (⇑e)^[k] ⁻¹' s =ᵐ[μ] s := he.preimage_iterate_ae_eq k hs

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℕ
hs : ⇑e ⁻¹' s =ᵐ[μ] s
he : (⇑e)^[k] ⁻¹' s =ᵐ[μ] s
⊢ ⇑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hf : Injective f
hf' : Measurable f
h : ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ
s : Set β
hs : MeasurableSet s
⊢ (comap f μ) (f ⁻¹' s) = μ (s ∩ range f)

Tactic:
by
  rw [comap_apply₀ _ _ hf h (hf' hs).nullMeasurableSet, image_preimage_eq_inter_range]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : μ s ≠ ∞
ε : ℝ≥0∞
h : μ t < μ s + ε
⊢ μ (t \ s) < ε

Tactic:
by
  rw [measure_sdiff hst hs hs']; rw [add_comm] at h
  exact ENNReal.sub_lt_of_lt_add (measure_mono hst) h

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : (↑s).Pairwise (AEDisjoint μ on t)
⊢ ∑ i ∈ s, μ (t i) ≤ μ univ

Tactic:
rw [← measure_biUnion_finset₀ H h]

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : (↑s).Pairwise (AEDisjoint μ on t)
⊢ μ (⋃ b ∈ s, t b) ≤ μ univ
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
union_inter_cancel_right,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict t + μ.restrict ((s ∪ t) \ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i✝ : ι
hi : μ (s i✝) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
i : ι
ω : α
hω : Monotone fun x ↦ ω ∈ s x
⊢ s i ω = t i ω

Tactic:
suffices ω ∈ s i ↔ ω ∈ t i from propext this

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i✝ : ι
hi : μ (s i✝) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
i : ι
ω : α
hω : Monotone fun x ↦ ω ∈ s x
⊢ ω ∈ s i ↔ ω ∈ t i
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
| s

Tactic:
rw [← compl_compl s]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
| sᶜᶜ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ ∅ < ∞

Tactic:
by simp only [measure_empty, zero_lt_top]

Goal state after: