mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case h'
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := ⋯
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := ⋯
⊢ ∀ x_1 ∈ x '' t, x_1 < y (f x_1)

Tactic:
rintro a ⟨c, hc, rfl⟩

Goal state after:
case h'
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
⊢ x c < y (f (x c))
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_4
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ (↑I').subtype.range ≤ (↑I').subtype.range ⊓ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I ⊔ (↑I').subtype.range ⊓ ↑J'

Tactic:
Submodule.range_subtype,

Goal state after:
case refine_4
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑I' ≤ ↑I' ⊓ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I ⊔ ↑I' ⊓ ↑J'
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝³ : FunLike 𝓕 E F
inst✝² : Group E
inst✝¹ : SeminormedGroup F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x y : E
⊢ dist x y = ‖f (x⁻¹ * y)‖

Tactic:
simp only [map_mul, map_inv, ← dist_eq_norm_inv_mul]; rfl

Goal state after:
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
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
⊢ H = closure {a}

Tactic:
refine le_antisymm ?_ (H.closure_le.mpr <| by simp [a_in])

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
⊢ H ≤ closure {a}
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
⊢ ∀ a_1 ∈ s, a_1 ∈ Ico a c → f a_1 < b

Tactic:
rintro x hx ⟨_, hxc⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
x : α
hx : x ∈ s
left✝ : a ≤ x
hxc : x < c
⊢ f x < b
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
⊢ ∀ a_1 ∈ s, a_1 ∈ Ico a c → f a_1 < b

Tactic:
rintro x hx ⟨_, hxc⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
x : α
hx : x ∈ s
left✝ : a ≤ x
hxc : x < c
⊢ f x < b
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: x : ℕ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
rcases le_or_gt 0 r with (hr | hr)
  · rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
    positivity
  · rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]
    calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ := floor_mono <| by linarith
    _ < ⌈↑x - r⌉₊ := by
      rw [floor_natCast, Nat.lt_ceil]
      linarith

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (⨅ s ∈ f, ⨆ a ∈ s, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ

Tactic:
rw [biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ ⨅ i ∈ f, (⨆ a ∈ i, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
inst✝ : Infinite α
⊢ map Finset.card atTop = atTop

Tactic:
rw [map_atTop_eq, atTop]

Goal state after:
α : Type u_3
inst✝ : Infinite α
⊢ ⨅ a, 𝓟 (Finset.card '' {a' | a ⊆ a'}) = ⨅ a, 𝓟 (Ici a)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ liminf u f ≤ limsup v f

Tactic:
by
  rcases f.eq_or_neBot with rfl | _
  · exact (frequently_bot h).rec
  have h₃ : f.IsCoboundedUnder (· ≥ ·) u := by
    obtain ⟨a, ha⟩ := h₂.eventually_le
    apply IsCoboundedUnder.of_frequently_le (a := a)
    exact (h.and_eventually ha).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x
  have h₄ : f.IsCoboundedUnder (· ≤ ·) v := by
    obtain ⟨a, ha⟩ := h₁.eventually_ge
    apply IsCoboundedUnder.of_frequently_ge (a := a)
    exact (ha.and_frequently h).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x
  refine (le_limsup_iff h₄ h₂).2 fun y y_v ↦ ?_
  have := (le_liminf_iff h₃ h₁).1 (le_refl (liminf u f)) y y_v
  exact (h.and_eventually this).mono fun x ⟨ux_vx, y_ux⟩ ↦ y_ux.trans_le ux_vx

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
⊢ ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e

Tactic:
use (s, s)

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
⊢ ∀ (b : Finset β × Finset β), (s, s) ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

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

Tactic:
by
  refine Iff.trans ?_ (range k).hasProd_compl_iff
  rw [← (notMemRangeEquiv k).symm.hasProd_iff, Function.comp_def, coe_notMemRangeEquiv_symm]

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

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n ↦ f ↑n) g
hf₂ : HasProd (fun n ↦ f (-↑n)) g'
⊢ HasProd (fun n ↦ f (-(↑n + 1))) (g' / f 0)

Tactic:
← hasProd_nat_add_iff' 1,

Goal state after:
G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n ↦ f ↑n) g
hf₂ : HasProd (fun n ↦ f (-↑(n + 1))) (g' / ∏ i ∈ range 1, f (-↑i))
⊢ HasProd (fun n ↦ f (-(↑n + 1))) (g' / f 0)
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
⊢ ∏' (y : β), extend g f 1 y = ∏' (x : γ), f x

Tactic:
← hg.tprod_eq this,

Goal state after:
α : 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
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith K₁ fun a ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
this : ¬Bornology.IsBounded (image2 f s {b})
⊢ ¬Bornology.IsBounded (image2 f s t)

Tactic:
exact mt (IsBounded.subset · (image2_subset subset_rfl (singleton_subset_iff.mpr hb))) this

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 : ℕ
hMl : M < l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
hMl' : (take M l).length = M
⊢ zipWith d (x :: take M l) (take M l ++ [(x :: l)[M + 1]]) = zipWith d (x :: take M l) (take M (l ++ [y]) ++ [l[M]])

Tactic:
take_append_of_le_length hMl.le,

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 : ℕ
hMl : M < l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
hMl' : (take M l).length = M
⊢ zipWith d (x :: take M l) (take M l ++ [(x :: l)[M + 1]]) = zipWith d (x :: take M l) (take M l ++ [l[M]])
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

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

Tactic:
rw [uniformContinuous₂_def, AbstractCompletion.extend₂, uncurry_curry]

Goal state after:
α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous ((pkg.prod pkg').extend (uncurry f))
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs' : (take (M + 1) L).sum + (drop (M + 1) L).sum ≤ (take (M + 1) L).sum + (take (M + 1) L).sum
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum

Tactic:
add_le_add_iff_left,

Goal state after:
case refine_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs' : (drop (M + 1) L).sum ≤ (take (M + 1) L).sum
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
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)
x y : X
n : ℕ
h : ∃ n, (x, y) ∉ U n
⊢ (∃ m ≤ n, (x, y) ∉ U m) ↔ (x, y) ∉ U n

Tactic:
exact ⟨fun ⟨m, hmn, hm⟩ hn => hm (hB.antitone hmn hn), fun h => ⟨n, le_rfl, h⟩⟩

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (Dilation.id α) = 1

Tactic:
refine (ratio_unique hne.1 hne.2 ?_).symm

Goal state after:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ edist ((Dilation.id α) x) ((Dilation.id α) y) = ↑1 * edist x y
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
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
⊢ edist (e x) (e y) = 0 ∨ edist (e x) (e y) = ∞

Tactic:
refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
h : edist x y = 0
⊢ edist (e x) (e y) = 0

case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
h : edist x y = ∞
⊢ edist (e x) (e y) = ∞
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: x : ℝ≥0
⊢ ↑‖↑x‖₊ = ↑x

Tactic:
simp [nnnorm]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : IsBoundedSMul α β
r : α
x : β
h : r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
simp [h, zero_smul α x]

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 : β
ε : ℝ
⊢ (fun x ↦ s • x) '' (closedBall x ε \ ball x ε) = closedBall (s • x) (‖s‖ * ε) \ ball (s • x) (‖s‖ * ε)

Tactic:
Set.image_sdiff (smul_right_injective β hs),

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
⊢ (fun x ↦ s • x) '' closedBall x ε \ (fun x ↦ s • x) '' ball x ε =
    closedBall (s • x) (‖s‖ * ε) \ ball (s • x) (‖s‖ * ε)
Module: Mathlib.Data.Prod.TProd

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

Tactic:
simp [TProd.elim, hji]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ∀ (s : Set α), s = ∅ ∨ s = univ → sᶜ = ∅ ∨ sᶜ = univ

Tactic:
simp +contextual [or_imp]

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

Goal state before:
pp: α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
⊢ (m₁ ⊔ m₂) s = max (m₁ s) (m₂ s)

Tactic:
have := iSup_apply (fun b => cond b m₁ m₂) s

Goal state after:
α : 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)
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
m : OuterMeasure β
s : Set β
⊢ f '' f ⁻¹' s = Subtype.val '' Subtype.val ⁻¹' s

Tactic:
by simp only [image_preimage_eq_inter_range, Subtype.range_coe]

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ ∀ (a : δ), Measurable fun x ↦ uniqueElim x a

Tactic:
Unique.forall_iff,

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ Measurable fun x ↦ uniqueElim x default
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
⊢ ∃ β x sgn g,
    (∀ (b : β), g b ∉ s → sgn b = 0) ∧ Fintype.card β = n ∧ ∀ a ∈ s, (∑ i, if g i = a then ↑(sgn i) else 0) = f a

Tactic:
refine
    ⟨β ⊕ (Fin (n - ∑ i ∈ s, (f i).natAbs)), inferInstance, Sum.elim sgn 0,
      Sum.elim g (Classical.arbitrary (Fin (n - Finset.sum s fun i => Int.natAbs (f i)) → α)),
        ?_, by simp [hβ, h], fun a ha => by simp [hf _ ha]⟩

Goal state after:
α : Type u
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
⊢ ∀ (b : β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs)),
    Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) b ∉ s → Sum.elim sgn 0 b = 0
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
by
  convert! (continuous_algebraMap ℚ≥0 𝕜).continuousAt.tendsto.comp tendsto_inv_atTop_nhds_zero_nat
  rw [map_zero]

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
⊢ ∀ a' ∈ Ioo 0 (liminf u f), ∀ b' ∈ Ioo 0 (liminf v f), a' * b' ≤ liminf (fun x ↦ u x * v x) f

Tactic:
refine fun a ha b hb ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ioo 0 (liminf u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
⊢ ∀ᶠ (a : α) in f, c < u a * v a
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: a c : ℝ
ha : a ≠ 0
⊢ Tendsto (fun x ↦ (a * x + c)⁻¹) atTop (𝓝 0)

Tactic:
obtain ha' | ha' := lt_or_gt_of_ne ha

Goal state after:
case inl
a c : ℝ
ha : a ≠ 0
ha' : a < 0
⊢ Tendsto (fun x ↦ (a * x + c)⁻¹) atTop (𝓝 0)

case inr
a c : ℝ
ha : a ≠ 0
ha' : 0 < a
⊢ Tendsto (fun x ↦ (a * x + c)⁻¹) atTop (𝓝 0)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)

Tactic:
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]
  refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds
    (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_
  simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2

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

Goal state before:
pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ c ^ n * u 0 < u n

Tactic:
by
  apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_le_of_lt hn _ _ h
  · simp
  · simp [_root_.pow_succ', mul_assoc]

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

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
⊢ m (f '' (fun k ↦ f ⁻¹' t k) n) ≤ m (t n)

Tactic:
rcases h with hl | hr

Goal state after:
case refine_2.inl
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
hl : Monotone m
⊢ m (f '' (fun k ↦ f ⁻¹' t k) n) ≤ m (t n)

case refine_2.inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
hr : Surjective f
⊢ m (f '' (fun k ↦ f ⁻¹' t k) n) ≤ m (t n)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ᶜ ∪ s₂ᶜ)

Tactic:
exact isCaratheodory_union _ (isCaratheodory_compl _ h₁) (isCaratheodory_compl _ h₂)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = ⨅ t, μ ↑t

Tactic:
by
  simp_rw [iInf_subtype, iInf_and, ← measure_eq_iInf]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ π i ∪ {univ}

Tactic:
exact subset_union_left

Goal state after: