mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case codisjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ ⊤ ⊆ Set.range Nat.cast ⊔ Set.range Int.negSucc

Tactic:
rintro (i | j) <;> simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
⊢ HasSum (fun i ↦ f i / a₂) (a₁ / a₂) L ↔ HasSum f a₁ L

Tactic:
by
  simpa only [div_eq_mul_inv] using hasSum_mul_right_iff (inv_ne_zero h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
hs : Pairwise (Disjoint on s)
f : β → α
⊢ (⋃ d, s d).mulIndicator f = fun i ↦ ∏' (d : γ), (s d).mulIndicator f i

Tactic:
by
  ext i
  exact mulIndicator_iUnion_of_pairwise_disjoint_on_mulSupport s f (pairwise_disjoint_mono hs
    <| fun _ _ hi ↦ hi.1) i

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : L.NeBot
hf : Multipliable f L
⊢ ∏'[L] (b : β), f b ^ 0 = (∏'[L] (b : β), f b) ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
B : Bornology.IsBounded K
this : IsCompact K
⊢ closedBall x₀ r = f '' K

Tactic:
exact (hf.image_preimage _).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
b' : β
⊢ b' ≠ b → Pi.mulSingle b a b' = 1

Tactic:
hb'

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
b' : β
hb' : b' ≠ b
⊢ Pi.mulSingle b a b' = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
c : γ
f : β × γ → α
⊢ ∏' (x : ↑(s ×ˢ {c})), f ↑x = ∏' (b : ↑s), f (↑b, c)

Tactic:
by
  rw [tprod_congr_set_coe _ Set.prod_singleton, tprod_image _ (Prod.mk_left_injective c).injOn]

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

Goal state before:
pp: case refine_2
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, a - f x ≤ ε

Tactic:
filter_upwards [h ε hε] with n hn
    have hN_left := hn.1
    rw [tsub_le_iff_right] at hN_left ⊢
    rwa [add_comm]

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

Goal state before:
pp: case refine_1.zero
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
hMl : 0 ≤ l.length
hMs : IsGreatest s 0
hM_lt : 0 < L.length
hM_ltx : 0 < (x :: l).length
hM_lty : 0 < (l ++ [y]).length
⊢ d x (x :: l)[0] ≤ L.sum

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
⊢ ∀ (a : α), pkg.map pkg' f (pkg.coe a) = g (pkg.coe a)

Tactic:
intro a

Goal state after:
α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.map pkg' f (pkg.coe a) = g (pkg.coe a)
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
⊢ ∀ (a : α), (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)

Tactic:
intro a

Goal state after:
α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ s, a i ≠ ∞
⊢ Tendsto (fun b ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))

Tactic:
induction s using Finset.induction with
  | empty => simp [tendsto_const_nhds]
  | insert _ _ has IH =>
    simp only [Finset.prod_insert has]
    apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
    · right
      exact prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)
    · exact IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi =>
        h' _ (Finset.mem_insert_of_mem hi)
    · exact Or.inr (h' _ (Finset.mem_insert_self _ _))

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

Goal state before:
pp: case zero
⊢ Continuous fun a ↦ a ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
⊢ IsClosed {p | p.1 ≤ p.2}

Tactic:
have : { p : G × G | p.fst ≤ p.snd } = (fun p : G × G ↦ p.snd - p.fst) ⁻¹' { x : G | 0 ≤ x } := by
    ext1 p; simp only [sub_nonneg, Set.preimage_ofPred_eq]

Goal state after:
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.1 ≤ p.2} = (fun p ↦ p.2 - p.1) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed {p | p.1 ≤ p.2}
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: a : ℝ≥0
b : ℝ≥0∞
⊢ (↑a * b).toNNReal = a * b.toNNReal

Tactic:
simp only [ENNReal.toNNReal_mul, ENNReal.toNNReal_coe]

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

Goal state before:
pp: case inr.refine_2
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
⊢ ∏ a, ⨆ i, f a i ≤ ⨆ i, ∏ a, f a (i a)

Tactic:
rw [Classical.nonempty_pi] at h
    have H a : ∃ i : ι a, f a i = ⨆ i, f a i := exists_eq_ciSup_of_finite
    choose i hi using H
    simp only [← hi]
    exact Finite.le_ciSup_of_le i le_rfl

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
⊢ updateFinset (updateFinset x s y) t z = updateFinset x t z

Tactic:
grind [updateFinset]

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

Goal state before:
pp: ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
⊢ TProd.elim' h ⁻¹' univ.pi t = Set.tprod l t

Tactic:
have h2 : { i | i ∈ l } = univ := by
    ext i
    simp [h]
  rw [← h2, ← mk_preimage_tprod, preimage_preimage]
  simp only [TProd.mk_elim hnd h]
  dsimp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℤ
x : E
⊢ ‖n • x‖ = ‖↑n‖ * ‖x‖

Tactic:
← norm_smul,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℤ
x : E
⊢ ‖n • x‖ = ‖↑n • x‖
Module: Mathlib.Data.Real.ENatENNReal

Goal state before:
pp: n : ℕ∞
⊢ ↑n = ∞ ↔ n = ⊤

Tactic:
by simp [← toENNReal_inj]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
⊢ μ s = 0

Tactic:
choose t ht using TopologicalSpace.countable_cover_nhdsWithin hxu

Goal state after:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
t : Set α
ht : t ⊆ s ∧ t.Countable ∧ s ⊆ ⋃ x ∈ t, u x
⊢ μ s = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

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

Tactic:
change Measurable ((fun p ↦ f (p.2, p.1)) ∘ Prod.swap)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable α
f : α × β → γ
hf : ∀ (x : α), Measurable fun y ↦ f (x, y)
h'f : ∀ (x x' : α) (y : β), x' ∈ measurableAtom x → f (x', y) = f (x, y)
⊢ Measurable ((fun p ↦ f (p.2, p.1)) ∘ Prod.swap)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case inr
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

Tactic:
· simp [measurableSet_pi_of_nonempty hs, h, ← not_nonempty_iff_eq_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ SemicontinuousOn r s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, ¬r x' y) → ¬r x y

Tactic:
simp only [← not_eventually, not_imp_not, SemicontinuousWithinAt, SemicontinuousOn]

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

Goal state before:
pp: a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ -(c * b) ≤ -(c * a)

Tactic:
← neg_mul c b,

Goal state after:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ -c * b ≤ -(c * a)
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
⊢ HasOpenCGraph fun x ↦ f x ∩ g x

Tactic:
have : {x : α × β | x.2 ∈ f x.1 ∩ g x.1} =
      {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1} := by ext; simp

Goal state after:
α : 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}
⊢ HasOpenCGraph fun x ↦ f x ∩ g x
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: ⊢ StrictAntiOn (fun x ↦ x⁻¹) (Ioi 0)

Tactic:
intro a

Goal state after:
a : EReal
⊢ a ∈ Ioi 0 → ∀ ⦃b : EReal⦄, b ∈ Ioi 0 → a < b → (fun x ↦ x⁻¹) b < (fun x ↦ x⁻¹) a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ StrictMono fun a ↦ a / b

Tactic:
intro a

Goal state after:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a : EReal
⊢ ∀ ⦃b_1 : EReal⦄, a < b_1 → (fun a ↦ a / b) a < (fun a ↦ a / b) b_1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b ≤ 0
⊢ Antitone fun a ↦ a / b

Tactic:
intro a

Goal state after:
b : EReal
h : b ≤ 0
a : EReal
⊢ ∀ ⦃b_1 : EReal⦄, a ≤ b_1 → (fun a ↦ a / b) b_1 ≤ (fun a ↦ a / b) a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ 0 ≤ -b

Tactic:
apply EReal.le_neg_of_le_neg

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ b ≤ -0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b < 0
h' : b ≠ ⊥
⊢ StrictAnti fun a ↦ a / b

Tactic:
intro a

Goal state after:
b : EReal
h : b < 0
h' : b ≠ ⊥
a : EReal
⊢ ∀ ⦃b_1 : EReal⦄, a < b_1 → (fun a ↦ a / b) b_1 < (fun a ↦ a / b) a
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : ↑univ), c = ↑(ENat.card α) * c

Tactic:
simpa [encard_univ] using tsum_set_const univ c

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuous f ↔ ∀ (x : α), f x ≤ liminf f (𝓝 x)

Tactic:
by
  simp only [← lowerSemicontinuousAt_iff_le_liminf, lowerSemicontinuous_iff]

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ ⊤ ≤ ⊤ + liminf v f

Tactic:
top_add_of_ne_bot h'

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ ⊤ ≤ ⊤
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ⨆ i, ∑ a ∈ Finset.range i, r ^ a = ∞

Tactic:
iSup_eq_top

Goal state after:
case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∀ b < ∞, ∃ i, b < ∑ a ∈ Finset.range i, r ^ a
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }

Tactic:
let f n := ε / 2 / 2 ^ n
  have hf : HasSum f ε := hasSum_geometric_two' _
  have f0 : ∀ n, 0 < f n := fun n ↦ div_pos (half_pos hε) (pow_pos zero_lt_two _)
  refine ⟨f ∘ Encodable.encode, fun i ↦ f0 _, ?_⟩
  rcases hf.summable.comp_injective (@Encodable.encode_injective ι _) with ⟨c, hg⟩
  refine ⟨c, hg, hasSum_le_inj _ (@Encodable.encode_injective ι _) ?_ ?_ hg hf⟩
  · intro i _
    exact le_of_lt (f0 _)
  · intro n
    exact le_rfl

Goal state after:
Module: Mathlib.Order.SetDissipate

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s = univ
⊢ s ∩ t ∈ insert univ S

Tactic:
rcases ht with ht | ht <;> simp [hs, ht]

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

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

Tactic:
simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₁

Goal state after:
case coe.bot
a✝ : ℝ
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
h₁ : ¬a✝ = 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊥)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case zero
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
h' : (dissipate s 0).Nonempty
⊢ dissipate s 0 ∈ C

Tactic:
| zero =>

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∀ (u : γ), u ≤ f x
⊢ ∀ (x : α), f x ∈ v

Tactic:
intro a

Goal state after:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∀ (u : γ), u ≤ f x
a : α
⊢ f a ∈ v
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
by_cases! Hu : ∃ u, f x < u
    · rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
      filter_upwards [h₂ u fxu] with a lfa
      apply hu
      exact ⟨Hl (f a), lfa⟩
    · apply Filter.Eventually.of_forall
      intro a
      have : f a = f x := le_antisymm (Hu _) (Hl _)
      rw [this]
      exact mem_of_mem_nhds hv

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
⊢ s n ∩ ⋃ k, ⋃ (_ : k < n), s k ⊆ ∅

Tactic:
intro a

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
a : α
⊢ a ∈ s n ∩ ⋃ k, ⋃ (_ : k < n), s k → a ∈ ∅
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
by
  by_cases! h : ∀ i, P (s i)
  · rw [extend_eq _ (PU h), congr_arg tsum _]
    · apply msU h
    funext i
    apply extend_eq _ (h i)
  · obtain ⟨i, hi⟩ := h
    exact le_trans (le_iInf fun h => hi.elim h) (ENNReal.le_tsum i)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : f.IsMeasurablyGenerated
inst✝ : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
⊢ ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg

Tactic:
rcases IsMeasurablyGenerated.exists_measurable_subset hsf with ⟨s'f, hs'f, hmf, hs'sf⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : f.IsMeasurablyGenerated
inst✝ : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
⊢ ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet (⋃ i, s i)

Tactic:
rcases exists_seq_forall_of_frequently hs with ⟨x, hx, hxm⟩
  rw [← hsm.iUnion_comp_tendsto_atTop hx]
  exact .iUnion hxm

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

Goal state before:
pp: case refine_1
α✝ : 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.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable fun a ↦ (Equiv.sumProdDistrib α β γ) ↑a

Tactic:
refine (Set.prod (range Sum.inl) univ).symm.measurable_comp_iff.1 ?_

Goal state after:
case refine_1
α✝ : 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.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable ((fun a ↦ (Equiv.sumProdDistrib α β γ) ↑a) ∘ ⇑(Set.prod (range Sum.inl) univ).symm)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_1.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
⊢ MeasurableSet (F^[0] univ)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable β
μ : Measure (α × β)
x : α
⊢ μ (Prod.fst ⁻¹' {x}) = ∑' (y : β), μ {(x, y)}

Tactic:
← measure_iUnion (by simp [Pairwise]) fun _ ↦ .singleton _,

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable β
μ : Measure (α × β)
x : α
⊢ μ (Prod.fst ⁻¹' {x}) = μ (⋃ i, {(x, i)})
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: case zero
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[0] ⁻¹' s =ᵐ[μ] s

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measure.comap (⇑e.symm) μ = Measure.map (⇑e) μ

Tactic:
ext s hs
  rw [e.map_apply, Measure.comap_apply _ e.symm.injective _ _ hs, image_symm]
  exact fun t ht ↦ e.symm.measurableSet_image.mpr ht

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case pos.mpr.refine_1
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
⊢ ∀ i < b, ∃ i', True ∧ Ici i' ⊆ Subtype.val ⁻¹' Ioo i b

Tactic:
intro a

Goal state after:
case pos.mpr.refine_1
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
a : X
⊢ a < b → ∃ i', True ∧ Ici i' ⊆ Subtype.val ⁻¹' Ioo a b