mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ x < i, (1 + -f x)
hprod : Multipliable fun x ↦ 1 + -f x
hsum' : Summable fun b ↦ -f b * ∏ x < b, (1 + -f x)
⊢ ∏' (i : ι), (1 + -f i) = 1 + -∑' (i : ι), f i * ∏ i < i, (1 + -f i)

Tactic:
simp_rw [← tsum_neg, ← neg_mul]

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ x < i, (1 + -f x)
hprod : Multipliable fun x ↦ 1 + -f x
hsum' : Summable fun b ↦ -f b * ∏ x < b, (1 + -f x)
⊢ ∏' (i : ι), (1 + -f i) = 1 + ∑' (b : ι), -f b * ∏ i < b, (1 + -f i)
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
⊢ Isometry (Pi.single i)

Tactic:
intro x y
  rw [edist_pi_def]
  refine le_antisymm (Finset.sup_le fun j ↦ ?_) (Finset.le_sup_of_le (Finset.mem_univ i) (by simp))
  obtain rfl | h := eq_or_ne i j
  · simp
  · simp [h]

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

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

Tactic:
← h.isometry.preimage_sphere (h.symm x) r,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.sphere x r = ⇑h ⁻¹' Metric.sphere (h (h.symm x)) r
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable (f b)
h₂ : ∀ (c : γ), Multipliable fun b ↦ f b c
⊢ ∏' (c : γ) (b : β), f b c = ∏' (b : β) (c : γ), f b c

Tactic:
rw [← h.tprod_prod_uncurry h₁, ← h.prod_symm.tprod_prod_uncurry h₂,
    ← (Equiv.prodComm γ β).tprod_eq (uncurry f)]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable (f b)
h₂ : ∀ (c : γ), Multipliable fun b ↦ f b c
⊢ ∏' (p : γ × β), uncurry (fun b c ↦ f c b) p = ∏' (c : γ × β), uncurry f ((Equiv.prodComm γ β) c)
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
M : ℕ
hMl : M < l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
hMl' : (take M l).length = M
⊢ zipWith d (x :: take M l) (take M l ++ [(x :: l)[M + 1]]) =
    zipWith d (x :: take M l) (take M (l ++ [y]) ++ ((fun a ↦ some a) l[M]).toList)

Tactic:
Option.toList_some,

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}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M < l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
hMl' : (take M l).length = M
⊢ zipWith d (x :: take M l) (take M l ++ [(x :: l)[M + 1]]) = zipWith d (x :: take M l) (take M (l ++ [y]) ++ [l[M]])
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ b⁻¹ ≠ 0 ∨ a ≠ ∞

Tactic:
simp [hb]

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hxb : x ≤ b
⊢ IccExtend h (f ∘ Subtype.val) x = f x

Tactic:
lift x to Icc a b using ⟨hax, hxb⟩

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : { x // x ∈ Icc a b }
hax : a ≤ ↑x
hxb : ↑x ≤ b
⊢ IccExtend h (f ∘ Subtype.val) ↑x = f ↑x
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case pos
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 : 1 / 2 ∈ Ioo 0 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
x₁ x₂ x₃ x₄ : X
H : ∃ n, (x₁, x₄) ∉ U n
⊢ d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))

pp: case neg
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 : 1 / 2 ∈ Ioo 0 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
x₁ x₂ x₃ x₄ : X
H : ¬∃ n, (x₁, x₄) ∉ U n
⊢ d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))

Tactic:
· refine (dif_pos H).trans_le ?_
      rw [← div_le_iff₀' zero_lt_two, ← mul_one_div (_ ^ _), ← pow_succ]
      simp only [le_max_iff, hle_d, ← not_and_or]
      rintro ⟨h₁₂, h₂₃, h₃₄⟩
      refine Nat.find_spec H (hU_comp (lt_add_one <| Nat.find H) ?_)
      exact ⟨x₂, h₁₂, x₃, h₂₃, h₃₄⟩

Goal state after:
case neg
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 : 1 / 2 ∈ Ioo 0 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
x₁ x₂ x₃ x₄ : X
H : ¬∃ n, (x₁, x₄) ∉ U n
⊢ d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ ↑(limsup u f) = limsup (fun i ↦ ↑(u i)) f

Tactic:
refine eq_of_forall_nnreal_le_iff fun r ↦ ?_

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
⊢ ↑r ≤ ↑(limsup u f) ↔ ↑r ≤ limsup (fun i ↦ ↑(u i)) f
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ↑(liminf u f) = liminf (fun i ↦ ↑(u i)) f

Tactic:
refine eq_of_forall_nnreal_le_iff fun r ↦ ?_

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
r : ℝ≥0
⊢ ↑r ≤ ↑(liminf u f) ↔ ↑r ≤ liminf (fun i ↦ ↑(u i)) f
Module: Mathlib.Topology.MetricSpace.IsometricSMul

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

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

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
p : E
⊢ mk p = 1 ↔ ‖p‖ = 0

Tactic:
← norm_mk',

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
p : E
⊢ mk p = 1 ↔ ‖mk p‖ = 0
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : α →ᵈ β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f; cases g; congr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
hne : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
rcases hne with ⟨x, y, hα⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (g.comp f) = ratio g * ratio f
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : Module R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : Module.IsTorsionFree R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ c • ∞ = if c = 0 then 0 else ∞

Tactic:
rw [← smul_one_mul, mul_top']
  simp_rw [smul_eq_zero, or_iff_left one_ne_zero]

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

Goal state before:
pp: r : ℝ≥0
s : ℝ≥0∞
⊢ (↑r).toReal * s.toReal = r • s.toReal

Tactic:
coe_toReal

Goal state after:
r : ℝ≥0
s : ℝ≥0∞
⊢ ↑r * s.toReal = r • s.toReal
Module: Mathlib.Analysis.Normed.Ring.Basic

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

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case inr.refine_1
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
⊢ ⨆ i, ∏ a, f a (i a) ≤ ∏ a, ⨆ i, f a i

case inr.refine_2
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
⊢ ∏ a, ⨆ i, f a i ≤ ⨆ i, ∏ a, f a (i a)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ Measurable (s.indicator fun x ↦ b) ↔ MeasurableSet s

Tactic:
constructor <;> intro h
  · convert! h (MeasurableSet.singleton (0 : β)).compl
    ext a
    simp [NeZero.ne b]
  · exact measurable_const.indicator 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:
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
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℤ
x : E
⊢ ‖n • x‖ = ‖↑n • x‖

Tactic:
← Int.smul_one_eq_cast,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℤ
x : E
⊢ ‖n • x‖ = ‖(n • 1) • 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✝¹ : Module 𝕜 E
inst✝ : Norm E
core : NormedSpace.Core 𝕜 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ x - y = 0

Tactic:
← core.norm_eq_zero_iff,

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✝¹ : Module 𝕜 E
inst✝ : Norm E
core : NormedSpace.Core 𝕜 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖x - y‖ = 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✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ x - y = 0

Tactic:
← core.norm_eq_zero_iff,

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✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖x - y‖ = 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✝¹ : Module 𝕜 E
inst✝ : Norm E
T : TopologicalSpace E
core : NormedSpace.Core 𝕜 E
H : T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ x - y = 0

Tactic:
← core.norm_eq_zero_iff,

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✝¹ : Module 𝕜 E
inst✝ : Norm E
T : TopologicalSpace E
core : NormedSpace.Core 𝕜 E
H : T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖x - y‖ = 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✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
B : Bornology E
core : NormedSpace.Core 𝕜 E
HU : 𝓤 E = 𝓤 E
HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ x - y = 0

Tactic:
← core.norm_eq_zero_iff,

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✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
B : Bornology E
core : NormedSpace.Core 𝕜 E
HU : 𝓤 E = 𝓤 E
HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖x - y‖ = 0
Module: Mathlib.Data.Sign.Basic

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

Tactic:
rcases lt_trichotomy y 0 with (hy | hy | hy)

Goal state after:
case inl.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : y < 0
⊢ sign (x * y) = sign x * sign y

case inl.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : y = 0
⊢ sign (x * y) = sign x * sign y

case inl.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : 0 < y
⊢ sign (x * y) = sign x * sign y
Module: Mathlib.Data.Sign.Basic

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

Tactic:
rcases lt_trichotomy y 0 with (hy | hy | hy)

Goal state after:
case inr.inl.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : y < 0
⊢ sign (x * y) = sign x * sign y

case inr.inl.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : y = 0
⊢ sign (x * y) = sign x * sign y

case inr.inl.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : 0 < y
⊢ sign (x * y) = sign x * sign y
Module: Mathlib.Data.Sign.Basic

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

Tactic:
rcases lt_trichotomy y 0 with (hy | hy | hy)

Goal state after:
case inr.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : y < 0
⊢ sign (x * y) = sign x * sign y

case inr.inr.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : y = 0
⊢ sign (x * y) = sign x * sign y

case inr.inr.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : 0 < y
⊢ sign (x * y) = sign x * sign y
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
⊢ sign (x * y) = sign x * sign y

Tactic:
by
  rcases lt_trichotomy x 0 with (hx | hx | hx) <;> rcases lt_trichotomy y 0 with (hy | hy | hy) <;>
    simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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

Goal state before:
pp: case coe_coe
x✝ y✝ : ℝ
⊢ (↑x✝ * ↑y✝).abs = (↑x✝).abs * (↑y✝).abs

Tactic:
| coe_coe =>

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

Goal state before:
pp: case coe_coe
x✝ y✝ : ℝ
⊢ sign (↑x✝ * ↑y✝) = sign ↑x✝ * sign ↑y✝

Tactic:
| coe_coe =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ (∀ (x : ↑s), SemicontinuousAt (s.domRestrict r) x) ↔ ∀ x ∈ s, SemicontinuousWithinAt r s x

Tactic:
SetCoe.forall

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ (∀ (x : α) (h : x ∈ s), SemicontinuousAt (s.domRestrict r) ⟨x, h⟩) ↔ ∀ x ∈ s, SemicontinuousWithinAt r s x
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
h : Summable f
⊢ (support f).Countable

Tactic:
rw [← NNReal.summable_coe] at h
  simpa [support] using h.countable_support

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

Goal state before:
pp: a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ ↑a.toReal⁻¹⁻¹ = ↑a.toReal

Tactic:
_root_.inv_inv a.toReal

Goal state after:
a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ ↑a.toReal = ↑a.toReal
Module: Mathlib.Topology.Semicontinuity.Defs

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

Tactic:
by
  simp_rw [lowerHemicontinuous_iff, lowerHemicontinuousAt_iff_frequently]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : HasOpenCGraph f
hg : HasOpenCGraph g
this : {x | x.2 ∈ f x.1 ∩ g x.1} = {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1}
⊢ HasOpenCGraph fun x ↦ f x ∩ g x

Tactic:
rw [HasOpenCGraph, this]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : HasOpenCGraph f
hg : HasOpenCGraph g
this : {x | x.2 ∈ f x.1 ∩ g x.1} = {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1}
⊢ IsOpen[instTopologicalSpaceProd] ({x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1})
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, ↑(f a) < ↑x) ↔ Tendsto f l atBot

Tactic:
atBot_basis_Iio.tendsto_right_iff

Goal state after:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, ↑(f a) < ↑x) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Iio i
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
⊢ μ ∅ = 0

Tactic:
rw [← nonpos_iff_eq_zero]
      exact (iInf_le_of_le fun _ => ∅) <| iInf_le_of_le (empty_subset _) <| by simpa

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

Goal state before:
pp: case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)

Tactic:
have obs := @Tendsto.inv ℝ≥0∞ ℕ _ _ _ (fun n ↦ (r⁻¹) ^ n) atTop 0

Goal state after:
case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
obs : Tendsto (fun n ↦ r⁻¹ ^ n) atTop (𝓝 0) → Tendsto (fun x ↦ (r⁻¹ ^ x)⁻¹) atTop (𝓝 0⁻¹)
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
refine iInf_le_of_le (fun n => (range f)ᶜ ∪ f '' t n) (iInf_le_of_le ?_ ?_)

Goal state after:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ n, (range f)ᶜ ∪ f '' t n

case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ∑' (n : ℕ), m (f ⁻¹' (fun n ↦ (range f)ᶜ ∪ f '' t n) n) ≤ ∑' (n : ℕ), m (t n)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m = boundedBy (sInfGen m)

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m ≤ boundedBy (sInfGen m)

case refine_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ IsPiSystem (Iio '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iio a ∩ Iio b ∈ Iio '' s
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ IsPiSystem (Iic '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iic a ∩ Iic b ∈ Iic '' s