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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ PseudoMetricSpace.toUniformSpace = PseudoMetricSpace.toUniformSpace

Tactic:
simp +instances [replaceDist_eq]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ PseudoMetricSpace.toBornology = PseudoMetricSpace.toBornology

Tactic:
simp +instances [replaceDist_eq]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ENNReal.ofReal ‖a⁻¹ * b‖ = ‖a⁻¹ * b‖ₑ

Tactic:
ofReal_norm'

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a⁻¹ * b‖ₑ = ‖a⁻¹ * b‖ₑ
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ENNReal.ofReal ‖a / b‖ = ‖a / b‖ₑ

Tactic:
ofReal_norm'

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖a / b‖ₑ = ‖a / b‖ₑ
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : ∀ i ∈ s, g i ≠ ∞
⊢ (↑s).Pairwise fun i j ↦ g i ≠ 0 ∨ g j ≠ ∞

Tactic:
grind [Set.Pairwise]

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

Goal state before:
pp: ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : ∀ i ∈ s, g i ≠ 0
⊢ (↑s).Pairwise fun i j ↦ g i ≠ 0 ∨ g j ≠ ∞

Tactic:
grind [Set.Pairwise]

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto f atTop (𝓝 a)

Tactic:
by
  suffices Tendsto (rangeFactorization f) atTop atTop from
    (SupConvergenceClass.tendsto_coe_atTop_isLUB _ _ ha).comp this
  exact h_mono.rangeFactorization.tendsto_atTop_atTop fun b => b.2.imp fun a ha => ha.ge

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

Goal state before:
pp: x y : EReal
⊢ (x + y).toENNReal ≤ x.toENNReal + y.toENNReal

Tactic:
induction x <;> induction y <;> try {· simp}
  exact ENNReal.ofReal_add_le

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
x y : α
h : edist x y ≠ ∞
⊢ ↑K * edist x y < ∞

Tactic:
by finiteness

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 : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
⊢ ∀ x ∈ s, ∀ y ∈ t, ∀ x_1 ∈ s, ∀ y_1 ∈ t, edist (f x y) (f x_1 y_1) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t

Tactic:
intro a₁ ha₁ b₁ hb₁ a₂ ha₂ b₂ hb₂

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
b₁ : β
hb₁ : b₁ ∈ t
a₂ : α
ha₂ : a₂ ∈ s
b₂ : β
hb₂ : b₂ ∈ t
⊢ edist (f a₁ b₁) (f a₂ b₂) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case refine_1
α : 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)
i : ↑{i | q i}
⊢ x ∈ u ((fun i ↦ g (b ↑i) ⋯) i)

pp: case refine_2
α : 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)
i : ↑{i | q i}
⊢ p ((fun i ↦ g (b ↑i) ⋯) i) ∧ (fun i ↦ g (b ↑i) ⋯) i ∈ b ↑i

Tactic:
· exact hg' (b i) (hl.mem_of_mem i.2)

Goal state after:
case refine_2
α : 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)
i : ↑{i | q i}
⊢ p ((fun i ↦ g (b ↑i) ⋯) i) ∧ (fun i ↦ g (b ↑i) ⋯) i ∈ b ↑i
Module: Mathlib.Logic.Encodable.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → x ∉ f b

Tactic:
rintro a rfl ha b rfl hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
x : α
a : β
ha : x ∈ f a
b : β
ij : encode a ≠ encode b
hb : x ∈ f b
⊢ False
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_left h =>

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : 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)
B : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i

Tactic:
simp_rw [hv.liminf_eq_sSup_iUnion_iInter, A, B, sSup_iUnion_Iic]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
⊢ liminf f v =
    if ∃ j, s ↑j = ∅ then sSup univ
    else if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i

Tactic:
rw [if_neg H]

Goal state after:
case neg
α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
⊢ liminf f v = if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg.H
α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∃ j, BddBelow (range fun i ↦ f ↑i)

Tactic:
push Not at H'
    exact H'

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a

Tactic:
by
  by_cases ha : a = 0
  · simp [ha]
  · exact ((Homeomorph.mulRight₀ a ha).isClosedEmbedding.map_tsum f
      (g := AddMonoidHom.mulRight a)).symm

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

Goal state before:
pp: case inr
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
hL : L.filter = ⊥
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L

Tactic:
· simp [Summable, HasSum, hL]

Goal state after:
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
⊢ Tendsto (fun n ↦ a - f n) l (𝓝 0) ↔ Tendsto (fun n ↦ f n) l (𝓝 a)

Tactic:
rw [ENNReal.tendsto_nhds_zero, ENNReal.tendsto_nhds ha]
  refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
  · filter_upwards [h ε hε] with n hn
    refine ⟨?_, (hfa n).trans (le_add_right le_rfl)⟩
    rw [tsub_le_iff_right] at hn ⊢
    rwa [add_comm]
  · filter_upwards [h ε hε] with n hn
    have hN_left := hn.1
    rw [tsub_le_iff_right] at hN_left ⊢
    rwa [add_comm]

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

Goal state before:
pp: β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ 2 ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: case refine_2
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
M : ℕ
hMl : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
⊢ d (x :: l)[M] (l ++ [y])[M] ≤ L.sum

Tactic:
exact single_le_sum (fun x _ => zero_le) _ (mem_iff_get.2 ⟨⟨M, hM_lt⟩, getElem_zipWith⟩)

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 : x ∈ Icc a b
⊢ projIcc a b h x = ⟨x, hx⟩

Tactic:
by
  simp [projIcc, hx.1, hx.2]

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

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
have B : ∀ y : α, BddBelow (range fun x : s => f x + K * dist y x) := fun y => by
    rcases hs with ⟨z, hz⟩
    refine ⟨f z - K * dist y z, ?_⟩
    rintro w ⟨t, rfl⟩
    dsimp
    rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]
    calc
      f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2
      _ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: 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))
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | hne
  · simpa using! tendsto_const_nhds
  · simp only [← sup'_eq_sup hne]
    exact finset_sup'_nhds 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 : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ - -a ⊔ -a ≤ |b|

Tactic:
← neg_inf

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ |b|
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 α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
⊢ (n, y) ∈ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < 1} →
    (n, y) ∈ (fun y ↦ (g y.2, G y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < 1} →
      (n, y) ∈ Prod.snd ⁻¹' {x | dist (f x) 0 ≤ C ∧ dist (g x) 0 ≤ C} →
        ((f (n, y).2, g (n, y).2), F (n, y).1 (n, y).2, G (n, y).1 (n, y).2) ∈
          Metric.ball 0 (C + 1) ×ˢ Metric.ball 0 (C + 1)

Tactic:
hFn

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : (n, y) ∈ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < 1}
⊢ (n, y) ∈ (fun y ↦ (g y.2, G y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < 1} →
    (n, y) ∈ Prod.snd ⁻¹' {x | dist (f x) 0 ≤ C ∧ dist (g x) 0 ≤ C} →
      ((f (n, y).2, g (n, y).2), F (n, y).1 (n, y).2, G (n, y).1 (n, y).2) ∈
        Metric.ball 0 (C + 1) ×ˢ Metric.ball 0 (C + 1)
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: case inl
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
⊢ ⨆ i, ∏ a, f a (i a) = ∏ a, ⨆ i, f a i

Tactic:
rw [iSup_of_isEmpty, eq_comm, Finset.prod_eq_zero_iff]

Goal state after:
case inl
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
⊢ ∃ a ∈ Finset.univ, ⨆ i, f a i = 0
Module: Mathlib.Data.Finset.Update

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

pp: case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π ↑i_1
j : ι
hj : ¬j = i
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j

Tactic:
· cases hj
    simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]

Goal state after:
case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π ↑i_1
j : ι
hj : ¬j = i
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ ‖k • e‖ < ‖e‖ ↔ k • e = ↑0

Tactic:
AddSubgroup.coe_zero,

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ ‖k • e‖ < ‖e‖ ↔ k • e = 0
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:
have : -y + x = (-1 : 𝕜) • (-x + y) := by simp; abel

Goal state after:
𝕜✝ : 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
this : -y + x = -1 • (-x + y)
⊢ ‖-x + y‖ = ‖-y + x‖
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:
by
    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.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
⊢ CauchySeq f

Tactic:
lift d to ℕ → ℝ≥0 using fun n ↦ dist_nonneg.trans (hf n)
  apply cauchySeq_of_edist_le_of_summable d (α := α) (f := f)
  · exact_mod_cast hf
  · exact_mod_cast hd

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

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

Tactic:
| neg_left h =>

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

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

Tactic:
| neg_left h =>

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

Goal state before:
pp: α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
h_f_coe : f = fun n ↦ ↑(f n).toNNReal
⊢ Tendsto (fun n ↦ ↑(f n).toNNReal) cofinite (𝓝 0)

Tactic:
← @coe_zero,

Goal state after:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
h_f_coe : f = fun n ↦ ↑(f n).toNNReal
⊢ Tendsto (fun n ↦ ↑(f n).toNNReal) cofinite (𝓝 ↑0)
Module: Mathlib.Data.EReal.Inv

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

Tactic:
simp only [abs_def a, coe_ennreal_ofReal, abs_nonneg, max_eq_left]

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ (↑|a|)⁻¹ = (↑a)⁻¹
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ LowerHemicontinuousAt f x ↔ ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t

Tactic:
by
  rw [← lowerHemicontinuousWithinAt_univ_iff, lowerHemicontinuousWithinAt_iff_frequently]
  simp

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun a ↦ ↑(f a).toNNReal

Tactic:
refine .of_nonneg_of_le (fun n => NNReal.coe_nonneg _) (fun n => ?_) hf.abs

Goal state after:
α : Type u_1
f : α → ℝ
hf : Summable f
n : α
⊢ ↑(f n).toNNReal ≤ |f n|
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : 0 ≤ d
⊢ d ≤ c

Tactic:
obtain ⟨a', aa', dab⟩ := exists_lt_mul_left_of_nonneg ha d0 dab

Goal state after:
case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab✝ : d < a * b
d0 : 0 ≤ d
a' : EReal
aa' : a' ∈ Ioo 0 a
dab : d < a' * b
⊢ d ≤ c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ ⊤ ≤ liminf u f + liminf v f

Tactic:
rw [h, top_add_of_ne_bot h']

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

Goal state before:
pp: case refine_1
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
⊢ False

Tactic:
by_cases hr : 1 = |r|
    · replace h : Tendsto (fun n : ℕ ↦ |r| ^ n) atTop (𝓝 0) := by simpa only [← abs_pow, h]
      simp only [hr.symm, one_pow] at h
      exact zero_ne_one <| tendsto_nhds_unique h tendsto_const_nhds
    · apply @not_tendsto_nhds_of_tendsto_atTop 𝕜 ℕ _ _ _ _ atTop _ (fun n ↦ |r| ^ n) _ 0 _
      · refine (pow_right_strictMono₀ <| lt_of_le_of_ne (le_of_not_gt hr_le)
          hr).monotone.tendsto_atTop_atTop (fun b ↦ ?_)
        obtain ⟨n, hn⟩ := (pow_unbounded_of_one_lt b (lt_of_le_of_ne (le_of_not_gt hr_le) hr))
        exact ⟨n, le_of_lt hn⟩
      · simpa only [← abs_pow]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
ι : Type u_4
γ : Type u_5
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : LinearOrder γ
inst✝³ : IsOrderedAddMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun z ↦ ∑ i ∈ a, f i z) x

Tactic:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  exact lowerSemicontinuousWithinAt_sum ha

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
n m : ℕ
hm : s m ⊆ dissipate s n
k : ℕ
hk : (fun x1 x2 ↦ x1 ⊇ x2) (s m) (s k) ∧ (fun x1 x2 ↦ x1 ⊇ x2) (s (n + 1)) (s k)
⊢ s k ⊆ dissipate s (n + 1)

Tactic:
simp; grind

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

Goal state before:
pp: case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1

Tactic:
refine (div_le_one <| mod_cast hn).mpr ?_

Goal state after:
case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ ↑x + 1 + 1 ≤ ↑k + 1
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
⊢ c • extend m = extend fun s h ↦ c • m s h

Tactic:
classical
  ext s; by_cases h : P s <;> simp [extend, ENNReal.smul_top, *]

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

Goal state before:
pp: case e'_3
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ m (t ∩ ⋃ i, s i) = m (⋃ i, t ∩ s i)

pp: case e'_4
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i) = ∑' (i : ℕ), m (t ∩ s i)

Tactic:
· simp [inter_iUnion]

Goal state after:
case e'_4
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i) = ∑' (i : ℕ), m (t ∩ s i)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case h
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
n i : ℕ
⊢ ⋃ (_ : i < n), s i ⊆ s i

Tactic:
exact iUnion_subset fun _ => .rfl

Goal state after: