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

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
⊢ cocompact α ≤ atBot

Tactic:
refine fun _ hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro
  · exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩
  · obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs
    refine ⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩
    exact (not_and_or.mp hx).casesOn (fun h ↦ ht _ (le_of_not_ge h)) (fun h ↦ (h le_top).elim)

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ n.natAbs‖ = ‖a ^ n‖

Tactic:
by
  rw [← zpow_natCast, ← Int.abs_eq_natAbs, norm_zpow_abs]

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
⊢ StrictMonoOn f (Icc a b)

Tactic:
have : Fact (a ≤ b) := ⟨hab⟩

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
⊢ StrictMonoOn f (Icc a b)
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
⊢ ∃ t, k ⊆ t ∧ IsOpen[inst✝] t ∧ Bornology.IsBounded (f '' (t ∩ s))

Tactic:
rcases ((((hasBasis_nhdsSet _).inf_principal _)).disjoint_iff ((basis_sets _).comap _)).1 this
    with ⟨U, ⟨hUo, hkU⟩, t, ht, hd⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst✝] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ ∃ t, k ⊆ t ∧ IsOpen[inst✝] t ∧ Bornology.IsBounded (f '' (t ∩ s))
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
h : ¬Bornology.IsBounded s
⊢ diam s = 0

Tactic:
rw [diam, ediam_of_unbounded h, ENNReal.toReal_top]

Goal state after:
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 β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst✝²] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure[inst✝²] (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b

Tactic:
rcases mem_closure_iff.1 (hb' ⟨hc'.1.le, hc'.2⟩) (Ioo (f a) b') isOpen_Ioo hc' with
    ⟨_, hc, ⟨c, hcs, rfl⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst✝²] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure[inst✝²] (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
c : α
hcs : c ∈ s
hc : f c ∈ Ioo (f a) b'
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: case cons.refine_1
ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = 0
j : ι
hj : j ∈ s
⊢ f j ≠ ∞

pp: case cons.refine_2
ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = ∞
j : ι
hj : j ∈ s
⊢ f j ≠ 0

Tactic:
· exact imp_iff_not_or.2 (hf (by simp) (by simp [hj]) <| .symm <| ne_of_mem_of_not_mem hj hi) hi₀

Goal state after:
case cons.refine_2
ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = ∞
j : ι
hj : j ∈ s
⊢ f j ≠ 0
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ (↑K)⁻¹ * edist (f x) (f y) ≤ edist x y

Tactic:
mul_comm,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ edist (f x) (f y) * (↑K)⁻¹ ≤ edist x y
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = 0 - ↑(-x)

pp: case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x

Tactic:
zero_sub,

Goal state after:
case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = -↑(-x)

case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case symm
x✝ y✝ : EReal
h : (x✝ * y✝).toReal = x✝.toReal * y✝.toReal
⊢ (y✝ * x✝).toReal = y✝.toReal * x✝.toReal

Tactic:
mul_comm,

Goal state after:
case symm
x✝ y✝ : EReal
h : (x✝ * y✝).toReal = x✝.toReal * y✝.toReal
⊢ (y✝ * x✝).toReal = x✝.toReal * y✝.toReal
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : (mulSupport f).Finite
⊢ (if L.HasSupport ∧ True then ∏ᶠ (b : β), f b else if HasProd (fun b ↦ f b) 1 L then 1 else Exists.choose ⋯) =
    ∏ᶠ (b : β), f b

Tactic:
if_pos

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : (mulSupport f).Finite
⊢ ∏ᶠ (b : β), f b = ∏ᶠ (b : β), f b

case pos.hc
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : (mulSupport f).Finite
⊢ L.HasSupport ∧ True
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ∃ j, s ↑j = ∅
⊢ liminf f v =
    if ∃ j, s ↑j = ∅ then sSup univ
    else if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i

pp: case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
⊢ liminf f v =
    if ∃ j, s ↑j = ∅ then sSup univ
    else if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i

Tactic:
· rw [if_pos H]
    rcases H with ⟨j, hj⟩
    simp [hv.liminf_eq_sSup_univ_of_empty j j.2 hj]

Goal state after:
case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
⊢ liminf f v =
    if ∃ j, s ↑j = ∅ then sSup univ
    else if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
⊢ ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f x = ∏ b ∈ v', f (g b)

Tactic:
refine ⟨s.preimage g hg.injOn, fun t ht => ?_⟩
    refine ⟨t.image g ∪ s, Finset.subset_union_right, ?_⟩
    rw [← Finset.prod_image hg.injOn]
    refine (prod_subset subset_union_left ?_).symm
    simp only [Finset.mem_union, Finset.mem_image]
    refine fun y hy hyt => hf y (mt ?_ hyt)
    rintro ⟨x, rfl⟩
    exact ⟨x, ht (Finset.mem_preimage.2 <| hy.resolve_left hyt), rfl⟩

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 : α
s : Finset β
⊢ HasProd f ((∏ b ∈ s, f b) * a) ↔ HasProd f (a * ∏ i ∈ s, f i)

Tactic:
by rw [mul_comm]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd f a₁
hg : HasProd g a₂
⊢ a₁ ≤ a₂

Tactic:
← hasProd_extend_one he

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
⊢ a₁ ≤ a₂
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
i : ℕ
⊢ ∏' (i : ℕ), f i = (∏' (k : ℕ), f (k + i)) * ∏ j ∈ range i, f j

Tactic:
mul_comm,

Goal state after:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
i : ℕ
⊢ ∏' (i : ℕ), f i = (∏ j ∈ range i, f j) * ∏' (k : ℕ), f (k + i)
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ (1 * ∏ i ∈ t \ s, g i) * ∏ i ∈ s, g i = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i

pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ ∏ i ∈ s, f i ≠ 0

Tactic:
one_mul,

Goal state after:
α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ (∏ i ∈ t \ s, g i) * ∏ i ∈ s, g i = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i

α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ ∏ i ∈ s, f i ≠ 0
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ b = x
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ ∀ (b' : β), b' ≠ b → (if b = b' then a b' else 1) = 1

Tactic:
intro b' hb'; simp [hb'.symm]

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

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
⊢ ∏ x ∈ image Nat.cast v' ∪ image Int.negSucc v', f x = ∏ b ∈ v', f ↑b * f (Int.negSucc b)

Tactic:
prod_union,

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
⊢ (∏ x ∈ image Nat.cast v', f x) * ∏ x ∈ image Int.negSucc v', f x = ∏ b ∈ v', f ↑b * f (Int.negSucc b)

case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
⊢ Disjoint (image Nat.cast v') (image Int.negSucc v')
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a : α
h : HasSum f a L
b : α
⊢ HasSum (fun i ↦ f i / b) (a / b) L

Tactic:
simp only [div_eq_mul_inv, h.mul_right b⁻¹]

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

Goal state before:
pp: α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ (∑' (n : A), f n) * ∑' (n : A), g n = ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2

Tactic:
hf.tsum_mul_tsum hg hfg,

Goal state after:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ ∑' (z : A × A), f z.1 * g z.2 = ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ (↑K)⁻¹ * edist x y ≤ edist (f x) (f y)

Tactic:
mul_comm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ edist x y * (↑K)⁻¹ ≤ edist (f x) (f y)
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < (↑K)⁻¹ * ε}
⊢ ↑K * edist (f x.1) (f x.2) < ε

Tactic:
mul_comm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < ε * (↑K)⁻¹}
⊢ ↑K * edist (f x.1) (f x.2) < ε
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 : X
⊢ ⨅ l, (zipWith d (x :: l) (l ++ [y])).sum = ⨅ l, (zipWith d (y :: l) (l ++ [x])).sum

Tactic:
refine reverse_surjective.iInf_congr _ fun l ↦ ?_

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
x y : X
l : List X
⊢ (zipWith d (y :: l.reverse) (l.reverse ++ [x])).sum = (zipWith d (x :: l) (l ++ [y])).sum
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 = Metric.eball (h x) r

Tactic:
by
  rw [← h.preimage_symm, h.symm.preimage_eball, symm_symm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
b : α
f : ↑(Iic b) → β
⊢ range (IicExtend f) = range f

Tactic:
simp only [IicExtend, range_comp f, range_projIic, image_univ]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
⊢ (∃ b, (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)) →
    ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε

Tactic:
· rintro ⟨b, ⟨b_bound, b_lim⟩⟩ ε εpos
    have : ∀ᶠ n in atTop, b n < ε := b_lim.eventually (gt_mem_nhds εpos)
    rcases this.exists with ⟨N, hN⟩
    refine ⟨N, fun m hm n hn => ?_⟩
    calc edist (s m) (s n) ≤ b N := b_bound m n N hm hn
    _ < ε := hN

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 : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ - -b ⊔ -b

Tactic:
← neg_inf,

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ -(-b ⊓ b)
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
z x y : α
⊢ dist (x ⊔ z) (y ⊔ z) ≤ 1 * dist x y

Tactic:
one_mul,

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
z x y : α
⊢ dist (x ⊔ z) (y ⊔ z) ≤ dist x y
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
⊢ edist (1 * b) (a * b⁻¹ * b) = edist a b

Tactic:
one_mul,

Goal state after:
G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
⊢ edist b (a * b⁻¹ * b) = edist a b
Module: Mathlib.Analysis.Normed.Group.Uniform

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

Tactic:
mul_comm,

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

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ ‖x‖₊ * y.toNNReal = ‖x * y‖₊

Tactic:
mul_comm,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ y.toNNReal * ‖x‖₊ = ‖x * y‖₊
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✝ : DilationClass F α β
f : F
s : Set α
⊢ ediam s ≤ ediam (⇑f '' s) * (↑(ratio f))⁻¹

Tactic:
mul_comm,

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ediam s ≤ (↑(ratio f))⁻¹ * ediam (⇑f '' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : Set α
ht : t ∈ supClosure s
⊢ MeasurableSet t

Tactic:
rcases ht with ⟨P, hP, PC, rfl⟩
  rw [Finset.sup'_eq_sup, Finset.sup_id_set_eq_sUnion]
  exact MeasurableSet.sUnion (Finset.countable_toSet P)
    (fun s hs ↦ measurableSet_generateFrom (PC hs))

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ generateFrom {∅} ⊔ generateFrom S = generateFrom S

Tactic:
generateFrom_singleton_empty,

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ ⊥ ⊔ generateFrom S = generateFrom S
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case top
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
⊢ MeasurableSet (f ⁻¹' {⊤})

Tactic:
rw [← WithTop.none_eq_top, ← compl_range_some, preimage_compl, ← iUnion_singleton_eq_range,
      preimage_iUnion]
    exact .compl <| .iUnion h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableEq α
⊢ ∀ (x : α), MeasurableSet {x}

Tactic:
simp_rw [← ofPred_eq_eq_singleton, measurableSet_setOfPred]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableEq α
⊢ ∀ (x : α), Measurable fun n ↦ n = x
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: s : SignType
z : ℤ
hz : Even z
hs : s ≠ 0
⊢ s ^ z = 1

Tactic:
cases s <;> simp_all [Even.neg_one_zpow]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m : ℕ
⊢ ↑(m / 0) ≤ ↑m / ↑0

pp: case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ ↑(m / (n✝ + 1)) ≤ ↑m / ↑(n✝ + 1)

Tactic:
· rw [cast_zero, div_zero, Nat.div_zero, cast_zero]

Goal state after:
case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ ↑(m / (n✝ + 1)) ≤ ↑m / ↑(n✝ + 1)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : 0 < a
⊢ (if 0 < a then 1 else if a < 0 then -1 else 0) = 1

Tactic:
if_pos

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : 0 < a
⊢ 1 = 1

case hc
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : 0 < a
⊢ 0 < a
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : a < 0
⊢ (if a < 0 then -1 else 0) = -1

Tactic:
if_pos

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : a < 0
⊢ -1 = -1

case hc
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : a < 0
⊢ a < 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case symm
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (y✝ * x✝).abs = y✝.abs * x✝.abs

Tactic:
mul_comm,

Goal state after:
case symm
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (y✝ * x✝).abs = x✝.abs * y✝.abs
Module: Mathlib.Data.EReal.Inv

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

Tactic:
mul_comm,

Goal state after:
case symm
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ sign (y✝ * x✝) = sign x✝ * sign y✝
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ 1 = 1 * sign ↑x✝

Tactic:
one_mul,

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ 1 = sign ↑x✝