mathlib-initiative/mathlib-tactics huggingface dataset:
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.map (Submodule.comap (↑I).subtype ↑J).mkQ
      (Submodule.comap (LinearMap.domRestrict ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I) ↑J') =
    ⊥

Tactic:
← le_bot_iff,

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.map (Submodule.comap (↑I).subtype ↑J).mkQ
      (Submodule.comap (LinearMap.domRestrict ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I) ↑J') ≤
    ⊥
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
t₁_mem : t₁ ∈ Icc a b
t : α
ht : t ∈ Icc a t₁
h : t < t₁
⊢ t ∈ s

Tactic:
· obtain ⟨c, cA, tc⟩ : ∃ c ∈ A, t < c := (lt_csSup_iff bdd_A ⟨a, a_mem⟩).1 h
      apply cA.2
      exact ⟨ht.1, tc.le⟩

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 : ℕ
h : ‖a⁻¹ * b‖ < r
hn : 0 < ↑n
⊢ ↑n * ‖a⁻¹ * b‖ < n • r

Tactic:
nsmul_eq_mul

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ < r
hn : 0 < ↑n
⊢ ↑n * ‖a⁻¹ * b‖ < ↑n * r
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ 1 ≤ ↑n * r

Tactic:
nsmul_eq_mul

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ ↑n * r
⊢ 1 ≤ ↑n * r
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: ⊢ Pairwise fun m n ↦ 1 ≤ dist m n

Tactic:
intro m n hne
  rw [dist_eq]; norm_cast; rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ (max (max (edist x y) (edist x z)) (edist y z)).toReal =
    max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal

Tactic:
rw [ENNReal.toReal_max, ENNReal.toReal_max]

Goal state after:
case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist x y ≠ ∞

case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist x z ≠ ∞

case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ max (edist x y) (edist x z) ≠ ∞

case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist y z ≠ ∞
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist x y ≠ ∞

Tactic:
apply_rules [ne_of_lt, edist_lt_top, max_lt]

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

Goal state before:
pp: case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist x z ≠ ∞

Tactic:
apply_rules [ne_of_lt, edist_lt_top, max_lt]

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

Goal state before:
pp: case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ max (edist x y) (edist x z) ≠ ∞

Tactic:
apply_rules [ne_of_lt, edist_lt_top, max_lt]

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

Goal state before:
pp: case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist y z ≠ ∞

Tactic:
apply_rules [ne_of_lt, edist_lt_top, max_lt]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 ↦ x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (f '' {x | f x ≤ b}) ∧ BddAbove (f '' {x | f x ≤ b}ᶜ)

Tactic:
exact ⟨⟨b, forall_mem_image.2 fun x => id⟩, (hb.image f).bddAbove⟩

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

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l)

Tactic:
by
  constructor <;> intro h
  · exact h.comp hg
  · rcases tendsto_atTop_of_monotone hf with (h' | ⟨l', hl'⟩)
    · exact (not_tendsto_atTop_of_tendsto_nhds h (h'.comp hg)).elim
    · rwa [tendsto_nhds_unique h (hl'.comp hg)]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
⊢ limsup (fun x ↦ ⊥) f = ⊥

Tactic:
rw [limsup_eq, eq_bot_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
⊢ sInf {a | ∀ᶠ (n : β) in f, ⊥ ≤ a} ≤ ⊥
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, f (⨆ i_1, (⇑f)^[i_1 + i] a) = ⨅ n, ⨆ i, (⇑f)^[i + n] a

Tactic:
_root_.map_iSup,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, ⨆ i_1, f ((⇑f)^[i_1 + i] a) = ⨅ n, ⨆ i, (⇑f)^[i + n] a
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ a ⊔ limsup u f = limsup (fun x ↦ a ⊔ u x) f

Tactic:
simp only [limsup_eq_iInf_iSup, iSup_sup_eq, sup_iInf₂_eq]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ ⨅ i ∈ f, a ⊔ ⨆ a ∈ i, u a = ⨅ s ∈ f, (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
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'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''

Tactic:
by
    rcases Set.eq_empty_or_nonempty (Set.Ioo b' b) with h | ⟨b'', hb'b'', hb''b⟩
    · refine ⟨b', ⟨le_rfl, hb'b⟩, ?_⟩
      have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b)
      filter_upwards [h_lt] with n hn
      contrapose! h
      exact ⟨u n r, h, hn⟩
    · refine ⟨b'', ⟨hb'b''.le, hb''b⟩ , ?_⟩
      have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b'')
      filter_upwards [h_lt] with n hn using hn.le

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

Goal state before:
pp: case neg_left
x✝ y✝ : EReal
h : -x✝ * y✝ = -(x✝ * y✝)
⊢ - -x✝ * y✝ = - -(x✝ * y✝)

Tactic:
neg_neg,

Goal state after:
case neg_left
x✝ y✝ : EReal
h : -x✝ * y✝ = -(x✝ * y✝)
⊢ x✝ * y✝ = - -(x✝ * y✝)
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case inl
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
b : β
⊢ f b ∈ (L.map f).support ↔ f b ∈ ⇑f '' L.support

Tactic:
simp [support]

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
L : SummationFilter β
f : γ ↪ β
⊢ (L.comap f).support = ⇑f ⁻¹' L.support

Tactic:
simp [support]

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

Goal state before:
pp: β : Type u_4
inst✝² : Finite β
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
⊢ L = unconditional β

Tactic:
by
  have := Fintype.ofFinite β
  have hAtTop : (atTop : Filter (Finset β)) = pure Finset.univ := by
    rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
  have hL := L.le_atTop
  have hL' : ∅ ∉ L.filter := empty_mem_iff_bot.not.mpr <| NeBot.ne_bot.ne'
  cases L with | mk F =>
  simp only [unconditional, hAtTop] at *
  congr 1
  refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
  contrapose! hL'
  obtain ⟨s, hs, hs'⟩ := hL'
  simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)

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

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

Tactic:
· simp_all [mul_top_of_pos hx]

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

Goal state before:
pp: ⊢ (conditional ℕ).filter = Filter.map Finset.range atTop

Tactic:
have (n : ℕ) : Finset.Iic n = Finset.range (n + 1) := by ext x; simp [Nat.lt_succ_iff]
  simp only [conditional_filter_eq_map_Iic, funext this]
  apply le_antisymm <;>
      rw [← Tendsto] <;>
      simp only [tendsto_atTop', mem_map, mem_atTop_sets, mem_preimage] <;>
      rintro s ⟨a, ha⟩
  · exact ⟨a + 1, fun b hb ↦ ha (b + 1) (by lia)⟩
  · exact ⟨a + 1, fun b hb ↦ by convert! ha (b - 1) (by lia); lia⟩

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

Goal state before:
pp: case succ
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ ↑n * x + x = (↑n + 1) * x

Tactic:
convert! (EReal.right_distrib_of_nonneg _ _).symm <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ HasProd (extend g f 1) a ↔ HasProd f a

Tactic:
rw [← hg.hasProd_iff, extend_comp hg]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ ∀ x ∉ Set.range g, extend g f 1 x = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
⊢ HasProd ((Set.range Subtype.val).mulIndicator f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a

Tactic:
Subtype.range_coe,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
⊢ HasProd (s.mulIndicator f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
by_cases hf : Multipliable f L

Goal state after:
case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
hf : Multipliable f L
⊢ ∏'[L] (i : ι), f i ≤ a₂

case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
hf : ¬Multipliable f L
⊢ ∏'[L] (i : ι), f i ≤ 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 : ι → α
h : ∀ (i : ι), f i ≤ 1
⊢ ∏'[L] (i : ι), f i ≤ 1

Tactic:
by_cases hf : Multipliable f L

Goal state after:
case pos
ι : 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
⊢ ∏'[L] (i : ι), f i ≤ 1

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
⊢ ∏'[L] (i : ι), f i ≤ 1
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case intro
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Countable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : β → α
val✝ : Encodable β
⊢ R (m (⨆ b, s b)) (∏' (b : β), m (s b))

Tactic:
rw [← iSup_decode₂, ← tprod_iSup_decode₂ _ m0 s]

Goal state after:
case intro
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Countable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : β → α
val✝ : Encodable β
⊢ R (m (⨆ i, ⨆ b ∈ decode₂ β i, s b)) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b))
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x ↦ b
s : Finset ι
⊢ #s • b ≤ ∑' (x : ι), b

Tactic:
simpa using sum_le_hasSum s (fun a _ ↦ hb.le) hf.hasSum

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : ι → α
x : α
hfx : HasProd f x
⊢ HasProd (fun x ↦ |f x|) |x|

Tactic:
simpa only [HasProd, ← abs_prod] using hfx.abs

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
hf : f 0 = 1
n : ℕ
hn : n ∈ mulSupport f
⊢ n ∈ Set.range PNat.val

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | h
    · exact absurd hf hn
    · exact ⟨⟨n, h⟩, rfl⟩

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

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
⊢ Isometry (Pi.single i)

Tactic:
by
  intro x y
  rw [edist_pi_def]
  refine le_antisymm (Finset.sup_le fun j ↦ ?_) (Finset.le_sup_of_le (Finset.mem_univ i) (by simp))
  obtain rfl | h := eq_or_ne i j
  · simp
  · simp [h]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : f x ∈ closure[inst✝¹] (f '' s)
⊢ x ∈ seqClosure s

Tactic:
mem_closure_iff_seq_limit

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : ∃ x_1, (∀ (n : ℕ), x_1 n ∈ f '' s) ∧ Tendsto x_1 atTop (𝓝 (f x))
⊢ x ∈ seqClosure s
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
⊢ HasProd (Pi.mulSingle b a) a

Tactic:
convert! hasProd_ite_eq (L := .unconditional β) b a

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
x✝ : β
⊢ Pi.mulSingle b a x✝ = if x✝ = b then a else 1
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n : ℕ
⊢ (v 0)⁻¹ * w 0 = 1

Tactic:
simp [v]

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f g : CauchyFilter α
⊢ (↑f).lim = (↑g).lim ↔ Inseparable f g

Tactic:
rw [← inseparable_iff_eq, inseparable_lim_iff]

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hbx : b < x
⊢ IccExtend h (f ∘ Subtype.val) x = f x

Tactic:
simp [IccExtend_of_right_le _ _ hbx.le, hb x hbx]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
⊢ LipschitzOnWith K f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
have := ENNReal.continuous_const_mul (ENNReal.coe_ne_top (r := K))

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous fun x ↦ ↑K * x
⊢ LipschitzOnWith K f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
⊢ liminf u f * liminf v f ≤ liminf (u * v) f

Tactic:
refine mul_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x
  exact c_ab.trans (mul_lt_mul a_x b_x)

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

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.sup' hne f) x

Tactic:
by
  simpa only [← Finset.sup'_apply] using finset_sup'_apply hne hs

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

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.sup' hne f) t x

Tactic:
by
  simpa only [← Finset.sup'_apply] using finset_sup'_apply hne hs

Goal state after:
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:
by
  rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]
  refine le_trans (solid ?_) (norm_add_le |a - c| |b - d|)
  rw [abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]
  calc
    |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)| := by rw [sub_add_sub_cancel]
    _ ≤ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| := abs_add_le _ _
    _ ≤ |a - c| + |b - d| := by
      gcongr ?_ + ?_
      · exact abs_sup_sub_sup_le_abs _ _ _
      · rw [sup_comm c, sup_comm c]
        exact abs_sup_sub_sup_le_abs _ _ _

Goal state after:
Module: Mathlib.Algebra.Order.AddTorsor

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ a • c < b • d

Tactic:
refine lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_right a b h₁ c) ?_

Goal state after:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ b • c < b • d
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort uι
s : Set α
m✝ m₁ m₂ : MeasurableSpace α
m' : MeasurableSpace β
f✝¹ : α → β
g : β → α
f✝ : α → β
m : MeasurableSpace α
f : ℕ → Set β
hf : ∀ (i : ℕ), MeasurableSet (f✝ ⁻¹' f i)
⊢ MeasurableSet (f✝ ⁻¹' ⋃ i, f i)

Tactic:
simpa only [preimage_iUnion] using! m.measurableSet_iUnion _ hf

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∃ c, c ≠ 0 ∧ ‖c‖ ≠ 1
⊢ NoncompactSpace E

pp: case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
⊢ NoncompactSpace E

Tactic:
· let := NontriviallyNormedField.ofNormNeOne H
    exact ⟨fun h ↦ NormedSpace.unbounded_univ 𝕜 E h.isBounded⟩

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
⊢ NoncompactSpace E
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
⊢ Continuous[inst✝², inst✝¹] ⇑(algebraMap R A) ↔ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ p.1 • p.2

Tactic:
refine ⟨fun h => ?_, fun h => have : ContinuousSMul R A := ⟨h⟩; continuous_algebraMap _ _⟩

Goal state after:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
h : Continuous[inst✝², inst✝¹] ⇑(algebraMap R A)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ p.1 • p.2
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
⊢ sign a = -1 ↔ a < 0

Tactic:
refine ⟨fun h => ?_, fun h => sign_neg h⟩

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : sign a = -1
⊢ a < 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : {i | ε ≤ a i}.Finite
⊢ ↑(#hf.toFinset) * ε = #hf.toFinset • ε

Tactic:
nsmul_eq_mul

Goal state after:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : {i | ε ≤ a i}.Finite
⊢ ↑(#hf.toFinset) * ε = ↑(#hf.toFinset) * ε