mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
n : ℕ
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
by
  lift f to ι → ℝ≥0 using hf; dsimp; exact mod_cast NNReal.iSup_pow f n

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 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:
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.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.ediam (⇑h ⁻¹' s) = Metric.ediam s

Tactic:
by
  rw [← image_symm, ediam_image]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.eball x r = ⇑h ⁻¹' Metric.eball (h (h.symm x)) r

Tactic:
h.apply_symm_apply

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.eball x r = ⇑h ⁻¹' Metric.eball x r
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.closedEBall x r = ⇑h ⁻¹' Metric.closedEBall (h (h.symm x)) r

Tactic:
h.apply_symm_apply

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.closedEBall x r = ⇑h ⁻¹' Metric.closedEBall x r
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.ball x r = ⇑h ⁻¹' Metric.ball (h (h.symm x)) r

Tactic:
h.apply_symm_apply

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.ball x r = ⇑h ⁻¹' Metric.ball x r
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.sphere x r = ⇑h ⁻¹' Metric.sphere (h (h.symm x)) r

Tactic:
h.apply_symm_apply

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.sphere x r = ⇑h ⁻¹' Metric.sphere x r
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.closedBall x r = ⇑h ⁻¹' Metric.closedBall (h (h.symm x)) r

Tactic:
h.apply_symm_apply

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.closedBall x r = ⇑h ⁻¹' Metric.closedBall x r
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
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 : ℕ
hm : m ∈ s
hLm : L.length ≤ m
⊢ False

Tactic:
mem_ofPred_eq,

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
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 : ℕ
hm : 2 * (take m L).sum ≤ L.sum
hLm : L.length ≤ m
⊢ False
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)
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
⊢ ∃ v,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

Tactic:
obtain ⟨φ : ℕ → ℕ, φ_extr : StrictMono φ, hφ : ∀ n, ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)⟩ :=
    lim_z.cauchySeq.subseq_mem mem_𝓤

Goal state after:
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)
⊢ ∃ v,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ (((𝓤 α).lift' gen).lift' fun s ↦ s ○ s) = (𝓤 α).lift' fun s ↦ gen s ○ gen s

Tactic:
lift'_lift'_assoc

Goal state after:
α : Type u
inst✝ : UniformSpace α
⊢ ((𝓤 α).lift' fun s ↦ gen s ○ gen s) = (𝓤 α).lift' fun s ↦ gen s ○ gen s

case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen

case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s ↦ s ○ s
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ ((𝓤 α).lift' fun s ↦ gen (s ○ s)) = ((𝓤 α).lift' fun s ↦ s ○ s).lift' gen

Tactic:
lift'_lift'_assoc

Goal state after:
α : Type u
inst✝ : UniformSpace α
⊢ ((𝓤 α).lift' fun s ↦ gen (s ○ s)) = (𝓤 α).lift' fun s ↦ gen (s ○ s)

case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s ↦ s ○ s

case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
⊢ ContinuousOn (fun x ↦ a - x) {x | x ≠ ∞}

Tactic:
rw [show (fun x => a - x) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨a, x⟩ by rfl]

Goal state after:
a : ℝ≥0∞
⊢ ContinuousOn ((fun p ↦ p.1 - p.2) ∘ fun x ↦ (a, x)) {x | x ≠ ∞}
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ Tendsto (fun n ↦ (f n).toReal) fi (𝓝 0) ↔ Tendsto f fi (𝓝 0)

Tactic:
rw [← ENNReal.toReal_zero, tendsto_toReal_iff hf ENNReal.zero_ne_top]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a x : α
hx : x ∈ Ici a
y : α
hy : y ∈ Ici a
hxy : x < y
⊢ projIci a x < projIci a y

Tactic:
simpa only [projIci_of_mem, hx, hy]

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

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

Tactic:
have liminf_le : f.liminf u ≤ b := by
    apply liminf_le_of_le ⟨0, by simp⟩
    intro y h
    obtain ⟨i, hi⟩ := (Eventually.and h le_b).exists
    exact hi.1.trans hi.2

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
⊢ liminf (fun i ↦ (u i).toReal) f = (liminf u f).toReal
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : EMetricSpace β
inst✝ : CompleteSpace β
s : Set α
hs : Dense s
f : ↑s → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend f)
⊢ IsClosed[instTopologicalSpaceProd] {p | edist (hs.extend f p.1) (hs.extend f p.2) ≤ ↑K * edist p.1 p.2}

Tactic:
apply isClosed_le (by fun_prop)

Goal state after:
α : Type u_4
β : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : EMetricSpace β
inst✝ : CompleteSpace β
s : Set α
hs : Dense s
f : ↑s → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend f)
⊢ Continuous[instTopologicalSpaceProd, _] fun b ↦ ↑K * edist b.1 b.2
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs)
  · exact ⟨fun _ => 0, (LipschitzWith.const _).weaken zero_le, eqOn_empty _ _⟩
  have : Nonempty s := by simp only [hs, nonempty_coe_sort]
  let g := fun y : α => iInf fun x : s => f x + K * dist y x
  have B : ∀ y : α, BddBelow (range fun x : s => f x + K * dist y x) := fun y => by
    rcases hs with ⟨z, hz⟩
    refine ⟨f z - K * dist y z, ?_⟩
    rintro w ⟨t, rfl⟩
    dsimp
    rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]
    calc
      f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2
      _ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left
  have E : EqOn f g s := fun x hx => by
    refine le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) ?_
    simpa only [add_zero, Subtype.coe_mk, mul_zero, dist_self] using ciInf_le (B x) ⟨x, hx⟩
  refine ⟨g, LipschitzWith.of_le_add_mul K fun x y => ?_, E⟩
  rw [← sub_le_iff_le_add]
  refine le_ciInf fun z => ?_
  rw [sub_le_iff_le_add]
  calc
    g x ≤ f z + K * dist x z := ciInf_le (B x) _
    _ ≤ f z + K * dist y z + K * dist x y := by
      rw [add_assoc, ← mul_add, add_comm (dist y z)]
      gcongr
      apply dist_triangle

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 - c| + |b - d|

Tactic:
calc
    |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)| := by rw [sub_add_sub_cancel]
    _ ≤ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| := abs_add_le _ _
    _ ≤ |a - c| + |b - d| := by
      gcongr ?_ + ?_
      · exact abs_sup_sub_sup_le_abs _ _ _
      · rw [sup_comm c, sup_comm c]
        exact abs_sup_sub_sup_le_abs _ _ _

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
a : G₀
inst✝ : PosMulReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
⊢ a * s.sup' hs f = s.sup' hs fun i ↦ a * f i

Tactic:
by
  by_cases! h : 0 = a
  · simp [← h]
  exact map_finset_sup' (OrderIso.mulLeft₀ _ (lt_of_le_of_ne ha h)) hs f

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: 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' hs f / a = s.sup' hs fun i ↦ f i / a

Tactic:
sup'_div₀ (ha := ha)

Goal state after:
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' hs fun i ↦ f i / a) = s.sup' hs fun i ↦ f i / a
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a : α
x✝ : 0 < 1
⊢ ‖a ^ 1‖₊ ≤ ‖a‖₊ ^ 1

Tactic:
simp only [pow_one, le_rfl]

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
inst✝⁷ : SeminormedRing α
inst✝⁶ : SeminormedAddGroup β✝
inst✝⁵ : SMul α β✝
inst✝⁴ : NormSMulClass α β✝
ι : Type u_3
β : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedAddGroup (β i)
inst✝¹ : (i : ι) → SMul α (β i)
inst✝ : ∀ (i : ι), NormSMulClass α (β i)
r : α
x : (i : ι) → β i
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
simp [nnnorm_def, ← coe_nnnorm, nnnorm_smul, ← NNReal.coe_mul, NNReal.mul_finset_sup]

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
inst✝ : DecidableEq ι
i : ι
is : List ι
v : TProd α (i :: is)
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ α j

Tactic:
subst hji
      exact v.1

Goal state after:
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 ↔ ∀ (i_1 : ι), i_1 ∈ {i_2 | i_2 ∈ i :: l} → f i_1 ∈ t i_1

Tactic:
mem_ofPred_eq,

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 ↔ ∀ (i_1 : ι), i_1 ∈ i :: l → f i_1 ∈ t i_1
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ : y ∈ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < r / 2}
hy₂ : y ∈ Prod.snd ⁻¹' U
⊢ r ≤ ‖f y.2‖

Tactic:
simp_all [Set.disjoint_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

Tactic:
by_cases h : b ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
h : b ∈ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
h : b ∉ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
⊢ MeasurableSet s

Tactic:
by rw [map_def]; by_cases h : b ∈ s <;> simp [h]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝¹ x✝ : IterateMulAct f
⊢ (x✝¹ * x✝).val = (x✝ * x✝¹).val

Tactic:
apply Nat.add_comm

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
i : Bool
⊢ MeasurableSet (bif i then s₁ else s₂)

Tactic:
by
  cases i
  exacts [h₂, h₁]

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

Goal state before:
pp: case hx
E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ x + r • ‖y‖⁻¹ • y ∈ sphere x r

Tactic:
simp [norm_smul, hy, abs_of_nonneg hr]

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

Goal state before:
pp: case hy
E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ x - r • ‖y‖⁻¹ • y ∈ sphere x r

Tactic:
simp [norm_smul, hy, abs_of_nonneg hr]

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

Goal state before:
pp: α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
this : (⨆ i, bif i then m₁ else m₂) s = ⨆ i, (bif i then m₁ else m₂) s
⊢ (m₁ ⊔ m₂) s = max (m₁ s) (m₂ s)

Tactic:
iSup_bool_eq,

Goal state after:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
this : ((bif true then m₁ else m₂) ⊔ bif false then m₁ else m₂) s = ⨆ i, (bif i then m₁ else m₂) s
⊢ (m₁ ⊔ m₂) s = max (m₁ s) (m₂ s)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
hsum : ∑' (x : α), f x ≠ ∞
⊢ HasSum (fun x ↦ (f x).toReal) (∑' (x : α), (f x).toReal)

Tactic:
lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hsum
  simp only [coe_toReal, ← NNReal.coe_tsum, NNReal.hasSum_coe]
  exact (tsum_coe_ne_top_iff_summable.1 hsum).hasSum

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
r' : α → β → Prop
h : SemicontinuousWithinAt r s x
h' : SemicontinuousWithinAt r' s x
b : β
hb : r x b
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (r ⊔ r') x' b

pp: case inr
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
r' : α → β → Prop
h : SemicontinuousWithinAt r s x
h' : SemicontinuousWithinAt r' s x
b : β
hb' : r' x b
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (r ⊔ r') x' b

Tactic:
· exact (h b hb).mono fun _ hx ↦ Or.inl hx

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
r' : α → β → Prop
h : SemicontinuousWithinAt r s x
h' : SemicontinuousWithinAt r' s x
b : β
hb' : r' x b
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (r ⊔ r') x' b
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
r' : α → β → Prop
h : SemicontinuousAt r x
h' : SemicontinuousAt r' x
b : β
hb : r x b
⊢ ∀ᶠ (x' : α) in 𝓝 x, (r ⊔ r') x' b

pp: case inr
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
r' : α → β → Prop
h : SemicontinuousAt r x
h' : SemicontinuousAt r' x
b : β
hb' : r' x b
⊢ ∀ᶠ (x' : α) in 𝓝 x, (r ⊔ r') x' b

Tactic:
· exact (h b hb).mono fun _ hx ↦ Or.inl hx

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
r' : α → β → Prop
h : SemicontinuousAt r x
h' : SemicontinuousAt r' x
b : β
hb' : r' x b
⊢ ∀ᶠ (x' : α) in 𝓝 x, (r ⊔ r') x' b
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: ⊢ StrictAntiOn (fun x ↦ x⁻¹) (Ioi 0)

Tactic:
intro a a_0 b b_0 a_b
  push _ ∈ _ at *
  lift a to ℝ using ⟨ne_top_of_lt a_b, ne_bot_of_gt a_0⟩
  match b with
  | ⊤ => exact inv_top ▸ inv_pos_of_pos_ne_top a_0 (coe_ne_top a)
  | ⊥ => exact (not_lt_bot b_0).rec
  | (b : ℝ) =>
    rw [← coe_inv a, ← coe_inv b, EReal.coe_lt_coe_iff]
    exact _root_.inv_strictAntiOn (EReal.coe_pos.1 a_0) (EReal.coe_pos.1 b_0)
      (EReal.coe_lt_coe_iff.1 a_b)

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
by_cases h' : x' ∈ s <;> simp [h', hz.trans_le hy, hz]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) →
    ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1

Tactic:
intro hf ⟨x, y⟩ h
    by_cases hx : x ∈ s
    · have ⟨y', hy', z, hz, h₁⟩ := (h hx).exists_disjoint_Iio_Ioi
      filter_upwards [(hf x hx z hz).prodMk_nhds (eventually_lt_nhds hy')]
        with _ ⟨h₂, h₃⟩ h₄ using h₁ _ h₃ _ <| h₂ h₄
    · filter_upwards [(continuous_fst.tendsto _).eventually (hs.isOpen_compl.eventually_mem hx)]
        with _ h₁ h₂ using (h₁ h₂).elim

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

Goal state before:
pp: C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
⊢ Tendsto (fun n ↦ C / ↑n) atTop (𝓝 0)

Tactic:
have : (fun n : ℕ ↦ C / n) = fun n : ℕ ↦ ((C.toReal / n : ℝ) : EReal) := by
    ext n
    nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]
  rw [this, ← coe_zero, tendsto_coe]
  exact _root_.tendsto_const_div_atTop_nhds_zero_nat C.toReal

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

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ¬∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
· obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v :=
        exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂
      filter_upwards [hf z₁ z₁lt, hg z₂ z₂lt] with z h₁z h₂z
      have A1 : min (f z) (f x) ∈ u := by
        by_cases! H : f z ≤ f x
        · simpa [H] using h₁ ⟨h₁z, H⟩
        · simpa [H.le]
      have A2 : min (g z) (g x) ∈ v := by
        by_cases! H : g z ≤ g x
        · simpa [H] using h₂ ⟨h₂z, H⟩
        · simpa [H.le]
      have : (min (f z) (f x), min (g z) (g x)) ∈ u ×ˢ v := ⟨A1, A2⟩
      calc
        y < min (f z) (f x) + min (g z) (g x) := h this
        _ ≤ f z + g z := add_le_add (min_le_left _ _) (min_le_left _ _)

Goal state after:
case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ¬∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x : α
⊢ ⋂ y, ⋂ (_ : y ≤ x), dissipate s y ⊆ dissipate s x

Tactic:
apply iInter_mono fun z y hy ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x z : α
y : β
hy : y ∈ ⋂ (_ : z ≤ x), dissipate s z
⊢ y ∈ ⋂ (_ : z ≤ x), s z