mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
s : Subgroup G
hd : ¬Dense ↑s
⊢ Xor (Dense ↑s) (∃ a, s = zpowers a)

Tactic:
else

Goal state after:
G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : LinearOrder G
inst✝⁵ : IsOrderedMonoid G
inst✝⁴ : TopologicalSpace G
inst✝³ : OrderTopology G
inst✝² : MulArchimedean G
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
s : Subgroup G
hd : ¬Dense ↑s
⊢ Xor (Dense ↑s) (∃ a, s = zpowers a)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun i ↦ F i a) ≤ s.sup' hs m

Tactic:
← eventually_all_finset s

Goal state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun i ↦ F i a) ≤ s.sup' hs m
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup fun i ↦ F i a) ≤ s.sup m

Tactic:
← eventually_all_finset s

Goal state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup fun i ↦ F i a) ≤ s.sup m
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot
a✝ : ℝ
hx : ¬↑a✝ = ⊥
hy : ¬⊥ = ⊥
⊢ ¬↑a✝ + ⊥ = ⊤ → ¬↑a✝ = ⊤ ∧ ¬⊥ = ⊤

Tactic:
simp_all only [not_false_eq_true, ne_eq, add_top_of_ne_bot, not_true_eq_false,
    coe_ne_top, and_self, implies_true]

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

Goal state before:
pp: case coe.coe
a✝¹ : ℝ
hx : ¬↑a✝¹ = ⊥
a✝ : ℝ
hy : ¬↑a✝ = ⊥
⊢ ¬↑a✝¹ + ↑a✝ = ⊤ → ¬↑a✝¹ = ⊤ ∧ ¬↑a✝ = ⊤

Tactic:
simp_all only [not_false_eq_true, ne_eq, add_top_of_ne_bot, not_true_eq_false,
    coe_ne_top, and_self, implies_true]

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

Goal state before:
pp: case coe.top
a✝ : ℝ
hx : ¬↑a✝ = ⊥
hy : ¬⊤ = ⊥
⊢ ¬↑a✝ + ⊤ = ⊤ → ¬↑a✝ = ⊤ ∧ ¬⊤ = ⊤

Tactic:
simp_all only [not_false_eq_true, ne_eq, add_top_of_ne_bot, not_true_eq_false,
    coe_ne_top, and_self, implies_true]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddAbove (range u)
⊢ (map u ⊤).limsSup = ⨆ i, u i

Tactic:
map_top,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddAbove (range u)
⊢ (𝓟 (range u)).limsSup = ⨆ i, u i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddBelow (range u)
⊢ (map u ⊤).limsInf = ⨅ i, u i

Tactic:
map_top,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddBelow (range u)
⊢ (𝓟 (range u)).limsInf = ⨅ i, u i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ (map u ⊤).limsSup = ⨆ i, u i

Tactic:
map_top,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ (𝓟 (range u)).limsSup = ⨆ i, u i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ (map u ⊤).limsInf = ⨅ i, u i

Tactic:
map_top,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ (𝓟 (range u)).limsInf = ⨅ i, u i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F

Tactic:
refine le_sInf fun b hb => sInf_le_of_le (mem_image_of_mem _ hb) <| sSup_le ?_

Goal state after:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
b : R
hb : b ∈ {a_1 | ∀ᶠ (n : R) in map a F, n ≤ a_1}
⊢ ∀ b_1 ∈ a '' a ⁻¹' {x | (fun n ↦ n ≤ b) x}, b_1 ≤ b
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, ⨆ i_1, (⇑f)^[(i_1 + i).succ] a = ⨅ n, ⨆ i, (⇑f)^[i + n] a

Tactic:
← Nat.add_succ

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, ⨆ i_1, (⇑f)^[i_1 + i.succ] a = ⨅ n, ⨆ i, (⇑f)^[i + n] a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y z t : EReal
h : x < y
h' : z ≤ t
hz : z ≠ ⊥
ht : t ≠ ⊤
⊢ -t ≠ ⊥

Tactic:
by simp [ht]

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

Goal state before:
pp: this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Filter.map (fun x ↦ Finset.range (x + 1)) atTop = Filter.map Finset.range atTop

Tactic:
apply le_antisymm <;>
      rw [← Tendsto] <;>
      simp only [tendsto_atTop', mem_map, mem_atTop_sets, mem_preimage] <;>
      rintro s ⟨a, ha⟩

Goal state after:
case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s

case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal

pp: case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
⊢ (⊤ * ↑a✝).toENNReal = ⊤.toENNReal * (↑a✝).toENNReal

Tactic:
· rcases eq_or_lt_of_le hx with (hx | hx)
    · simp [← hx]
    · simp_all [mul_top_of_pos hx]

Goal state after:
case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
⊢ (⊤ * ↑a✝).toENNReal = ⊤.toENNReal * (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr.bot
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + z) = ↑x * ⊥ + ↑x * z

Tactic:
cases z

Goal state after:
case inr.bot.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + ⊥) = ↑x * ⊥ + ↑x * ⊥

case inr.bot.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (⊥ + ↑a✝) = ↑x * ⊥ + ↑x * ↑a✝

case inr.bot.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + ⊤) = ↑x * ⊥ + ↑x * ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr.coe
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + z) = ↑x * ↑a✝ + ↑x * z

Tactic:
cases z

Goal state after:
case inr.coe.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + ⊥) = ↑x * ↑a✝ + ↑x * ⊥

case inr.coe.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝¹ a✝ : ℝ
⊢ ↑x * (↑a✝¹ + ↑a✝) = ↑x * ↑a✝¹ + ↑x * ↑a✝

case inr.coe.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + ⊤) = ↑x * ↑a✝ + ↑x * ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr.top
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + z) = ↑x * ⊤ + ↑x * z

Tactic:
cases z

Goal state after:
case inr.top.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + ⊥) = ↑x * ⊤ + ↑x * ⊥

case inr.top.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (⊤ + ↑a✝) = ↑x * ⊤ + ↑x * ↑a✝

case inr.top.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + ⊤) = ↑x * ⊤ + ↑x * ⊤
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 (extend e f 1) a₁
hg : HasProd g a₂
⊢ a₁ ≤ a₂

Tactic:
refine hasProd_le (fun c ↦ ?_) hf hg

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₂
c : κ
⊢ extend e f 1 c ≤ g c
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁵ : CommMonoidWithZero α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : ZeroLEOneClass α
inst✝¹ : PosMulMono α
inst✝ : ClosedIciTopology α
f : ι → α
hf : ∀ (i : ι), 0 ≤ f i
h : Multipliable f L
hbot : L.NeBot
⊢ 0 ≤ ∏'[L] (x : ι), f x

Tactic:
exact h.hasProd.nonneg hf

Goal state after:
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
⊢ (fun x ↦ (∏ b ∈ x, f b) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)) =ᶠ[(SummationFilter.unconditional α).filter] fun s ↦
    ∏ b ∈ s, g b

Tactic:
filter_upwards [eventually_ge_atTop s] with t ht

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
⊢ (∏ b ∈ t, f b) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) = ∏ b ∈ t, g b
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
⊢ HasProd (fun n ↦ f ↑n * f (-↑n)) (m * f 0)

Tactic:
apply (hf.mul (hasProd_ite_eq (0 : ℤ) (f 0))).hasProd_of_prod_eq fun u ↦ ?_

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
⊢ ∃ v, ∀ (v' : Finset ℕ), v ⊆ v' → ∃ u', u ⊆ u' ∧ (∏ x ∈ u', f x * if x = 0 then f 0 else 1) = ∏ b ∈ v', f ↑b * f (-↑b)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : i ∈ ⋃ d, s d
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
j : γ
hj : i ∈ s j
⊢ (mulSupport fun d ↦ (s d).mulIndicator f i) ⊆ {j}

Tactic:
· exact Set.mulSupport_subset_subsingleton_of_disjoint_on_mulSupport f hs i j hj

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

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ (zipWith d (x :: lxy ++ y :: lyz) (lxy ++ y :: lyz ++ [z])).sum =
    (zipWith d (x :: lxy ++ y :: lyz) (lxy ++ [y] ++ (lyz ++ [z]))).sum

pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ (x :: lxy).length = (lxy ++ [y]).length

Tactic:
cons_append,

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 z : X
lxy lyz : List X
⊢ (zipWith d (x :: (lxy ++ y :: lyz)) (lxy ++ y :: lyz ++ [z])).sum =
    (zipWith d (x :: (lxy ++ y :: lyz)) (lxy ++ [y] ++ (lyz ++ [z]))).sum

X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ (x :: lxy).length = (lxy ++ [y]).length
Module: Mathlib.Topology.MetricSpace.Isometry

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

Tactic:
h.symm.preimage_sphere,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ Metric.sphere (h.symm.symm x) r = Metric.sphere (h x) r
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: case refine_2.succ
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n✝ : ℕ
⊢ v (n✝ + 1) ∈ s

Tactic:
· exact s.mul_mem (s.inv_mem (u_in _)) (u_in _)

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

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ (if UniformContinuous f then ⋯.extend f else fun x ↦ f ⋯.some) (pureCauchy a) = f a

Tactic:
if_pos hf

Goal state after:
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pureCauchy a) = f a
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case pos
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (if UniformContinuous f then ⋯.extend f else fun x ↦ f ⋯.some)

Tactic:
if_pos hf

Goal state after:
case pos
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)
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:
by congr

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f g : CauchyFilter α
⊢ (↑f).lim = (↑g).lim ↔ Inseparable f g

Tactic:
by
  rw [← inseparable_iff_eq, inseparable_lim_iff]

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

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ‖a * b * a⁻¹ * b⁻¹ - 1‖₊ ≤ 2 * ‖a‖₊⁻¹ * ‖b‖₊⁻¹ * ‖a - 1‖₊ * ‖b - 1‖₊

Tactic:
by
  simpa using nnnorm_commutator_units_sub_one_le (.mk0 a ha) (.mk0 b hb)

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

Goal state before:
pp: R : Type u_1
r : R
s : ℝ≥0
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0∞
⊢ ↑(r • s) = ↑(r • 1 * s)

Tactic:
smul_mul_assoc,

Goal state after:
R : Type u_1
r : R
s : ℝ≥0
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0∞
⊢ ↑(r • s) = ↑(r • (1 * s))
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: x : ℝ≥0
y : ℝ≥0∞
hx : x ≠ 0
⊢ x • y ≠ ∞ → y ≠ ∞

Tactic:
by rintro h rfl; simp [smul_top (R := ℝ≥0), hx] at h

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ dist p (s • x) < ‖s‖ * ε → ∃ x_1, dist x_1 x < ε ∧ s • x_1 = p

Tactic:
· refine fun h ↦ ⟨s⁻¹ • p, ?_, by simp [smul_smul, hs]⟩
    refine lt_of_mul_lt_mul_of_nonneg_left ?_ (norm_nonneg s)
    rw [← dist_smul₀]
    simpa [smul_smul, hs] using h

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ dist x⁻¹ y⁻¹ = ‖x‖⁻¹ * dist y x * ‖y‖⁻¹

Tactic:
simp [dist_eq_norm, inv_sub_inv' (hs₀ x hx) (hs₀ y hy)]

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
P : Finset (Set α)
hP : P.Nonempty
PC : ↑P ⊆ s
⊢ MeasurableSet (P.sup' hP id)

Tactic:
rw [Finset.sup'_eq_sup, Finset.sup_id_set_eq_sUnion]

Goal state after:
α : Type u_1
s : Set (Set α)
P : Finset (Set α)
hP : P.Nonempty
PC : ↑P ⊆ s
⊢ MeasurableSet (⋃₀ ↑P)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

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

Tactic:
by
  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
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:
by congr

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖

Tactic:
by
  rw [Algebra.algebraMap_eq_smul_one]
  exact norm_smul _ _

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

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

Tactic:
by simp [ht]

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

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
⊢ MeasurableSet (measurableAtom x)

Tactic:
have : ∀ (y : β), y ∉ measurableAtom x → ∃ s, x ∈ s ∧ MeasurableSet s ∧ y ∉ s :=
    fun y hy ↦ by simpa [measurableAtom] using hy
  choose! s hs using this
  have : measurableAtom x = ⋂ (y ∈ (measurableAtom x)ᶜ), s y := by
    apply Subset.antisymm
    · intro z hz
      simp only [mem_iInter, mem_compl_iff]
      intro i hi
      exact mem_of_mem_measurableAtom hz (hs i hi).2.1 (hs i hi).1
    · apply compl_subset_compl.1
      intro z hz
      simp only [compl_iInter, mem_iUnion, mem_compl_iff, exists_prop]
      exact ⟨z, hz, (hs z hz).2.2⟩
  rw [this]
  exact MeasurableSet.biInter (to_countable (measurableAtom x)ᶜ) (fun i hi ↦ (hs i hi).2.1)

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:
by
        rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]
        exact hf₁

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Icc 0 1)
⊢ 0 ≤ 1 - ↑x

Tactic:
simpa using x.2.2

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Ioo 0 1)
⊢ 0 < 1 - ↑x

Tactic:
simpa using x.2.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ (map f) ⊤ = ⊤

Tactic:
map_top,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ (restrict (range f)) ⊤ = ⊤
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ ¬Summable f ↔ ¬¬Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop

Tactic:
Classical.not_not,

Goal state after:
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ ¬Summable f ↔ Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
t : SignType
h : ∀ i ∈ s, sign (f i) = t
⊢ sign (∑ i ∈ s, f i) = t

Tactic:
by
  cases t
  · simp_rw [zero_eq_zero, sign_eq_zero_iff] at h ⊢
    exact Finset.sum_eq_zero h
  · simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h ⊢
    exact Finset.sum_neg h hs
  · simp_rw [pos_eq_one, sign_eq_one_iff] at h ⊢
    exact Finset.sum_pos h hs

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
β : Type u
t : Finset β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
ht : #t = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b ∈ t, if g b = a then ↑(sgn b) else 0) = f a
⊢ Fintype.card ↥t = ∑ a ∈ s, (f a).natAbs

Tactic:
by simp [ht]

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
⊢ sign a = -1 ↔ a < 0

Tactic:
by
  refine ⟨fun h => ?_, fun h => sign_neg h⟩
  rw [sign_apply] at h
  split_ifs at h
  assumption

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

Goal state before:
pp: a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
⊢ ∃ m, ↑a * ↑n ≤ ↑m

Tactic:
by
    obtain ⟨m, an_m⟩ := exists_nat_ge (a * n)
    use m
    rwa [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, ← EReal.coe_mul, EReal.coe_le_coe_iff]

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

Goal state before:
pp: f : ℕ → ℝ≥0
⊢ ¬Summable f ↔ ¬¬Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop

Tactic:
Classical.not_not,

Goal state after:
f : ℕ → ℝ≥0
⊢ ¬Summable f ↔ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ (↑a.toReal⁻¹)⁻¹ = ↑a.toReal

Tactic:
← coe_inv a.toReal⁻¹,

Goal state after:
a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ ↑a.toReal⁻¹⁻¹ = ↑a.toReal
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a * -b⁻¹ ≤ -b⁻¹ * a'

Tactic:
mul_comm (-b⁻¹) a',

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a * -b⁻¹ ≤ a' * -b⁻¹
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_2
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
⊢ HasSum (fun i ↦ (fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1) ↑i) c

Tactic:
simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]

Goal state after: