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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
⊢ LocallyLipschitz f^[0]

Tactic:
by simpa only [pow_zero] using! LocallyLipschitz.id

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f^[n] ∘ f)

Tactic:
exact (hf.iterate n).comp hf

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
h : LocallyLipschitz f
⊢ LocallyLipschitz (f ^ 0)

Tactic:
by simpa only [pow_zero] using! LocallyLipschitz.id

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

Goal state before:
pp: case top_pos
x✝ : ℝ
hx : 0 < x✝
⊢ 0 < ⊤ * ↑x✝ ↔ 0 < ⊤ ∧ 0 < ↑x✝ ∨ ⊤ < 0 ∧ ↑x✝ < 0

Tactic:
simp [EReal.top_mul_coe_of_pos hx, hx]

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

Goal state before:
pp: case pos
β : Type u_2
L : SummationFilter β
h : L.filter = ⊥
⊢ L.NeBot ∨ L.filter = ⊥

Tactic:
exact .inr h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.HasSupport
f : γ ↪ β
⊢ ∀ᶠ (a : Finset β) in L.filter, ⇑f ⁻¹' ↑a ⊆ ⇑f ⁻¹' L.support

Tactic:
filter_upwards [L.eventually_le_support] with a using Set.preimage_mono

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : 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)
j : Subtype p
hj : j ∈ m
⊢ ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
have : j = liminfReparam f s p j := by simp only [m, liminfReparam, hj, ite_true]
        conv_lhs => rw [this]
        apply subset_iUnion _ j

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

Goal state before:
pp: case top_pos
x✝ : ℝ
hx : 0 < x✝
⊢ ⊤ * ↑x✝ = ⊤ ↔ ⊤ = ⊥ ∧ ↑x✝ < 0 ∨ ⊤ < 0 ∧ ↑x✝ = ⊥ ∨ ⊤ = ⊤ ∧ 0 < ↑x✝ ∨ 0 < ⊤ ∧ ↑x✝ = ⊤

Tactic:
simp [EReal.top_mul_coe_of_pos hx, hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
⊢ HasProd f a L

Tactic:
by
  have : L.filter = ⊥ := by contrapose! hL; exact ⟨hL⟩
  rw [HasProd, this]
  exact tendsto_bot

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
⊢ (if L.HasSupport ∧ (mulSupport fun b ↦ f b).Finite then ∏ᶠ (b : β), f b
    else if HasProd (fun b ↦ f b) 1 L then 1 else Exists.choose ⋯) =
    ∏ᶠ (b : β), f b

Tactic:
rwa [if_neg (by tauto), if_pos (hasProd_bot hL _ _), finprod_of_infinite_mulSupport]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a₁ : α
inst✝¹ : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ Function.update f b a b = (if b = b then a / f b else 1) * f b

Tactic:
update_self

Goal state after:
case pos
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a₁ : α
inst✝¹ : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ a = (if b = b then a / f b else 1) * f b
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
γ : Type u_5
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : γ → α
t : Finset γ
⊢ R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d))

Tactic:
iSup_subtype',

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
γ : Type u_5
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : γ → α
t : Finset γ
⊢ R (m (⨆ x, s ↑x)) (∏ d ∈ t, m (s d))
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd ((s ∪ t).mulIndicator f) (a * b)

Tactic:
rw [Set.mulIndicator_union_of_disjoint hs]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd (fun a ↦ s.mulIndicator f a * t.mulIndicator f a) (a * b)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case refine_2
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'
⊢ (∏ x ∈ image Nat.cast v', f x) * ∏ x ∈ image Int.negSucc v', f x = ∏ b ∈ v', f ↑b * f (Int.negSucc b)

pp: case refine_2
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'
⊢ Disjoint (image Nat.cast v') (image Int.negSucc v')

Tactic:
prod_image Nat.cast_injective.injOn,

Goal state after:
case refine_2
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'
⊢ (∏ x ∈ v', f ↑x) * ∏ x ∈ image Int.negSucc v', f x = ∏ b ∈ v', f ↑b * f (Int.negSucc b)

case refine_2
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'
⊢ Disjoint (image Nat.cast v') (image Int.negSucc v')
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
⊢ HasProd g (c * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i))

Tactic:
by
  classical
  refine (Tendsto.mul_const ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) hc).congr' ?_
  filter_upwards [eventually_ge_atTop s] with t ht
  calc (∏ i ∈ t, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)
  _ = ((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * _ := by
    conv_lhs => rw [← union_sdiff_of_subset ht, prod_union disjoint_sdiff,
      prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2]
  _ = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i := by
    rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]
    exact prod_ne_zero_iff.mpr hs
  _ = ∏ i ∈ t, g i := by
    rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]

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 β
inst✝ : L.LeAtTop
b : β
hb : f b = 0
⊢ HasProd f 0 L

Tactic:
apply tendsto_const_nhds.congr'

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b : β
hb : f b = 0
⊢ (fun x ↦ 0) =ᶠ[L.filter] fun s ↦ ∏ b ∈ s, f b
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 z : X
⊢ ↑(⨅ l, (zipWith d (x :: l) (l ++ [z])).sum) ≤
    ↑(⨅ l, (zipWith d (x :: l) (l ++ [y])).sum) + ↑(⨅ l, (zipWith d (y :: l) (l ++ [z])).sum)

Tactic:
rw [← NNReal.coe_add, NNReal.coe_le_coe]
    refine NNReal.le_iInf_add_iInf fun lxy lyz ↦ ?_
    calc
      ⨅ l, (zipWith d (x::l) (l ++ [z])).sum ≤
          (zipWith d (x::lxy ++ y::lyz) ((lxy ++ y::lyz) ++ [z])).sum :=
        ciInf_le (OrderBot.bddBelow _) (lxy ++ y::lyz)
      _ = (zipWith d (x::lxy) (lxy ++ [y])).sum + (zipWith d (y::lyz) (lyz ++ [z])).sum := by
        rw [← sum_append, ← zipWith_append, cons_append, ← @singleton_append _ y, append_assoc,
          append_assoc, append_assoc]
        rw [length_cons, length_append, length_singleton]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.eball x r = Metric.eball (h.symm x) r

Tactic:
rw [← h.isometry.preimage_eball (h.symm x) r, h.apply_symm_apply]

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 := ⋯
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
⊢ ∃ z z', d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum

Tactic:
set s : Set ℕ := { m : ℕ | 2 * (take m L).sum ≤ L.sum }

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
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}
⊢ ∃ z z', d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

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

Tactic:
by
  convert! hasProd_ite_eq (L := .unconditional β) b a
  simp [Pi.mulSingle_apply]

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}
hs₀ : 0 ∈ s
hsne : s.Nonempty
hs_ub : l.length ∈ upperBounds s
hs_bdd : BddAbove s
⊢ ∃ M ≤ l.length, IsGreatest s M

Tactic:
exact ⟨sSup s, csSup_le hsne hs_ub, ⟨Nat.sSup_mem hsne hs_bdd, fun k => le_csSup hs_bdd⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst✝¹.toTopologicalSpace] v
hv : a ∈ v
A : ∀ᶠ (t0 : Finset β) in atTop, ∏ i ∈ t0, g i ∈ v
⊢ ∃ t0, ∏ i ∈ t0, g i ∈ v ∧ image Sigma.fst s ⊆ t0

Tactic:
exact (A.and (Ici_mem_atTop _)).exists

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

Goal state before:
pp: case succ
n : ℕ
IH : Continuous fun a ↦ a ^ n
⊢ Continuous fun a ↦ a ^ (n + 1)

Tactic:
simp_rw [pow_add, pow_one, continuous_iff_continuousAt]
    intro x
    refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_ <;> by_cases H : x = 0
    · simp only [H, zero_ne_top, Ne, or_true, not_false_iff]
    · exact Or.inl fun h => H (eq_zero_of_pow_eq_zero h)
    · simp only [H, pow_eq_top_iff, zero_ne_top, false_or, not_true, Ne,
        not_false_iff, false_and]
    · simp only [H, true_or, Ne, not_false_iff]

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

Goal state before:
pp: case hg
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul n)

Tactic:
exact uniformContinuous_const_smul _

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

Goal state before:
pp: case hf
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul m)

Tactic:
exact uniformContinuous_const_smul _

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

Goal state before:
pp: case hg
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul m)

Tactic:
exact uniformContinuous_const_smul _

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

Goal state before:
pp: case hf
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul n)

Tactic:
exact uniformContinuous_const_smul _

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

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ (1 / 2) ^ n / 2 ≤ d x.1 x.2 / 2

Tactic:
div_le_iff₀ zero_lt_two,

Goal state after:
case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ (1 / 2) ^ n ≤ d x.1 x.2 / 2 * 2
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
x y : α
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖

Tactic:
by
  have h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖ := norm_inf_sub_inf_le_add_norm x y 0 0
  simpa only [inf_idem, sub_zero] using h

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

Goal state after:
case neg
α : 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 ≠ ∞
⊢ ratio (Isometry.toDilation f hf) = 1
Module: Mathlib.Analysis.Normed.Ring.Basic

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

Tactic:
rw [n.cast_succ, n.cast_succ, add_mul, one_mul]
    exact norm_add_le_of_le (Nat.norm_cast_le n) le_rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖a * (b :: l).prod‖ ≤ ‖a‖ * (map norm (b :: l)).prod

Tactic:
refine le_trans (norm_mul_le _ _) (mul_le_mul_of_nonneg_left ?_ (norm_nonneg _))

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖(b :: l).prod‖ ≤ (map norm (b :: l)).prod
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: case neg
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ (TProd.mk (i :: is) f).elim hj = f j

Tactic:
rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]

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

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

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

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

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

Tactic:
simp [hs']

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
t : Set α
ht : t ⊆ s ∧ t.Countable ∧ s ⊆ ⋃ x ∈ t, u x
⊢ μ s = 0

Tactic:
rcases ht with ⟨ts, t_count, ht⟩

Goal state after:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
t : Set α
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ ⋃ x ∈ t, u x
⊢ μ s = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
| Measurable fun x ↦ a = f x

Tactic:
enter [

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
| Measurable fun x ↦ a = f x
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inr
s : SignType
z : ℤ
hz : Odd z
hs : s ≠ 0
⊢ s ^ z = s

Tactic:
obtain ⟨k, rfl⟩ := hz

Goal state after:
case inr
s : SignType
hs : s ≠ 0
k : ℤ
⊢ s ^ (2 * k + 1) = s
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ -c * b ≤ -(c * a)

Tactic:
← neg_mul c a

Goal state after:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ -c * b ≤ -c * a
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
x : α
s : Set α
⊢ LowerSemicontinuousWithinAt f s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≤ y) → f x ≤ y

Tactic:
simp [semicontinuousWithinAt_iff_frequently]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
x : α
s : Set α
⊢ UpperSemicontinuousWithinAt f s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≥ y) → f x ≥ y

Tactic:
simp [semicontinuousWithinAt_iff_frequently]

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

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

Tactic:
neg_one_mul,

Goal state after:
case coe.inl
a : ℝ
a_neg : a < 0
⊢ -(↑(↑a).abs)⁻¹ = (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

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

Tactic:
neg_one_mul,

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

Goal state before:
pp: α : Type u_4
s : Set α
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Tactic:
by
  obtain (hfin | hinf) := Set.finite_or_infinite s
  · lift s to Finset α using hfin
    simp [tsum_fintype]
  · have : Infinite s := infinite_coe_iff.mpr hinf
    rw [tsum_const_eq_top_of_ne_zero one_ne_zero, encard_eq_top hinf, ENat.toENNReal_top]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ f x ≤ liminf f (𝓝[s] x) → LowerSemicontinuousWithinAt f s x

Tactic:
exact fun hf y ylt => eventually_lt_of_lt_liminf (ylt.trans_le hf)

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

Goal state before:
pp: C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
⊢ C / ↑n = ↑(C.toReal / ↑n)

Tactic:
nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]

Goal state after: