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

Goal state before:
pp: case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ∃ a, Tendsto (fun s ↦ ∏ x ∈ s, g (f x)) L.filter (𝓝 a)
⊢ ∃ a, Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
obtain ⟨b, hb⟩ := h

Goal state after:
case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
b : α'
hb : Tendsto (fun s ↦ ∏ x ∈ s, g (f x)) L.filter (𝓝 b)
⊢ ∃ a, Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
f : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

Tactic:
by_cases hf : Summable f L
  · rw [SemiconjBy, ← hf.tsum_mul_right a, ← hf.tsum_mul_left b, tsum_congr h]
  · simp [tsum_eq_zero_of_not_summable hf]

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

Goal state before:
pp: α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f x.1 * g x.2
⊢ Summable fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Tactic:
rw [summable_mul_prod_iff_summable_mul_sigma_antidiagonal] at h

Goal state after:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
⊢ Summable fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case e_a.refine_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
⊢ ∀ x ∈ u1 ∩ u2, f x = if x = 0 then f 0 else 1

Tactic:
intro x hx
        simp only [u1, u2, mem_inter, mem_image] at hx
        suffices x = 0 by simp only [this, if_true]
        lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
K : ℝ≥0
x y : α
⊢ edist x y ≤ ↑K * edist (f x) (f y)

Tactic:
by
  simp only [Subsingleton.elim x y, edist_self, zero_le]

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

Goal state before:
pp: 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)
⊢ {x | ‖x⁻¹ * a‖ < b 0} ∈ 𝓝 a

Tactic:
simp_rw [← dist_eq_norm_inv_mul]
      exact Metric.ball_mem_nhds _ (b_pos _)

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

Goal state before:
pp: b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)
⊢ ↑x < y.1 - y.2

Tactic:
grw [lt_tsub_iff_left, hy.2]

Goal state after:
b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)
⊢ ↑(b + 1) + ↑x < y.1
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ Continuous[instTopologicalSpaceProd, _] fun p ↦ edist p.1 p.2

Tactic:
apply continuous_of_le_add_edist 2 (by decide)
  rintro ⟨x, y⟩ ⟨x', y'⟩
  calc
    edist x y ≤ edist x x' + edist x' y' + edist y' y := edist_triangle4 _ _ _ _
    _ = edist x' y' + (edist x x' + edist y y') := by rw [edist_comm y y']; abel
    _ ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) := by
      gcongr <;> apply_rules [le_max_left, le_max_right]
    _ = edist x' y' + 2 * edist (x, y) (x', y') := by rw [← mul_two, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)|

Tactic:
sub_add_sub_cancel

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ d|
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)|

Tactic:
sub_add_sub_cancel

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ d|
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x ↦ x * a) ⁻¹' eball b r = eball (b * a⁻¹) r

Tactic:
exact preimage_smul_eball (MulOpposite.op a) b r

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
a b : α
⊢ ‖1‖ * ‖1‖ = ‖1‖ * 1

Tactic:
← norm_mul,

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
a b : α
⊢ ‖1 * 1‖ = ‖1‖ * 1
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
⊢ ∀ (a₁ a₂ : ↑(Set.range nnnorm)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
rintro ⟨-, x, rfl⟩ ⟨-, y, rfl⟩ hxy
    let ⟨z, h⟩ := exists_lt_nnnorm_lt α hxy
    exact ⟨⟨‖z‖₊, z, rfl⟩, h⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - e.1 * x.2 + (e.1 * x.2 - x.1 * x.2)‖

Tactic:
sub_add_sub_cancel

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - x.1 * x.2‖
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X : Type u_1
Y : Type u_2
F : Type u_3
inst✝³ : PseudoMetricSpace X
inst✝² : PseudoMetricSpace Y
inst✝¹ : EquivLike F X Y
inst✝ : DilationEquivClass F X Y
e : F
⊢ map (⇑e) (cobounded X) = cobounded Y

Tactic:
rw [← Dilation.comap_cobounded e, map_comap_of_surjective (EquivLike.surjective e)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ p ∈ (fun x ↦ s • x) '' ball x ε ↔ p ∈ ball (s • x) (‖s‖ * ε)

Tactic:
simp_rw [Set.mem_image, mem_ball]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ (∃ x_1, dist x_1 x < ε ∧ s • x_1 = p) ↔ dist p (s • x) < ‖s‖ * ε
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case neg
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : ↥t) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
h✝ : i ∉ t
⊢ x₁ i = x₂ i

Tactic:
simp_all

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)
h2 : {i | i ∈ l} = univ
⊢ TProd.elim' h ⁻¹' {i | i ∈ l}.pi t = Set.tprod l t

Tactic:
← mk_preimage_tprod,

Goal state after:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ TProd.elim' h ⁻¹' TProd.mk l ⁻¹' Set.tprod l t = Set.tprod l t
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
y : E
hy : y ≠ 0
⊢ dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) ≤ diam (sphere x r)

Tactic:
apply dist_le_diam_of_mem isBounded_sphere <;> simp [norm_smul, hy, abs_of_nonneg hr]

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

Goal state before:

Tactic:
a * r' ≤ 2 * r' := by gcongr
    _ ≤ _ := by 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.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ s ≤ μ (s ∩ t) + μ (s \ t)

Tactic:
by
  simpa using measure_union_le (s ∩ t) (s \ t)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
this✝ : MeasurableSet ((fun x ↦ (x, y)) ⁻¹' s ×ˢ t)
this : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
⊢ CauchySeq f

Tactic:
lift d to ℕ → ℝ≥0 using fun n ↦ dist_nonneg.trans (hf n)

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable fun i ↦ ↑(d i)
⊢ CauchySeq f
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case zero
n : ℕ
hn : Even n
hs : zero ≠ 0
⊢ zero ^ n = 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : ℕ
hn : Even n
hs : neg ≠ 0
⊢ neg ^ n = 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : ℕ
hn : Even n
hs : pos ≠ 0
⊢ pos ^ n = 1

Tactic:
simp_all

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

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
simp_all

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

Goal state before:
pp: case inl.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
simp_all

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

Goal state before:
pp: case inl.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
simp_all

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

Goal state before:
pp: case inr.inl.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
simp_all

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

Goal state before:
pp: case inr.inl.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
simp_all

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

Goal state before:
pp: case inr.inl.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
simp_all

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

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
simp_all

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

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
simp_all

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

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
simp_all

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

Goal state before:
pp: case top
⊢ ⊤.abs = 0 ↔ ⊤ = 0

Tactic:
simp only [abs_top, ENNReal.top_ne_zero, top_ne_zero]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
⊢ ∑' (a : α), ↑(f a) ≠ ∞ ↔ Summable fun a ↦ ↑(f a)

Tactic:
rw [NNReal.summable_coe]
  exact tsum_coe_ne_top_iff_summable

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

Goal state before:
pp: case inl
x y : EReal
h : x ≤ y
⊢ min (-x) (-y) = -max x y

Tactic:
simp_all

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

Goal state before:
pp: case inr
x y : EReal
h : y ≤ x
⊢ min (-x) (-y) = -max x y

Tactic:
simp_all

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

Goal state before:
pp: case inl
x y : EReal
h : x ≤ y
⊢ max (-x) (-y) = -min x y

Tactic:
simp_all

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

Goal state before:
pp: case inr
x y : EReal
h : y ≤ x
⊢ max (-x) (-y) = -min x y

Tactic:
simp_all

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

Goal state before:
pp: a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
← @mul_div_cancel a b (ne_bot_of_gt h) h' h.ne'

Goal state after:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * (a / b) ≤ c / b ↔ a * b ≤ c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a < c / b ↔ a * b < c

Tactic:
← @mul_div_cancel a b (ne_bot_of_gt h) h' h.ne'

Goal state after:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * (a / b) < c / b ↔ a * b < c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < a ↔ b < a * c

Tactic:
nth_rw 1 [← @mul_div_cancel a c (ne_bot_of_gt h) h' h.ne']
  rw [EReal.mul_div c a c, mul_comm a c]
  exact (strictMono_div_right_of_pos h h').lt_iff_lt

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

Goal state before:
pp: α : Type u_2
m : α → EReal
f : Filter α
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Iio ↑i) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x

Tactic:
simp only [true_implies, mem_Iio]

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

Goal state before:
pp: case inl
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
⊢ limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥

Tactic:
limsup_bot,

Goal state after:
case inl
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
⊢ ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
⊢ ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥

Tactic:
limsup_bot,

Goal state after:
case inl
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
⊢ ⊥ * liminf v ⊥ ≤ ⊥
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ ∀ (ε : ℝ≥0), 0 < ε → ∑' (i : ℕ), μ (s i) < ∞ → μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε

Tactic:
by
        intro ε hε (hb : (∑' i, μ (s i)) < ∞)
        rcases ENNReal.exists_pos_sum_of_countable (ENNReal.coe_pos.2 hε).ne' ℕ with ⟨ε', hε', hl⟩
        grw [← hl]
        rw [← ENNReal.tsum_add]
        choose f hf using
          show ∀ i, ∃ f : ℕ → Set α, (s i ⊆ ⋃ i, f i) ∧ (∑' i, m (f i)) < μ (s i) + ε' i by
            intro i
            have : μ (s i) < μ (s i) + ε' i :=
              ENNReal.lt_add_right (ne_top_of_le_ne_top hb.ne <| ENNReal.le_tsum _)
                (by simpa using (hε' i).ne')
            rcases iInf_lt_iff.mp this with ⟨t, ht⟩
            exists t
            contrapose! ht
            exact le_iInf ht
        refine le_trans ?_ (ENNReal.tsum_le_tsum fun i => le_of_lt (hf i).2)
        rw [← ENNReal.tsum_prod, ← Nat.pairEquiv.symm.tsum_eq]
        refine iInf_le_of_le _ (iInf_le _ ?_)
        apply iUnion_subset
        intro i
        apply Subset.trans (hf i).1
        apply iUnion_subset
        simp only [Nat.pairEquiv_symm_apply]
        rw [iUnion_unpair]
        intro j
        apply subset_iUnion₂ i

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

Goal state before:
pp: α : Type u_4
G : Type u_5
inst✝ : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
x : α
hx : x ∈ g ⁻¹' {0}ᶜ
⊢ f x / g x * g x = f x

Tactic:
simp_all

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

Goal state before:
pp: case h.refine_1
x : ℝ
⊢ ∀ y ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1, ↑x < y.1 * y.2

pp: case h.refine_2.refine_1
x : ℝ
⊢ IsOpen (Ioi (max (↑x) 0) ×ˢ Ioi 1)

pp: case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (max (↑x) 0)

pp: case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1

Tactic:
· intro p p_in_prod
    simp only [Set.mem_prod, Set.mem_Ioi, max_lt_iff] at p_in_prod
    rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩
    have := mul_le_mul_of_nonneg_left (le_of_lt p2_gt_1) (le_of_lt p1_pos)
    rw [mul_one p.1] at this
    exact lt_of_lt_of_le p1_gt_x this

Goal state after:
case h.refine_2.refine_1
x : ℝ
⊢ IsOpen (Ioi (max (↑x) 0) ×ˢ Ioi 1)

case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (max (↑x) 0)

case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ y ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2

pp: case h.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2))

pp: case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * max (x + 1) 0 / a)

pp: case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)

Tactic:
· intro p p_in_prod
    simp only [Set.mem_prod, Set.mem_Ioi] at p_in_prod
    rcases p_in_prod with ⟨p1_gt, p2_gt⟩
    have p1_pos : 0 < p.1 := by
      apply lt_of_le_of_lt _ p1_gt
      rw [EReal.coe_nonneg]
      apply mul_nonneg _ (le_of_lt (inv_pos_of_pos h))
      simp only [Nat.ofNat_pos, mul_nonneg_iff_of_pos_left, le_max_iff, le_refl, or_true]
    have a2_pos : 0 < ((a / 2 : ℝ) : EReal) := by rw [EReal.coe_pos]; linarith
    have lock := mul_le_mul_of_nonneg_right (le_of_lt p1_gt) (le_of_lt a2_pos)
    have key := mul_le_mul_of_nonneg_left (le_of_lt p2_gt) (le_of_lt p1_pos)
    replace lock := le_trans lock key
    apply lt_of_lt_of_le _ lock
    rw [← EReal.coe_mul, EReal.coe_lt_coe_iff, _root_.div_mul_div_comm, mul_comm,
      ← _root_.div_mul_div_comm, mul_div_right_comm]
    simp only [ne_eq, Ne.symm (ne_of_lt h), not_false_eq_true, _root_.div_self, OfNat.ofNat_ne_zero,
      one_mul, lt_max_iff, lt_add_iff_pos_right, zero_lt_one, true_or]

Goal state after:
case h.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2))

case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * max (x + 1) 0 / a)

case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
⊢ ∀ (s₁ s₂ : Set α), m.caratheodoryDynkin.Has s₁ → m.caratheodoryDynkin.Has s₂ → m.caratheodoryDynkin.Has (s₁ ∩ s₂)

Tactic:
intro s₁

Goal state after:
α : Type u
m : OuterMeasure α
s s₁✝ s₂ s₁ : Set α
⊢ ∀ (s₂ : Set α), m.caratheodoryDynkin.Has s₁ → m.caratheodoryDynkin.Has s₂ → m.caratheodoryDynkin.Has (s₁ ∩ s₂)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mp
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ f ⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
⊢ a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨b, h_b⟩

Tactic:
have h2 := h1 b h_b h_b_in_T

Goal state after:
case refine_1.mp
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ f ⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
h2 : a ∈ f ⟨b, h_b⟩
⊢ a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨b, h_b⟩
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
⊢ a ∈ f ⟨b, h_b⟩

Tactic:
have h2 := h1 b h_b h_b_in_T

Goal state after:
case refine_1.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
h2 : a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨b, h_b⟩
⊢ a ∈ f ⟨b, h_b⟩
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ ∀ t ∈ piiUnionInter (fun k ↦ {s k}) S, MeasurableSet t

Tactic:
rintro _ ⟨I, hI, f, hf, rfl⟩

Goal state after:
case refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ x ∈ I, f x ∈ (fun k ↦ {s k}) x
⊢ MeasurableSet (⋂ x ∈ I, f x)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
this : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ
⊢ d.Has ((t ∩ s)ᶜ \ sᶜ)

Tactic:
exact
      d.has_sdiff (d.has_compl hts) (d.has_compl h)
        (compl_subset_compl.mpr inter_subset_right)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ (𝓟 s).IsMeasurablyGenerated ↔ MeasurableSet s

Tactic:
refine ⟨?_, fun hs => ⟨fun t ht => ⟨s, mem_principal_self s, hs, ht⟩⟩⟩
  rintro ⟨hs⟩
  rcases hs (mem_principal_self s) with ⟨t, ht, htm, hts⟩
  have : t = s := hts.antisymm ht
  rwa [← this]

Goal state after: