mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
A : ∃ᶠ (n : β) in f, u n < a
B : ∃ᶠ (n : β) in f, b < u n
⊢ False

Tactic:
exact H a as b bs ab ⟨A, B⟩

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:

Tactic:
edist (f (a, b)) (f (x, y)) ≤ edist (f (a, b)) (f (x', b)) + edist (f (x', b)) (f (x', y)) +
        edist (f (x', y)) (f (x, y)) := edist_triangle4 _ _ _ _
    _ ≤ K * (δ + δ) + ε / 2 + K * δ := by
      gcongr
      · refine (hb b hbt).edist_le_mul_of_le has (hs' hx') ?_
        exact (edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)
      · exact hby
      · exact (hb y hy).edist_le_mul_of_le (hs' hx') hx ((edist_comm _ _).trans_le hxx'.le)
    _ = δ * ↑(3 * K) + ε / 2 := by push_cast; ring
    _ ≤ ε / 2 + ε / 2 := by gcongr
    _ = ε := ENNReal.add_halves _

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

Goal state before:
pp: a b : EReal
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
rcases lt_trichotomy a 0 with (h | h | h) <;> rcases lt_trichotomy b 0 with (h' | h' | h')
    <;> simp only [h, h', true_or, true_and, or_true, and_true]

Goal state after:
case inl.inr.inr
a b : EReal
h : a < 0
h' : 0 < b
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0

case inr.inr.inl
a b : EReal
h : 0 < a
h' : b < 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.HasSupport
f : β ↪ γ
⊢ ∀ᶠ (s : Finset γ) in (L.map f).filter, ↑s ⊆ (L.map f).support

Tactic:
obtain (h | h) := L.neBot_or_eq_bot

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.HasSupport
f : β ↪ γ
h : L.NeBot
⊢ ∀ᶠ (s : Finset γ) in (L.map f).filter, ↑s ⊆ (L.map f).support

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.HasSupport
f : β ↪ γ
h : L.filter = ⊥
⊢ ∀ᶠ (s : Finset γ) in (L.map f).filter, ↑s ⊆ (L.map f).support
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
EReal.neg_le,

Goal state after:
a b : EReal
⊢ 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case zero
x : EReal
⊢ 0 = ↑0 * x

Tactic:
Nat.cast_zero,

Goal state after:
case zero
x : EReal
⊢ 0 = 0 * x
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hf : u = fun i ↦ g.symm (g (u i))
⊢ g.symm (limsup (fun x ↦ g (u x)) f) ≤ limsup (fun i ↦ g.symm (g (u i))) f

Tactic:
refine (OrderIso.to_galoisConnection g.symm).l_limsup_le ?_ hgu_co

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hf : u = fun i ↦ g.symm (g (u i))
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g.symm (g (u x))
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
⊢ HasProd f (∏'[L] (b : β), f b) L

Tactic:
classical
  rw [tprod_def, dif_pos ha]
  split_ifs with h h'
  · convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
    · simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
      simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
      rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
      · exact Finset.prod_congr rfl (by simp_all)
      · simp
    · grind [Set.Finite.mem_toFinset, mem_mulSupport]
    · exact h.1
  · exact h'
  · exact ha.choose_spec

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
L : SummationFilter β
inst✝ : ContinuousMul α
hf : Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
hg : Tendsto (fun s ↦ ∏ b ∈ s, g b) L.filter (𝓝 b)
⊢ Tendsto (fun s ↦ ∏ b ∈ s, f b * g b) L.filter (𝓝 (a * b))

Tactic:
simp_rw [prod_mul_distrib]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
L : SummationFilter β
inst✝ : ContinuousMul α
hf : Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
hg : Tendsto (fun s ↦ ∏ b ∈ s, g b) L.filter (𝓝 b)
⊢ Tendsto (fun s ↦ (∏ x ∈ s, f x) * ∏ x ∈ s, g x) L.filter (𝓝 (a * b))
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
ht : Multipliable fun a ↦ f ↑a
t' : Finset ↑t
⊢ ∏ b ∈ t', (fun a ↦ f ↑a) b ∈ o

Tactic:
rw [← prod_subtype_map_embedding fun _ _ ↦ by rfl]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
ht : Multipliable fun a ↦ f ↑a
t' : Finset ↑t
⊢ ∏ x ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ t) t', f x ∈ o
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ (if h : Multipliable (f ∘ g) then if HasProd (f ∘ g) 1 then 1 else Exists.choose ⋯ else 1) =
    if h : Multipliable fun b ↦ f b then if HasProd (fun b ↦ f b) 1 then 1 else Exists.choose ⋯ else 1

Tactic:
Multipliable

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ (if h : ∃ a, HasProd (f ∘ g) a then if HasProd (f ∘ g) 1 then 1 else Exists.choose ⋯ else 1) =
    if h : ∃ a, HasProd (fun b ↦ f b) a then if HasProd (fun b ↦ f b) 1 then 1 else Exists.choose ⋯ else 1
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n ↦ f ↑n) g
hf₂ : HasProd (fun n ↦ f (-↑(n + 1))) (g' / f (-↑0))
⊢ HasProd (fun n ↦ f (-(↑n + 1))) (g' / f 0)

Tactic:
Nat.cast_zero,

Goal state after:
G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n ↦ f ↑n) g
hf₂ : HasProd (fun n ↦ f (-↑(n + 1))) (g' / f (-0))
⊢ HasProd (fun n ↦ f (-(↑n + 1))) (g' / f 0)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
i : ↑(mulSupport g) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x
⊢ ∏' (x : β), f x = ∏' (y : γ), g y

Tactic:
rw [← tprod_subtype_mulSupport g, ← hi.tprod_eq hf]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
i : ↑(mulSupport g) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x
⊢ ∏' (c : ↑(mulSupport g)), f (i c) = ∏' (x : ↑(mulSupport g)), g ↑x
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:
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.MetricSpace.Isometry

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
g : β → γ
K : ℝ≥0
h : Isometry g
⊢ LipschitzWith K (g ∘ f) ↔ LipschitzWith K f

Tactic:
by
  simp [LipschitzWith, h.edist_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
⊢ ∀ (a : Finset ((b : β) × γ b)), ∃ b, a ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
s

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ⊢ ContinuousOn (fun p ↦ p.1 - p.2) {p | p ≠ (∞, ∞)}

Tactic:
rw [ContinuousOn]
  rintro ⟨x, y⟩ hp
  simp only [Ne, Set.mem_ofPred_eq, Prod.mk_inj] at hp
  exact tendsto_nhdsWithin_of_tendsto_nhds (tendsto_sub (not_and_or.mp hp))

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ limsup (fun i ↦ (u i).toReal) f = (limsup u f).toReal

Tactic:
simp_rw [limsup_congr aux, aux']

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ limsup (fun a ↦ b.truncateToReal (u a)) f = b.truncateToReal (limsup u f)
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
z x y : α
⊢ dist (x ⊔ z) (y ⊔ z) ≤ ↑1 * dist x y

Tactic:
rw [NNReal.coe_one, one_mul, dist_eq_norm, dist_eq_norm]
    exact norm_sup_sub_sup_le_norm x y z

Goal state after:
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 α β
inst✝¹ : SMul αᵐᵒᵖ β
inst✝ : IsCentralScalar α β
x₁ x₂ : α
y : β
⊢ dist (MulOpposite.op x₁ • y) (MulOpposite.op x₂ • y) ≤ dist (MulOpposite.op x₁) (MulOpposite.op x₂) * dist y 0

Tactic:
by simpa only [op_smul_eq_smul] using! dist_pair_smul x₁ x₂ y

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
hr : ratio f ≠ 0
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (f x) (f y)

Tactic:
exact mod_cast
    (ENNReal.mul_le_iff_le_inv (ENNReal.coe_ne_zero.2 hr) ENNReal.coe_ne_top).1 (edist_eq f x y).ge

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a : α
n : ℕ
x✝ : 0 < n + 2
⊢ ‖a ^ (n + 2)‖₊ ≤ ‖a‖₊ ^ (n + 2)

Tactic:
simpa only [pow_succ' _ (n + 1)] using
      le_trans (nnnorm_mul_le _ _) (mul_le_mul_right (nnnorm_pow_le' a n.succ_pos) _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
a b : ℚ
⊢ ‖a * b‖ = ‖a‖ * ‖b‖

Tactic:
simp only [norm, Rat.cast_mul, abs_mul]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
h_eq : {x | p x → q x} = {x | p x}ᶜ ∪ {x | q x}
⊢ MeasurableSet {x | p x → q x}

Tactic:
h_eq

Goal state after:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
h_eq : {x | p x → q x} = {x | p x}ᶜ ∪ {x | q x}
⊢ MeasurableSet ({x | p x}ᶜ ∪ {x | q x})
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
h_eq : {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x}
⊢ MeasurableSet {x | p x ↔ q x}

Tactic:
h_eq

Goal state after:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
h_eq : {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x}
⊢ MeasurableSet ({x | p x → q x} ∩ {x | q x → p x})
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: case iUnion
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), x ∈ f n ↔ y ∈ f n
⊢ x ∈ ⋃ i, f i ↔ y ∈ ⋃ i, f i

Tactic:
simp only [mem_iUnion, hf]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
⊢ ∃ x, c < ‖x‖

Tactic:
rcases exists_ne (0 : E) with ⟨x, hx⟩
  rcases NormedField.exists_lt_norm 𝕜 (c / ‖x‖) with ⟨r, hr⟩
  use r • x
  rwa [norm_smul, ← div_lt_iff₀]
  rwa [norm_pos_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → ↑(t i) → β
hfm : ∀ (i : ι), Measurable (f i)
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
htU : ⋃ i, t i = univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (liftCover t f hf htU ⁻¹' s)

Tactic:
rw [preimage_liftCover]

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → ↑(t i) → β
hfm : ∀ (i : ι), Measurable (f i)
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
htU : ⋃ i, t i = univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (⋃ i, Subtype.val '' f i ⁻¹' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet {a | ∀ (i : ι), p i a}

Tactic:
ofPred_forall

Goal state after:
α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋂ i, {x | p i x})
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: s : SignType
n : ℕ
hn : Odd n
⊢ s ^ n = s

Tactic:
obtain ⟨k, rfl⟩ := hn
  rw [pow_add, pow_one, pow_mul, sq]
  cases s <;> simp

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

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

Tactic:
le_div_iff₀,

Goal state after:
case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ ↑(m / (n✝ + 1)) * ↑(n✝ + 1) ≤ ↑m

case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ 0 < ↑(n✝ + 1)
Module: Mathlib.Data.Nat.Cast.Order.Field

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

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

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

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬x✝ = 0

Tactic:
exact h.ne'

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

Goal state before:
pp: x : SignType
⊢ ↑↑x = ↑x

Tactic:
cases x <;> rfl

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

Goal state before:
pp: a b c : EReal
⊢ c * (a / b) = a * c / b

Tactic:
EReal.mul_div,

Goal state after:
a b c : EReal
⊢ c * a / b = a * c / b
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: x : EReal
hx : ⊥ < x
y : ℚ
hxy : ↑↑y < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x

Tactic:
exact ⟨_, trivial, Iio_subset_Iio hxy.le⟩

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

Goal state before:
pp: case pos
α : 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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v :=
        exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂

Goal state after:
case pos
α : 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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
← Nat.cast_one (R := ℤ),

Goal state after:
⊢ ∑' (m : ℕ), (2 ^ (↑m + ↑1))⁻¹ = 1
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : 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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v :=
        exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂

Goal state after:
case pos
α : 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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∀ c ∉ Set.range Encodable.encode, 0 ≤ f c

pp: case refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∀ (i : ι), (f ∘ Encodable.encode) i ≤ f (Encodable.encode i)

Tactic:
· intro i _
    exact le_of_lt (f0 _)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∀ (i : ι), (f ∘ Encodable.encode) i ≤ f (Encodable.encode i)
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩

Goal state after:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i ↦ ε' ↑i) c
hcε : c ≤ ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
f✝ : ℕ → Set α
x✝ : Pairwise (Disjoint on f✝)
hf : ∀ (i : ℕ), m.IsCaratheodory (f✝ i)
hn : Set α
⊢ m hn = m (hn ∩ ⋃ i, f✝ i) + m (hn \ ⋃ i, f✝ i)

Tactic:
by apply isCaratheodory_iUnion m hf

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
i : ι
x✝ : i ∈ {k}
⊢ s i ∈ (fun k ↦ {s k}) i

Tactic:
exact Set.mem_singleton _

Goal state after: