mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
hq : p' ∈ s
⊢ a p' ∈ J * (↑⟨p', hq⟩).asIdeal

Tactic:
convert! sub_mem H₁ H₂

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
hq : p' ∈ s
⊢ a p' = ∑ p ∈ s, a p - ∑ q ∈ s \ {p'}, a q
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedEBall x ε = univ
⊢ ∀ ε > 0, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, closedEBall x ε

Tactic:
simpa only [univ_subset_iff] using hs

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 : (Ioi a).Nonempty
⊢ frontier (Ioi a) = {a}

Tactic:
simp [frontier, closure_Ioi' ha]

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsClosed[inst✝³] (Ico a b)

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsClosed[inst✝³] (Ioc a b)

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsClosed[inst✝³] (Ioo a b)

Tactic:
simp_all

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
⊢ False

Tactic:
have : x ∈ Icc a b := ⟨by grind, le_of_not_gt fun h ↦ hxf (mem_of_superset hfab (by grind))⟩

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
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
⊢ False
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v (N^[x✝] 0) < v (N^[x✝ + 1] 0)

Tactic:
rw [iterate_succ_apply']

Goal state after:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v (N^[x✝] 0) < v (N (N^[x✝] 0))
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ N^[x✝] 0 < N^[x✝ + 1] 0

Tactic:
rw [iterate_succ_apply']

Goal state after:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ N^[x✝] 0 < N (N^[x✝] 0)
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
hnonempty : (Ioo y x ∩ s).Nonempty
hx : IsLUB (Ioo y x ∩ s) x
⊢ ∀ (a : ℕ → α),
    (StrictMono a ∧ (∀ (n : ℕ), a n < x) ∧ Tendsto a atTop (𝓝 x) ∧ ∀ (n : ℕ), a n ∈ Ioo y x ∩ s) →
      StrictMono a ∧ (∀ (n : ℕ), a n ∈ Ioo y x ∩ s) ∧ Tendsto a atTop (𝓝 x)

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
⊢ ∀ (a : ℕ → α),
    StrictMono a ∧ (∀ (n : ℕ), a n ∈ Ioo ⋯.choose x ∩ s) ∧ Tendsto a atTop (𝓝 x) →
      StrictMono a ∧ (∀ (n : ℕ), a n ∈ Iio x ∩ s) ∧ Tendsto a atTop (𝓝 x)

Tactic:
simp_all

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

Goal state before:
pp: case inl
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
f : ι → F
hf : Surjective f
g : F → E
h : IsEmpty F
this : IsEmpty ι
⊢ ‖g ∘ f‖ = ‖g‖

Tactic:
simp [Subsingleton.elim g 1]

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

Goal state before:
pp: case inr
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
f : ι → F
hf : Surjective f
g : F → E
h : Nonempty F
⊢ ‖g ∘ f‖ = ‖g‖

Tactic:
apply le_antisymm (pi_norm_comp_le' g f)

Goal state after:
case inr
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
f : ι → F
hf : Surjective f
g : F → E
h : Nonempty F
⊢ ‖g‖ ≤ ‖g ∘ f‖
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsCompact (Ico a b)

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsCompact (Ioc a b)

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsCompact (Ioo a b)

Tactic:
simp_all

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
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this : IsClosed[instTopologicalSpace] (⇑ofDual ⁻¹' s ∩ Icc (toDual b) (toDual a))
⊢ toDual b ∈ ⇑ofDual ⁻¹' s

Tactic:
simp_all

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
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this : IsClosed[instTopologicalSpace] (⇑ofDual ⁻¹' s ∩ Icc (toDual b) (toDual a))
⊢ toDual b ≤ toDual a

Tactic:
simp_all

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

Goal state before:
pp: case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : b < a
⊢ Icc a b ⊆ s

Tactic:
simp_all

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

Goal state before:
pp: X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
⊢ ediam (s ∪ t) ≤ ediam s + edist x y + ediam t

Tactic:
have A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t := fun a ha b hb =>
    calc
      edist a b ≤ edist a x + edist x y + edist y b := edist_triangle4 _ _ _ _
      _ ≤ ediam s + edist x y + ediam t := by
        gcongr
        exacts [edist_le_ediam_of_mem ha xs, edist_le_ediam_of_mem yt hb]
  refine ediam_le fun a ha b hb => ?_
  rw [mem_union] at ha hb
  rcases ha with h'a | h'a <;> rcases hb with h'b | h'b
  · calc
      edist a b ≤ ediam s := edist_le_ediam_of_mem h'a h'b
      _ ≤ ediam s + (edist x y + ediam t) := le_self_add
      _ = ediam s + edist x y + ediam t := (add_assoc _ _ _).symm
  · exact A a h'a b h'b
  · have Z := A b h'b a h'a
    rwa [edist_comm] at Z
  · calc
      edist a b ≤ ediam t := edist_le_ediam_of_mem h'a h'b
      _ ≤ ediam s + edist x y + ediam t := le_add_self

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht₁ : Icc a t₁ ⊆ s
t₁a : a ≤ t₁
t₁b : t₁ ≤ b
t₁b' : t₁ < b
m : α
t₁m : m > t₁
H : Ioo t₁ m ⊆ s
t : α
hat : t₁ < t
ht : t < min m b
⊢ t ∈ A

Tactic:
refine ⟨⟨by order, ht.le.trans (min_le_right _ _)⟩, fun t' ht' ↦ ?_⟩

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht₁ : Icc a t₁ ⊆ s
t₁a : a ≤ t₁
t₁b : t₁ ≤ b
t₁b' : t₁ < b
m : α
t₁m : m > t₁
H : Ioo t₁ m ⊆ s
t : α
hat : t₁ < t
ht : t < min m b
t' : α
ht' : t' ∈ Icc a t
⊢ t' ∈ s
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
⊢ ⋃ i, (fun i ↦ ∅) i = ∅ ∧
    ∀ (i : ℕ),
      Bornology.IsBounded ((fun i ↦ ∅) i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((fun i ↦ ∅) i)

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f a ≤ f ⊥
u : α
hu : u ∈ Ioc b ⊤ ∧ f u = f ⊥
this : u = ⊥
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: case inr.refine_3
α : Type u
inst✝ : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
i : ℕ
⊢ Bornology.IsBounded ((fun i ↦ U ∩ ball x ↑i) i)

Tactic:
exact isBounded_ball.subset inter_subset_right

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

Goal state before:
pp: case neg
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b < f ⊥
u : α
hu : u ∈ Ioo a b ∧ f u = f ⊥
this : u = ⊥
⊢ False

Tactic:
simp_all

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
⊢ ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f

Tactic:
rintro ⟨b, hb⟩
  rw [eventually_map] at hb
  obtain ⟨b', h⟩ := exists_gt b
  have hb' := (tendsto_atTop.mp hf) b'
  have : { x : α | f x ≤ b } ∩ { x : α | b' ≤ f x } = ∅ :=
    eq_empty_of_subset_empty fun x hx => (not_le_of_gt h) (le_trans hx.2 hx.1)
  exact (nonempty_of_mem (hb.and hb')).ne_empty this

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

Goal state before:
pp: case bot.bot
hx hy : 0 ≤ ⊥
⊢ (⊥ + ⊥).toENNReal = ⊥.toENNReal + ⊥.toENNReal

Tactic:
simp_all

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

Goal state before:
pp: case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊥ + ↑a✝).toENNReal = ⊥.toENNReal + (↑a✝).toENNReal

Tactic:
simp_all

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

Goal state before:
pp: case bot.top
hx : 0 ≤ ⊥
hy : 0 ≤ ⊤
⊢ (⊥ + ⊤).toENNReal = ⊥.toENNReal + ⊤.toENNReal

Tactic:
simp_all

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊥
⊢ (↑a✝ + ⊥).toENNReal = (↑a✝).toENNReal + ⊥.toENNReal

Tactic:
simp_all

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

Goal state before:
pp: case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ + ↑a✝).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
simp_all

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
hx : 0 ≤ a✝¹
hy : 0 ≤ a✝
⊢ (↑a✝¹ + ↑a✝).toENNReal = ENNReal.ofReal a✝¹ + ENNReal.ofReal a✝
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
⊢ ∀ (a : β),
    (∀ᶠ (x : β) in Filter.map (fun a ↦ s.sup' hs fun i ↦ F i a) f, (fun x1 x2 ↦ x1 ≤ x2) x a) →
      (fun x1 x2 ↦ x1 ≤ x2) b a

Tactic:
refine fun c hc ↦ hb c ?_

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 : ∀ᶠ (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
Module: Mathlib.Data.EReal.Operations

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

Tactic:
simp_all

Goal state after:
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 : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (s.sup' hs fun i ↦ F i a) c
a : α
h : (fun x1 x2 ↦ x1 ≤ x2) (s.sup' hs fun i ↦ F i a) c
⊢ (fun x1 x2 ↦ x1 ≤ x2) (F i a) c

Tactic:
simp only [sup'_le_iff] at h ⊢

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 : α
h : ∀ b ∈ s, F b a ≤ c
⊢ F i a ≤ c
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ (⊤ + ⊥).toENNReal = ⊤.toENNReal + ⊥.toENNReal

Tactic:
simp_all

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

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

Tactic:
simp_all

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

Goal state before:
pp: case top.top
hx hy : 0 ≤ ⊤
⊢ (⊤ + ⊤).toENNReal = ⊤.toENNReal + ⊤.toENNReal

Tactic:
simp_all

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

Goal state before:
pp: x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤

Tactic:
by
  cases x <;> simp [add_ne_top_iff_ne_top₂, hy, hy']

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ blimsup u f p = blimsup v f p

Tactic:
by
  simpa only [blimsup_eq_limsup] using! limsup_congr <| eventually_inf_principal.2 h

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

Goal state before:
pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊥ ∨ -y ≠ ⊤

Tactic:
simp_all

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

Goal state before:
pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊤ ∨ -y ≠ ⊥

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ liminf u f ≤ x

Tactic:
rw [liminf_eq]

Goal state after:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ sSup {a | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : ℝ
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

Tactic:
rcases le_total 0 x with (h | h)

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

case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case pos
x z t : EReal
h' : z < t
hx_top : x ≠ ⊤
y : ℝ
h : x ≤ ↑y
hy_bot : ↑y ≠ ⊥
hy_top : ¬↑y = ⊤
hxy : x = ↑y
htz_top : t - z = ⊤
⊢ ↑y < ↑y + (t - z)

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C (⋃ b ∈ none, f b)

Tactic:
simp only [Option.mem_def, iUnion_of_empty, iUnion_empty, reduceCtorEq]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C ∅
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ Tendsto Finset.toLeft atTop atTop

Tactic:
by
  intro s hs
  simp only [mem_atTop_sets, Filter.mem_map, Set.mem_preimage] at hs ⊢
  obtain ⟨t, H⟩ := hs
  exact ⟨t.disjSum ∅, fun b hb ↦ H _ (by simpa [← Finset.coe_subset, Set.subset_def] using hb)⟩

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

Goal state before:
pp: ⊢ ∀ {a b : EReal}, a * b = 0 → a = 0 ∨ b = 0

Tactic:
intro a b h
    contrapose! h
    cases a <;> cases b <;> try {· simp_all [← EReal.coe_mul]}
    · rcases lt_or_gt_of_ne h.2 with (h | h)
        <;> simp [EReal.bot_mul_of_neg, EReal.bot_mul_of_pos, h]
    · rcases lt_or_gt_of_ne h.1 with (h | h)
        <;> simp [EReal.mul_bot_of_pos, EReal.mul_bot_of_neg, h]
    · rcases lt_or_gt_of_ne h.1 with (h | h)
        <;> simp [EReal.mul_top_of_neg, EReal.mul_top_of_pos, h]
    · rcases lt_or_gt_of_ne h.2 with (h | h)
        <;> simp [EReal.top_mul_of_pos, EReal.top_mul_of_neg, h]

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
hL : ¬L.NeBot
⊢ L.support = univ

Tactic:
simp [SummationFilter.support, L.neBot_or_eq_bot.resolve_left hL]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : 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 = ∅
H' : ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∀ (j : Subtype p), ¬(⋂ i, Iic (f ↑i)).Nonempty

Tactic:
nonempty_iInter_Iic_iff

Goal state after:
α : 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 = ∅
H' : ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst✝ : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
⊢ HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L

Tactic:
by
  simp only [HasProd, SummationFilter.comap_filter, tendsto_map'_iff, comp_apply,
    Embedding.coeFn_mk, Function.comp_def]
  refine tendsto_congr' ?_
  filter_upwards [L.eventually_le_support] with s hs
  rw [s.prod_preimage]
  exact fun x h h' ↦ hf x (hs h) h'

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 : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ ∀ x ∈ ⋯.toFinset, L.support.mulIndicator (fun b ↦ f b) x = f x

Tactic:
simp_all

Goal state after: