mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ 0 < ‖a‖ ↔ a ≠ 1

Tactic:
rw [← not_le, norm_le_zero_iff']

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case pos
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
⊢ False

Tactic:
obtain ⟨u, hu⟩ := intermediate_value_Ioo bot_le hf_c.continuousOn ⟨hb, H⟩

Goal state after:
case pos
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
u : α
hu : u ∈ Ioo ⊥ a ∧ f u = f b
⊢ False
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case pos
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
⊢ False

pp: case neg
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b ≤ f ⊥
⊢ False

Tactic:
· obtain ⟨u, hu⟩ := intermediate_value_Ioo bot_le hf_c.continuousOn ⟨hb, H⟩
      rw [hf_i hu.2] at hu
      exact (hab.trans hu.1.2).false

Goal state after:
case neg
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b ≤ f ⊥
⊢ False
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
ha : IsLeast {g | g ∈ H ∧ 1 < g} a
⊢ H = closure {a}

Tactic:
obtain ⟨⟨a_in, a_pos⟩, a_min⟩ := ha
  refine le_antisymm ?_ (H.closure_le.mpr <| by simp [a_in])
  intro g g_in
  obtain ⟨k, ⟨nonneg, lt⟩, _⟩ := existsUnique_zpow_near_of_one_lt a_pos g
  have h_zero : g / (a ^ k) = 1 := by
    by_contra h
    have h : a ≤ g / (a ^ k) := by
      refine a_min ⟨?_, ?_⟩
      · exact Subgroup.div_mem H g_in (Subgroup.zpow_mem H a_in k)
      · exact lt_of_le_of_ne (by simpa using nonneg) (Ne.symm h)
    have h' : ¬a ≤ g / (a ^ k) := not_le.mpr (by simpa [zpow_add_one, div_lt_iff_lt_mul'] using lt)
    contradiction
  simp [div_eq_one.mp h_zero, mem_closure_singleton]

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
⊢ Dense ↑S

Tactic:
cases subsingleton_or_nontrivial G
  · refine fun x => _root_.subset_closure ?_
    rw [Subsingleton.elim x 1]
    exact one_mem S
  refine dense_of_exists_between fun a b hlt => ?_
  rcases hS (b / a) (one_lt_div'.2 hlt) with ⟨g, hgS, hg0, hg⟩
  rcases (existsUnique_add_zpow_mem_Ioc hg0 1 a).exists with ⟨m, hm⟩
  rw [one_mul] at hm
  refine ⟨g ^ m, zpow_mem hgS _, hm.1, hm.2.trans_lt ?_⟩
  rwa [lt_div_iff_mul_lt'] at hg

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ (∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal

Tactic:
by
  rw [← coe_inj, coe_toNNReal, ofNNReal_finsetSum, sum_congr rfl]
  · intro x hx
    exact (coe_toNNReal (hf x hx)).symm
  · exact sum_ne_top.2 hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
s : Set β
hs : ∀ᶠ (x : β) in f, x ∈ s
b : α
hb : b ∈ upperBounds (u '' s)
⊢ ∀ x ∈ s, u x ∈ {x | (fun x ↦ (fun x1 x2 ↦ x1 ≤ x2) x b) x}

Tactic:
by simpa [upperBounds] using hb

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

Goal state before:
pp: case inr
y z t : EReal
h2 : z < t
x : ℝ
h1 : ↑x < y
hx : ↑x ≠ ⊥
⊢ ↑x + z < y + t

Tactic:
calc (x : EReal) + z < x + t := add_lt_add_left_coe h2 _
    _ ≤ y + t := by gcongr

Goal state after:
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))

Tactic:
· exact fun _ hb => le_of_tendsto' ha fun x => hb (Set.mem_range_self x)

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

Goal state before:
pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ -(x - y) = -x + y

Tactic:
rw [sub_eq_add_neg, neg_add _ _, sub_eq_add_neg, neg_neg] <;> simp_all

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

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : ℝ≥0∞
y : EReal
hy : ↑x = y
H₁ : 0 ≤ y
⊢ y.toENNReal = x

Tactic:
by simp [← hy]

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

Goal state before:
pp: x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ x - y ↔ y ≤ x

Tactic:
by
  cases x <;> cases y <;> simp_all [← EReal.coe_sub]

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

Goal state before:
pp: x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
⊢ x - y < 0 ↔ x < y

Tactic:
by
  cases x <;> cases y <;> simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ Tendsto Finset.toLeft atTop atTop

Tactic:
intro s hs

Goal state after:
α : Type u_3
β : Type u_4
s : Set (Finset α)
hs : s ∈ atTop
⊢ s ∈ map Finset.toLeft atTop
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ Tendsto Finset.toRight atTop atTop

Tactic:
intro s hs

Goal state after:
α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : s ∈ atTop
⊢ s ∈ map Finset.toRight atTop
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst✝³ : ConditionallyCompleteLinearOrder β
f✝¹ : Filter α
u : α → β
inst✝² : ConditionallyCompleteLinearOrder α
f✝ : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
j : Subtype p
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
g : ℕ → Subtype p := ⋯.choose
⊢ ∃ n, g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
by_cases! H : ∃ j, j ∈ m
    · rcases H with ⟨j, hj⟩
      rcases (exists_surjective_nat (Subtype p)).choose_spec j with ⟨n, rfl⟩
      exact ⟨n, Or.inl hj⟩
    · exact ⟨0, Or.inr H⟩

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
⊢ limsup (fun a ↦ max (u a) (v a)) f ≤ max (limsup u f) (limsup v f)

Tactic:
refine (limsup_le_iff cobddmax bddmax).2 (fun b hb ↦ ?_)
    have hu := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_left _ _) hb) h₃
    have hv := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_right _ _) hb) h₄
    refine mem_of_superset (inter_mem hu hv) (fun _ ↦ by simp)

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

Goal state before:
pp: case pos.convert_6
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ L.HasSupport

Tactic:
· exact h.1

Goal state after:
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:
rw [mul_div_cancel]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f : β → α
inst✝ : CompleteSpace α
⊢ (CauchySeq fun s ↦ ∏ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
cauchySeq_finset_iff_tprod_vanishing

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f : β → α
inst✝ : CompleteSpace α
⊢ (∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e) ↔
    ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case refine_2
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
e : Set G
he : e ∈ 𝓝 1
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
⊢ ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
exact ⟨range N, fun t ht ↦ hN _ fun n hnt ↦
      le_of_not_gt fun h ↦ Set.disjoint_left.mp ht hnt (mem_range.mpr h)⟩

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 β
⊢ (if h : Multipliable (fun x ↦ 1) L then
      if L.HasSupport ∧ ((mulSupport fun x ↦ 1) ∩ L.support).Finite then finprod (L.support.mulIndicator fun x ↦ 1)
      else if HasProd (fun x ↦ 1) 1 L then 1 else Exists.choose h
    else 1) =
    1

Tactic:
dif_pos multipliable_one,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
⊢ (if L.HasSupport ∧ ((mulSupport fun x ↦ 1) ∩ L.support).Finite then finprod (L.support.mulIndicator fun x ↦ 1)
    else if HasProd (fun x ↦ 1) 1 L then 1 else Exists.choose ⋯) =
    1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
γ : Type u_4
g : γ → β
hg : Injective g
f : γ → α
this : mulSupport (extend g f 1) ⊆ Set.range g
⊢ ∏' (c : γ), extend g f 1 (g c) = ∏' (x : γ), f x

Tactic:
hg.extend_apply

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

Goal state before:
pp: case inl
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
h✝ : L.NeBot
⊢ HasSum (fun x ↦ (f x).toNNReal) y.toNNReal L

Tactic:
lift y to ℝ≥0 using hy.nonneg hf₀
    lift f to α → ℝ≥0 using hf₀
    simpa [hasSum_coe] using hy

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
⊢ Isometry ⇑(AddMonoidHom.inl α β)

Tactic:
intro x y
  rw [Prod.edist_eq]
  simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
⊢ Isometry ⇑(AddMonoidHom.inr α β)

Tactic:
intro x y
  rw [Prod.edist_eq]
  simp

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}
⊢ ∃ u, (∀ (n : ℕ), u n ∈ s) ∧ ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V

Tactic:
simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), t.Finite → ∃ a ∈ s, ∀ (x : X), ¬(x ∈ t ∧ a ∈ {x_1 | (x_1, x) ∈ V})
⊢ ∃ u, (∀ (n : ℕ), u n ∈ s) ∧ ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) atTop (𝓝 (a * b))

Tactic:
← prod_atTop_atTop_eq

Goal state after:
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) (atTop ×ˢ atTop) (𝓝 (a * b))
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: case pos
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (pkg.extend f)

Tactic:
rw [pkg.extend_def hf]
    exact uniformContinuous_uniformly_extend pkg.isUniformInducing pkg.dense hf

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁴ : UniformSpace X
inst✝³ : UniformSpace Y
inst✝² : Monoid M
inst✝¹ : MulAction M X
inst✝ : UniformContinuousConstSMul M X
x y : M
a : X
⊢ (x * y) • ↑a = x • y • ↑a

Tactic:
by
      simp only [← coe_smul, mul_smul]

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

Goal state before:
pp: case pos
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)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
x₁ x₂ x₃ x₄ : X
H : ∃ n, (x₁, x₄) ∉ U n
⊢ ¬((x₁, x₂) ∈ U (Nat.find H + 1) ∧ (x₂, x₃) ∈ U (Nat.find H + 1) ∧ (x₃, x₄) ∈ U (Nat.find H + 1))

Tactic:
rintro ⟨h₁₂, h₂₃, h₃₄⟩

Goal state after:
case pos
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)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
x₁ x₂ x₃ x₄ : X
H : ∃ n, (x₁, x₄) ∉ U n
h₁₂ : (x₁, x₂) ∈ U (Nat.find H + 1)
h₂₃ : (x₂, x₃) ∈ U (Nat.find H + 1)
h₃₄ : (x₃, x₄) ∈ U (Nat.find H + 1)
⊢ False
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : FunLike F α β
inst✝¹ : Subsingleton α
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist x y = 0 ∨ edist x y = ∞

Tactic:
simp [Subsingleton.elim x y]

Goal state after:
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: c : ℝ≥0
⊢ c • 1 = ↑c

Tactic:
by simp [smul_def]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵢ Y
⊢ ratio e.toDilationEquiv = 1

Tactic:
by
  rw [← ratio_toDilation, IsometryEquiv.toDilationEquiv_toDilation, Isometry.toDilation_ratio]

Goal state after:
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: r : ℝ≥0
s : ℝ≥0∞
⊢ (↑r * s).toReal = r • s.toReal

Tactic:
toReal_mul,

Goal state after:
r : ℝ≥0
s : ℝ≥0∞
⊢ (↑r).toReal * s.toReal = r • s.toReal
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:
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 : β
h : dist p (s • x) ≤ ‖s‖ * ε
⊢ s • s⁻¹ • p = p

Tactic:
simp [smul_smul, hs]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
⊢ Measurable fun x ↦ Nat.findGreatest (p x) N

Tactic:
refine measurable_findGreatest' fun k hk => ?_

Goal state after:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet {x | Nat.findGreatest (p x) N = k}
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: case h
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
ht : μ t = 0
⊢ s ∩ t ⊆ t

Tactic:
apply inter_subset_right

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

Goal state before:
pp: case h
α : 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 α := ⋯
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⋯
k : ι
⊢ S ∩ s k ⊆ s k

Tactic:
apply inter_subset_right

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

Goal state before:
pp: G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f

Tactic:
obtain ⟨C, hC⟩ := (isBounded_iff_subset_ball 0).1 (hbounded.subset <| image_mono hUε)

Goal state after:
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C : ℝ
hC : ⇑f '' ball 0 δ ⊆ ball 0 C
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:

Tactic:
‖f x‖
    _ = ‖(n : ℝ)⁻¹ • f (n • x)‖ := by simp [← Nat.cast_smul_eq_nsmul ℝ, hn₀]
    _ ≤ ‖(n : ℝ)⁻¹‖ * ‖f (n • x)‖ := norm_smul_le ..
    _ < ‖(n : ℝ)⁻¹‖ * C := by
      gcongr
      · simpa [pos_iff_ne_zero]
      · refine hC _ <| norm_nsmul_le.trans_lt ?_
        simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ
    _ = (n : ℝ)⁻¹ * C := by simp
    _ < (C / ε : ℝ)⁻¹ * C := by gcongr
    _ = ε := by simp [hC₀.ne']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ MeasurableSpace.comap Prod.fst mβ ≤ MeasurableSpace.map f m

Tactic:
MeasurableSpace.comap_le_iff_le_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ mβ ≤ MeasurableSpace.map Prod.fst (MeasurableSpace.map f m)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ MeasurableSpace.comap Prod.snd mγ ≤ MeasurableSpace.map f m

Tactic:
MeasurableSpace.comap_le_iff_le_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ mγ ≤ MeasurableSpace.map Prod.snd (MeasurableSpace.map f m)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)

Tactic:
inhabit ι
  set g' : (i : ι) → t i → β := fun i => g i ∘ (↑)
  -- see https://github.com/leanprover-community/mathlib4/issues/2184
  have ht' : ∀ (i j) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩ := by
    intro i j x hxi hxj
    rcases eq_or_ne i j with rfl | hij
    · rfl
    · exact ht hij ⟨hxi, hxj⟩
  set f : (⋃ i, t i) → β := iUnionLift t g' ht' _ Subset.rfl
  have hfm : Measurable f := measurable_iUnionLift _ _ t_meas
    (fun i => (hg i).comp measurable_subtype_coe)
  classical
    refine ⟨fun x => if hx : x ∈ ⋃ i, t i then f ⟨x, hx⟩ else g default x,
      hfm.dite ((hg default).comp measurable_subtype_coe) (.iUnion t_meas), fun i x hx => ?_⟩
    simp only [dif_pos (mem_iUnion.2 ⟨i, hx⟩)]
    exact iUnionLift_of_mem ⟨x, mem_iUnion.2 ⟨i, hx⟩⟩ hx

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

Goal state before:
pp: α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋂ i, {x | p i x})

Tactic:
exact MeasurableSet.iInter fun i ↦ (hp i).setOf

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

Goal state before:
pp: ⊢ zero ≤ zero

Tactic:
by constructor

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

Goal state before:
pp: ⊢ zero ≤ neg

Tactic:
by constructor

Goal state after:
⊢ zero ≤ neg
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ zero ≤ pos

Tactic:
by constructor

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

Goal state before:
pp: ⊢ neg ≤ zero

Tactic:
by constructor

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

Goal state before:
pp: ⊢ neg ≤ neg

Tactic:
by constructor

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

Goal state before:
pp: ⊢ neg ≤ pos

Tactic:
by constructor

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

Goal state before:
pp: ⊢ pos ≤ zero

Tactic:
by constructor

Goal state after:
⊢ pos ≤ zero