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

Goal state before:
pp: case hbc
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := ⋯
y z : α
hz : z ∈ s
t : ↑s
⊢ dist z ↑t ≤ dist y z + dist y ↑t

Tactic:
;

Goal state after:
case hbc
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := ⋯
y z : α
hz : z ∈ s
t : ↑s
⊢ dist z ↑t ≤ dist y z + dist y ↑t
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
⊢ ∀ (i' : ℕ), True → ∃ i, True ∧ {p | dist p.1 p.2 < ↑(1 / 2) ^ i} ⊆ U i'

Tactic:
· refine fun n _ => ⟨n + 1, trivial, fun x hx => ?_⟩
    rw [mem_ofPred_eq] at hx
    contrapose! hx
    refine le_trans ?_ ((div_le_iff₀' zero_lt_two).2 (hd_le x.1 x.2))
    rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ,
      mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]

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

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
x✝ : α
⊢ x✝ ∈ {x | 0 ≤ x} ↔ x✝ ∈ negPart ⁻¹' {0}

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
x✝ : α
⊢ x✝ ∈ {x | 0 ≤ x} ↔ x✝ ∈ negPart ⁻¹' {0}
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
p : G × G
⊢ p ∈ {p | p.1 ≤ p.2} ↔ p ∈ (fun p ↦ p.2 - p.1) ⁻¹' {x | 0 ≤ x}

Tactic:
;

Goal state after:
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
p : G × G
⊢ p ∈ {p | p.1 ≤ p.2} ↔ p ∈ (fun p ↦ p.2 - p.1) ⁻¹' {x | 0 ≤ x}
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
a : G₀
inst✝ : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
⊢ s.sup' hs f / a = s.sup' hs fun i ↦ f i / a

Tactic:
by_cases! h : 0 = a
  · simp [← h]
  exact map_finset_sup' (OrderIso.divRight₀ _ (lt_of_le_of_ne ha h)) hs f

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
a b : α
⊢ ‖1‖ * ‖1‖ = ‖1‖ * 1

Tactic:
rw [← norm_mul, mul_one, mul_one]

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
⊢ ∏ k ∈ range (n + 1), u k = (d * fun n ↦ ∏ k ∈ range (n + 1), v k) n

Tactic:
;

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
⊢ ∏ k ∈ range (n + 1), u k = (d * fun n ↦ ∏ k ∈ range (n + 1), v k) n
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
⊢ (𝓝[≠] x).NeBot

Tactic:
rw [← mem_closure_iff_nhdsWithin_neBot, Metric.mem_closure_iff]
  rintro ε ε0
  rcases exists_norm_lt α ε0 with ⟨b, hb0, hbε⟩
  refine ⟨x + b, mt (Set.mem_singleton_iff.trans add_eq_left).1 <| norm_pos_iff.1 hb0, ?_⟩
  rwa [dist_comm, dist_eq_norm, add_sub_cancel_left]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x ↦ ‖f x‖) l atTop ↔ Tendsto (norm ∘ f) l atTop

Tactic:
;

Goal state after:
α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x ↦ ‖f x‖) l atTop ↔ Tendsto (norm ∘ f) l atTop
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
g : α →ᵈ β
toFun✝ : α → β
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝ x) (toFun✝ y) = ↑r * edist x y
h : { toFun := toFun✝, edist_eq' := edist_eq'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, edist_eq' := edist_eq'✝ } = g

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
g : α →ᵈ β
toFun✝ : α → β
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝ x) (toFun✝ y) = ↑r * edist x y
h : { toFun := toFun✝, edist_eq' := edist_eq'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, edist_eq' := edist_eq'✝ } = g
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
toFun✝¹ : α → β
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝¹ x) (toFun✝¹ y) = ↑r * edist x y
toFun✝ : α → β
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝ x) (toFun✝ y) = ↑r * edist x y
h : { toFun := toFun✝¹, edist_eq' := edist_eq'✝¹ }.toFun = { toFun := toFun✝, edist_eq' := edist_eq'✝ }.toFun
⊢ { toFun := toFun✝¹, edist_eq' := edist_eq'✝¹ } = { toFun := toFun✝, edist_eq' := edist_eq'✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
toFun✝¹ : α → β
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝¹ x) (toFun✝¹ y) = ↑r * edist x y
toFun✝ : α → β
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝ x) (toFun✝ y) = ↑r * edist x y
h : { toFun := toFun✝¹, edist_eq' := edist_eq'✝¹ }.toFun = { toFun := toFun✝, edist_eq' := edist_eq'✝ }.toFun
⊢ { toFun := toFun✝¹, edist_eq' := edist_eq'✝¹ } = { toFun := toFun✝, edist_eq' := edist_eq'✝ }
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ (if ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞ then 1 else ⋯.choose) ≠ 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ (if ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞ then 1 else ⋯.choose) ≠ 0
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (x : ℝ) in map (Norm.norm ∘ g) l, (fun x1 x2 ↦ x1 ≤ x2) x C
⊢ Tendsto (fun x ↦ op (f x) (g x)) l (𝓝 1)

Tactic:
;

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (x : ℝ) in map (Norm.norm ∘ g) l, (fun x1 x2 ↦ x1 ≤ x2) x C
⊢ Tendsto (fun x ↦ op (f x) (g x)) l (𝓝 1)
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist (f x) (f y) = ↑(if ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞ then 1 else ⋯.choose) * edist x y

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist (f x) (f y) = ↑(if ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞ then 1 else ⋯.choose) * edist x y
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: case h₂
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ ‖g i‖ ≤ C

Tactic:
;

Goal state after:
case h₂
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ ‖g i‖ ≤ C
Module: Mathlib.Topology.MetricSpace.Dilation

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ ediam (⇑f '' univ) = ↑(ratio f) * ediam univ
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ ↑(ratio f) * edist y x < ↑(ratio f) * r

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ ↑(ratio f) * edist y x < ↑(ratio f) * r
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r' : ℝ≥0∞
y : α
hy : y ∈ closedEBall x r'
⊢ edist y x ≤ r'

Tactic:
;

Goal state after:
case h₂
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r' : ℝ≥0∞
y : α
hy : y ∈ closedEBall x r'
⊢ edist y x ≤ r'
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case ha
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
⊢ 0 < ↑(ratio f)

pp: case hbc
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
⊢ dist y x < r'

Tactic:
;

Goal state after:
case ha
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
⊢ 0 < ↑(ratio f)

case hbc
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
⊢ dist y x < r'
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
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝¹.toFun x) (toEquiv✝¹.toFun y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝.toFun x) (toEquiv✝.toFun y) = ↑r * edist x y
h :
  ⇑{ toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ }.toEquiv =
    ⇑{ toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }.toEquiv
⊢ { toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ } = { toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝¹.toFun x) (toEquiv✝¹.toFun y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝.toFun x) (toEquiv✝.toFun y) = ↑r * edist x y
h :
  ⇑{ toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ }.toEquiv =
    ⇑{ toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }.toEquiv
⊢ { toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ } = { toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }
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
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝¹.toFun x) (toEquiv✝¹.toFun y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝.toFun x) (toEquiv✝.toFun y) = ↑r * edist x y
h :
  ⇑{ toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ }.toEquiv =
    ⇑{ toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }.toEquiv
⊢ toEquiv✝¹ = toEquiv✝

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝¹.toFun x) (toEquiv✝¹.toFun y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝.toFun x) (toEquiv✝.toFun y) = ↑r * edist x y
h :
  ⇑{ toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ }.toEquiv =
    ⇑{ toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }.toEquiv
⊢ toEquiv✝¹ = toEquiv✝
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ (⇑(toPerm e))^[n] = (⇑e)^[n]

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ (⇑(toPerm e))^[n] = (⇑e)^[n]
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
h : x • ∞ ≠ ∞
⊢ False

Tactic:
;

Goal state after:
x : ℝ≥0
hx : x ≠ 0
h : x • ∞ ≠ ∞
⊢ False
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - a‖ + ‖a * (1 - b)‖

Tactic:
simpa [mul_one_sub] using norm_sub_le_norm_sub_add_norm_sub c a (a * b)

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

Goal state before:
pp: case h₂
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖a * (1 - b)‖ ≤ ‖a‖ * ‖1 - b‖

Tactic:
;

Goal state after:
case h₂
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖a * (1 - b)‖ ≤ ‖a‖ * ‖1 - b‖
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b c : α
hb : ‖b‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - b‖ + ‖1 - a‖

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
hb : ‖b‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - b‖ + ‖1 - a‖
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑a * ↑b - ↑b * ↑a‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ = ‖↑a * ↑b - ↑a - (↑b - 1) - (↑b * ↑a - ↑b - (↑a - 1))‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑a * ↑b - ↑b * ↑a‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ = ‖↑a * ↑b - ↑a - (↑b - 1) - (↑b * ↑a - ↑b - (↑a - 1))‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: case hbc
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖(↑a - 1) * (↑b - 1) - (↑b - 1) * (↑a - 1)‖ ≤ ‖(↑a - 1) * (↑b - 1)‖ + ‖(↑b - 1) * (↑a - 1)‖

Tactic:
;

Goal state after:
case hbc
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖(↑a - 1) * (↑b - 1) - (↑b - 1) * (↑a - 1)‖ ≤ ‖(↑a - 1) * (↑b - 1)‖ + ‖(↑b - 1) * (↑a - 1)‖
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: x : ℝ≥0
⊢ ↑‖↑x‖₊ = ↑x

Tactic:
;

Goal state after:
x : ℝ≥0
⊢ ↑‖↑x‖₊ = ↑x
Module: Mathlib.Analysis.Normed.MulAction

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

Tactic:
;

Goal state after:
case hbc
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r⁻¹ • r • x‖ ≤ ‖r⁻¹‖ * ‖r • x‖
Module: Mathlib.Analysis.Normed.MulAction

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

Tactic:
apply norm_smul_le

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case pos
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : ↥t) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
h✝ : i ∈ t
⊢ y ⟨i, h✝⟩ = y ⟨i, h✝⟩

pp: case neg
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : ↥t) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
h✝ : i ∉ t
⊢ x₁ i = x₂ i

Tactic:
;

Goal state after:
case pos
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : ↥t) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
h✝ : i ∈ t
⊢ y ⟨i, h✝⟩ = y ⟨i, h✝⟩

case neg
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : ↥t) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
h✝ : i ∉ t
⊢ x₁ i = x₂ i
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ False

Tactic:
;

Goal state after:
case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ False
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s : Finset ι
y z : (i : ↥s) → π ↑i
⊢ updateFinset x s y = updateFinset x s fun i ↦ y ⟨↑i, ⋯⟩

Tactic:
;

Goal state after:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s : Finset ι
y z : (i : ↥s) → π ↑i
⊢ updateFinset x s y = updateFinset x s fun i ↦ y ⟨↑i, ⋯⟩
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
inst✝ : UniformSpace X
f : X → α
hf : UniformContinuousOn f Set.univ
hf₀ : (f '' Set.univ)ᶜ ∈ 𝓝 0
⊢ UniformContinuousOn f⁻¹ Set.univ

Tactic:
exact hf.inv₀ hf₀

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
a b c : IterateMulAct f
⊢ (a * b * c).val = (a * (b * c)).val

Tactic:
;

Goal state after:
α : Type u_1
f : α → α
a b c : IterateMulAct f
⊢ (a * b * c).val = (a * (b * c)).val
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ (1 * x✝).val = x✝.val

Tactic:
;

Goal state after:
α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ (1 * x✝).val = x✝.val
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ (x✝ ^ 0).val = val 1

Tactic:
;

Goal state after:
α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ (x✝ ^ 0).val = val 1
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
a : IterateMulAct f
⊢ (a ^ (n + 1)).val = (a ^ n * a).val

Tactic:
;

Goal state after:
α : Type u_1
f : α → α
n : ℕ
a : IterateMulAct f
⊢ (a ^ (n + 1)).val = (a ^ n * a).val
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝¹ x✝ : IterateMulAct f
⊢ (x✝¹ * x✝).val = (x✝ * x✝¹).val

Tactic:
;

Goal state after:
α : Type u_1
f : α → α
x✝¹ x✝ : IterateMulAct f
⊢ (x✝¹ * x✝).val = (x✝ * x✝¹).val
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ i, (f i)ᶜ)

Tactic:
;

Goal state after:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ i, (f i)ᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ i ∈ s, (f i)ᶜ)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ i ∈ s, (f i)ᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₂ ⊔ s₁ᶜ)

Tactic:
;

Goal state after:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₂ ⊔ s₁ᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
x✝ : α
⊢ x✝ ∈ {x | p x ↔ q x} ↔ x✝ ∈ {x | p x → q x} ∩ {x | q x → p x}

Tactic:
;

Goal state after:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
x✝ : α
⊢ x✝ ∈ {x | p x ↔ q x} ↔ x✝ ∈ {x | p x → q x} ∩ {x | q x → p x}
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
x✝ : α
⊢ (p x✝ ↔ q x✝) ↔ (p x✝ → q x✝) ∧ (q x✝ → p x✝)

Tactic:
;

Goal state after:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
x✝ : α
⊢ (p x✝ ↔ q x✝) ↔ (p x✝ → q x✝) ∧ (q x✝ → p x✝)