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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ioc a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
exact this hab.le

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

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < ↑r
⊢ dist f g < ↑r ↔ ∀ (b : β), dist (f b) (g b) < ↑r

Tactic:
exact nndist_pi_lt_iff hr

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 : α
h : IsClosed[inst✝³] (Ioo a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
exact this hab.le

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∉ t
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
exact ⟨u, hu.1.monotone, fun n => (hu.2.1 n).le, hu.2.2⟩

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 α
x : α
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x
  rcases exists_seq_strictMono_tendsto' hy with ⟨u, hu_mono, hu_mem, hux⟩
  exact ⟨u, hu_mono, fun n => (hu_mem n).2, hux⟩

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

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ ‖r‖ₑ = ENNReal.ofReal r

Tactic:
by
  rw [← ofReal_norm, norm_of_nonneg hr]

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

Goal state before:
pp: case refine_2
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
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.comap (↑I).subtype ↑J ≤
    Submodule.comap (LinearMap.domRestrict ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I) ↑J'

Tactic:
LinearMap.domRestrict,

Goal state after:
case refine_2
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
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.comap (↑I).subtype ↑J ≤ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J') ∘ₗ (↑I).subtype) ↑J'
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_3
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
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.comap (LinearMap.domRestrict ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I) ↑J' ≤
    Submodule.comap (↑I).subtype ↑J

Tactic:
LinearMap.domRestrict,

Goal state after:
case refine_3
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
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J') ∘ₗ (↑I).subtype) ↑J' ≤ Submodule.comap (↑I).subtype ↑J
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
⊢ ContinuousAt (fun x ↦ sSup (f x '' K)) x

Tactic:
obtain ⟨y, hyK, h2y, hy⟩ :=
    hK.exists_sSup_image_eq_and_ge h0K
      (show Continuous (f x) from hf.comp <| .prodMk_right x).continuousOn

Goal state after:
case inr
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
⊢ ContinuousAt (fun x ↦ sSup (f x '' K)) x
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ |‖a‖ - ‖b‖| ≤ ‖a⁻¹ * b‖

Tactic:
by
  simpa [dist_eq_norm_inv_mul] using abs_dist_sub_le a b 1

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

Goal state before:
pp: case inr
α : 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
⊢ Icc a b ⊆ s

Tactic:
have t₁_mem : t₁ ∈ Icc a b := ⟨le_csSup bdd_A a_mem, csSup_le ⟨a, a_mem⟩ (fun t ht ↦ ht.1.2)⟩

Goal state after:
case inr
α : 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
⊢ Icc a b ⊆ s
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: case inr.inr
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
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.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : a ∈ ball b r
⊢ a ^ n ∈ ball (b ^ n) (n • r)

Tactic:
simp only [mem_ball, dist_eq_norm_inv_mul, ← inv_pow, ← mul_pow] at h ⊢
  refine lt_of_le_of_lt norm_pow_le_mul_norm ?_
  replace hn : 0 < (n : ℝ) := by norm_cast
  rw [nsmul_eq_mul]
  nlinarith

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
⊢ s ∈ 𝓝[>] z

Tactic:
have zt : z ∈ tᶜ := fun zt => hst ⟨z, xyab <| Ico_subset_Icc_self hz, zs, zt⟩

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
⊢ s ∈ 𝓝[>] z
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
this : tᶜ ∩ Ioc z y ∈ 𝓝[>] z
⊢ s ∈ 𝓝[>] z

Tactic:
apply mem_of_superset this

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
this : tᶜ ∩ Ioc z y ∈ 𝓝[>] z
⊢ tᶜ ∩ Ioc z y ⊆ s
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 f l atTop

Tactic:
by
  rw [← @Rat.comap_cast_atTop R, tendsto_comap_iff]; rfl

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: x : ℤ
r : ℝ
⊢ Int.cast ⁻¹' ball (↑x) r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉

Tactic:
Real.ball_eq_Ioo,

Goal state after:
x : ℤ
r : ℝ
⊢ Int.cast ⁻¹' Ioo (↑x - r) (↑x + r) = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
⊢ ∀ b ∈ {a | ∀ᶠ (n : α) in ⊤, a ≤ n}, b ≤ ⊥

Tactic:
simpa [eq_univ_iff_forall] using fun b hb => bot_unique <| hb _

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
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ ∃ᶠ (x_1 : α) in f, b ≤ x

Tactic:
contrapose! h

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

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

Tactic:
contrapose! h

Goal state after:
a b c : EReal
h : b ≤ a + c
⊢ b - c ≤ a
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: ι : 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
h : ¬(Set.Ioo c b).Nonempty
r : α
hr : limsup (fun i ↦ u i r) cofinite < b
⊢ limsup (fun x ↦ u x r) cofinite ≤ c

Tactic:
contrapose! h

Goal state after:
ι : 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
r : α
hr : limsup (fun i ↦ u i r) cofinite < b
h : c < limsup (fun x ↦ u x r) cofinite
⊢ (Set.Ioo c b).Nonempty
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
h : a < f.limsSup
⊢ ∃ᶠ (n : α) in f, a < n

Tactic:
contrapose! h

Goal state after:
α : Type u_1
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
h : ∀ᶠ (x : α) in f, x ≤ a
⊢ f.limsSup ≤ a
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : b < limsup u f
⊢ ∃ᶠ (x : α) in f, b < u x

Tactic:
contrapose! h

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ᶠ (x : α) in f, u x ≤ b
⊢ limsup u f ≤ b
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: ι : 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 : ι
hn : u n r < b
⊢ u n r ≤ b'

Tactic:
contrapose! h

Goal state after:
ι : 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_lt : ∀ᶠ (a : ι) in cofinite, u a r < b
n : ι
hn : u n r < b
h : b' < u n r
⊢ (Set.Ioo b' b).Nonempty
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
h : a * b = 0
⊢ a = 0 ∨ b = 0

Tactic:
contrapose! h

Goal state after:
a b : EReal
h : a ≠ 0 ∧ b ≠ 0
⊢ a * b ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
⊢ ↑a✝ * ⊥ ≠ 0

pp: case coe.top
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
⊢ ↑a✝ * ⊤ ≠ 0

pp: case top.coe
a✝ : ℝ
h : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊤ * ↑a✝ ≠ 0

Tactic:
· rcases lt_or_gt_of_ne h.1 with (h | h)
        <;> simp [EReal.mul_bot_of_pos, EReal.mul_bot_of_neg, h]

Goal state after:
case coe.top
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
⊢ ↑a✝ * ⊤ ≠ 0

case top.coe
a✝ : ℝ
h : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊤ * ↑a✝ ≠ 0
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
⊢ Tendsto f atTop atTop

Tactic:
simp only [atTop_finset_eq_iInf, tendsto_iInf, tendsto_principal]
  intro a
  rcases h' a with ⟨b, hb⟩
  exact (eventually_ge_atTop b).mono fun b' hb' => (Finset.singleton_subset_iff.2 hb).trans (h hb')

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

Goal state before:
pp: case top_pos
x✝ : ℝ
hx : 0 < x✝
⊢ 0 < ⊤ * ↑x✝ ↔ 0 < ⊤ ∧ 0 < ↑x✝ ∨ ⊤ < 0 ∧ ↑x✝ < 0

Tactic:
| top_pos _ hx =>

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

Goal state before:
pp: ι : 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'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r✝ ≤ b''
n : ι
h : ¬(Set.Ioo c b).Nonempty
r : α
hr : u n r < b
⊢ u n r ≤ c

Tactic:
contrapose! h

Goal state after:
ι : 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'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r✝ ≤ b''
n : ι
r : α
hr : u n r < b
h : c < u n r
⊢ (Set.Ioo c b).Nonempty
Module: Mathlib.Data.EReal.Operations

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

Tactic:
rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]

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

Goal state before:
pp: case top_pos
x✝ : ℝ
hx : 0 < x✝
⊢ ⊤ * ↑x✝ = ⊤ ↔ ⊤ = ⊥ ∧ ↑x✝ < 0 ∨ ⊤ < 0 ∧ ↑x✝ = ⊥ ∨ ⊤ = ⊤ ∧ 0 < ↑x✝ ∨ 0 < ⊤ ∧ ↑x✝ = ⊤

Tactic:
| top_pos _ hx =>

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

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

Tactic:
· exact ⟨a + 1, fun b hb ↦ by convert! ha (b - 1) (by lia); lia⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
b : Finset β
x✝ : True
v : Finset α
hv : ∀ (v' : Finset α), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
⊢ (fun s ↦ ∏ b ∈ s, f b) '' Set.Ici v ⊆ (fun s ↦ ∏ x ∈ s, g x) '' Set.Ici b

Tactic:
simpa [Finset.image_subset_iff] using! hv

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
⊢ HasProd f (∏ b ∈ (↑s ∩ L.support).toFinset, f b) L

Tactic:
apply tendsto_nhds_of_eventually_eq
  have h1 : ⋂ b ∈ (↑s ∩ L.support), {s | b ∈ s} ∈ L.filter :=
    (L.filter.biInter_mem (Set.toFinite _)).mpr (fun b hb ↦ hb.2)
  filter_upwards [h1, L.eventually_le_support] with t ht ht'
  simp only [Set.mem_iInter] at ht
  apply Finset.prod_congr_of_eq_on_inter <;> grind

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd f a₁
hg : HasProd g a₂
⊢ a₁ ≤ a₂

Tactic:
rw [← hasProd_extend_one he] at hf

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
⊢ a₁ ≤ a₂
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ ∀ x ∈ t, x ∉ {b ∈ t | g b = f b} → g x = 1

Tactic:
intro b hbt hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
hb : b ∉ {b ∈ t | g b = f b}
⊢ g b = 1
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
⊢ f ⁻¹' Metric.closedEBall (f x) r = Metric.closedEBall x r

Tactic:
by
  ext y
  simp [h.edist_eq]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
⊢ f ⁻¹' Metric.eball (f x) r = Metric.eball x r

Tactic:
by
  ext y
  simp [h.edist_eq]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
s : Set X
h : ∀ ⦃x : ℕ → X⦄, (∀ (n : ℕ), x n ∈ s) → ∃ a ∈ s, ∃ φ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
V : Set (X × X)
V_in : V ∈ 𝓤 X
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}

Tactic:
contrapose! h

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}
⊢ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ ∀ a ∈ s, ∀ (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 a)
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ ||a - c| + |b - d||

Tactic:
abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ ||a - c| + |b - d||

Tactic:
abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
Module: Mathlib.Analysis.Normed.Group.Submodule

Goal state before:
pp: R : Type u_3
R' : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R'
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R' M'
σ₁₂ : R →+* R'
f : M →ₛₗ[σ₁₂] M'
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
hf : Continuous ⇑f
p : Submodule R M
⊢ Continuous ⇑(f.domRestrict p)

Tactic:
rw [coe_domRestrict]
  fun_prop

Goal state after: