mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: case inl
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)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hmn : m < n
⊢ False

pp: case inr
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)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ False

Tactic:
· exact hmin m hmn ⟨y, hyH, hm, hya⟩

Goal state after:
case inr
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)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ False
Module: Mathlib.Analysis.Normed.Group.Rat

Goal state before:
pp: r₁ r₂ : ℚ
⊢ |↑r₁ - ↑r₂| = |-↑r₁ + ↑r₂|

Tactic:
rw [← abs_neg, neg_sub]

Goal state after:
r₁ r₂ : ℚ
⊢ |↑r₂ - ↑r₁| = |-↑r₁ + ↑r₂|
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ blimsup u f p = blimsup u f q

Tactic:
simp only [blimsup_eq]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ limsup u (f ⊔ g) = limsup u f ⊔ limsup u g

Tactic:
refine le_antisymm ?_
    (sup_le (limsup_le_limsup_of_le le_sup_left) (limsup_le_limsup_of_le le_sup_right))
  simp_rw [limsup_eq, sInf_sup_eq, sup_sInf_eq, mem_ofPred_eq, le_iInf₂_iff]
  intro a ha b hb
  exact sInf_le ⟨ha.mono fun _ h ↦ h.trans le_sup_left, hb.mono fun _ h ↦ h.trans le_sup_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 : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ edist ((fun x ↦ (f x, g x)) x) ((fun x ↦ (f x, g x)) y) ≤ max ↑Kf ↑Kg * edist x y

Tactic:
Prod.edist_eq,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ max (edist ((fun x ↦ (f x, g x)) x).1 ((fun x ↦ (f x, g x)) y).1)
      (edist ((fun x ↦ (f x, g x)) x).2 ((fun x ↦ (f x, g x)) y).2) ≤
    max ↑Kf ↑Kg * edist x y
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ClusterPt f.limsSup f

Tactic:
by
  by_cases! hn : Nontrivial α
  · by_cases! htop : ∀ x, x ≤ f.limsSup
    · let : OrderTop α := { top := f.limsSup, le_top := htop }
      exact nhds_top_basis.clusterPt_iff_frequently |>.mpr fun a => frequently_lt_of_lt_limsSup hc
    · by_cases! hbot : ∀ x, f.limsSup ≤ x
      · let : OrderBot α := { bot := f.limsSup, bot_le := hbot }
        refine nhds_bot_basis.clusterPt_iff_frequently |>.mpr fun a h => ?_
        exact lt_mem_sets_of_limsSup_lt hb h |>.frequently
      · refine (nhds_basis_Ioo' hbot htop).clusterPt_iff_frequently |>.mpr fun a ⟨hl, hg⟩ => ?_
        exact frequently_lt_of_lt_limsSup hc hl |>.and_eventually <| lt_mem_sets_of_limsSup_lt hb hg
  · simp_all [ClusterPt, Filter.eq_top_of_neBot]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x✝ : α
hx : x✝ ∈ s
y✝ : α
hy : y✝ ∈ s
⊢ edist ((fun x ↦ (f x, g x)) x✝) ((fun x ↦ (f x, g x)) y✝) ≤ max ↑Kf ↑Kg * edist x✝ y✝

Tactic:
Prod.edist_eq,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x✝ : α
hx : x✝ ∈ s
y✝ : α
hy : y✝ ∈ s
⊢ max (edist ((fun x ↦ (f x, g x)) x✝).1 ((fun x ↦ (f x, g x)) y✝).1)
      (edist ((fun x ↦ (f x, g x)) x✝).2 ((fun x ↦ (f x, g x)) y✝).2) ≤
    max ↑Kf ↑Kg * edist x✝ y✝
Module: Mathlib.Data.EReal.Operations

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

Tactic:
by
  rw [add_comm, ← add_sub_assoc, add_sub_cancel_left]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
hx : ∀ i ∈ l, ∃ i_2, (p i_2 ∧ i_2 ∈ i) ∧ x ∈ u i_2
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i

Tactic:
choose g hg hg' using hx

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst✝³ : ConditionallyCompleteLinearOrder β
f✝¹ : Filter α
u : α → β
inst✝² : ConditionallyCompleteLinearOrder α
f✝ : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
j✝ : Subtype p
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
g : ℕ → Subtype p := ⋯.choose
j : Subtype p
hj : j ∈ m
⊢ ∃ n, g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
rcases (exists_surjective_nat (Subtype p)).choose_spec j with ⟨n, rfl⟩

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst✝³ : ConditionallyCompleteLinearOrder β
f✝¹ : Filter α
u : α → β
inst✝² : ConditionallyCompleteLinearOrder α
f✝ : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
j : Subtype p
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
g : ℕ → Subtype p := ⋯.choose
n : ℕ
hj : ⋯.choose n ∈ m
⊢ ∃ n, g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
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.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst✝ : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
⊢ Tendsto (fun x ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔ Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
refine tendsto_congr' ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst✝ : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
⊢ (fun x ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) =ᶠ[L.filter] fun s ↦ ∏ b ∈ s, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
⊢ HasProd (fun n ↦ f ↑n * f (-(↑n + 1))) m

Tactic:
change HasProd (fun n : ℕ ↦ f n * f (Int.negSucc n)) m

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
⊢ HasProd (fun n ↦ f ↑n * f (Int.negSucc n)) m
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case refine_1.ofNat
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
a✝ : ℕ
hx : Int.ofNat a✝ ∈ u
⊢ (∃ a ∈ v', ↑a = Int.ofNat a✝) ∨ ∃ a ∈ v', Int.negSucc a = Int.ofNat a✝

Tactic:
exact Or.inl ⟨_, hv' (by simpa using Or.inl hx), rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
hf : ∃ b, f b = 0
inst✝ : L.LeAtTop
⊢ HasProd f 0 L

Tactic:
obtain ⟨b, hb⟩ := hf

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b : β
hb : f b = 0
⊢ HasProd f 0 L
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (fun s ↦ ∑' (b : { x // x ∉ s }), f ↑b) atTop (𝓝 0)

Tactic:
simp_rw [← tendsto_coe, coe_tsum, NNReal.coe_zero]

Goal state after:
α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (fun a ↦ ∑' (a_1 : { x // x ∉ a }), ↑(f ↑a_1)) atTop (𝓝 0)
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
hx : x ∉ s
⊢ ∃ u, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ (x : ℕ) in atTop, u x ∈ s

Tactic:
by
      simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop,
        ← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not, not_false_eq_true,
        not_true_eq_false] using h (· ∉ s) x

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
rcases exists_antitone_basis (𝓤 X) with ⟨V, hV⟩

Goal state after:
X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
⊢ ∃ x ∈ s, l ≤ 𝓝 x
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
have := hl.1
  rcases exists_antitone_basis (𝓤 X) with ⟨V, hV⟩
  choose W hW hWV using fun n => comp_mem_uniformity_sets (hV.mem n)
  have hWV' : ∀ n, W n ⊆ V n := fun n ⟨x, y⟩ hx =>
    @hWV n (x, y) ⟨x, refl_mem_uniformity <| hW _, hx⟩
  obtain ⟨t, ht_anti, htl, htW, hts⟩ :
      ∃ t : ℕ → Set X, Antitone t ∧ (∀ n, t n ∈ l) ∧ (∀ n, t n ×ˢ t n ⊆ W n) ∧ ∀ n, t n ⊆ s := by
    have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s := by
      rw [le_principal_iff] at hls
      have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
      simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff,
        prod_self_subset_prod_self, and_assoc] using! this
    choose t htl htW hts using this
    have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
    exact ⟨fun n => ⋂ k ≤ n, t k, fun m n h =>
      biInter_subset_biInter_left fun k (hk : k ≤ m) => hk.trans h, fun n =>
      (biInter_mem (finite_le_nat n)).2 fun k _ => htl k, fun n =>
      (prod_mono (this n) (this n)).trans (htW n), fun n => (this n).trans (hts n)⟩
  choose u hu using fun n => Filter.nonempty_of_mem (htl n)
  have huc : CauchySeq u := hV.toHasBasis.cauchySeq_iff.2 fun N _ =>
      ⟨N, fun m hm n hn => hWV' _ <| @htW N (_, _) ⟨ht_anti hm (hu _), ht_anti hn (hu _)⟩⟩
  rcases hs.exists_tendsto (fun n => hts n (hu n)) huc with ⟨x, hxs, hx⟩
  refine ⟨x, hxs, (nhds_basis_uniformity' hV.toHasBasis).ge_iff.2 fun N _ => ?_⟩
  obtain ⟨n, hNn, hn⟩ : ∃ n, N ≤ n ∧ u n ∈ ball x (W N) :=
    ((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists
  refine mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩
  exact ⟨ht_anti hNn (hu n), ht_anti hNn hy⟩

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
u : Finset ((b : β) × γ b)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → b ∈ (fun s ↦ ∏ b ∈ s, f b) ⁻¹' s
bs : Finset β
⊢ bs ∈ Set.Ici (image Sigma.fst u) → ∏ b ∈ bs, g b ∈ id s

Tactic:
hbs

Goal state after:
case right
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
u : Finset ((b : β) × γ b)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → b ∈ (fun s ↦ ∏ b ∈ s, f b) ⁻¹' s
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
⊢ ∏ b ∈ bs, g b ∈ id s
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ (((𝓤 α).lift' gen).lift' fun s ↦ s ○ s) ≤ (𝓤 α).lift' gen

Tactic:
by exact comp_gen

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : NormedAddCommGroup α
inst✝¹ : Lattice α
inst✝ : HasSolidNorm α
x y : ℤ
h : |x| ≤ |y|
⊢ ‖x‖ ≤ ‖y‖

Tactic:
simpa [← Int.norm_cast_real, ← Int.cast_abs] using h

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
z x y : α
⊢ dist (x ⊔ z) (y ⊔ z) ≤ ↑1 * dist x y

Tactic:
NNReal.coe_one,

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
z x y : α
⊢ dist (x ⊔ z) (y ⊔ z) ≤ 1 * dist x y
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ * (‖z‖ * ‖w‖)⁻¹

Tactic:
mul_inv

Goal state after:
α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹)
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ediam s ≤ (↑(ratio f))⁻¹ * ediam (⇑f '' s)

Tactic:
← ENNReal.coe_inv

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ediam s ≤ ↑(ratio f)⁻¹ * ediam (⇑f '' s)

α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ratio f ≠ 0
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: c : ℝ≥0
⊢ c • 1 = ↑c

Tactic:
simp [smul_def]

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
⊢ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t = {i_1 | i_1 ∈ i :: l}.pi t

Tactic:
ext f
    have h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ i : ι, i ∈ l → f i ∈ t i := by
      change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ { x | x ∈ l }.pi t
      rw [mk_preimage_tprod l t]
    -- `simp [Set.TProd, TProd.mk, this]` can close this goal but is slow.
    rw [Set.tprod, TProd.mk, mem_preimage, mem_pi, prodMk_mem_set_prod_eq]
    simp_rw [mem_ofPred_eq, mem_cons]
    rw [forall_eq_or_imp, and_congr_right_iff]
    exact fun _ => h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ MeasurableSet (insert a s) ↔ MeasurableSet s

Tactic:
by
  classical
  exact ⟨fun h =>
    if ha : a ∈ s then by rwa [← insert_eq_of_mem ha]
    else insert_sdiff_self_of_notMem ha ▸ h.diff (.singleton _),
    fun h => h.insert a⟩

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x y : 𝕜
⊢ dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y * ‖1‖

Tactic:
simp only [dist_eq_norm, ← map_sub, norm_algebraMap]

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

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
s : Set β
x : β
hs : MeasurableSet s
hx : x ∈ s
a : β
⊢ a ∈ ⋂ (_ : MeasurableSet s), s → a ∈ s

Tactic:
simp [hs]

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

Goal state before:
pp: case hd
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable fun i ↦ ↑(d i)
⊢ Summable d

Tactic:
· exact_mod_cast hd

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Tactic:
rcases h with ⟨f, hf⟩

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi t
⊢ MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_4
β : α → Type u_3
f : (x : α) × β x → ℝ
hf : ∀ (x : (x : α) × β x), 0 ≤ f x
⊢ Summable f ↔ (∀ (x : α), Summable fun y ↦ f ⟨x, y⟩) ∧ Summable fun x ↦ ∑' (y : β x), f ⟨x, y⟩

Tactic:
lift f to (Σ x, β x) → ℝ≥0 using hf
  simpa using mod_cast NNReal.summable_sigma

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

Goal state before:
pp: case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ ↑(sign x) * |x| = x

Tactic:
simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ↑(sign 0) * |0| = 0

Tactic:
simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ ↑(sign x) * |x| = x

Tactic:
simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ |x| * ↑(sign x) = x

Tactic:
simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ |0| * ↑(sign 0) = 0

Tactic:
simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ |x| * ↑(sign x) = x

Tactic:
simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ ↑(sign x) * x = |x|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ↑(sign 0) * 0 = |0|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ ↑(sign x) * x = |x|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ x * ↑(sign x) = |x|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ 0 * ↑(sign 0) = |0|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ x * ↑(sign x) = |x|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ ↑(m / (n✝ + 1) * (n✝ + 1)) ≤ ↑m

pp: case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ 0 < ↑(n✝ + 1)

Tactic:
@Nat.cast_le

Goal state after:
case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ m / (n✝ + 1) * (n✝ + 1) ≤ m

case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ 0 < ↑(n✝ + 1)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a ↦ ↑(f a)) ↑a

Tactic:
rw [ha]

Goal state after:
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a ↦ ↑(f a)) (∑' (b : β), ↑(f b))
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∀ (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
rw [← ENNReal.tsum_eq_zero] at hf
    have : Tendsto (fun s : Finset α => ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' i, f i)) := by
      simp only [← Finset.mul_sum]
      exact ENNReal.Tendsto.const_mul ENNReal.summable.hasSum (Or.inl hf)
    exact HasSum.tsum_eq this

Goal state after: