mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), (T n).Countable
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (T n)
⊢ SeparableSpace α

Tactic:
refine ⟨⟨⋃ n, T n, countable_iUnion hTc, fun x => ?_⟩⟩

Goal state after:
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), (T n).Countable
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (T n)
x : α
⊢ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ n, T n)
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun f g ↦ ↑(Finset.univ.sup fun b ↦ nndist (f b) (g b))) ⋯ ⋯
s : Set ((b : β) → X b)
C : ℝ≥0
⊢ (∀ (i : β) ⦃x : (x : β) → X x⦄,
      x ∈ s → ∀ ⦃x_1 : (x : β) → X x⦄, x_1 ∈ s → ↑(nndist (Function.eval i x) (Function.eval i x_1)) ≤ ↑C) ↔
    ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ ↑C

Tactic:
refine ⟨fun H x hx y hy ↦ NNReal.coe_le_coe.2 <| Finset.sup_le fun b _ ↦ H b hx hy,
    fun H b x hx y hy ↦ NNReal.coe_le_coe.2 ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun f g ↦ ↑(Finset.univ.sup fun b ↦ nndist (f b) (g b))) ⋯ ⋯
s : Set ((b : β) → X b)
C : ℝ≥0
H : ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ ↑C
b : β
x : (x : β) → X x
hx : x ∈ s
y : (x : β) → X x
hy : y ∈ s
⊢ nndist (Function.eval b x) (Function.eval b y) ≤ C
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
S : Set α
hS : S.Nonempty
hS' : BddAbove S
⊢ ∃ u, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S

Tactic:
rcases (isLUB_csSup hS hS').exists_seq_monotone_tendsto hS with ⟨u, hu⟩
  exact ⟨u, hu.1, hu.2.2⟩

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

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ r.toNNReal = ‖r‖₊

Tactic:
by
  rw [Real.toNNReal_of_nonneg hr]
  congr
  rw [Real.norm_eq_abs r, abs_of_nonneg hr]

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

Goal state before:
pp: α : Type u_1
s✝ t : Set α
inst✝⁵ : Bornology α
inst✝⁴ : Preorder α
inst✝³ : IsOrderBornology α
β : Type u_2
inst✝² : Preorder β
inst✝¹ : Bornology β
inst✝ : IsOrderBornology β
s : Set (α × β)
⊢ IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove (fst '' s) ∧ BddAbove (snd '' s)

Tactic:
and_and_and_comm,

Goal state after:
α : Type u_1
s✝ t : Set α
inst✝⁵ : Bornology α
inst✝⁴ : Preorder α
inst✝³ : IsOrderBornology α
β : Type u_2
inst✝² : Preorder β
inst✝¹ : Bornology β
inst✝ : IsOrderBornology β
s : Set (α × β)
⊢ IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : BddBelow sᶜ ∧ BddAbove sᶜ
b : α
hb : b ∈ upperBounds sᶜ
c : α
hbc : b < c
⊢ s ∈ Filter.atTop

Tactic:
refine Filter.mem_of_superset (Filter.mem_atTop c) fun x hx ↦ ?_

Goal state after:
α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : BddBelow sᶜ ∧ BddAbove sᶜ
b : α
hb : b ∈ upperBounds sᶜ
c : α
hbc : b < c
x : α
hx : x ∈ {b | c ≤ b}
⊢ x ∈ s
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
hs : IsPreconnected ∅
⊢ ∅ ∈
    {Icc (sInf ∅) (sSup ∅), Ico (sInf ∅) (sSup ∅), Ioc (sInf ∅) (sSup ∅), Ioo (sInf ∅) (sSup ∅), Ici (sInf ∅),
      Ioi (sInf ∅), Iic (sSup ∅), Iio (sSup ∅), univ, ∅}

Tactic:
apply_rules [Or.inr, mem_singleton]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
⊢ ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs')

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
a : α
hs : IsCompact ∅
hf : ContinuousOn f ∅
hf' : ∀ b ∈ ∅, a < f b
⊢ ∃ a', a < a' ∧ ∀ b ∈ ∅, a' ≤ f b

case inr
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
⊢ ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖a⁻¹‖ = ‖a‖

Tactic:
simpa using norm_div_rev 1 a

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

Goal state before:
pp: X : Type u_2
s : Set X
inst✝ : EMetricSpace X
⊢ 0 < ediam s ↔ s.Nontrivial

Tactic:
by
  simp only [pos_iff_ne_zero, Ne, ediam_eq_zero_iff, Set.not_subsingleton_iff]

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

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a b : E
h : ‖a / b‖ ≤ 0
⊢ a = b

Tactic:
by
  rwa [← div_eq_one, ← norm_le_zero_iff']

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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ (factorization I) p.asIdeal = multiplicity p.asIdeal I

Tactic:
by
  rw [factorization_eq_count, count_normalizedFactors_eq_multiplicity hI]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis (fun a ↦ x ∈ a ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧ Bornology.IsBounded a)
    id

Tactic:
by
  simp_rw [← and_assoc]
  apply (nhds_basis_opens x).restrict fun s hs ↦ ?_
  exact ⟨s ∩ Metric.ball x 1,
    by aesop (add safe apply IsOpen.inter),
    by simpa using Metric.isBounded_ball.subset Set.inter_subset_right⟩

Goal state after:
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 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ r * ↑n * max b 0 = r * (↑n * max b 0)

Tactic:
rw [mul_assoc]

Goal state after:
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
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * (↑n * r) = max b 0 * ↑n * r

Tactic:
rw [mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
ha : IsLeast {g | g ∈ H ∧ 1 < g} a
⊢ H = closure {a}

Tactic:
by
  obtain ⟨⟨a_in, a_pos⟩, a_min⟩ := ha
  refine le_antisymm ?_ (H.closure_le.mpr <| by simp [a_in])
  intro g g_in
  obtain ⟨k, ⟨nonneg, lt⟩, _⟩ := existsUnique_zpow_near_of_one_lt a_pos g
  have h_zero : g / (a ^ k) = 1 := by
    by_contra h
    have h : a ≤ g / (a ^ k) := by
      refine a_min ⟨?_, ?_⟩
      · exact Subgroup.div_mem H g_in (Subgroup.zpow_mem H a_in k)
      · exact lt_of_le_of_ne (by simpa using nonneg) (Ne.symm h)
    have h' : ¬a ≤ g / (a ^ k) := not_le.mpr (by simpa [zpow_add_one, div_lt_iff_lt_mul'] using lt)
    contradiction
  simp [div_eq_one.mp h_zero, mem_closure_singleton]

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℕ
hm : g ≤ a ^ (↑m + 1)
hm' : a ^ ↑m < g
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
simp only [← Nat.cast_succ, zpow_natCast] at hm hm'
      exact ⟨m, hm', hm⟩

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

Goal state before:
pp: x y : ℤ
⊢ dist ↑x ↑y = dist x y

Tactic:
← Int.dist_cast_real,

Goal state after:
x y : ℤ
⊢ dist ↑x ↑y = dist ↑x ↑y
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_3
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)

Tactic:
by
  simp_rw [ENNReal.ofReal, ← ofNNReal_finsetProd, coe_inj]
  exact Real.toNNReal_prod_of_nonneg hf

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

Goal state before:
pp: case cons
ι : Type u_3
α : Type u_4
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
i j : ι
⊢ ∃ k, f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_

Goal state after:
case cons
ι : Type u_3
α : Type u_4
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
i j k : ι
hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝² : LinearOrder R
inst✝¹ : LinearOrder S
f : R → S
f_decr : Antitone f
inst✝ : F.NeBot
cobdd : IsCobounded (fun x1 x2 ↦ x2 ≤ x1) F
l : R
hl : ∃ᶠ (x : R) in F, x ≤ l
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f

Tactic:
exact IsCobounded.of_frequently_ge <| f_decr.frequently_ge_map_of_frequently_le hl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (s.domRestrict fst)) (a, b).1 ∧ IsLUB (range (s.domRestrict snd)) (a, b).2
A : Tendsto (fun x ↦ (↑x).1) atTop (𝓝 a)
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))

Tactic:
have B : Tendsto (fun x : s => (x : α × β).2) atTop (𝓝 b) :=
    tendsto_atTop_isLUB (monotone_snd.domRestrict s) h.2

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (s.domRestrict fst)) (a, b).1 ∧ IsLUB (range (s.domRestrict snd)) (a, b).2
A : Tendsto (fun x ↦ (↑x).1) atTop (𝓝 a)
B : Tendsto (fun x ↦ (↑x).2) atTop (𝓝 b)
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, a ≤ u i
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
b : α
hb : ∀ᶠ (n : ι) in f, u n ≤ b
⊢ a ≤ b

Tactic:
obtain ⟨n, han, hnb⟩ := (hu.and_eventually hb).exists

Goal state after:
α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, a ≤ u i
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
b : α
hb : ∀ᶠ (n : ι) in f, u n ≤ b
n : ι
han : a ≤ u n
hnb : u n ≤ b
⊢ a ≤ b
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (blimsup u f fun x ↦ p x ∨ q x) = blimsup u f p ⊔ blimsup u f q

Tactic:
simp only [blimsup_eq_limsup, ← limsup_sup_filter, ← inf_sup_left, sup_principal, ofPred_or]

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

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

Tactic:
EReal.add_sub_cancel_right

Goal state after:
a : EReal
b : ℝ
⊢ a = a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
b a✝ : ℝ
⊢ b - (a✝ + b) = -a✝

Tactic:
exact _root_.sub_add_cancel_right _ _

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ a \ limsup u f = liminf (fun b ↦ a \ u b) f

Tactic:
rw [← compl_inj_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ (a \ limsup u f)ᶜ = (liminf (fun b ↦ a \ u b) f)ᶜ
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ a \ liminf u f = limsup (fun b ↦ a \ u b) f

Tactic:
rw [← compl_inj_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (a \ liminf u f)ᶜ = (limsup (fun b ↦ a \ u b) f)ᶜ
Module: Mathlib.Order.LiminfLimsup

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

Tactic:
rw [← compl_inj_iff]

Goal state after:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ (bliminf s cofinite p)ᶜ = {x | {n | p n ∧ x ∉ s n}.Finite}ᶜ
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
y : β
y_x : y < x
z : β
y_z : y < z
z_x : z < x
⊢ y < limsup u f

Tactic:
exact y_z.trans_le (le_limsup_of_frequently_le ((h z z_x).mono (fun _ ↦ le_of_lt)) h₂)

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

Goal state before:
pp: a b : EReal
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
rcases lt_trichotomy a 0 with (h | h | h) <;> rcases lt_trichotomy b 0 with (h' | h' | h')
    <;> simp only [h, h', true_or, true_and, or_true, and_true] <;> tauto

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

Goal state before:
pp: γ : Type u_4
inst✝² : PartialOrder γ
inst✝¹ : LocallyFiniteOrder γ
inst✝ : OrderBot γ
⊢ (conditional γ).filter = Filter.map Finset.Iic atTop

Tactic:
by
  simp [isBot_bot.atBot_eq, comp_def, Finset.Icc_bot]

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

Goal state before:
pp: ι : 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₂
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
by
  by_cases hL : L.NeBot
  · by_cases hf : Multipliable f L
    · exact hf.tprod_le_of_prod_le h
    · rwa [tprod_eq_one_of_not_multipliable hf]
  · by_cases hf : f.mulSupport.Finite
    · simpa [tprod_bot hL, finprod_eq_prod _ hf] using h _
    · rwa [tprod_bot hL, finprod_of_infinite_mulSupport hf]

Goal state after:
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 = a ^ Nat.card β

Tactic:
simp only [Nat.card_eq_zero_of_infinite, pow_zero]

Goal state after:
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
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
⊢ edist x y ≤ ↑K * ediam s

Tactic:
hf x y,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
⊢ ↑K * edist (f x) (f y) ≤ ↑K * ediam s
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
l : List X
⊢ (zipWith d (y :: l.reverse) (l.reverse ++ [x])).sum = (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
← sum_reverse,

Goal state after:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
l : List X
⊢ (zipWith d (y :: l.reverse) (l.reverse ++ [x])).reverse.sum = (zipWith d (x :: l) (l ++ [y])).sum
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
this✝ : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, y n ∈ closure[inst✝¹] {x k}
φ : ℕ → ℕ
hφ : StrictMono φ ∧ ∀ (n : ℕ), ∃ n_1 ≥ n, y n_1 ∈ closure[inst✝¹] {x (φ n)}
ψ : ℕ → ℕ
hψ1 : ∀ (n : ℕ), ψ n ≥ n
hψ2 : ∀ (n : ℕ), y (ψ n) ∈ closure[inst✝¹] {x (φ n)}
this : Tendsto ψ atTop atTop
n : ℕ
⊢ (x ∘ φ) n ⤳ (y ∘ ψ) n

Tactic:
exact specializes_iff_mem_closure.2 (hψ2 n)

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
⊢ 0 ∈ s

Tactic:
simp [s]

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_3.inl
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
hMl : l.length ≤ l.length
hMs : IsGreatest s l.length
hM_lt : l.length < L.length
hM_ltx : l.length < (x :: l).length
hM_lty : l.length < (l ++ [y]).length
⊢ d (l ++ [y])[l.length] y ≤ L.sum

Tactic:
simp only [getElem_append_right le_rfl, getElem_singleton, dist_self, zero_le]

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✝¹ : SemilatticeInf L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.inf' hne f) x

Tactic:
by
  simpa only [← Finset.inf'_apply] using finset_inf'_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✝¹ : SemilatticeInf L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.inf' hne f) t x

Tactic:
by
  simpa only [← Finset.inf'_apply] using finset_inf'_apply hne hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x✝¹ x✝ : α × β
a : α
b : β
hab : (a, b) ∈ s
x : α
y : β
hxy : (x, y) ∈ s
h : dist (a, b) (x, y) ≤ ε / (2 * C)
⊢ dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) (a, b)) (Function.uncurry (fun x1 x2 ↦ x1 • x2) (x, y)) ≤ ε

Tactic:
hC,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x✝¹ x✝ : α × β
a : α
b : β
hab : (a, b) ∈ Metric.ball 0 C
x : α
y : β
hxy : (x, y) ∈ Metric.ball 0 C
h : dist (a, b) (x, y) ≤ ε / (2 * C)
⊢ dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) (a, b)) (Function.uncurry (fun x1 x2 ↦ x1 • x2) (x, y)) ≤ ε
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
x y : α
h₁ : edist x y ≠ 0
h₂ : edist x y ≠ ∞
⊢ edist ((Isometry.toDilation f hf) x) ((Isometry.toDilation f hf) y) = ↑1 * edist x y

Tactic:
simp [hf x y]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
· obtain ⟨x, y, h₁, h₂⟩ := h
    exact ratio_unique h₁ h₂ (by simp [hf x y]) |>.symm

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : Prop
⊢ MeasurableSet {_a | p}

Tactic:
by_cases p

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
p : Prop
h✝ : p
⊢ MeasurableSet {_a | p}

case neg
α : Type u_1
m : MeasurableSpace α
p : Prop
h✝ : ¬p
⊢ MeasurableSet {_a | p}
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
⊢ Measurable f ↔ ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})

Tactic:
by
  refine ⟨fun hf n ↦ hf <| measurableSet_singleton _, fun h ↦ measurable_to_countable' fun n ↦ ?_⟩
  cases n with
  | top =>
    rw [← WithTop.none_eq_top, ← compl_range_some, preimage_compl, ← iUnion_singleton_eq_range,
      preimage_iUnion]
    exact .compl <| .iUnion h
  | coe n => exact h n

Goal state after: