mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.bot
h : ⊤ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊤ * ⊥ ≠ 0

Tactic:
{· simp_all [← EReal.coe_mul]}

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

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

Tactic:
simp_all [← EReal.coe_mul]

Goal state after:
case top.coe
a✝ : ℝ
h : ¬a✝ = 0
⊢ ¬⊤ * ↑a✝ = 0
Module: Mathlib.Data.EReal.Operations

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

Tactic:
{· simp_all [← EReal.coe_mul]}

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

Goal state before:
pp: case top.top
h : ⊤ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊤ * ⊤ ≠ 0

Tactic:
simp_all [← EReal.coe_mul]

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

Goal state before:
pp: case top.top
h : ⊤ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊤ * ⊤ ≠ 0

Tactic:
{· simp_all [← EReal.coe_mul]}

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg.inl
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
j : Subtype p
Hj : j ∉ m
Z : ∃ n, ⋯.choose n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
hZ : ⋯.choose (Nat.find Z) ∈ m
⊢ ⋯.choose (Nat.find ⋯) ∈ {j | BddBelow (range fun i ↦ f ↑i)}

Tactic:
exact hZ

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
i : ι
i_s : i ∈ s
bddsup : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' ⋯ fun i ↦ F i a
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)

Tactic:
exact h₁ i i_s

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

Goal state before:
pp: case e'_6
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b : β
⊢ a / f b = 1 * a / f b

Tactic:
one_mul

Goal state after:
case e'_6
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b : β
⊢ a / f b = a / f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

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

Tactic:
simp [← _root_.map_prod]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
ht : Multipliable fun a ↦ f ↑a
t' : Finset ↑t
⊢ ∏ b ∈ t', (fun a ↦ f ↑a) b ∈ o

Tactic:
← prod_subtype_map_embedding fun _ _ ↦ by rfl

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
ht : Multipliable fun a ↦ f ↑a
t' : Finset ↑t
⊢ ∏ x ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ t) t', f x ∈ o
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
b : β
hbt : b ∈ t
hb : ¬g b = f b
⊢ g b = 1

Tactic:
exact (h b).resolve_right hb

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

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
⊢ (CauchySeq fun s ↦ ∏ n ∈ s, f n) ↔ ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e

Tactic:
refine cauchySeq_finset_iff_tprod_vanishing.trans ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩
  · obtain ⟨s, hs⟩ := vanish e he
    refine ⟨if h : s.Nonempty then s.max' h + 1 else 0,
      fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩
    split_ifs at ht with h
    · exact fun m hmt hms ↦ (s.le_max' _ hms).not_gt (Nat.succ_le_iff.mp <| ht hmt)
    · exact fun _ _ hs ↦ h ⟨_, hs⟩
  · obtain ⟨N, hN⟩ := vanish e he
    exact ⟨range N, fun t ht ↦ hN _ fun n hnt ↦
      le_of_not_gt fun h ↦ Set.disjoint_left.mp ht hnt (mem_range.mpr h)⟩

Goal state after:
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
this : Injective Int.negSucc
⊢ HasProd (fun n ↦ f ↑n * f (Int.negSucc n)) m

Tactic:
refine hf.hasProd_of_prod_eq fun u ↦ ?_

Goal state after:
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, ∀ (v' : Finset ℕ), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', f x = ∏ b ∈ v', f ↑b * f (Int.negSucc b)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case codisjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
· rw [codisjoint_iff_le_sup]
      rintro (i | j) <;> simp

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

Goal state before:
pp: ⊢ comap Real.toNNReal atTop = atTop

Tactic:
by
  refine le_antisymm ?_ tendsto_real_toNNReal_atTop.le_comap
  refine (atTop_basis_Ioi' 0).ge_iff.2 fun a ha ↦ ?_
  filter_upwards [preimage_mem_comap (Ioi_mem_atTop a.toNNReal)] with x hx
  exact (Real.toNNReal_lt_toNNReal_iff_of_nonneg ha.le).1 hx

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 X
s : Set X
hs : IsSeqClosed s
⊢ closure[inst✝²] s = s

Tactic:
← seqClosure_eq_closure,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
⊢ seqClosure s = s
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
⊢ a - ε ≤ f n

Tactic:
tsub_le_iff_right

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a ≤ ε + f n
⊢ a ≤ f n + ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a - ε ≤ f n
⊢ a - f n ≤ ε

Tactic:
tsub_le_iff_right

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a ≤ f n + ε
⊢ a ≤ ε + f n
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen

Tactic:
exact monotone_gen

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

Goal state before:
pp: case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen

Tactic:
exact monotone_gen

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

Goal state before:
pp: case refine_3
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
k : ℕ
hl : 0 < k + 1
⊢ ‖v (k + 1)‖ < b (k + 1)

Tactic:
← norm_inv'

Goal state after:
case refine_3
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
k : ℕ
hl : 0 < k + 1
⊢ ‖(v (k + 1))⁻¹‖ < b (k + 1)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun x_1 ↦ x_1 * x) (𝓝[<] 1) (𝓝 (1 * x))
⊢ x ≤ y

Tactic:
one_mul

Goal state after:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun x_1 ↦ x_1 * x) (𝓝[<] 1) (𝓝 x)
⊢ x ≤ y
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : ↑f ≤ 𝓝 a
hb : ↑g ≤ 𝓝 b
⊢ Inseparable a b ↔ Inseparable f g

Tactic:
by
  rw [← tendsto_id'] at ha hb
  rw [inseparable_iff, (ha.comp tendsto_fst).inseparable_iff_uniformity (hb.comp tendsto_snd)]
  simp only [Function.comp_apply, id_eq, Prod.mk.eta, ← Function.id_def, tendsto_id']

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : b ≤ x
⊢ projIcc a b h x = ⟨b, ⋯⟩

Tactic:
simp [projIcc, hx, h]

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

Goal state before:
pp: case mp.refine_1
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
n m N : β
hn : N ≤ n
hm : N ≤ m
⊢ edist (s n) (s m) ≤ (fun N ↦ ediam (s '' Ici N)) N

Tactic:
exact Metric.edist_le_ediam_of_mem (mem_image_of_mem _ hn) (mem_image_of_mem _ hm)

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

Goal state before:
pp: case inr
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))

Tactic:
simp only [← sup'_eq_sup hne]
    exact finset_sup'_nhds 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
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.sup' hne f) x

Tactic:
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:
simpa only [← Finset.sup'_apply] using finset_sup'_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 : dist a 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
⊢ dist a 0 * dist b y + dist a x * dist y 0 ≤ ε

Tactic:
hab.1,

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 : dist a 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
⊢ C * dist b y + dist a x * dist y 0 ≤ ε
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' ball b r = ball (b / a) r

Tactic:
rw [div_eq_mul_inv]
  exact preimage_smul_ball (MulOpposite.op a) b r

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

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

Tactic:
norm_mul,

Goal state after:
α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖z⁻¹ * (w - z)‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
Module: Mathlib.Analysis.Normed.Field.Basic

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

Tactic:
norm_mul,

Goal state after:
α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖z⁻¹‖ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r

Tactic:
by rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
x y : X
⊢ edist x y = 1 * edist x y

Tactic:
one_mul

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
x y : X
⊢ edist x y = edist x y
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: R : Type u_1
r : R
s : ℝ≥0
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0∞
⊢ ↑(r • s) = ↑(r • (1 * s))

Tactic:
one_mul

Goal state after:
R : Type u_1
r : R
s : ℝ≥0
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0∞
⊢ ↑(r • s) = ↑(r • s)
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑n + 1‖ ≤ ↑n * ‖1‖ + 1 * ‖1‖

Tactic:
one_mul

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑n + 1‖ ≤ ↑n * ‖1‖ + ‖1‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ 1 * ‖r • x‖ = ‖r • x‖

Tactic:
one_mul

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r • x‖ = ‖r • x‖
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π ↑i_1
⊢ updateFinset x {i} y = update x i (y ⟨i, ⋯⟩)

Tactic:
by
  congr with j
  by_cases hj : j = i
  · cases hj
    simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]
  · simp [hj, updateFinset]

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

Goal state before:
pp: E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ 2 * r ≤ diam (sphere x r)

Tactic:
calc
    2 * r = dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) := by
      simp [dist_eq_norm, ← two_nsmul, ← smul_assoc, norm_smul, abs_of_nonneg hr, hy, mul_assoc]
    _ ≤ diam (sphere x r) := by
      apply dist_le_diam_of_mem isBounded_sphere <;> simp [norm_smul, hy, abs_of_nonneg hr]

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

Goal state before:
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
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ ‖x‖ ≤ 1 * ‖x‖

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
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (Infinite.natEmbedding 𝕜) k - (Infinite.natEmbedding 𝕜) n ≠ 0

Tactic:
one_mul

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
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ ‖x‖ ≤ ‖x‖

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
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (Infinite.natEmbedding 𝕜) k - (Infinite.natEmbedding 𝕜) n ≠ 0
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
hc : Bornology.IsCobounded c
⊢ Bornology.IsCobounded (⇑(algebraMap 𝕜 𝕜') ⁻¹' c)

Tactic:
← isBounded_compl_iff,

Goal state after:
𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
hc : Bornology.IsBounded cᶜ
⊢ Bornology.IsBounded (⇑(algebraMap 𝕜 𝕜') ⁻¹' c)ᶜ
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
⊢ ‖-x + y‖ = ‖-y + x‖

Tactic:
show ‖-x + y‖ = ‖-y + x‖
    have : -y + x = (-1 : 𝕜) • (-x + y) := by simp; abel
    rw [this, core.norm_smul]
    simp

Goal state after:
Module: Mathlib.Data.Real.ENatENNReal

Goal state before:
pp: n : ℕ∞
⊢ ↑n = ∞ ↔ n = ⊤

Tactic:
simp [← toENNReal_inj]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ μ (⋃ i, t i) = μ (⋃ i, disjointed t i)

Tactic:
iUnion_disjointed

Goal state after:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ μ (⋃ i, t i) = μ (⋃ i, t i)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)

Tactic:
have ht' : ∀ (i j) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩ := by
    intro i j x hxi hxj
    rcases eq_or_ne i j with rfl | hij
    · rfl
    · exact ht hij ⟨hxi, hxj⟩

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
ht' : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ Measurable uniqueElim

Tactic:
simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ Measurable fun x ↦ x
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case neg
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = neg
⊢ sign (∑ i ∈ s, f i) = neg

Tactic:
simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h ⊢

Goal state after:
case neg
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, f i < 0
⊢ ∑ i ∈ s, f i < 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : ℝ
⊢ ↑(sign x) * ↑(↑x).abs = ↑x

Tactic:
coe_abs,

Goal state after:
x : ℝ
⊢ ↑(sign x) * ↑|x| = ↑x
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ 1 * (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Tactic:
one_mul

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ (↑(↑a).abs)⁻¹ = (↑a)⁻¹
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
h : ∑' (i : α), (fun i ↦ ↑(f i)) i ≠ ∞
⊢ (support fun i ↦ ↑(f i)).Countable

Tactic:
simpa [support] using (ENNReal.tsum_coe_ne_top_iff_summable.1 h).countable_support_nnreal

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ ∑ i ∈ Finset.Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)

Tactic:
Finset.sum_Ico_eq_sum_range

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ ∑ k ∈ Finset.range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)