mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
i : PseudoMetricSpace (α × β) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun x y ↦ max (dist x.1 y.1) (dist x.2 y.2)) ⋯ ⋯
s : Set (α × β)
⊢ (∀ᶠ (x : ℝ) in atTop, ∀ x_1 ∈ s, ∀ x_3 ∈ s, max (dist x_1.1 x_3.1) (dist x_1.2 x_3.2) ≤ x) ↔
    ∀ᶠ (C : ℝ) in atTop, ∀ ⦃x : α × β⦄, x ∈ s → ∀ ⦃y : α × β⦄, y ∈ s → dist x y ≤ C

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
x' : α
y' : β
hr : 0 < dist x' x.1
⊢ dist y' x.2 ≤ dist x' x.1 ↔ dist y' x.2 ≤ dist x' x.1

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case inr.inr.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
x' : α
y' : β
hr : 0 < dist y' x.2
⊢ dist x' x.1 ≤ dist y' x.2 ↔ dist x' x.1 ≤ dist y' x.2

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ (closure[inst✝³] (Iio a))ᶜ = Ioi a

Tactic:
closure_Iio' ha,

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ (Iic a)ᶜ = Ioi a
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : BddAbove (range f)
h✝ : Nonempty γ
⊢ f '' S ⊆ range f

Tactic:
grind

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

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
⊢ False

Tactic:
have ha : a ∈ s := by simp [s, *]

Goal state after:
α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
⊢ False
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
i : α
hic : i < c
j : α
hj : j ∈ s
hij : i < j
hjc : j ≤ c
⊢ ∀ a_1 ∈ (Icc a j)ᶜ, a_1 ∈ Icc a b → a_1 ∈ Ioi i

Tactic:
grind

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

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝¹ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
x✝ : Icc a c ∈ f
⊢ Icc a c ⊆ Iio x

Tactic:
grind

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

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝ : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this : Icc a c ∉ f
⊢ a ≤ x

Tactic:
grind

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

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝ : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this : Icc a c ∉ f
h : b < x
⊢ Icc a b ⊆ Iio x

Tactic:
grind

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

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝² : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this✝¹ : Icc a c ∉ f
this✝ : x ∈ Icc a b
this : Icc a x ∈ f
⊢ ∀ a_1 ∈ (Iio x)ᶜ, a_1 ∈ Icc a x → a_1 ∈ {x}

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ dist (Pi.single i a) (Pi.single j b) = max (dist a 0) (dist b 0)

Tactic:
by
  simp only [dist_nndist, nndist_single_single i j a b h, NNReal.coe_max]

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h✝ : ∃ b, d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
n : ℕ
⊢ d < u n

Tactic:
grind

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

Goal state before:
pp: q : ℚ≥0
⊢ NNReal.mk ↑q ⋯ = ↑q

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
bdd : BddAbove (range g)
⊢ f (sSup (range fun i ↦ g i)) = ⨆ i, f (g i)

Tactic:
Monotone.map_csSup_of_continuousAt Cf Mf (range_nonempty g) bdd,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
bdd : BddAbove (range g)
⊢ sSup (f '' range g) = ⨆ i, f (g i)
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun n ↦ nndist (u n) (u N)
n : ℕ
h : N ≤ n
⊢ dist (u n) (u N) < ↑R + 1

Tactic:
exact lt_of_lt_of_le (hN _ h) (le_add_of_nonneg_left R.2)

Goal state after:
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 = dist (f x) (f y)

Tactic:
rfl

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
f : α → α
hf : ContinuousOn f (Icc a b)
hle : a ≤ b
h_surj : SurjOn f (Icc a b) (Icc a b)
x₀ : α
hx₀ : x₀ ∈ Icc a b ∧ f x₀ = a
x₁ : α
hx₁ : x₁ ∈ Icc a b ∧ f x₁ = b
⊢ f x₀ ≤ x₀

Tactic:
grind

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
f : α → α
hf : ContinuousOn f (Icc a b)
hle : a ≤ b
h_surj : SurjOn f (Icc a b) (Icc a b)
x₀ : α
hx₀ : x₀ ∈ Icc a b ∧ f x₀ = a
x₁ : α
hx₁ : x₁ ∈ Icc a b ∧ f x₁ = b
⊢ x₁ ≤ f x₁

Tactic:
grind

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 : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atTop
y : δ
hy : y ∈ Ioi (f a)
this : y ∈ f '' Ici a
⊢ y ∈ f '' Ioi a

Tactic:
grind

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 : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atBot
y : δ
hy : y ∈ Iio (f a)
this : y ∈ f '' Ici a
⊢ y ∈ f '' Ioi a

Tactic:
grind

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 : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atBot
y : δ
hy : y ∈ Iio (f a)
this : y ∈ f '' Iic a
⊢ y ∈ f '' Iio a

Tactic:
grind

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 : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atTop
y : δ
hy : y ∈ Ioi (f a)
this : y ∈ f '' Iic a
⊢ y ∈ f '' Iio a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atTop ↔ Tendsto (Int.cast ∘ f) l atTop

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atBot ↔ Tendsto (Int.cast ∘ f) l atBot

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
⊢ Tendsto (fun x ↦ dist (f x) c) l atTop ↔ Tendsto ((fun x ↦ dist x c) ∘ f) l atTop

Tactic:
Function.comp_def

Goal state after:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
⊢ Tendsto (fun x ↦ dist (f x) c) l atTop ↔ Tendsto (fun x ↦ dist (f x) c) l atTop
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atTop ↔ Tendsto (Rat.cast ∘ f) l atTop

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atBot ↔ Tendsto (Rat.cast ∘ f) l atBot

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x ↦ f x • r) l atTop

Tactic:
by simpa using hf.atBot_zsmul_const (neg_pos.2 hr)

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ I ⊔ J ≠ ⊥

Tactic:
grind

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

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

Tactic:
rfl

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

Goal state before:
pp: case mpr.top
h : ⊤ ≠ ⊥
⊢ ⊤ + ⊤ = ⊤

Tactic:
rfl

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

Goal state before:
pp: x : EReal
⊢ x + ⊤ = ⊤ ↔ x ≠ ⊥

Tactic:
by rw [add_comm, top_add_iff_ne_bot]

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

Goal state before:
pp: x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h'y : ↑y ≠ ⊥
⊢ (↑x + ↑y).toReal = (↑x).toReal + (↑y).toReal

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ i, ⨆ a ∈ Ici i, u a = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
rfl

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

Goal state before:
pp: case inl
x : ℝ≥0
⊢ ↑↑x = ↑↑x

Tactic:
rfl

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

Goal state before:
pp: x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h'y : ↑y ≠ ⊥
⊢ (↑x - ↑y).toReal = (↑x).toReal - (↑y).toReal

Tactic:
rfl

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

Goal state before:
pp: a b c d : EReal
h1 : c ≠ ⊥ ∨ d ≠ ⊤
h2 : c ≠ ⊤ ∨ d ≠ ⊥
⊢ a + b + (-c + -d) = a + -c + (b + -d)

Tactic:
grind

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x ↦ (f x, g x)) t

Tactic:
rcases hf x with ⟨Kf, t₁, h₁t, hfL⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x ↦ (f x, g x)) t
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ {x | {n | p n ∧ x ∈ (s n)ᶜ}.Infinite} = {x | {n | p n ∧ x ∉ s n}.Finite}ᶜ

Tactic:
rfl

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

Goal state before:
pp: x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : ¬y = ⊤
hxy : ¬x = y
⊢ x < y

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Encodable.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
⊢ (Disjoint on fun i ↦ ⋃ b ∈ decode₂ β i, f b) i j

Tactic:
refine disjoint_left.mpr fun x => ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ x ∈ (fun i ↦ ⋃ b ∈ decode₂ β i, f b) i → x ∉ (fun i ↦ ⋃ b ∈ decode₂ β i, f b) j
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: case pos
α : Type u_3
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h✝ : Nonempty α
h : IsDirectedOrder α
⊢ Tendsto Finset.Iic atTop atTop

Tactic:
refine tendsto_atTop_atTop.mpr fun s ↦ ?_
    obtain ⟨a, ha⟩ := Finset.exists_le s
    exact ⟨a, fun b hb c hc ↦ by simpa using (ha c hc).trans hb⟩

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

Goal state before:
pp: α : Type u_3
i : α
⊢ ∀ᶠ (s : Finset α) in atTop, i ∈ s

Tactic:
(Tactic.simpa
 "simpa"
 []
 []
 (Tactic.simpaArgsRest
  (Tactic.optConfig [])
  []
  []
  []
  ["using"
   (Term.app
    `eventually_finset_atTop_subset
    [(choice
      («term{_}» "{" [`i] "}")
      (Term.structInst
       "{"
       []
       (Term.structInstFields [(Term.structInstField (Term.structInstLVal `i []) [])])
       (Term.optEllipsis [])
       []
       "}"))])]))

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Infinite α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun s ↦ f s.card) atTop l ↔ Tendsto (f ∘ Finset.card) atTop l

Tactic:
rfl

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun s ↦ f s.card) atTop l ↔ Tendsto (f ∘ Finset.card) atTop l

Tactic:
rfl

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

Goal state before:
pp: case top_top
⊢ -⊤ * ⊤ = -(⊤ * ⊤)

Tactic:
rfl

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

Goal state before:
pp: case top_bot
⊢ -⊤ * ⊥ = -(⊤ * ⊥)

Tactic:
rfl

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
c : γ
hc : c ∉ range ⇑f
hc' : c ∈ (L.map f).support
this : ∃ x, Finset.map f x ∈ {x | (fun s ↦ c ∈ s) x}
⊢ c ∈ ⇑f '' L.support

Tactic:
grind

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
c : γ
hc : c ∉ range ⇑f
⊢ c ∈ ⇑f '' L.support → c ∈ (L.map f).support

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.HasSupport
f : β ↪ γ
h : L.NeBot
a : Finset β
⊢ ↑a ⊆ L.support → ↑a ⊆ ⇑f ⁻¹' ⇑f '' L.support

Tactic:
grind

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

Goal state before:
pp: a b : EReal
⊢ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Tactic:
rfl

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

Goal state before:
pp: case mk
β : Type u_4
inst✝² : Finite β
this : Fintype β
F : Filter (Finset β)
inst✝¹ : { filter := F }.LeAtTop
inst✝ : { filter := F }.NeBot
hL' : ∅ ∉ F
hAtTop : True
hL : F ≤ pure Finset.univ
⊢ ∀ s ∈ F, Finset.univ ∈ s

Tactic:
contrapose! hL'

Goal state after:
case mk
β : Type u_4
inst✝² : Finite β
this : Fintype β
F : Filter (Finset β)
inst✝¹ : { filter := F }.LeAtTop
inst✝ : { filter := F }.NeBot
hAtTop : True
hL : F ≤ pure Finset.univ
hL' : ∃ s ∈ F, Finset.univ ∉ s
⊢ ∅ ∈ F
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
rfl

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

Goal state before:
pp: 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

Tactic:
simp only [and_true]

Goal state after:
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
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case e_s
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : Fintype β
f : β → α
L : SummationFilter β
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s | b ∉ s} ∈ L.filter
s : Finset β
hs : ∀ i ∈ L.support, i ∈ s
hs' : ∀ i ∉ L.support, i ∉ s
⊢ s = L.support.toFinset

Tactic:
grind

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

Goal state before:
pp: case h₁
α : 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}
⊢ ∀ a ∈ t, a ∉ (↑s ∩ L.support).toFinset → f a = 1

Tactic:
grind

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

Goal state before:
pp: case h₂
α : 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}
⊢ ∀ a ∈ (↑s ∩ L.support).toFinset, a ∉ t → f a = 1

Tactic:
grind

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

Goal state before:
pp: case h
α : 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}
⊢ ∀ a ∈ t, a ∈ (↑s ∩ L.support).toFinset → f a = f a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
ht : Multipliable fun a ↦ f ↑a
t' : Finset ↑t
x✝¹ : { x // x ∈ t }
x✝ : x✝¹ ∈ t'
⊢ ?m.138 ↑x✝¹ = f ↑x✝¹

Tactic:
rfl

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s) → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
obtain ⟨o, ho, o_closed, oe⟩ := exists_mem_nhds_isClosed_subset he
    obtain ⟨s, hs⟩ := vanish o ho
    refine ⟨s, fun t hts ↦ oe ?_⟩
    by_cases ht : Multipliable fun a : t ↦ f a
    · classical
      refine o_closed.mem_of_tendsto ht.hasProd (Eventually.of_forall fun t' ↦ ?_)
      rw [← prod_subtype_map_embedding fun _ _ ↦ by rfl]
      apply hs
      simp_rw [Finset.mem_map]
      rintro _ ⟨b, -, rfl⟩
      exact hts b.prop
    · exact tprod_eq_one_of_not_multipliable ht ▸ mem_of_mem_nhds ho

Goal state after: