mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : α
⊢ edist ((AddMonoidHom.inl α β) x) ((AddMonoidHom.inl α β) y) = edist x y

Tactic:
rw [Prod.edist_eq]

Goal state after:
α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : α
⊢ max (edist ((AddMonoidHom.inl α β) x).1 ((AddMonoidHom.inl α β) y).1)
      (edist ((AddMonoidHom.inl α β) x).2 ((AddMonoidHom.inl α β) y).2) =
    edist x y
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : β
⊢ edist ((AddMonoidHom.inr α β) x) ((AddMonoidHom.inr α β) y) = edist x y

Tactic:
rw [Prod.edist_eq]

Goal state after:
α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : β
⊢ max (edist ((AddMonoidHom.inr α β) x).1 ((AddMonoidHom.inr α β) y).1)
      (edist ((AddMonoidHom.inr α β) x).2 ((AddMonoidHom.inr α β) y).2) =
    edist x y
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 z : X
lxy lyz : List X
⊢ (zipWith d (x :: lxy ++ y :: lyz) (lxy ++ y :: lyz ++ [z])).sum =
    (zipWith d (x :: lxy) (lxy ++ [y])).sum + (zipWith d (y :: lyz) (lyz ++ [z])).sum

Tactic:
by
        rw [← sum_append, ← zipWith_append, cons_append, ← @singleton_append _ y, append_assoc,
          append_assoc, append_assoc]
        rw [length_cons, length_append, length_singleton]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case neg
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
hx : x ∉ s
⊢ x ∈ seqClosure s

Tactic:
obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s := by
      simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop,
        ← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not, not_false_eq_true,
        not_true_eq_false] using h (· ∉ s) x
    rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩
    exact ⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩

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

Goal state before:
pp: case inr.refine_1.refine_2
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ x + min ε ↑δ < (a, b).2

Tactic:
min_le_right

Goal state after:
case inr.refine_1.refine_2
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ x + ↑δ < (a, b).2
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_2
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
· obtain ⟨n, hn⟩ := h ε hε
    exact ⟨n, fun m hm ↦ (hf hm).trans hn⟩

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

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

Tactic:
pkg.compare_coe pkg'

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

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

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

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

Goal state before:
pp: case refine_3
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)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
k : ℕ
hl : 0 < k + 1
⊢ ‖(v (k + 1))⁻¹‖ < b (k + 1)

Tactic:
simp only [Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte, add_tsub_cancel_right,
      mul_inv_rev, inv_inv, v]

Goal state after:
case refine_3
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)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
k : ℕ
hl : 0 < k + 1
⊢ ‖(w (k + 1))⁻¹ * w k‖ < b (k + 1)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case mp.refine_2
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∀ᶠ (x : β) in atTop, ediam (s '' Ici x) ≤ ε

Tactic:
rcases hs ε ε0 with ⟨N, hN⟩

Goal state after:
case mp.refine_2
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
⊢ ∀ᶠ (x : β) in atTop, ediam (s '' Ici x) ≤ ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞
h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0
a : ℝ≥0∞
a_u : a > limsup u f
b : ℝ≥0∞
b_v : b > limsup v f
c : ℝ≥0∞
c_ab : c > a * b
x : ι
a_x : u x < a
b_x : v x < b
⊢ (u * v) x < c

Tactic:
exact (mul_lt_mul a_x b_x).trans c_ab

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ↑(liminf u f) = liminf (fun i ↦ ↑(u i)) f

Tactic:
refine eq_of_forall_nnreal_le_iff fun r ↦ ?_
  rw [coe_le_coe, le_liminf_iff, le_liminf_iff]
  simp [forall_ennreal]

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

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
⊢ ↑Kf⁻¹ * dist x y - ↑Kg * dist x y ≤ dist (f x * g x) (f y * g y)

Tactic:
calc
    ↑Kf⁻¹ * dist x y - Kg * dist x y ≤ dist (f x) (f y) - dist (g x) (g y) :=
      sub_le_sub (hf.mul_le_dist x y) (hg.dist_le_mul x y)
    _ ≤ _ := le_trans (le_abs_self _) (abs_dist_sub_le_dist_mul_mul _ _ _ _)

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

Goal state before:

Tactic:
‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
              rw [mul_sub, sub_mul, sub_add_sub_cancel]
            _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
              norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)

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 : β
h : dist p (s • x) < ‖s‖ * ε
⊢ s • s⁻¹ • p = p

Tactic:
by simp [smul_smul, hs]

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 : β
⊢ (∃ x_1 ∈ closedBall x ε, s • x_1 = p) ↔ p ∈ closedBall (s • x) (‖s‖ * ε)

Tactic:
mem_closedBall

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: ι : 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
⊢ updateFinset (updateFinset x s y) t z = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z))

Tactic:
set e := Equiv.Finset.union s t hst

Goal state after:
ι : 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
⊢ updateFinset (updateFinset x s y) t z = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z))
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 : β
h : dist p (s • x) ≤ ‖s‖ * ε
⊢ s • s⁻¹ • p = p

Tactic:
by simp [smul_smul, hs]

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

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
⊢ (cobounded α)⁻¹ = 𝓝[≠] 0

Tactic:
← comap_norm_atTop,

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
⊢ (comap norm atTop)⁻¹ = 𝓝[≠] 0
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: 𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ x = 0 ∧ n < 0 → ¬ContinuousAt (fun x ↦ x ^ n) x

Tactic:
rintro ⟨rfl, hm⟩ hc

Goal state after:
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
hm : n < 0
hc : ContinuousAt (fun x ↦ x ^ n) 0
⊢ False
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case neg._
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (Infinite.natEmbedding 𝕜) k - (Infinite.natEmbedding 𝕜) n ≠ 0

Tactic:
rwa [sub_ne_zero, (Embedding.injective _).ne_iff]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ 0 < ↑n + 1

Tactic:
exact Nat.cast_add_one_pos _

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

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

Tactic:
exact Nat.cast_add_one_pos _

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

Goal state before:
pp: case neg_left
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ sign (-x✝ * y✝) = sign (-x✝) * sign y✝

Tactic:
rw [neg_mul, sign_neg, sign_neg, h, neg_mul]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
hf : Summable f
i : α
⊢ ∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x

Tactic:
refine (NNReal.summable_of_le (fun i' => ?_) hf).tsum_eq_add_tsum_ite' i

Goal state after:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ update f i 0 i' ≤ f i'
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case bot
⊢ ⊥ < ⊥⁻¹

Tactic:
exact inv_bot ▸ bot_lt_zero

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

Goal state before:
pp: β : Type u_2
f g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
hgf : ∀ (b : β), g b ≤ f b
hf : Summable f
⊢ Summable g

Tactic:
by
  lift f to β → ℝ≥0 using fun b => (hg b).trans (hgf b)
  lift g to β → ℝ≥0 using hg
  rw [NNReal.summable_coe] at hf ⊢
  exact NNReal.summable_of_le (fun b => NNReal.coe_le_coe.1 (hgf b)) hf

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ m ∈ {x | (fun c ↦ edist (f n) (f c) ≤ ∑' (m : ℕ), d (n + m)) x}

Tactic:
change edist _ _ ≤ _

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ edist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)
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
x_b : v x < b
v_0 : 0 x ≤ v x
⊢ (u * v) x ≤ a * b

Tactic:
rcases lt_or_ge (u x) 0 with hux | hux

Goal state after:
case inl
α : 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
v_0 : 0 x ≤ v x
hux : u x < 0
⊢ (u * v) x ≤ a * b

case inr
α : 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
v_0 : 0 x ≤ v x
hux : 0 ≤ u x
⊢ (u * v) x ≤ a * b
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : ∃ a, ∀ (b : ℕ), a ≤ b → 1 < r ^ b
⊢ False

Tactic:
obtain ⟨n, hn⟩ := h_tends

Goal state after:
case refine_1
r : ℝ≥0∞
r_le_one : r ≤ 1
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 1 < r ^ b
⊢ False
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Sort u_2
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ (⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)

Tactic:
rw [iInf, sInf_apply' hs]

Goal state after:
α : Type u_1
ι : Sort u_2
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range fun i ↦ m i, μ (t n) =
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)
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:
classical
  rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
  refine ⟨ε', hpos, fun t ht ↦ ?_⟩
  rw [← sum_subtype_of_mem _ ht]
  refine (sum_le_hasSum _ ?_ hε'c).trans hcε
  exact fun _ _ ↦ (hpos _).le

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : (fun x' ↦ ⨆ i, f i x') x > y
i : ι
hi : y < f i x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun x' ↦ ⨆ i, f i x') x1 > x2) x' y

Tactic:
filter_upwards [h i y hi, bdd] with y hy hy' using hy.trans_le (le_ciSup hy' i)

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : m.IsCaratheodory s₁
t : Set α
⊢ m (t ∩ (s₁ ∪ s₂) ∩ s₁) + m ((t ∩ (s₁ ∪ s₂)) \ s₁) = m (t ∩ s₁) + m (t ∩ s₂)

Tactic:
Set.inter_assoc,

Goal state after:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : m.IsCaratheodory s₁
t : Set α
⊢ m (t ∩ ((s₁ ∪ s₂) ∩ s₁)) + m ((t ∩ (s₁ ∪ s₂)) \ s₁) = m (t ∩ s₁) + m (t ∩ s₂)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
⊢ (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ ⨆ (_ : t.Nonempty), m t

Tactic:
rcases t.eq_empty_or_nonempty with rfl | h

Goal state after:
case inl
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ (⨆ (_ : (∅ ∩ s).Nonempty), m (∅ ∩ s)) + ⨆ (_ : (∅ \ s).Nonempty), m (∅ \ s) ≤ ⨆ (_ : ∅.Nonempty), m ∅

case inr
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ ⨆ (_ : t.Nonempty), m t
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
⊢ IsPiSystem (piiUnionInter π S)

Tactic:
rintro t1 ⟨p1, hp1S, f1, hf1m, ht1_eq⟩ t2 ⟨p2, hp2S, f2, hf2m, ht2_eq⟩ h_nonempty

Goal state after:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
⊢ t1 ∩ t2 ∈ piiUnionInter π S
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 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) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (inducedOuterMeasure m P0 m0) s = ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht

Tactic:
by
  apply le_antisymm
  · simp only [le_iInf_iff]
    intro t ht hs
    grw [hs]
    exact le_of_eq (inducedOuterMeasure_eq' _ msU m_mono _)
  · refine le_iInf ?_
    intro f
    refine le_iInf ?_
    intro hf
    refine le_trans ?_ (extend_iUnion_le_tsum_nat' _ msU _)
    refine le_iInf ?_
    intro h2f
    exact iInf_le_of_le _ (iInf_le_of_le h2f <| iInf_le _ hf)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s

Tactic:
by
  simpa only [← measure_eq_trim] using! μ.toOuterMeasure.exists_measurable_superset_eq_trim s

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n ↦ f n x

Tactic:
by
  have h_eq : (fun n => f n x) = fun n => aeSeq hf p n x :=
    funext fun n => (aeSeq_eq_fun_of_mem_aeSeqSet hf hx n).symm
  rw [h_eq]
  exact prop_of_mem_aeSeqSet hf hx

Goal state after:
Module: Mathlib.Order.Interval.Set.Monotone

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
⊢ m ≤ φ m

Tactic:
by_cases hk : IsMax k

Goal state after:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : IsMax k
⊢ m ≤ φ m

case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : ¬IsMax k
⊢ m ≤ φ m
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
⊢ α ≃ᵐ β

Tactic:
by
  let F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
  -- We follow the proof of the usual SB theorem in mathlib,
  -- the crux of which is finding a fixed point of this F.
  -- However, we must find this fixed point manually instead of invoking Knaster-Tarski
  -- in order to make sure it is measurable.
  suffices Σ' A : Set α, MeasurableSet A ∧ F A = A by
    classical
    rcases this with ⟨A, Ameas, Afp⟩
    let B := f '' A
    have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
    refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
    apply MeasurableEquiv.sumCongr (hf.equivImage _)
    have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
    rw [this]
    exact (hg.equivImage _).symm
  have Fmono : ∀ {A B}, A ⊆ B → F A ⊆ F B := fun h =>
    compl_subset_compl.mpr <| Set.image_mono <| compl_subset_compl.mpr <| Set.image_mono h
  let X : ℕ → Set α := fun n => F^[n] univ
  refine ⟨iInter X, ?_, ?_⟩
  · refine MeasurableSet.iInter fun n ↦ ?_
    induction n with
    | zero => exact MeasurableSet.univ
    | succ n ih =>
      rw [Function.iterate_succ', Function.comp_apply]
      exact (hg.measurableSet_image' (hf.measurableSet_image' ih).compl).compl
  apply subset_antisymm
  · apply subset_iInter
    intro n
    cases n
    · exact subset_univ _
    rw [Function.iterate_succ', Function.comp_apply]
    exact Fmono (iInter_subset _ _)
  rintro x hx ⟨y, hy, rfl⟩
  rw [mem_iInter] at hx
  apply hy
  rw [hf.injective.injOn.image_iInter_eq]
  rw [mem_iInter]
  intro n
  specialize hx n.succ
  rw [Function.iterate_succ', Function.comp_apply] at hx
  by_contra h
  apply hx
  exact ⟨y, h, rfl⟩

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ (h.1.add h.2).trans ?_⟩
  · have : ∀ s, ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0 := by intro s hs0; simpa using h hs0
    exact ⟨fun s hs0 ↦ (this s hs0).1, fun s hs0 ↦ (this s hs0).2⟩
  · rw [← two_smul ℝ≥0]
    exact AbsolutelyContinuous.rfl.smul_left 2

Goal state after: