mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f x + C * edist y x ≤ f x + C * ↑δ

Tactic:
gcongr

Goal state after:
case h₂
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ edist y x ≤ ↑δ
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y y')

Tactic:
rw [edist_comm y y']

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y' y)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x' y' + (edist x x' + edist y y') ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y'))

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' ≤ edist (x, y) (x', y')

case h₂
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist y y' ≤ edist (x, y) (x', y')
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)
x y : X
n : ℕ
h : ∃ n, (x, y) ∉ U n
⊢ (1 / 2) ^ n ≤ (1 / 2) ^ Nat.find h ↔ (x, y) ∉ U n

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)
x y : X
n : ℕ
h : ¬∃ n, (x, y) ∉ U n
⊢ (1 / 2) ^ n ≤ 0 ↔ (x, y) ∉ U n

Tactic:
· rw [(pow_right_strictAnti₀ hr.1 hr.2).le_iff_ge, Nat.find_le_iff]
      exact ⟨fun ⟨m, hmn, hm⟩ hn => hm (hB.antitone hmn hn), fun h => ⟨n, le_rfl, 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)
x y : X
n : ℕ
h : ¬∃ n, (x, y) ∉ U n
⊢ (1 / 2) ^ n ≤ 0 ↔ (x, y) ∉ U n
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: t : ℝ≥0∞
t_ne_top : t ≠ ∞
x : ℝ≥0∞
⊢ (min t x).toReal ≤ t.toReal

Tactic:
gcongr

Goal state after:
case h
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x : ℝ≥0∞
⊢ min t x ≤ t
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: t : ℝ≥0∞
t_ne_top : t ≠ ∞
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ (min t x).toReal ≤ (min t y).toReal

Tactic:
gcongr

Goal state after:
case hb
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ min t y ≠ ∞
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K * dist x y ≤ ↑K.toNNReal * dist x y

Tactic:
gcongr

Goal state after:
case hbc
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K ≤ ↑K.toNNReal
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ
hf : LipschitzWith K f
hr : dist x y ≤ r
⊢ ↑K * dist x y ≤ ↑K * r

Tactic:
gcongr

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ
hf : LipschitzWith K f
hK : K ≠ 0
hr : dist x y < r
⊢ ↑K * dist x y < ↑K * r

Tactic:
gcongr

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
f : α → β
K : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ K * dist x y ≤ ↑K.toNNReal * dist x y

Tactic:
gcongr

Goal state after:
case hbc
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
f : α → β
K : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ K ≤ ↑K.toNNReal
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z ≤ f ↑t + (↑K * dist y ↑t + ↑K * dist y z)

Tactic:
← mul_add,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z ≤ f ↑t + ↑K * (dist y ↑t + dist y z)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg✝ : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
a : ℝ≥0∞
hba : a > b
i : ι
hf : f i ≤ b
hg : g i ≤ a - b
⊢ f i + g i ≤ b + g i

Tactic:
gcongr

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f ↑t + ↑K * dist z ↑t ≤ f ↑t + ↑K * (dist y z + dist y ↑t)

Tactic:
gcongr

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.MetricSpace.Lipschitz

Goal state before:
pp: α : 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)
E : EqOn f g s
x y : α
z : ↑s
⊢ f ↑z + ↑K * dist x ↑z ≤ f ↑z + (↑K * dist y ↑z + ↑K * dist x y)

Tactic:
← mul_add,

Goal state after:
α : 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)
E : EqOn f g s
x y : α
z : ↑s
⊢ f ↑z + ↑K * dist x ↑z ≤ f ↑z + ↑K * (dist y ↑z + dist x y)
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : 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)
E : EqOn f g s
x y : α
z : ↑s
⊢ f ↑z + ↑K * dist x ↑z ≤ f ↑z + ↑K * (dist x y + dist y ↑z)

Tactic:
gcongr

Goal state after:
case hbc
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := ⋯
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
z : ↑s
⊢ dist x ↑z ≤ dist x y + dist y ↑z
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
s : Set E
a b : E
r : ℝ
f : E → F
C : ℝ≥0
h : LipschitzOnWith C f s
ha : a ∈ s
hb : b ∈ s
hr : ‖a⁻¹ * b‖ ≤ r
⊢ ↑C * ‖a⁻¹ * b‖ ≤ ↑C * r

Tactic:
gcongr

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
a b : E
r : ℝ
f : E → F
C : ℝ≥0
h : LipschitzWith C f
hr : ‖a⁻¹ * b‖ ≤ r
⊢ ↑C * ‖a⁻¹ * b‖ ≤ ↑C * r

Tactic:
gcongr

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 : ℕ
hn : n ≥ N
⊢ N + 1 ≤ n + 1

Tactic:
gcongr

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
f : E → F
C : ℝ≥0
s : Set E
a b : E
r : ℝ
h : LipschitzOnWith C f s
ha : a ∈ s
hb : b ∈ s
hr : ‖a / b‖ ≤ r
⊢ ↑C * ‖a / b‖ ≤ ↑C * r

Tactic:
gcongr

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
f : E → F
C : ℝ≥0
a b : E
r : ℝ
h : LipschitzWith C f
hr : ‖a / b‖ ≤ r
⊢ ↑C * ‖a / b‖ ≤ ↑C * r

Tactic:
gcongr

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

Goal state before:
pp: ⊢ ∀ (x y : ℤ), dist ↑x ↑y = dist x y

Tactic:
by tauto

Goal state after:
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✝ : ∀ ε > 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
⊢ A * ‖f i‖ * ‖g i‖ ≤ A * δ * C

Tactic:
gcongr

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
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ ↑(ratio f) * edist y x < ↑(ratio f) * r

Tactic:
gcongr

Goal state after:
case h0
α : 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) ≠ 0

case hinf
α : 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) ≠ ∞
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 : y ∈ closedEBall x r'
⊢ ↑(ratio f) * edist y x ≤ ↑(ratio f) * r'

Tactic:
gcongr

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: α : 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'
⊢ ↑(ratio f) * dist y x < ↑(ratio f) * r'

Tactic:
gcongr

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
e : X ≃ᵈ Y
x y : X
⊢ edist (e.symm.toFun (e.toEquiv x)) (e.symm.toFun (e.toEquiv y)) = ↑(ratio e)⁻¹ * edist (e.toEquiv x) (e.toEquiv y)

Tactic:
Equiv.toFun_as_coe,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
x y : X
⊢ edist (e.symm (e.toEquiv x)) (e.symm (e.toEquiv y)) = ↑(ratio e)⁻¹ * edist (e.toEquiv x) (e.toEquiv y)
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: a✝ b✝ c✝ d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
hab : a ≤ b
c : ℝ≥0
⊢ c • a ≤ c • b

Tactic:
gcongr

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

Goal state before:
pp: a✝ b✝ c✝ d : ℝ≥0∞
r p q a b : ℝ≥0
hab : a ≤ b
c : ℝ≥0∞
⊢ a • c ≤ b • c

Tactic:
gcongr

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

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

Tactic:
gcongr

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 : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a‖ + ‖a‖ * ‖1 - b‖ ≤ ‖c - a‖ + 1 * ‖1 - b‖

Tactic:
gcongr

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

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

Tactic:
gcongr

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: α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ (‖(↑a - 1) * (↑b - 1)‖ + ‖(↑b - 1) * (↑a - 1)‖) * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ ≤
    (‖↑a - 1‖ * ‖↑b - 1‖ + ‖↑b - 1‖ * ‖↑a - 1‖) * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖(↑a - 1) * (↑b - 1)‖ ≤ ‖↑a - 1‖ * ‖↑b - 1‖

case h₂
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖(↑b - 1) * (↑a - 1)‖ ≤ ‖↑b - 1‖ * ‖↑a - 1‖
Module: Mathlib.Analysis.Normed.MulAction

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

Tactic:
gcongr

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.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ ‖x‖⁻¹ * dist x y * ‖y‖⁻¹ ≤ r⁻¹ * (ε * r ^ 2) * r⁻¹

Tactic:
gcongr

Goal state after:
case hba
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ r ≤ ‖x‖

case hba
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ r ≤ ‖y‖
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet s

Tactic:
← biUnion_of_singleton s

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet (⋃ x ∈ s, {x})
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
⊢ a * r' ≤ 2 * r'

Tactic:
gcongr

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

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

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
i : ℕ
⊢ disjointed t i ⊆ t i
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
s t : Set α
ht : μ t = 0
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ t + μ (s \ t)

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
ht : μ t = 0
⊢ s ∩ t ⊆ t
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
k : ι
⊢ μ (S ∩ s k) + μ (S \ s k) ≤ μ (s k) + μ (S \ s k)

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋯
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⋯
k : ι
⊢ S ∩ s k ⊆ s k
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
k : ι
⊢ μ (s k) + μ (S \ s k) ≤ M + μ (S \ s k)

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋯
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⋯
k : ι
⊢ μ (s k) ≤ M
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ‖(↑n)⁻¹‖ * ‖f (n • x)‖ < ‖(↑n)⁻¹‖ * C

Tactic:
gcongr

Goal state after:
case ha
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ 0 < ‖(↑n)⁻¹‖

case hbc
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ‖f (n • x)‖ < C
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ (↑n)⁻¹ * C < (C / ε)⁻¹ * C

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.15
f : α → β
m : OuterMeasure β
x✝¹ x✝ : Set α
h : x✝¹ ⊆ x✝
⊢ m (f '' x✝¹) ≤ m (f '' x✝)

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ((map f) ⊤) s = ((restrict (range f)) ⊤) s

Tactic:
by
    rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
      Set.image_eq_empty]

Goal state after:
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:
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.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0∞
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
rw [← hasSum_iff_tendsto_nat]
  exact ENNReal.summable.hasSum

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

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : ∑' (n : ℕ), f n = ∞
hf0 : f 0 ≠ ∞
⊢ ∑' (n : ℕ), f (n + 1) = ∞

Tactic:
by
  rw [tsum_eq_zero_add' ENNReal.summable, add_eq_top] at hf
  exact hf.resolve_left hf0

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

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

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
⊢ LowerSemicontinuousOn (fun x ↦ f (M x) x) s

Tactic:
by
  intro x hx b hb
  apply Filter.Eventually.mp <| hfy (M x) (M_mem x hx) x hx b hb
  apply eventually_nhdsWithin_of_forall
  intro z hz h
  exact lt_of_lt_of_le h (M_max z hz (M_mem x hx))

Goal state after: