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

Goal state before:
pp: case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : ¬Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
· simp only [Set.disjoint_left, not_forall, Classical.not_not] at H
    rcases H with ⟨c, ⟨hac, hcb⟩, hc⟩
    have hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a :=
      subset_ordConnectedComponent (left_mem_Icc.2 hab) hsub
    have hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t)) :=
      disjoint_left_ordSeparatingSet.mono_right ordConnectedSection_subset
    replace hac : a < c := hac.lt_of_ne <| Ne.symm <| ne_of_mem_of_not_mem hc <|
      disjoint_left.1 hd ha
    filter_upwards [Ico_mem_nhdsGE hac] with x hx hx'
    refine hx.2.ne (eq_of_mem_ordConnectedSection_of_uIcc_subset hx' hc ?_)
    refine subset_inter (subset_iUnion₂_of_subset a ha ?_) ?_
    · exact OrdConnected.uIcc_subset inferInstance (hsub' ⟨hx.1, hx.2.le.trans hcb⟩)
        (hsub' ⟨hac.le, hcb⟩)
    · rcases mem_iUnion₂.1 (ordConnectedSection_subset hx').2 with ⟨y, hyt, hxy⟩
      refine subset_iUnion₂_of_subset y hyt (OrdConnected.uIcc_subset inferInstance hxy ?_)
      refine subset_ordConnectedComponent left_mem_uIcc hxy ?_
      suffices c < y by
        rw [uIcc_of_ge (hx.2.trans this).le]
        exact ⟨hx.2.le, this.le⟩
      refine lt_of_not_ge fun hyc => ?_
      have hya : y < a := not_le.1 fun hay => hsub ⟨hay, hyc.trans hcb⟩ hyt
      exact hxy (Icc_subset_uIcc ⟨hya.le, hx.1⟩) ha

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

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
obtain rfl | ha := eq_or_ne a ∞
  · simp
  refine le_antisymm ?_ <| iSup_le fun i ↦ by grw [← le_iSup]
  refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_
  exact iSup_le fun i ↦ ENNReal.le_sub_of_add_le_left ha <| le_iSup (a + f ·) i

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

Goal state before:
pp: case coe
x z : EReal
h : x < z
a₀ : ℝ
ha₁ : x < ↑a₀
ha₂ : ↑a₀ < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Tactic:
exact ⟨a₀, ha₁, ha₂⟩

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

Goal state before:
pp: case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑(∞ * ↑x) = ⊤ * ↑↑x

Tactic:
· rw [ENNReal.top_mul (ENNReal.coe_ne_zero.2 h0)]
    exact Eq.symm <| if_pos <| NNReal.coe_pos.2 h0.bot_lt

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

Goal state before:
pp: a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b

Tactic:
rw [← one_div, ENNReal.div_le_iff_le_mul, mul_comm]

Goal state after:
case hb0
a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
⊢ a ≠ 0 ∨ b ≠ ∞

case hbt
a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
⊢ a ≠ ∞ ∨ b ≠ 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ∞

Tactic:
by
  rw [← pos_iff_ne_zero, div_pos_iff]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ count K v (exps.prod fun x1 x2 ↦ ↑x1.asIdeal ^ x2) = exps v

Tactic:
Finsupp.prod,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ count K v (∏ a ∈ exps.support, ↑a.asIdeal ^ exps a) = exps v
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε

Tactic:
simp [ContinuousOn, continuousWithinAt_iff']

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

Goal state before:
pp: case inl
γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ (closedBall x r).Subsingleton

Tactic:
closedBall_eq_empty.2 hr

Goal state after:
case inl
γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ ∅.Subsingleton
Module: Mathlib.Analysis.Normed.Group.Defs

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✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist x y = ‖x⁻¹ * y‖

Tactic:
rw [h₁]; apply le_antisymm
    · simpa only [div_eq_mul_inv, ← inv_mul_cancel x] using h₂ x y x⁻¹
    · simpa only [mul_inv_cancel, mul_one, ← mul_assoc, one_mul] using h₂ 1 (x⁻¹ * y) x

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε \ ball x ε = sphere x ε

Tactic:
by
  rw [← ball_union_sphere, Set.union_sdiff_cancel_left sphere_disjoint_ball.symm.le_bot]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε

Tactic:
simp [ContinuousOn, continuousWithinAt_iff']

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

Goal state before:
pp: α : 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
H : (x '' t).Countable
⊢ InjOn x t

Tactic:
intro c hc d hd hcd

Goal state after:
α : 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
H : (x '' t).Countable
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c = x d
⊢ c = d
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
⊢ ∀ a ∈ t, ∀ a_2 ∈ t, x a ≠ x a_2 → Disjoint (Ioo (x a) (y (f (x a)))) (Ioo (x a_2) (y (f (x a_2))))

Tactic:
intro c hc d hd hcd

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
hcd : x c ≠ x d
⊢ Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : 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
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y (f (x c))
xda : x d < a
ayd : a < y (f (x d))
⊢ False

Tactic:
rw [hfx _ hc] at ayc

Goal state after:
α : 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
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y c
xda : x d < a
ayd : a < y (f (x d))
⊢ False
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))
x : αᵒᵈ
hx : x ∈ ⇑ofDual.symm '' (s ∩ Ioc a b)
⊢ (⇑ofDual ⁻¹' s ∩ Ioc x (toDual a)).Nonempty

Tactic:
mem_image

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
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this : IsClosed[instTopologicalSpace] (⇑ofDual ⁻¹' s ∩ Icc (toDual b) (toDual a))
x : αᵒᵈ
hx : ∃ x_1 ∈ s ∩ Ioc a b, ofDual.symm x_1 = x
⊢ (⇑ofDual ⁻¹' s ∩ Ioc x (toDual a)).Nonempty
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
x y z : X
inst✝ : PseudoEMetricSpace X
⊢ ediam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)

Tactic:
by
  simp only [ediam_insert, iSup_insert, iSup_singleton, ediam_singleton, max_zero]

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

Goal state before:
pp: α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ edist (s.mulIndicator f x) (t.mulIndicator f x) = ↑‖(s ∆ t).mulIndicator f x‖₊

Tactic:
by
  rw [edist_nndist, nndist_mulIndicator]

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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
f : E → F
x : E
y : F
⊢ Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε

Tactic:
by
  simpa [norm_inv_mul] using NormedGroup.tendsto_nhds_nhds (f := f) (x := x) (y := y)

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

Goal state before:
pp: case bot
h : ⊥ ≠ ⊥
⊢ False

Tactic:
exact h (Eq.refl ⊥)

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

Goal state before:
pp: case pos
x y : ℝ
hy : 0 ≤ ↑y
hxy : x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal

pp: case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal

Tactic:
· rw [toENNReal_of_nonpos <| sub_nonpos.mpr <| EReal.coe_le_coe_iff.mpr hxy]
    exact (tsub_eq_zero_of_le <| toENNReal_le_toENNReal <| EReal.coe_le_coe_iff.mpr hxy).symm

Goal state after:
case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a : EReal
b : ℝ
⊢ ↑b - (a + ↑b) = -a

Tactic:
cases a <;> norm_cast
  exact _root_.sub_add_cancel_right _ _

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 : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
b₁ : β
hb₁ : b₁ ∈ t
a₂ : α
ha₂ : a₂ ∈ s
⊢ ∀ y ∈ t, edist (f a₁ b₁) (f a₂ y) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t

Tactic:
b₂

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
b₁ : β
hb₁ : b₁ ∈ t
a₂ : α
ha₂ : a₂ ∈ s
b₂ : β
⊢ b₂ ∈ t → edist (f a₁ b₁) (f a₂ b₂) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
h : a < b - c
⊢ a + c < b

Tactic:
by
  contrapose! h
  exact sub_le_of_le_add h

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : ι → Set α
⊢ liminf s cofinite = {x | {n | x ∉ s n}.Finite}

Tactic:
simp only [← cofinite.bliminf_true s, cofinite.bliminf_set_eq, true_and]

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

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

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

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

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

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

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

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

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

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

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

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

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

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

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

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

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

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

Tactic:
try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

Goal state before:
pp: case pos
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∃ c < F.limsSup, Set.Ioo c F.limsSup = ∅
⊢ liminf f F ≤ f F.limsSup

pp: case neg
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
⊢ liminf f F ≤ f F.limsSup

Tactic:
· rcases h' with ⟨c, c_lt, hc⟩
      have B : ∃ᶠ n in F, F.limsSup ≤ n := by
        apply (frequently_lt_of_lt_limsSup cobdd c_lt).mono
        intro x hx
        by_contra!
        have : (Set.Ioo c F.limsSup).Nonempty := ⟨x, ⟨hx, this⟩⟩
        simp only [hc, Set.not_nonempty_empty] at this
      apply liminf_le_of_frequently_le _ (bdd_above.isBoundedUnder f_decr)
      exact B.mono fun x hx ↦ f_decr hx

Goal state after:
case neg
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
⊢ liminf f F ≤ f F.limsSup
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b n : β
⊢ (if n = b then 1 else f n) = update f b 1 n

Tactic:
Function.update_apply

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b n : β
⊢ (if n = b then 1 else f n) = if n = b then 1 else f n
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ Tendsto (fun x ↦ (∏ b ∈ x.2, f b) / ∏ b ∈ x.1, f b) atTop (𝓝 1) ↔
    ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
tendsto_atTop'

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ (∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s) ↔
    ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
b : α'
hb : Tendsto (fun s ↦ ∏ x ∈ s, g (f x)) L.filter (𝓝 b)
a : α
ha : g a = b
⊢ ∃ a, Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
use a

Goal state after:
case h
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
b : α'
hb : Tendsto (fun s ↦ ∏ x ∈ s, g (f x)) L.filter (𝓝 b)
a : α
ha : g a = b
⊢ Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommMonoid α
inst✝⁶ : Preorder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderClosedTopology α
f : ι → α
a : α
inst✝² : L.NeBot
inst✝¹ : L.LeAtTop
inst✝ : MulRightStrictMono α
hf : HasProd f a L
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
⊢ f i < a

Tactic:
classical
  calc
    f i < f j * f i := lt_mul_of_one_lt_left' (f i) hj
    _ = ∏ k ∈ {j, i}, f k := by rw [Finset.prod_pair hij]
    _ ≤ a := prod_le_hasProd _ (fun k hk ↦ hi k (hk ∘ mem_insert_of_mem ∘ mem_singleton.mpr)) hf

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hgf : Multipliable (⇑g ∘ f) L
a : α
ha : g a = ∏'[L] (i : β), g (f i)
⊢ Multipliable f L

Tactic:
use a

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hgf : Multipliable (⇑g ∘ f) L
a : α
ha : g a = ∏'[L] (i : β), g (f i)
⊢ HasProd f a L
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℕ → M
he : HasProd (fun k ↦ f (2 * k)) m
ho : HasProd (fun k ↦ f (2 * k + 1)) m'
⊢ HasProd f (m * m')

Tactic:
have := mul_right_injective₀ (two_ne_zero' ℕ)

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℕ → M
he : HasProd (fun k ↦ f (2 * k)) m
ho : HasProd (fun k ↦ f (2 * k + 1)) m'
this : Injective fun x ↦ 2 * x
⊢ HasProd f (m * m')
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
hL : ¬L.NeBot
⊢ ∏ᶠ (i : ι), f i ≤ 1

Tactic:
exact finprod_induction (· ≤ 1) le_rfl (fun _ _ ↦ mul_le_one') h

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_5
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : γ → α
t : Finset γ
⊢ R (m (⨆ x, s ↑x)) (∏ d ∈ t, m (s d))

Tactic:
← Finset.tprod_subtype

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
γ : Type u_5
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : γ → α
t : Finset γ
⊢ R (m (⨆ x, s ↑x)) (∏' (x : ↥t), m (s ↑x))
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
⊢ ∏' (x : β), a = 1

Tactic:
rcases eq_or_ne a 1 with rfl | ha

Goal state after:
case inr.inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
hβ : Infinite β
⊢ ∏' (x : β), 1 = 1

case inr.inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
ha : a ≠ 1
⊢ ∏' (x : β), a = 1
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ∞
hb✝ : b✝ ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < ↑ε
hεb : ↑ε < b
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), ↑n < a.1 * a.2

Tactic:
have : ∀ᶠ c : ℝ≥0∞ × ℝ≥0∞ in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2 :=
      (lt_mem_nhds <| div_lt_top coe_ne_top hε.ne').prod_nhds (lt_mem_nhds hεb)

Goal state after:
a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ∞
hb✝ : b✝ ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < ↑ε
hεb : ↑ε < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), ↑n < a.1 * a.2