mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
⊢ StrictMonoOn f (Icc a b)

Tactic:
by
  have : Fact (a ≤ b) := ⟨hab⟩
  refine StrictMono.of_domRestrict ?_
  set g : Icc a b → δ := Set.domRestrict (Icc a b) f
  have hgab : g ⊥ ≤ g ⊤ := by aesop
  exact Continuous.strictMono_of_inj_boundedOrder (f := g) hf_c.domRestrict hgab hf_i.injective

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x • r) l atBot

Tactic:
simpa using hf.atTop_zsmul_const (neg_pos.2 hr)

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)

Tactic:
simp only [diam, ediam_triple, dist_edist]
  rw [ENNReal.toReal_max, ENNReal.toReal_max] <;> apply_rules [ne_of_lt, edist_lt_top, max_lt]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
⊢ Dense ↑S ∨ ∃ a, S = closure {a}

Tactic:
by
  refine (em _).imp (dense_of_not_isolated_one S) fun h => ?_
  push Not at h
  rcases h with ⟨ε, ε1, hε⟩
  exact cyclic_of_isolated_one ε1 (disjoint_left.2 hε)

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

Goal state before:
pp: case some.some
α : Type u
β : Type v
γ : Type w
a b : ℝ≥0
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (some a, some b)

Tactic:
simp only [ContinuousAt, some_eq_coe, nhds_coe_coe, ← coe_add, tendsto_map'_iff,
    Function.comp_def, tendsto_coe, tendsto_add]

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ (∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s) → IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u

Tactic:
rintro ⟨s, ⟨b, hb⟩, hs⟩
    exact ⟨b, hs.mono <| by simpa [upperBounds] using hb⟩

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
rcases h' with ⟨b, hb⟩

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
rcases h' with ⟨b, hb⟩

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderInf α
inst✝ : InfConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddBelow (range f)
⊢ Tendsto f atBot (𝓝 (⨅ i, f i))

Tactic:
convert! tendsto_atTop_ciSup h_mono.dual hbdd.dual using 1

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

Goal state before:
pp: a b c a' : EReal
hc' : c - b < a'
ha' : a' < a
hc : b = ⊥
⊢ a + b ≤ c

Tactic:
exact hc ▸ (add_bot a).symm ▸ bot_le

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

Goal state before:
pp: case coe.top
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
⊢ ↑a✝ * ⊤ ≠ 0

Tactic:
rcases lt_or_gt_of_ne h.1 with (h | h)
        <;> simp [EReal.mul_top_of_neg, EReal.mul_top_of_pos, h]

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

Goal state before:
pp: case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ e ∈ Filter.map (fun s ↦ ∏' (a : { x // x ∉ s }), f ↑a) atTop

Tactic:
obtain ⟨s, hs⟩ := H.tprod_vanishing he

Goal state after:
case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
⊢ e ∈ Filter.map (fun s ↦ ∏' (a : { x // x ∉ s }), f ↑a) atTop
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst✝¹ : SetLike S α
inst✝ : SubmonoidClass S α
h_closed : IsClosed[inst✝²] ↑s
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : ¬Multipliable f
⊢ ∏' (i : ι), f i ∈ s

Tactic:
· simp [tprod_eq_one_of_not_multipliable hf, one_mem]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
⊢ f ⁻¹' Metric.closedEBall (f x) r = Metric.closedEBall x r

Tactic:
ext y
  simp [h.edist_eq]

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

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

Tactic:
ext y
  simp [h.edist_eq]

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
⊢ l.length ∈ upperBounds s

Tactic:
intro m hm

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 : ℕ
hm : m ∈ s
⊢ m ≤ l.length
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
⊢ HasProd g a

Tactic:
refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
⊢ ∀ (ib : Set α), ib ∈ 𝓝 a ∧ IsClosed[inst✝²] ib → ∃ ia, True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id ib
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
⊢ ∃ ia, True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s

Tactic:
rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
u : Finset ((b : β) × γ b)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → b ∈ (fun s ↦ ∏ b ∈ s, f b) ⁻¹' s
⊢ ∃ ia, True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ Tendsto f atTop (𝓝 0) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε

Tactic:
rw [ENNReal.tendsto_atTop_zero_iff_le_of_antitone hf]

Goal state after:
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
ι : Type u_4
X : α → Type u_5
inst✝¹ : (x : α) → CommMonoid (X x)
inst✝ : (x : α) → TopologicalSpace (X x)
L : SummationFilter ι
f : ι → (x : α) → X x
g : (x : α) → X x
⊢ HasProd f g L ↔ ∀ (x : α), HasProd (fun i ↦ f i x) (g x) L

Tactic:
by
  simp only [HasProd, tendsto_pi_nhds, Finset.prod_apply]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s ↦ s ○ s

Tactic:
· exact monotone_id.relComp monotone_id

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s ↦ s ○ s

pp: case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen

Tactic:
· exact monotone_id.relComp monotone_id

Goal state after:
case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
⊢ 2 * (zipWith d (l[M] :: drop (M + 1) l) (drop (M + 1) l ++ [y])).sum ≤ L.sum

Tactic:
cons_getElem_drop_succ

Goal state after:
case refine_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ Tendsto (fun n ↦ (f n).toReal) fi (𝓝 (ENNReal.toReal 0)) ↔ Tendsto f fi (𝓝 0)

Tactic:
tendsto_toReal_iff hf ENNReal.zero_ne_top

Goal state after:
ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ Tendsto f fi (𝓝 0) ↔ Tendsto f fi (𝓝 0)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : 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 y ∈ Icc (f x - ε) (f x + ε)

Tactic:
refine ⟨tsub_le_iff_right.2 <| (h x y).trans ?_, (h y x).trans ?_⟩

Goal state after:
case refine_1
α : 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 y + C * edist x y ≤ f y + ε

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 + ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ 2 ≠ ∞

Tactic:
decide

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

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ a ⊔ -a ≤ |b|

Tactic:
nth_rw 1 [← neg_neg a]

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ - -a ⊔ -a ≤ |b|
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: M : Type u
inst✝² : DivInvMonoid M
inst✝¹ : PseudoEMetricSpace M
inst✝ : IsIsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ edist (a / c) (b / c) = edist a b

Tactic:
simp only [div_eq_mul_inv, edist_mul_right]

Goal state after:
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) ⁻¹' eball b r = eball (b / a) r

Tactic:
rw [div_eq_mul_inv]

Goal state after:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x ↦ x * a) ⁻¹' eball b r = eball (b * a⁻¹) r
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:
rw [div_eq_mul_inv]

Goal state after:
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
Module: Mathlib.Topology.MetricSpace.IsometricSMul

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

Tactic:
rw [div_eq_mul_inv]

Goal state after:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' ball b r = ball (b * a⁻¹) r
Module: Mathlib.Topology.MetricSpace.IsometricSMul

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

Tactic:
rw [div_eq_mul_inv]

Goal state after:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: case mp
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : ‖x‖ = 1
⊢ x ≠ 0

Tactic:
contrapose! hx
    simp [hx]

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 ≥ N + 1, u n / v n = 1

Tactic:
intro m hm

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 : ℕ
hn : n ≥ N
m : ℕ
hm : m ≥ N + 1
⊢ u m / v m = 1
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (e.trans e') = ratio e * ratio e'

Tactic:
have hY : ∀ x y : Y, edist x y = 0 ∨ edist x y = ∞ := e.surjective.forall₂.2 fun x y ↦ by
      refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_ <;> simp [*, Dilation.ratio_ne_zero]
    simp [Dilation.ratio_of_trivial, *]

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

Goal state before:
pp: α : Type u_2
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖(AddMonoidHom.mulRight x) y‖ ≤ ‖y‖ * ‖x‖

Tactic:
exact norm_mul_le y x

Goal state after:
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:
by gcongr; apply norm_smul_le

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ : y ∈ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < r / 2}
hy₂ : y ∈ Prod.snd ⁻¹' U
this✝ : r ≤ ‖f y.2‖
this : r / 2 < ‖F y.1 y.2‖
⊢ (f y.2, F y.1 y.2) ∈ (closedBall 0 (r / 2))ᶜ ×ˢ (closedBall 0 (r / 2))ᶜ

Tactic:
simp_all [(half_lt_self hr₀).trans_le]

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

Goal state before:
pp: case mpr.inr
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), ((fun x_1 ↦ x_1 / x) ∘ u) n ∈ closedBall 0 1
a : K
ha' : Tendsto ((fun x_1 ↦ x_1 / x) ∘ u) atTop (𝓝 a)
hx' : x ≠ 0
⊢ ∀ (x_1 : ℕ), ((fun x_2 ↦ x_2 * x) ∘ (fun x_2 ↦ x_2 / x) ∘ u) x_1 = u x_1

Tactic:
simp [div_mul_cancel₀ _ hx']

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

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
⊢ z ∉ measurableAtom y

Tactic:
hzy

Goal state after:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
⊢ False
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : ↑(Icc 0 1)
⊢ ↑x = 0 ↔ x = 0

Tactic:
symm

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : ↑(Icc 0 1)
⊢ x = 0 ↔ ↑x = 0
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : ↑(Icc 0 1)
⊢ ↑x = 1 ↔ x = 1

Tactic:
symm

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : ↑(Icc 0 1)
⊢ x = 1 ↔ ↑x = 1
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Nontrivial R
x : ↑(Ico 0 1)
⊢ ↑x = 0 ↔ x = 0

Tactic:
symm

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Nontrivial R
x : ↑(Ico 0 1)
⊢ x = 0 ↔ ↑x = 0
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
x : ↑(Ioc 0 1)
⊢ ↑x = 1 ↔ x = 1

Tactic:
symm

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
x : ↑(Ioc 0 1)
⊢ x = 1 ↔ ↑x = 1
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : s.Nonempty
⊢ ((comap f) ⊤) s = ⊤ s

Tactic:
rw [comap_apply, top_apply hs, top_apply (hs.image _)]

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ∀ (a b c : SignType), a * b * c = a * (b * c)

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ∀ (a b : SignType), a * b = b * a

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ∀ (a b c : SignType), a ≤ b → b ≤ c → a ≤ c

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ∀ (a b : SignType), a ≤ b → b ≤ a → a = b

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ∀ (a b : SignType), a ≤ b ∨ b ≤ a

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: ⊢ Finset.univ = {0, -1, 1}

Tactic:
decide

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ s, ∑ a ∈ s, f a = ⨆ i, ∑ a ∈ s i, f a

Tactic:
symm

Goal state after:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ i, ∑ a ∈ s i, f a = ⨆ s, ∑ a ∈ s, f a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mpr
x y : EReal
⊢ x = y → x.abs = y.abs ∧ sign x = sign y

Tactic:
rintro rfl
    exact ⟨rfl, rfl⟩

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
hsum : ∑' (x : α), f x ≠ ∞
⊢ HasSum (fun x ↦ (f x).toReal) (∑' (x : α), (f x).toReal)

Tactic:
lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hsum

Goal state after:
α : Type u_1
f : α → ℝ≥0
hsum : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
⊢ HasSum (fun x ↦ ((fun i ↦ ↑(f i)) x).toReal) (∑' (x : α), ((fun i ↦ ↑(f i)) x).toReal)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: ⊢ Covariant { x // 0 < x } EReal (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 ≤ x2

Tactic:
by
  rintro ⟨x, x0⟩ a b h
  simp only [le_iff_sign, EReal.sign_mul, sign_pos x0, one_mul, EReal.abs_mul] at h ⊢
  exact h.imp_right <| Or.imp (And.imp_right <| And.imp_right (mul_le_mul_right · _)) <|
    Or.imp_right <| And.imp_right <| And.imp_right (mul_le_mul_right · _)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ LowerSemicontinuousOn f s ↔ ∀ (b : γ), ∃ v, IsClosed[inst✝¹] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v

Tactic:
simp only [← lowerSemicontinuous_restrict_iff, domRestrict_eq,
      lowerSemicontinuous_iff_isClosed_preimage, preimage_comp,
      isClosed_induced_iff, Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]

Goal state after: