mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
h_top : ⊥ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ y ≠ ⊥
⊢ ⊥ - y < 0 ↔ ⊥ < y

Tactic:
cases y

Goal state after:
case bot.bot
h_top : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ⊥ - ⊥ < 0 ↔ ⊥ < ⊥

case bot.coe
a✝ : ℝ
h_top : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ⊥ - ↑a✝ < 0 ↔ ⊥ < ↑a✝

case bot.top
h_top : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ⊥ - ⊤ < 0 ↔ ⊥ < ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ y ≠ ⊥
⊢ ↑a✝ - y < 0 ↔ ↑a✝ < y

Tactic:
cases y

Goal state after:
case coe.bot
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ↑a✝ - ⊥ < 0 ↔ ↑a✝ < ⊥

case coe.coe
a✝¹ a✝ : ℝ
h_top : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ↑a✝¹ - ↑a✝ < 0 ↔ ↑a✝¹ < ↑a✝

case coe.top
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ↑a✝ - ⊤ < 0 ↔ ↑a✝ < ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
y : EReal
h_top : ⊤ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ y ≠ ⊥
⊢ ⊤ - y < 0 ↔ ⊤ < y

Tactic:
cases y

Goal state after:
case top.bot
h_top : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ⊤ - ⊥ < 0 ↔ ⊤ < ⊥

case top.coe
a✝ : ℝ
h_top : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ⊤ - ↑a✝ < 0 ↔ ⊤ < ↑a✝

case top.top
h_top : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ⊤ - ⊤ < 0 ↔ ⊤ < ⊤
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
hl : l.HasBasis (fun x ↦ True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Tactic:
by
  obtain ⟨f, hf⟩ := exists_forall_mem_of_hasBasis_mem_blimsup hl hx
  exact ⟨fun i => f ⟨i, trivial⟩, fun i => hf ⟨i, trivial⟩⟩

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

Goal state before:
pp: case neg_bot
x✝ : ℝ
hx : x✝ < 0
⊢ 0 < ↑x✝ * ⊥ ↔ 0 < ↑x✝ ∧ 0 < ⊥ ∨ ↑x✝ < 0 ∧ ⊥ < 0

Tactic:
simp [hx, EReal.coe_mul_bot_of_neg hx]

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

Goal state before:
pp: x y : EReal
⊢ x * -y = -(x * y)

Tactic:
by
    rw [x.mul_comm, x.mul_comm]
    exact y.neg_mul x

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

Goal state before:
pp: case neg_bot
x✝ : ℝ
hx : x✝ < 0
⊢ ↑x✝ * ⊥ = ⊤ ↔ ↑x✝ = ⊥ ∧ ⊥ < 0 ∨ ↑x✝ < 0 ∧ ⊥ = ⊥ ∨ ↑x✝ = ⊤ ∧ 0 < ⊥ ∨ 0 < ↑x✝ ∧ ⊥ = ⊤

Tactic:
simp [hx, EReal.coe_mul_bot_of_neg hx]

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

Goal state before:
pp: case inr
y z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (y + z) = ↑x * y + ↑x * z

Tactic:
cases y

Goal state after:
case inr.bot
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + z) = ↑x * ⊥ + ↑x * z

case inr.coe
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + z) = ↑x * ↑a✝ + ↑x * z

case inr.top
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + z) = ↑x * ⊤ + ↑x * z
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
⊢ Filter.map (fun s ↦ ∏ i ∈ s, f (g i)) atTop = Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop

Tactic:
by
  have := Classical.decEq β
  apply le_antisymm <;> refine map_atTop_finsetProd_le_of_prod_eq fun s => ?_
  · refine ⟨s.preimage g hg.injOn, fun t ht => ?_⟩
    refine ⟨t.image g ∪ s, Finset.subset_union_right, ?_⟩
    rw [← Finset.prod_image hg.injOn]
    refine (prod_subset subset_union_left ?_).symm
    simp only [Finset.mem_union, Finset.mem_image]
    refine fun y hy hyt => hf y (mt ?_ hyt)
    rintro ⟨x, rfl⟩
    exact ⟨x, ht (Finset.mem_preimage.2 <| hy.resolve_left hyt), rfl⟩
  · refine ⟨s.image g, fun t ht => ?_⟩
    simp only [← prod_preimage _ _ hg.injOn _ fun x _ => hf x]
    exact ⟨_, (image_subset_iff_subset_preimage _).1 ht, rfl⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
⊢ 1 ≤ ∏'[L] (i : ι), g i

Tactic:
by
  by_cases hg : Multipliable g L
  · by_cases hL : L.NeBot
    · exact hg.hasProd.one_le h
    · simpa [tprod_bot hL] using one_le_finprod' h
  · rw [tprod_eq_one_of_not_multipliable hg]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun x ↦ ∏ i ∈ x, f i) a
⊢ Tendsto (fun s ↦ ∏ x ∈ s, (1 + f x)) (SummationFilter.unconditional ι).filter (nhds a)

Tactic:
prod_one_add

Goal state after:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun x ↦ ∏ i ∈ x, f i) a
⊢ Tendsto (fun s ↦ ∑ t ∈ s.powerset, ∏ i ∈ t, f i) (SummationFilter.unconditional ι).filter (nhds a)
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith K₁ fun a ↦ f a b
s : Set α
t : Set β
hst : Bornology.IsBounded (image2 f s t)
⊢ Bornology.IsBounded s ∨ Bornology.IsBounded t

Tactic:
by
  contrapose! hst
  obtain ⟨b, hb⟩ : t.Nonempty := nonempty_of_not_isBounded hst.2
  have : ¬IsBounded (Set.image2 f s {b}) := by
    intro h
    apply hst.1
    rw [Set.image2_singleton_right] at h
    replace h := (hf b).isBounded_preimage h
    exact h.subset (subset_preimage_image _ _)
  exact mt (IsBounded.subset · (image2_subset subset_rfl (singleton_subset_iff.mpr hb))) this

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
n : ℕ
⊢ ⋂ k, ⋂ (_ : k ≤ n), t k ⊆ t n

Tactic:
apply iInter₂_subset; rfl

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

Goal state before:
pp: case refine_3
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
k : ℕ
hl : 0 < k + 1
⊢ ‖(w (k + 1))⁻¹ * w k‖ < b (k + 1)

Tactic:
apply 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
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
refine le_mul_of_forall_lt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_

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
⊢ ∀ᶠ (a : ι) in f, (u * v) a < c
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: β : Type u_2
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ ∀ (p q : β × β), dist (p.1 * p.2) (q.1 * q.2) ≤ ↑(LipschitzMul.C β) * dist p q

Tactic:
← lipschitzWith_iff_dist_le_mul

Goal state after:
β : Type u_2
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzMul.C β) fun p ↦ p.1 * p.2
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ diam (range ⇑f) = ↑(ratio f) * diam univ

Tactic:
rw [← image_univ, diam_image]

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ l → f i_1 ∈ t i_1

Tactic:
rw [forall_eq_or_imp, and_congr_right_iff]

Goal state after:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i → (TProd.mk l f ∈ Set.tprod l t ↔ ∀ (a : ι), a ∈ l → f a ∈ t a)
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
⊢ 2 * r' ≤ diam (ball x r)

Tactic:
simpa only [← Metric.diam_sphere_eq x hr'.le]
      using diam_mono (sphere_subset_ball hr'') isBounded_ball

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.15
f : α → β
m : OuterMeasure β
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ m (f '' ⋃ i, s i) ≤ ∑' (i : ℕ), m (f '' s i)

Tactic:
by simpa only [image_iUnion] using measure_iUnion_le _

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Icc 0 1)
⊢ 1 - ↑x ≤ 1

Tactic:
by simpa using x.2.1

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Ioo 0 1)
⊢ 1 - ↑x < 1

Tactic:
by simpa using x.2.1

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

Goal state before:
pp: β : Type u_2
δ : Type u_4
X✝ : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X✝ a)
X : (a : δ) → β → X✝ a
⊢ MeasurableSpace.comap (fun b a ↦ X a b) inferInstance = ⨆ a, MeasurableSpace.comap (X a) inferInstance

Tactic:
by
  simp_rw [MeasurableSpace.pi, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp]
  rfl

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

Goal state before:
pp: case zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ↑(zero * y) = ↑zero * ↑y

Tactic:
cases y

Goal state after:
case zero.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * zero) = ↑zero * ↑zero

case zero.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * neg) = ↑zero * ↑neg

case zero.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * pos) = ↑zero * ↑pos
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ↑(neg * y) = ↑neg * ↑y

Tactic:
cases y

Goal state after:
case neg.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * zero) = ↑neg * ↑zero

case neg.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * neg) = ↑neg * ↑neg

case neg.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * pos) = ↑neg * ↑pos
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ↑(pos * y) = ↑pos * ↑y

Tactic:
cases y

Goal state after:
case pos.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * zero) = ↑pos * ↑zero

case pos.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * neg) = ↑pos * ↑neg

case pos.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * pos) = ↑pos * ↑pos
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddRightMono α
n : ℕ
⊢ 0 ≤ 1 - 1 / ↑n

Tactic:
rw [sub_nonneg, one_div]
  exact cast_inv_le_one n

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (i : ι) (x : ↑(t i)), f ↑x

Tactic:
by
  nth_rw 2 [← tsum_univ]
  rw [← ENNReal.tsum_biUnion' h, Set.biUnion_univ]

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

Goal state before:
pp: x : ℝ
⊢ ENNReal.ofReal |(-x)| = ENNReal.ofReal |x|

Tactic:
abs_neg

Goal state after:
x : ℝ
⊢ ENNReal.ofReal |x| = ENNReal.ofReal |x|
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
⊢ SemicontinuousWithinAt r univ x ↔ SemicontinuousAt r x

Tactic:
simp [SemicontinuousWithinAt, SemicontinuousAt, nhdsWithin_univ]

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

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

Tactic:
by
  simp_rw [lowerHemicontinuousOn_iff, lowerHemicontinuousWithinAt_iff_frequently]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : HasOpenCGraph f
hg : HasOpenCGraph g
this : {x | x.2 ∈ f x.1 ∩ g x.1} = {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1}
⊢ IsOpen[instTopologicalSpaceProd] ({x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1})

Tactic:
exact IsOpen.inter hf hg

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

Goal state before:
pp: ⊢ (range ENNReal.toEReal).OrdConnected

Tactic:
range_coe_ennreal

Goal state after:
⊢ (Ici 0).OrdConnected
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ IsClosed (range ENNReal.toEReal)

Tactic:
range_coe_ennreal

Goal state after:
⊢ IsClosed (Ici 0)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x) ↔ IsClosed[instTopologicalSpaceProd] {p | p.1 ∈ s ∧ f p.1 ≤ p.2}

Tactic:
lowerSemicontinuousWithinAt_iff,

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x' : α) in 𝓝[s] x, y < f x') ↔ IsClosed[instTopologicalSpaceProd] {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hl
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ∀ (x : ℕ), x ≠ 0 → (fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) x = (fun k ↦ (a + c * ↑k) / (b + d * ↑k)) x

Tactic:
intro h hx

Goal state after:
case hl
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
hx : h ≠ 0
⊢ (fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) h = (fun k ↦ (a + c * ↑k) / (b + d * ↑k)) h
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < 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 : α
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
hux : 0 ≤ u x
⊢ (u * v) x ≤ a * b

Tactic:
exact mul_le_mul x_a.le x_b.le v_0 (hux.trans x_a.le)

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

Goal state before:
pp: case refine_1
r : ℝ≥0∞
r_le_one : r ≤ 1
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 1 < r ^ b
⊢ False

Tactic:
exact lt_irrefl _ <| lt_of_lt_of_le (hn n le_rfl) <| pow_le_one₀ zero_le r_le_one

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

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ LowerSemicontinuousWithinAt f⁻¹ s a ↔ UpperSemicontinuousWithinAt f s a

Tactic:
lowerSemicontinuousWithinAt_iff,

Goal state after:
α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ (∀ y < f⁻¹ a, ∀ᶠ (x' : α) in 𝓝[s] a, y < f⁻¹ x') ↔ UpperSemicontinuousWithinAt f s a
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

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

Tactic:
rw [← isCaratheodory_compl_iff, Set.compl_inter]

Goal state after:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ᶜ ∪ s₂ᶜ)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case inl
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ (⨆ (_ : (∅ ∩ s).Nonempty), m (∅ ∩ s)) + ⨆ (_ : (∅ \ s).Nonempty), m (∅ \ s) ≤ ⨆ (_ : ∅.Nonempty), m ∅

pp: case inr
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ ⨆ (_ : t.Nonempty), m t

Tactic:
· simp [Set.not_nonempty_empty]

Goal state after:
case inr
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ ⨆ (_ : t.Nonempty), m t
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ (a • m) t = (a • m) (t ∩ s) + (a • m) (t \ s)

Tactic:
simp only [smul_apply, smul_eq_mul]
      rw [(isCaratheodory_iff m).mp h t]
      simp [mul_add]

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)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
hs : (inducedOuterMeasure m P0 m0) s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
h : (inducedOuterMeasure m P0 m0) s < (inducedOuterMeasure m P0 m0) s + ε
⊢ ∃ t, P t ∧ s ⊆ t ∧ (inducedOuterMeasure m P0 m0) t ≤ (inducedOuterMeasure m P0 m0) s + ε

Tactic:
conv at h =>
    lhs
    rw [inducedOuterMeasure_eq_iInf _ msU m_mono]

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)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
hs : (inducedOuterMeasure m P0 m0) s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
h : ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht < (inducedOuterMeasure m P0 m0) s + ε
⊢ ∃ t, P t ∧ s ⊆ t ∧ (inducedOuterMeasure m P0 m0) t ≤ (inducedOuterMeasure m P0 m0) 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 : t =ᵐ[μ] ∅
⊢ s ∩ t =ᵐ[μ] ∅

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

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) + μ (s \ t) = μ s

Tactic:
by
  refine le_antisymm ?_ (measure_le_inter_add_sdiff _ _ _)
  rcases exists_measurable_superset μ s with ⟨s', hsub, hs'm, hs'⟩
  replace hs'm : NullMeasurableSet s' μ := hs'm.nullMeasurableSet
  calc
    μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t) := by gcongr
    _ = μ (s' ∩ t ∪ s' \ t) :=
      (measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) <|
          (@disjoint_inf_sdiff _ s' t _).aedisjoint).symm
    _ = μ s' := congr_arg μ (inter_union_sdiff _ _)
    _ = μ s := hs'

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

Goal state before:
pp: β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ (comap (fun x ↦ x) μ) s = μ s

Tactic:
rw [comap_apply, image_id']

Goal state after:
case hfi
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Injective fun x ↦ x

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

case hs
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ (fun x ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s

Tactic:
preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹),

Goal state after:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ g • s ∩ s = (fun x ↦ g₂⁻¹ • x) '' (g₁ • s ∩ g₂ • s)
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ (g₂⁻¹ * g₂) • s

Tactic:
inv_mul_cancel,

Goal state after:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ 1 • s
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsSuccPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f (𝓝[<] a) l

Tactic:
rw [← map_coe_Iio_atTop a ha, tendsto_map'_iff, Function.comp_def]

Goal state after: