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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a
i : ι
i_s : i ∈ s
a : α
⊢ F i a ≤ (fun a ↦ s.sup' hs fun i ↦ F i a) a

Tactic:
simp only [le_sup'_iff]

Goal state after:
case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a
i : ι
i_s : i ∈ s
a : α
⊢ ∃ b ∈ s, F i a ≤ F b a
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ HasProd (⇑g ∘ f) (g a) L ↔ HasProd f a L

Tactic:
HasProd,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ Tendsto (fun s ↦ ∏ b ∈ s, (⇑g ∘ f) b) L.filter (𝓝 (g a)) ↔ Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case mp.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hf : Multipliable f L
⊢ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g

Tactic:
by_cases hL : L.NeBot
      · exact ⟨_, hf.map_tprod g hg.continuous⟩
      · by_cases hfs : (mulSupport fun x ↦ g (f x)).Finite
        · simp [tprod_bot hL, finprod_eq_prod _ hfs, ← _root_.map_prod]
        · exact ⟨1, by simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : CommGroup α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ (∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : β), f x

Tactic:
rw [← hf.tprod_subtype_mul_tprod_subtype_compl s]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : CommGroup α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ (∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = (∏' (x : ↑↑s), f ↑x) * ∏' (x : ↑(↑s)ᶜ), f ↑x
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f : α → K
L : SummationFilter α
a : K
inst✝ : ContinuousInv₀ K
h : HasProd f a L
ha : a ≠ 0
⊢ HasProd (fun x ↦ (f x)⁻¹) a⁻¹ L

Tactic:
HasProd,

Goal state after:
α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f : α → K
L : SummationFilter α
a : K
inst✝ : ContinuousInv₀ K
h : HasProd f a L
ha : a ≠ 0
⊢ Tendsto (fun s ↦ ∏ x ∈ s, (f x)⁻¹) L.filter (𝓝 a⁻¹)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
ha : ¬a = 0
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a

Tactic:
· exact ((Homeomorph.mulRight₀ a ha).isClosedEmbedding.map_tsum f
      (g := AddMonoidHom.mulRight a)).symm

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

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
⊢ Multipliable f ↔ (Multipliable fun n ↦ f ↑n) ∧ Multipliable fun n ↦ f (-↑n)

Tactic:
by
  refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg hf₁ hf₂⟩ <;>
  apply p.comp_injective
  exacts [Nat.cast_injective, neg_injective.comp Nat.cast_injective]

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
⊢ HasProd (fun x ↦ 1 + f x) a

Tactic:
HasProd,

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 ↦ ∏ x ∈ s, (1 + f x)) (SummationFilter.unconditional ι).filter (nhds a)
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < ε / ↑K}
⊢ edist (f x.1) (f x.2) * ↑K < ε

Tactic:
exact ENNReal.mul_lt_of_lt_div hx

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : x ∈ closure[inst✝²] s
⊢ x ∈ seqClosure s

Tactic:
hf.closure_eq_preimage_closure_image,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : x ∈ f ⁻¹' closure[inst✝¹] (f '' s)
⊢ x ∈ seqClosure s
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case h.inl
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
⊢ d x y ≤ 2 * L.sum

Tactic:
simp only [hd₀, zero_le]

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

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

Tactic:
· exact Or.inr (h' _ (Finset.mem_insert_self _ _))

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

Goal state before:
pp: α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ Tendsto (fun b ↦ a / m b) f (𝓝 (a / b))

Tactic:
apply Tendsto.const_mul (tendsto_inv_iff.2 hm)

Goal state after:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ b⁻¹ ≠ 0 ∨ a ≠ ∞
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed[Pi.topologicalSpace] {f | LipschitzOnWith K f s}

Tactic:
simp only [LipschitzOnWith, ofPred_forall]

Goal state after:
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed[Pi.topologicalSpace] (⋂ i ∈ s, ⋂ i_1 ∈ s, {x | edist (x i) (x i_1) ≤ ↑K * edist i i_1})
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
x y : G
⊢ edist x⁻¹⁻¹ y⁻¹ = edist x y⁻¹

Tactic:
inv_inv

Goal state after:
G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
x y : G
⊢ edist x y⁻¹ = edist x y⁻¹
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a (b * a) = dist 1 b

Tactic:
← dist_mul_left a 1 b,

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a (b * a) = dist (a * 1) (a * b)
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
⊢ s.sup f / a = s.sup fun i ↦ f i / a

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Goal state after:
case inl
ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
f : ι → G₀
⊢ ∅.sup f / a = ∅.sup fun i ↦ f i / a

case inr
ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
⊢ s.sup f / a = s.sup fun i ↦ f i / a
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ edist (f x) (f y) = ↑⋯.choose * edist x y

Tactic:
exact (DilationClass.edist_eq' f).choose_spec.2 x y

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ A * ‖f i‖ * ‖g i‖ ≤ A * δ * C

Tactic:
gcongr; exact hg

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 : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ f y ∈ eball (f x) (↑(ratio f) * r)

Tactic:
Metric.mem_eball,

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ edist (f y) (f x) < ↑(ratio f) * r
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖(AddMonoidHom.mulRight x) y‖ ≤ ‖x‖ * ‖y‖

Tactic:
rw [mul_comm]
  exact norm_mul_le y x

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

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

Tactic:
by_cases his : i ∈ s

Goal state after:
case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

case neg
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i
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 ↔ f i ∈ t i ∧ ∀ (a : ι), a ∈ l → f a ∈ t a

Tactic:
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.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
⊢ (cobounded α)⁻¹⁻¹ = cobounded α

Tactic:
inv_inv

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
⊢ cobounded α = cobounded α
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
m : ℤ
hm : m < 0
⊢ Tendsto (fun x ↦ x ^ m) (𝓝[≠] 0) (cobounded α)

Tactic:
obtain ⟨m, rfl⟩ := neg_surjective m

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℤ
hm : -m < 0
⊢ Tendsto (fun x ↦ x ^ (-m)) (𝓝[≠] 0) (cobounded α)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₂.h₁
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ k ≠ 0 → MeasurableSet {x | p x k}

Tactic:
intros

Goal state after:
case h₂.h₁
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : k ≠ 0
⊢ MeasurableSet {x | p x k}
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ ∀ (b : ℕ), MeasurableSet (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a | p a b}ᶜ)

Tactic:
intros

Goal state after:
case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : ℕ
⊢ MeasurableSet (⋂ (_ : k < b✝), ⋂ (_ : b✝ ≤ N), {a | p a b✝}ᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : ℕ
⊢ k < b✝ → MeasurableSet (⋂ (_ : b✝ ≤ N), {a | p a b✝}ᶜ)

Tactic:
intros

Goal state after:
case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝¹ : ℕ
b✝ : k < b✝¹
⊢ MeasurableSet (⋂ (_ : b✝¹ ≤ N), {a | p a b✝¹}ᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝¹ : ℕ
b✝ : k < b✝¹
⊢ b✝¹ ≤ N → MeasurableSet {a | p a b✝¹}ᶜ

Tactic:
intros

Goal state after:
case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝² : ℕ
b✝¹ : k < b✝²
b✝ : b✝² ≤ N
⊢ MeasurableSet {a | p a b✝²}ᶜ
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 α
⊢ c • m ∅ = 0

Tactic:
simp only [measure_empty]; rw [← smul_one_mul c]; simp

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

Goal state before:
pp: case map_const
α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ ∀ {α β : Type u_3}, Functor.mapConst = Functor.map ∘ const β

Tactic:
intros

Goal state after:
case map_const
α : Type u_1
β : Type u_2
m : OuterMeasure α
α✝ β✝ : Type u_3
⊢ Functor.mapConst = Functor.map ∘ const β✝
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: case id_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ ∀ {α : Type u_3} (x : OuterMeasure α), id <$> x = x

Tactic:
intros

Goal state after:
case id_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
α✝ : Type u_3
x✝ : OuterMeasure α✝
⊢ id <$> x✝ = x✝
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: case comp_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ ∀ {α β γ : Type u_3} (g : α → β) (h : β → γ) (x : OuterMeasure α), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
intros

Goal state after:
case comp_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
α✝ β✝ γ✝ : Type u_3
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : OuterMeasure α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
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 ((fun p ↦ f (p.2, p.1)) ∘ Prod.swap)

Tactic:
exact (measurable_from_prod_countable_left' hf h'f).comp measurable_swap

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ m (u ∩ s) ≤ m' (u ∩ t)

Tactic:
exact (hm _).trans (m'.mono <| inter_subset_inter_right _ h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⊤ (f ⁻¹' s) = ((restrict (range f)) ⊤) s

Tactic:
restrict_apply,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⊤ (f ⁻¹' s) = ⊤ (s ∩ range f)
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
h : Continuous[inst✝², inst✝¹] ⇑(algebraMap R A)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ (algebraMap R A) p.1 * p.2

Tactic:
exact (h.comp continuous_fst).mul continuous_snd

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

Goal state before:
pp: f : ℕ → ℝ≥0
⊢ Tendsto (fun i ↦ ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)

Tactic:
rw [← tendsto_coe]

Goal state after:
f : ℕ → ℝ≥0
⊢ Tendsto (fun a ↦ ↑(∑' (k : ℕ), f (k + a))) atTop (𝓝 ↑0)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : EReal
⊢ ⊥ < x⁻¹

Tactic:
cases x with
  | bot => exact inv_bot ▸ bot_lt_zero
  | top => exact EReal.inv_top ▸ bot_lt_zero
  | coe x => exact (coe_inv x).symm ▸ bot_lt_coe (x⁻¹)

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
⊢ limsup (u + v) f ≤ limsup u f + limsup v f

Tactic:
by
  refine le_add_of_forall_gt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x
  exact (add_lt_add a_x b_x).trans c_ab

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

Goal state before:
pp: α : 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
⊢ v x < b → 0 x ≤ v x → (u * v) x < c

Tactic:
x_b

Goal state after:
α : 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
⊢ 0 x ≤ v x → (u * v) x < c
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0
h : Tendsto (HPow.hPow r) atTop (𝓝 0)
⊢ r < 1

Tactic:
exact NNReal.tendsto_pow_atTop_nhds_zero_iff.mp h

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

Goal state before:
pp: ⊢ 2⁻¹ * 2⁻¹⁻¹ = 1

Tactic:
inv_inv

Goal state after:
⊢ 2⁻¹ * 2 = 1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ C * 2⁻¹ ^ n * 2 = C * 2⁻¹ ^ n * 2⁻¹⁻¹

Tactic:
inv_inv

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ C * 2⁻¹ ^ n * 2 = C * 2⁻¹ ^ n * 2
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
⊢ (map f) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun s ↦ m (f ⁻¹' s)) m_empty

Tactic:
refine (map_ofFunction_le _).antisymm fun s => ?_
  simp only [ofFunction_apply, map_apply, le_iInf_iff]
  intro t ht
  refine iInf_le_of_le (fun n => (range f)ᶜ ∪ f '' t n) (iInf_le_of_le ?_ ?_)
  · rw [← union_iUnion, ← inter_subset, ← image_preimage_eq_inter_range, ← image_iUnion]
    exact image_mono ht
  · refine ENNReal.tsum_le_tsum fun n => le_of_eq ?_
    simp [hf.preimage_image]

Goal state after:
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:
by
  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.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
⊢ 0 < (fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1) i

Tactic:
conv_rhs => simp

Goal state after:
case refine_1
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
⊢ 0 < if h : i ∈ s then f ⟨i, h⟩ else 1
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_1
α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ n, f '' t n ∪ (range f)ᶜ

Tactic:
← iUnion_union,

Goal state after:
case refine_1
α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ (⋃ i, f '' t i) ∪ (range f)ᶜ
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set (OuterMeasure α)
s : Set α
hm : m.Nonempty
⊢ (restrict s) (sInf m) = sInf (⇑(restrict s) '' m)

Tactic:
by
  simp only [sInf_eq_iInf, restrict_biInf, hm, iInf_image]

Goal state after: