mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x • r) l atTop

Tactic:
by
  refine tendsto_atTop.mpr fun s => ?_
  obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
  replace hn : s ≤ (n : ℤ) • r := by simpa
  exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (zsmul_le_zsmul_left hr.le ha)

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsCobounded r ⊤ ↔ Nonempty α

Tactic:
simp +contextual [IsCobounded,
    exists_true_iff_nonempty]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, u i ≤ a
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ liminf u f ≤ a

Tactic:
by
  refine liminf_le_of_le hu_le fun b hb ↦ ?_
  obtain ⟨n, hna, hbn⟩ := (hu.and_eventually hb).exists
  exact hbn.trans hna

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F

Tactic:
· refine le_sInf fun b hb => sInf_le_of_le (mem_image_of_mem _ hb) <| sSup_le ?_
    rintro _ ⟨_, h, rfl⟩
    exact h

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
⊢ a ∈ liminf s 𝓕 ↔ ∀ᶠ (i : ι) in 𝓕, a ∈ s i

Tactic:
simpa only [liminf_eq_iSup_iInf, iSup_eq_iUnion, iInf_eq_iInter, mem_iUnion, mem_iInter]
    using ⟨fun ⟨S, hS, hS'⟩ ↦ mem_of_superset hS (by tauto), fun h ↦ ⟨{i | a ∈ s i}, h, by tauto⟩⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set α
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ LipschitzOnWith (max Kf Kg) (fun x ↦ (f x, g x)) (t₁ ∩ t₂)

Tactic:
exact (hfL.mono inter_subset_left).prodMk (hgL.mono inter_subset_right)

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

Goal state before:
pp: a b c : EReal
h : a ≤ b - c
⊢ a + c ≤ b

Tactic:
rw [← neg_neg c]

Goal state after:
a b c : EReal
h : a ≤ b - c
⊢ a + - -c ≤ b
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case neg
β : Type u_2
L : SummationFilter β
h : ¬L.filter = ⊥
⊢ L.NeBot ∨ L.filter = ⊥

Tactic:
· exact .inl ⟨⟨h⟩⟩

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
B : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i

Tactic:
hv.liminf_eq_sSup_iUnion_iInter,

Goal state after:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
B : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)
⊢ sSup (⋃ j, ⋂ i, Iic (f ↑i)) = ⨆ j, ⨅ i, f ↑i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
A : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = ∅
⊢ liminf f v = sSup ∅

Tactic:
hv.liminf_eq_sSup_iUnion_iInter,

Goal state after:
case pos
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
A : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = ∅
⊢ sSup (⋃ j, ⋂ i, Iic (f ↑i)) = sSup ∅
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (f ∘ Subtype.val) a₁
⊢ HasProd f (a₁ * (a₂ / a₁)) ↔ HasProd f a₂

Tactic:
by rw [mul_div_cancel]

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 α
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
hL : ¬L.NeBot
hfs : ¬(mulSupport fun x ↦ g (f x)).Finite
⊢ g 1 = ∏'[L] (i : β), g (f i)

Tactic:
by simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]

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 α
L : SummationFilter β
inst✝ : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ (a_1 : γ) (s : Finset γ),
    a_1 ∉ s →
      ((∀ i ∈ s, HasProd (f i) (a i) L) → HasProd (fun b ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L) →
        (∀ i ∈ insert a_1 s, HasProd (f i) (a i) L) →
          HasProd (fun b ↦ ∏ i ∈ insert a_1 s, f i b) (∏ i ∈ insert a_1 s, a i) L

Tactic:
by
    simp +contextual only [mem_insert, forall_eq_or_imp, not_false_iff,
      prod_insert, and_imp]
    exact fun x s _ IH hx h ↦ hx.mul (IH h)

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

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n ↦ f (n + k)) (g / ∏ i ∈ range k, f i) ↔ HasProd f g

Tactic:
simp [hasProd_nat_add_iff]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x ↦ b
s : Finset ι
⊢ #s • b ≤ ∑' (x : ι), b

Tactic:
by
    simpa using sum_le_hasSum s (fun a _ ↦ hb.le) hf.hasSum

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∀ b_1 ∉ {b}, f b_1 = 1

Tactic:
exact fun b' hb' ↦ hf b' (by simpa using hb')

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 α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
⊢ ∏' (c : γ), f (g c) = ∏' (b : β), f b

Tactic:
classical
  have : mulSupport f = g '' mulSupport (f ∘ g) := by
    rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf]
  rw [← Function.comp_def]
  by_cases hf_fin : (mulSupport f).Finite
  · have hfg_fin : (mulSupport (f ∘ g)).Finite := hf_fin.preimage hg.injOn
    lift g to γ ↪ β using hg
    simp_rw [tprod_eq_prod' hf_fin.coe_toFinset.ge, tprod_eq_prod' hfg_fin.coe_toFinset.ge,
      comp_apply, ← Finset.prod_map]
    refine Finset.prod_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl
    simp [this]
  · have hf_fin' : ¬ Set.Finite (mulSupport (f ∘ g)) := by
      rwa [this, Set.finite_image_iff hg.injOn] at hf_fin
    simp_rw [tprod_def, SummationFilter.support_eq_univ, Set.inter_univ,
      show (unconditional β).HasSupport by infer_instance,
      show (unconditional γ).HasSupport by infer_instance, true_and,
      if_neg hf_fin, if_neg hf_fin', Multipliable]
    simp [hg.hasProd_iff (mulSupport_subset_iff'.1 hf)]

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:
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.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
a : ℝ≥0
⊢ ↑(∑'[L] (x : α), f x * a) = ↑((∑'[L] (x : α), f x) * a)

Tactic:
by simp only [coe_tsum, NNReal.coe_mul, tsum_mul_right]

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

Goal state before:
pp: 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
x y : X
l : List X
⊢ (zipWith d (y :: l.reverse).reverse ([x].reverse ++ l)).sum = (zipWith d (x :: l) (l ++ [y])).sum

pp: 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
x y : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length

Tactic:
reverse_singleton,

Goal state after:
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
x y : X
l : List X
⊢ (zipWith d (y :: l.reverse).reverse ([x] ++ l)).sum = (zipWith d (x :: l) (l ++ [y])).sum

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
x y : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
⊢ FrechetUrysohnSpace X

Tactic:
refine ⟨fun s x hcx => ?_⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
⊢ x ∈ seqClosure s
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedGroup E
x : E
⊢ Tendsto (fun a ↦ ‖a⁻¹ * x‖) (𝓝 x) (𝓝 0)

Tactic:
by
  simpa [dist_eq_norm_inv_mul] using
    tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (x : E)) (𝓝 x) _)

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

Goal state before:
pp: case refine_3.inr
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
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
⊢ 2 * (zipWith d (l[M] :: drop (M + 1) l) (drop (M + 1) l ++ [y])).sum ≤ L.sum

Tactic:
rw [cons_getElem_drop_succ]

Goal state after:
case refine_3.inr
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
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
Module: Mathlib.Topology.MetricSpace.IsometricSMul

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

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

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)

Tactic:
simpa only [dist_mul_left, dist_mul_right, dist_comm b₂] using
    abs_dist_sub_le (a₁ * a₂) (b₁ * b₂) (b₁ * a₂)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
hgf : ↑(ratio (g.comp f)) = ↑(ratio g) * ↑(ratio f)
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
← ENNReal.coe_inj,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
hgf : ↑(ratio (g.comp f)) = ↑(ratio g) * ↑(ratio f)
⊢ ↑(ratio (g.comp f)) = ↑(ratio g * ratio f)
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
⊢ ‖↑z.natAbs‖ = ‖↑z‖

Tactic:
rcases z.natAbs_eq with hz | hz

Goal state after:
case inl
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = ↑z.natAbs
⊢ ‖↑z.natAbs‖ = ‖↑z‖

case inr
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = -↑z.natAbs
⊢ ‖↑z.natAbs‖ = ‖↑z‖
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ (⋃ n, s n) ×ˢ ⋃ n, t n = univ

Tactic:
h2s,

Goal state after:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ univ ×ˢ ⋃ n, t n = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ ⊥ ⊔ generateFrom S = generateFrom S

Tactic:
bot_sup_eq

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ generateFrom S = generateFrom S
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 α
hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, μ u = 0
⊢ μ s = 0

Tactic:
by
  choose! u hxu hu₀ using hs
  choose t ht using TopologicalSpace.countable_cover_nhdsWithin hxu
  rcases ht with ⟨ts, t_count, ht⟩
  apply measure_mono_null ht
  exact (measure_biUnion_null_iff t_count).2 fun x hx => hu₀ x (ts hx)

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

Goal state before:
pp: α : Type u_1
β : Type u_3
ι : Sort u_4
f : α → β
m : ι → OuterMeasure β
s : Set α
⊢ ((comap f) (⨆ i, m i)) s = (⨆ i, (comap f) (m i)) s

Tactic:
simp only [comap_apply, iSup_apply]

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

Goal state before:
pp: case top_zero
⊢ (⊤ * 0).abs = ⊤.abs * EReal.abs 0

Tactic:
simp only [mul_zero, abs_zero]

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

Goal state before:
pp: case mp
x y : EReal
⊢ x ≤ y →
    sign x < sign y ∨
      sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
        sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs

pp: case mpr
x y : EReal
⊢ sign x < sign y ∨
      sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
        sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs →
    x ≤ y

Tactic:
· intro h
    refine (sign.monotone h).lt_or_eq.imp_right (fun hs => ?_)
    rw [← x.sign_mul_abs, ← y.sign_mul_abs] at h
    cases hy : sign y <;> rw [hs, hy] at h ⊢
    · simp
    · left; simpa using h
    · right; right; simpa using h

Goal state after:
case mpr
x y : EReal
⊢ sign x < sign y ∨
      sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
        sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs →
    x ≤ y
Module: Mathlib.Data.EReal.Inv

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

Tactic:
← mul_div a,

Goal state after:
a b c d : EReal
⊢ a / b * (c / d) = a * (c / (b * d))
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
⊢ b * (a / b) = a'

Tactic:
← hyp,

Goal state after:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
⊢ b * (a' / b) = a'
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : DivisionSemiring 𝕜
inst✝² : CharZero 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℚ≥0 𝕜
⊢ Tendsto (fun n ↦ (↑n)⁻¹) atTop (𝓝 0)

Tactic:
convert! NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat 𝕜
  simp

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

Goal state before:
pp: case neg
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ∃ i, ¬P (t i)
⊢ ∑' (i : ℕ), m (t i) = ∞

Tactic:
obtain ⟨i, hti_notMem⟩ := ht

Goal state after:
case neg
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
i : ℕ
hti_notMem : ¬P (t i)
⊢ ∑' (i : ℕ), m (t i) = ∞
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case neg
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
⊢ (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x, (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x' y

Tactic:
by_cases hx₂ : x.2 = ⊥

Goal state after:
case pos
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : x.2 = ⊥
⊢ (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x, (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x' y

case neg
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : ¬x.2 = ⊥
⊢ (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x, (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x' y
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
simpa only [_root_.pow_zero, mul_one] using edist_le_of_edist_le_geometric_of_tendsto r C hu ha 0

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

Goal state before:
pp: m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ (1 / m) ^ a

Tactic:
div_pow,

Goal state after:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ 1 ^ a / m ^ a
Module: Mathlib.MeasureTheory.PiSystem

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

Tactic:
dissipate_succ

Goal state after:
case succ
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : (dissipate s n).Nonempty → dissipate s n ∈ C
h' : (dissipate s n ∩ s (n + 1)).Nonempty
⊢ dissipate s n ∩ s (n + 1) ∈ C
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case e_f
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
f : ℕ → Set α
hm : ∀ (i : ℕ), P (f i)
mU : m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
i : ℕ
⊢ m (f i) ⋯ = extend m (f i)

Tactic:
extend_eq

Goal state after:
case e_f
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
f : ℕ → Set α
hm : ∀ (i : ℕ), P (f i)
mU : m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
i : ℕ
⊢ m (f i) ⋯ = m (f i) ?e_f.h

case e_f.h
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
f : ℕ → Set α
hm : ∀ (i : ℕ), P (f i)
mU : m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
i : ℕ
⊢ P (f i)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case pos
α : 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 α
h : ∀ (i : ℕ), P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

pp: case neg
α : 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 α
h : ∃ i, ¬P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
· rw [extend_eq _ (PU h), congr_arg tsum _]
    · apply msU h
    funext i
    apply extend_eq _ (h i)

Goal state after:
case neg
α : 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 α
h : ∃ i, ¬P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ b, g b)
⊢ ∃ T f, t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
classical
  induction h_t with
  | @base s h_s =>
    rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩
    refine ⟨{b}, fun _ => s, ?_⟩
    simpa using h_s_in_t'
  | inter h_gen_s h_gen_t' h_nonempty h_s h_t' =>
    rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩
    rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩
    use T_s ∪ T_t', fun b : β =>
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b
      else if b ∈ T_t' then f_t' b else (∅ : Set α)
    constructor
    · ext a
      simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
      grind
    intro b h_b
    split_ifs with hbs hbt hbt
    · refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)
      exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)
    · exact h_s b hbs
    · exact h_t' b hbt
    · rw [Finset.mem_union] at h_b
      apply False.elim (h_b.elim hbs hbt)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

Tactic:
have ht_empty : t = ∅ := by
        ext1 x
        simp only [Finset.notMem_empty, iff_false]
        exact fun hx => hi (hti x hx ▸ hx)
      simp [ht_empty, iInter_univ, Set.mem_singleton univ]

Goal state after: