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 β := {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
d : β
⊢ d ∈ t → x c ≠ x d → Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))

Tactic:
hd

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
d : β
hd : d ∈ t
⊢ x c ≠ x d → Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_nonempty : t.Nonempty
⊢ s ∈ atBot

Tactic:
· have := h_nonempty.nonempty
    obtain ⟨a, ha⟩ := ht.exists_isLeast h_nonempty
    obtain ⟨b, hb⟩ := exists_lt a
    exact Filter.mem_atBot_sets.mpr ⟨b, fun b' hb' ↦ hts <| Classical.byContradiction
      fun hc ↦ LT.lt.false <| hb'.trans_lt <| hb.trans_le <| ha.2 (not_notMem.mp hc)⟩

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
y : α
hy : y ∈ Icc a b
⊢ y ∈ s

Tactic:
have : IsClosed (s ∩ Icc y b) := by
    suffices s ∩ Icc y b = s ∩ Icc a b ∩ Icc y b from this ▸ hs.inter isClosed_Icc
    grind [Icc_subset_Icc_left, inter_eq_self_of_subset_right, inter_assoc]

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
y : α
hy : y ∈ Icc a b
this : IsClosed[inst✝²] (s ∩ Icc y b)
⊢ y ∈ s
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
f : Filter E
⊢ Disjoint (𝓝 1) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖

Tactic:
simpa using disjoint_nhds 1 f

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
by
  refine hf.exists_forall_le' (x₀ := x₀) ?_
  have hU : {x : β | f x₀ < f x} ∈ Filter.cocompact β := by
    refine Filter.mem_cocompact'.mpr ⟨_, ?_, fun ⦃_⦄ a ↦ a⟩
    simp only [Set.compl_ofPred, not_lt]
    exact Metric.isCompact_of_isClosed_isBounded (isClosed_le (by fun_prop) (by fun_prop)) h
  filter_upwards [hU] with x hx using hx.le

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
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
by
  refine continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono hs fun b hb => ?_
  rcases (mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset hb).1 hfs with ⟨b', ⟨hab', hbb'⟩, hb'⟩
  rcases exists_between hab' with ⟨c', hc'⟩
  rcases mem_closure_iff.1 (hb' ⟨hc'.1.le, hc'.2⟩) (Ioo (f a) b') isOpen_Ioo hc' with
    ⟨_, hc, ⟨c, hcs, rfl⟩⟩
  exact ⟨c, hcs, hc.1, hc.2.trans_le hbb'⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (x : β) in map f l, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ False

Tactic:
eventually_map

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) (f a) b
⊢ False
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f

Tactic:
eventually_map

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((g ∘ f) a) c
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ ∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x c

Tactic:
eventually_map

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (max (u a) (v a)) c
⊢ ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (u a) c
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ ∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x c

Tactic:
eventually_map

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (max (u a) (v a)) c
⊢ ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (v a) c
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in Filter.map (fun a ↦ s.sup' hs fun i ↦ F i a) f, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ ∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 ↦ x1 ≤ x2) x c

Tactic:
eventually_map

Goal state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (s.sup' hs fun i ↦ F i a) c
⊢ ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (F i a) c
Module: Mathlib.Order.LiminfLimsup

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

Tactic:
by
  rw [liminf, map_top, limsInf_principal_eq_csSup hu (range_nonempty _), sInf_range]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
⊢ liminf (fun i ↦ f (i + k)) atTop = liminf f atTop

Tactic:
← Function.comp_def,

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
⊢ liminf (f ∘ fun i ↦ i + k) atTop = liminf f atTop
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
⊢ ∀ᶠ (n : ι) in cofinite, u n r ≤ b'

Tactic:
have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b)

Goal state after:
case inl
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b
⊢ ∀ᶠ (n : ι) in cofinite, u n r ≤ b'
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ (↑x✝ * ⊥).toReal = (↑x✝).toReal * ⊥.toReal

Tactic:
| pos_bot _ h =>

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

Goal state before:
pp: case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊥ = -(↑x✝ * ⊥)

Tactic:
| pos_bot _ h =>

Goal state after:
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 : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this✝ : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
j : Subtype p
hj : j ∈ m
this : j = liminfReparam f s p j
⊢ ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
apply subset_iUnion _ j

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∏ b ∈ t, f b = ∏ b ∈ (↑s ∩ L.support).toFinset, f b

Tactic:
apply Finset.prod_congr_of_eq_on_inter <;> grind

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
⊢ ∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b) = ∏' (b : β), m (s b)

Tactic:
by
  rw [← tprod_extend_one (@encode_injective β _)]
  refine tprod_congr fun n ↦ ?_
  rcases em (n ∈ Set.range (encode : β → ℕ)) with ⟨a, rfl⟩ | hn
  · simp [encode_injective.extend_apply]
  · rw [extend_apply' _ _ _ hn]
    rw [← decode₂_ne_none_iff, ne_eq, not_not] at hn
    simp [hn, m0]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommGroup α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsTopologicalGroup α
inst✝² : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ a₁ < a₂

Tactic:
have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩

Goal state after:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommGroup α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsTopologicalGroup α
inst✝² : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
this : update f i 1 ≤ update g i 1
⊢ a₁ < a₂
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (f ∘ Subtype.val) a
hb : HasProd (f ∘ Subtype.val) b
⊢ HasProd (f ∘ Subtype.val) (a * b)

Tactic:
rw [hasProd_subtype_iff_mulIndicator] at *

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd ((s ∪ t).mulIndicator f) (a * b)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
⊢ (if L.HasSupport ∧ ∅.Finite then finprod (L.support.mulIndicator fun x ↦ 1)
    else if HasProd (fun x ↦ 1) 1 L then 1 else Exists.choose ⋯) =
    1

Tactic:
Set.mulIndicator_one,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
⊢ (if L.HasSupport ∧ ∅.Finite then ∏ᶠ (x : β), 1 else if HasProd (fun x ↦ 1) 1 L then 1 else Exists.choose ⋯) = 1
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
this : Tendsto ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) (Filter.map (⇑sumEquiv) atTop) (𝓝 (a * b))
⊢ HasProd f (a * b)

Tactic:
simpa [Tendsto, ← Filter.map_map] using! this

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ Nonempty (CauchyFilter α) ↔ Nonempty α

Tactic:
constructor <;> rintro ⟨c⟩
  · have := eq_univ_iff_forall.1 isDenseEmbedding_pureCauchy.isDenseInducing.closure_range c
    obtain ⟨_, ⟨_, a, _⟩⟩ := mem_closure_iff.1 this _ isOpen_univ trivial
    exact ⟨a⟩
  · exact ⟨pureCauchy c⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
Kf : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith Kf fun x ↦ max a (f x)

Tactic:
simpa only [max_comm] using hf.max_const a

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂

Tactic:
by
  simp only [edist_nndist]
  norm_cast
  apply nndist_mul_mul_le

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
⊢ CauchySeq fun n ↦ ∏ k ∈ range (n + 1), u k

Tactic:
show (fun n => ∏ k ∈ range (n + 1), u k) = d * fun n => ∏ k ∈ range (n + 1), v k
      by ext n; simp [d]

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
⊢ CauchySeq (d * fun n ↦ ∏ k ∈ range (n + 1), v k)
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (x : ℝ) in map (Norm.norm ∘ g) l, (fun x1 x2 ↦ x1 ≤ x2) x C
⊢ Tendsto (fun x ↦ op (f x) (g x)) l (𝓝 1)

Tactic:
eventually_map

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
⊢ Tendsto (fun x ↦ op (f x) (g x)) l (𝓝 1)
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ (f i, TProd.mk l f) ∈ t i ×ˢ Set.tprod l t ↔ f ∈ {i_1 | i_1 ∈ i :: l}.pi t

Tactic:
mem_pi,

Goal state after:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ (f i, TProd.mk l f) ∈ t i ×ˢ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 ∈ {i_2 | i_2 ∈ i :: l} → f i_1 ∈ t i_1
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
⊢ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t = {i_1 | i_1 ∈ i :: l}.pi t

Tactic:
by
    ext f
    have h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ i : ι, i ∈ l → f i ∈ t i := by
      change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ { x | x ∈ l }.pi t
      rw [mk_preimage_tprod l t]
    -- `simp [Set.TProd, TProd.mk, this]` can close this goal but is slow.
    rw [Set.tprod, TProd.mk, mem_preimage, mem_pi, prodMk_mem_set_prod_eq]
    simp_rw [mem_ofPred_eq, mem_cons]
    rw [forall_eq_or_imp, and_congr_right_iff]
    exact fun _ => h

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

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ b, f b)

Tactic:
← iUnion_congr_of_surjective _ he (fun _ => rfl)

Goal state after:
case inr
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ x, f (e x))
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

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

Tactic:
refine ⟨fun hf n ↦ hf <| measurableSet_singleton _, fun h ↦ measurable_to_countable' fun n ↦ ?_⟩
  cases n with
  | top =>
    rw [← WithTop.none_eq_top, ← compl_range_some, preimage_compl, ← iUnion_singleton_eq_range,
      preimage_iUnion]
    exact .compl <| .iUnion h
  | coe n => exact h n

Goal state after:
Module: Mathlib.Data.Real.ENatENNReal

Goal state before:
pp: n : ℕ∞
⊢ ↑n = 0 ↔ n = 0

Tactic:
← toENNReal_zero,

Goal state after:
n : ℕ∞
⊢ ↑n = ↑0 ↔ n = 0
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
⊢ c • m ∅ = 0

Tactic:
simp only [measure_empty]

Goal state after:
α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
⊢ c • 0 = 0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.zero
⊢ Decidable (zero ≤ zero)

Tactic:
exact isTrue (by constructor)

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

Goal state before:
pp: case zero.neg
⊢ Decidable (zero ≤ neg)

Tactic:
exact isTrue (by constructor)

Goal state after:
case zero.neg
⊢ Decidable (zero ≤ neg)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.pos
⊢ Decidable (zero ≤ pos)

Tactic:
exact isTrue (by constructor)

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

Goal state before:
pp: case neg.zero
⊢ Decidable (neg ≤ zero)

Tactic:
exact isTrue (by constructor)

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

Goal state before:
pp: case neg.neg
⊢ Decidable (neg ≤ neg)

Tactic:
exact isTrue (by constructor)

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

Goal state before:
pp: case neg.pos
⊢ Decidable (neg ≤ pos)

Tactic:
exact isTrue (by constructor)

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

Goal state before:
pp: case pos.zero
⊢ Decidable (pos ≤ zero)

Tactic:
exact isTrue (by constructor)

Goal state after:
case pos.zero
⊢ Decidable (pos ≤ zero)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos.neg
⊢ Decidable (pos ≤ neg)

Tactic:
exact isTrue (by constructor)

Goal state after:
case pos.neg
⊢ Decidable (pos ≤ neg)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos.pos
⊢ Decidable (pos ≤ pos)

Tactic:
exact isTrue (by constructor)

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n < m
⊢ 1 / (↑m + 1) < 1 / (↑n + 1)

Tactic:
refine one_div_lt_one_div_of_lt ?_ ?_
  · exact Nat.cast_add_one_pos _
  · simpa

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

Goal state before:
pp: α : Type u_4
s : Set α
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Tactic:
obtain (hfin | hinf) := Set.finite_or_infinite s
  · lift s to Finset α using hfin
    simp [tsum_fintype]
  · have : Infinite s := infinite_coe_iff.mpr hinf
    rw [tsum_const_eq_top_of_ne_zero one_ne_zero, encard_eq_top hinf, ENat.toENNReal_top]

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

Goal state before:
pp: case inr.inr.inl.inl
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : a * ⊤ < c
b0 : 0 < ⊤
a0 : a < 0
a' : EReal
aa' : a < a'
a0' : a' < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
rw [mul_top_of_neg a0] at hc

Goal state after:
case inr.inr.inl.inl
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : ⊥ < c
b0 : 0 < ⊤
a0 : a < 0
a' : EReal
aa' : a < a'
a0' : a' < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inr.inr
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
b_top : b < ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
obtain ⟨a', aa', hc'⟩ := exists_between ((lt_div_iff b0 b_top.ne).2 hc)

Goal state after:
case inr.inr.inr
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
b_top : b < ⊤
a' : EReal
aa' : a < a'
hc' : a' < c / b
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
x : ℝ
⊢ ∀ y ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1, ↑x < y.1 * y.2

Tactic:
intro p p_in_prod

Goal state after:
case h.refine_1
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1
⊢ ↑x < p.1 * p.2
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ y ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2

Tactic:
intro p p_in_prod

Goal state after:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2)
⊢ ↑x < p.1 * p.2