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 : α
⊢ ∀ (x2 : α), edist ((AddMonoidHom.inl α β) x) ((AddMonoidHom.inl α β) x2) = edist x x2

Tactic:
y

Goal state after:
α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : α
⊢ edist ((AddMonoidHom.inl α β) x) ((AddMonoidHom.inl α β) y) = 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 : β
⊢ ∀ (x2 : β), edist ((AddMonoidHom.inr α β) x) ((AddMonoidHom.inr α β) x2) = edist x x2

Tactic:
y

Goal state after:
α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : β
⊢ edist ((AddMonoidHom.inr α β) x) ((AddMonoidHom.inr α β) y) = edist x y
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: α : Type u_1
ι : Type u_2
κ : Type u_3
E : Type u_4
F✝ : Type u_5
G : Type u_6
F : Type u_7
inst✝ : NormedGroup F
⊢ ‖1‖ₑ = 0

Tactic:
by simp [enorm_eq_nnnorm]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
κ : Type u_3
E : Type u_4
F✝ : Type u_5
G : Type u_6
F : Type u_7
inst✝ : NormedGroup F
⊢ ∀ (x : F), ‖x‖ₑ = 0 ↔ x = 1

Tactic:
by simp [enorm_eq_nnnorm]

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
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 ≤ l.length, IsGreatest s M

Tactic:
have hs_ub : length l ∈ upperBounds s := by
      intro m hm
      rw [← not_lt, Nat.lt_iff_add_one_le, ← hL_len]
      intro hLm
      rw [mem_ofPred_eq, take_of_length_le hLm, two_mul, add_le_iff_nonpos_left, nonpos_iff_eq_zero,
          sum_eq_zero_iff, ← forall_iff_forall_mem, forall_zipWith,
          ← isChain_cons_append_singleton_iff_forall₂]
          at hm <;>
        [skip; simp]
      exact hd₀ (hm.rel_cons (mem_append.2 <| Or.inr <| mem_singleton_self _))
    have hs_bdd : BddAbove s := ⟨length l, hs_ub⟩
    exact ⟨sSup s, csSup_le hsne hs_ub, ⟨Nat.sSup_mem hsne hs_bdd, fun k => le_csSup hs_bdd⟩⟩

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ UniformCauchySeqOnFilter f l (𝓟 s) ↔ TendstoUniformlyOnFilter (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)

Tactic:
SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one

Goal state after:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ TendstoUniformlyOnFilter (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s) ↔
    TendstoUniformlyOnFilter (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: h : ∞ ∈ {x | x ≠ ∞}
⊢ False

Tactic:
exact h none_eq_top

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

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
a _b : CauchyFilter α
⊢ f ⋯.some = f ⋯.some

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Bornology.Hom

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : Bornology γ
inst✝ : Bornology δ
toFun✝¹ : α → β
comap_cobounded_le'✝¹ : comap toFun✝¹ (cobounded β) ≤ cobounded α
toFun✝ : α → β
comap_cobounded_le'✝ : comap toFun✝ (cobounded β) ≤ cobounded α
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, comap_cobounded_le' := comap_cobounded_le'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, comap_cobounded_le' := comap_cobounded_le'✝ }
⊢ { toFun := toFun✝¹, comap_cobounded_le' := comap_cobounded_le'✝¹ } =
    { toFun := toFun✝, comap_cobounded_le' := comap_cobounded_le'✝ }

Tactic:
congr

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

Goal state before:
pp: X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
x : X
⊢ ∀ {y : X}, d x y = 0 ↔ Inseparable x y

Tactic:
y

Goal state after:
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
x y : X
⊢ d x y = 0 ↔ Inseparable x y
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x : X
⊢ ∀ {y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n

Tactic:
y

Goal state after:
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x y : X
⊢ ∀ {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: t : ℝ≥0∞
t_ne_top : t ≠ ∞
x : ℝ≥0∞
⊢ ∀ ⦃b : ℝ≥0∞⦄, x ≤ b → t.truncateToReal x ≤ t.truncateToReal b

Tactic:
y

Goal state after:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x y : ℝ≥0∞
⊢ x ≤ y → t.truncateToReal x ≤ t.truncateToReal y
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n

Tactic:
iterate_succ,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) ((f^[n] ∘ f) x) ≤ dist x (f x) * ↑K ^ n
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: case h₁
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| ≤ |a - c|

pp: case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |c ⊓ b - c ⊓ d| ≤ |b - d|

Tactic:
· exact abs_inf_sub_inf_le_abs _ _ _

Goal state after:
case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |c ⊓ b - c ⊓ d| ≤ |b - d|
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
toFun✝¹ : α → β
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝¹ x) (toFun✝¹ y) = ↑r * edist x y
toFun✝ : α → β
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝ x) (toFun✝ y) = ↑r * edist x y
h : { toFun := toFun✝¹, edist_eq' := edist_eq'✝¹ }.toFun = { toFun := toFun✝, edist_eq' := edist_eq'✝ }.toFun
⊢ { toFun := toFun✝¹, edist_eq' := edist_eq'✝¹ } = { toFun := toFun✝, edist_eq' := edist_eq'✝ }

Tactic:
congr

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (Dilation.id α) = 1

Tactic:
ratio,

Goal state after:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ (if ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞ then 1 else ⋯.choose) = 1
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝¹.toFun x) (toEquiv✝¹.toFun y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝.toFun x) (toEquiv✝.toFun y) = ↑r * edist x y
h :
  ⇑{ toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ }.toEquiv =
    ⇑{ toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }.toEquiv
⊢ { toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ } = { toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }

Tactic:
congr

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝¹.toFun x) (toEquiv✝¹.toFun y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝.toFun x) (toEquiv✝.toFun y) = ↑r * edist x y
h :
  ⇑{ toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ }.toEquiv =
    ⇑{ toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }.toEquiv
⊢ toEquiv✝¹ = toEquiv✝
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x : R
⊢ ∀ {y : R}, v (-x + y) = 0 → x = y

Tactic:
y

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
⊢ v (-x + y) = 0 → x = y
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
MeasurableSet'✝¹ : Set α → Prop
measurableSet_empty✝¹ : MeasurableSet'✝¹ ∅
measurableSet_compl✝¹ : ∀ (s : Set α), MeasurableSet'✝¹ s → MeasurableSet'✝¹ sᶜ
measurableSet_iUnion✝¹ : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet'✝¹ (f i)) → MeasurableSet'✝¹ (⋃ i, f i)
MeasurableSet'✝ : Set α → Prop
measurableSet_empty✝ : MeasurableSet'✝ ∅
measurableSet_compl✝ : ∀ (s : Set α), MeasurableSet'✝ s → MeasurableSet'✝ sᶜ
measurableSet_iUnion✝ : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet'✝ (f i)) → MeasurableSet'✝ (⋃ i, f i)
x✝ : MeasurableSet = MeasurableSet
⊢ { MeasurableSet' := MeasurableSet'✝¹, measurableSet_empty := measurableSet_empty✝¹,
      measurableSet_compl := measurableSet_compl✝¹, measurableSet_iUnion := measurableSet_iUnion✝¹ } =
    { MeasurableSet' := MeasurableSet'✝, measurableSet_empty := measurableSet_empty✝,
      measurableSet_compl := measurableSet_compl✝, measurableSet_iUnion := measurableSet_iUnion✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
x y : α
⊢ (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) ↔ ∀ s ∈ S, x ∈ s ↔ y ∈ s

Tactic:
by
  refine ⟨fun H s hs ↦ H s (.basic s hs), fun H s ↦ ?_⟩
  apply generateFrom_induction
  · exact fun s hs _ ↦ H s hs
  · rfl
  · exact fun _ _ ↦ Iff.not
  · intro f _ hf
    simp only [mem_iUnion, hf]

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
core : NormedSpace.Core 𝕜 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x : E
⊢ ∀ {y : E}, dist x y = 0 → x = y

Tactic:
y

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
core : NormedSpace.Core 𝕜 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
⊢ dist x y = 0 → x = y
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x : E
⊢ ∀ {y : E}, dist x y = 0 → x = y

Tactic:
y

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
⊢ dist x y = 0 → x = y
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
T : TopologicalSpace E
core : NormedSpace.Core 𝕜 E
H : T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x : E
⊢ ∀ {y : E}, dist x y = 0 → x = y

Tactic:
y

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
T : TopologicalSpace E
core : NormedSpace.Core 𝕜 E
H : T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
⊢ dist x y = 0 → x = y
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
B : Bornology E
core : NormedSpace.Core 𝕜 E
HU : 𝓤 E = 𝓤 E
HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x : E
⊢ ∀ {y : E}, dist x y = 0 → x = y

Tactic:
y

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
B : Bornology E
core : NormedSpace.Core 𝕜 E
HU : 𝓤 E = 𝓤 E
HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
⊢ dist x y = 0 → x = y
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
k : ι
⊢ μ (s k) + μ (S \ s k) ≤ M + μ (S \ s k)

Tactic:
gcongr; exact le_iSup (μ ∘ s) k

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set α
t : Set ↑s
hs : MeasurableSet s
⊢ MeasurableSet t → MeasurableSet (Subtype.val '' t)

Tactic:
rintro ⟨u, hu, rfl⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (Subtype.val '' Subtype.val ⁻¹' u)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ ⋃ i, t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (iUnionLift t f htf T hT ⁻¹' s)

Tactic:
rw [preimage_iUnionLift]
  exact .preimage (.iUnion fun i => .image_inclusion _ (htm _) (hfm i hs)) (measurable_inclusion _)

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
⊢ Measurable ⇑(Equiv.piEquivPiSubtypeProd p X).symm

Tactic:
refine measurable_pi_iff.2 fun j => ?_

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
⊢ Measurable fun x ↦ (Equiv.piEquivPiSubtypeProd p X).symm x j
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
⊢ Measurable ⇑(Equiv.piEquivPiSubtypeProd p X).symm

Tactic:
by
  refine measurable_pi_iff.2 fun j => ?_
  by_cases hj : p j
  · simp only [hj, dif_pos, Equiv.piEquivPiSubtypeProd_symm_apply]
    have : Measurable fun (f : ∀ i : { x // p x }, X i.1) => f ⟨j, hj⟩ :=
      measurable_pi_apply (X := fun i : {x // p x} => X i.1) ⟨j, hj⟩
    exact Measurable.comp this measurable_fst
  · simp only [hj, Equiv.piEquivPiSubtypeProd_symm_apply, dif_neg, not_false_iff]
    have : Measurable fun (f : ∀ i : { x // ¬p x }, X i.1) => f ⟨j, hj⟩ :=
      measurable_pi_apply (X := fun i : {x // ¬p x} => X i.1) ⟨j, hj⟩
    exact Measurable.comp this measurable_snd

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : β → ℝ
hf : 0 ≤ f
s : α → Set β
hs : ∀ (i : β), ∃! j, i ∈ s j
⊢ Summable f ↔ (∀ (j : α), Summable fun i ↦ f ↑i) ∧ Summable fun j ↦ ∑' (i : ↑(s j)), f ↑i

Tactic:
simpa only [← (Set.sigmaEquiv s hs).summable_iff] using! summable_sigma_of_nonneg (fun _ ↦ hf _)

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsSemitopologicalSemiring A
x : A
⊢ IsClosed[inst✝³] (range Subtype.val)

Tactic:
by simpa using isClosed R x

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

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (↑a✝).abs = 0 ↔ ↑a✝ = 0

pp: case top
⊢ ⊤.abs = 0 ↔ ⊤ = 0

Tactic:
· simp only [abs_def, coe_eq_zero, ENNReal.ofReal_eq_zero, abs_nonpos_iff]

Goal state after:
case top
⊢ ⊤.abs = 0 ↔ ⊤ = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x

Tactic:
exact tsum_iUnion_le_tsum f t

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

Goal state before:
pp: case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ (↑|a|)⁻¹ = (↑a)⁻¹

Tactic:
congr

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ |a| = a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑|a|⁻¹ = ↑a⁻¹

Tactic:
congr

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ |a| = a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
⊢ ↑(sign a) * ↑a.abs⁻¹ = a⁻¹

Tactic:
induction a with
  | bot | top => simp
  | coe a =>
    rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
    · rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_neg a_neg), coe_ennreal_ofReal,
        max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_neg |a|⁻¹, ← coe_inv a, abs_of_neg a_neg,
        ← _root_.inv_neg, neg_neg]
    · simp
    · rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_pos a_pos), coe_ennreal_ofReal,
          max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_inv a]
      congr
      exact abs_of_pos a_pos

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

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

Tactic:
by
  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.Data.EReal.Inv

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

Tactic:
← mul_div_left_comm (c / d),

Goal state after:
a b c d : EReal
⊢ a / b * (c / d) = c / d * (a / b)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
hfs : ∀ (b : γ), ∃ v, IsClosed[inst✝¹] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v
ks : IsCompact s
c : γ
⊢ IsCompact (s ∩ f ⁻¹' Iic c)

Tactic:
obtain ⟨v, hv, hv'⟩ := hfs c

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
hfs : ∀ (b : γ), ∃ v, IsClosed[inst✝¹] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v
ks : IsCompact s
c : γ
v : Set α
hv : IsClosed[inst✝¹] v
hv' : s ∩ f ⁻¹' Iic c = s ∩ v
⊢ IsCompact (s ∩ f ⁻¹' Iic c)
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
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ∑' (i : ℕ), ↑(ε' i)

Tactic:
← ENNReal.tsum_add

Goal state after:
α : 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
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ μ (⋃ i, s i) ≤ ∑' (a : ℕ), (μ (s a) + ↑(ε' a))
Module: Mathlib.Topology.Semicontinuity.Basic

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

Tactic:
y

Goal state after:
case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
x : α
a✝ : x ∈ s
y : γ
⊢ y < f x → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup u f * c ≤ limsup (fun x ↦ u x * c) f

Tactic:
rw [le_limsup_iff]

Goal state after:
case a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ ∀ y < limsup u f * c, ∃ᶠ (a : α) in f, y < u a * c
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞) ↔ 1 < r

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
r : ℝ≥0∞
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞) → 1 < r

case refine_2
r : ℝ≥0∞
⊢ 1 < r → Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)