mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ ‖1‖ = 0

Tactic:
← dist_one_right,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ dist 1 1 = 0
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
⊢ UniformCauchySeqOn F atTop s ↔ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε

Tactic:
by
  constructor
  · intro h ε hε
    let u := { a : α × α | dist a.fst a.snd < ε }
    have hu : u ∈ 𝓤 α := Metric.mem_uniformity_dist.mpr ⟨ε, hε, by simp [u]⟩
    rw [← Filter.eventually_atTop_prod_self' (p := fun m =>
      ∀ x ∈ s, dist (F m.fst x) (F m.snd x) < ε)]
    specialize h u hu
    rw [prod_atTop_atTop_eq] at h
    exact h.mono fun n h x hx => h x hx
  · intro h u hu
    rcases Metric.mem_uniformity_dist.mp hu with ⟨ε, hε, hab⟩
    rcases h ε hε with ⟨N, hN⟩
    rw [prod_atTop_atTop_eq, eventually_atTop]
    use (N, N)
    intro b hb x hx
    rcases hb with ⟨hbl, hbr⟩
    exact hab (hN b.fst hbl.ge b.snd hbr.ge x hx)

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
⊢ a ∈ s

Tactic:
by
  suffices OrderDual.toDual a ∈ ofDual ⁻¹' s by aesop
  have : IsClosed (OrderDual.ofDual ⁻¹' (s ∩ Icc a b)) := hs
  rw [preimage_inter, ← Icc_toDual] at this
  apply this.mem_of_ge_of_forall_exists_gt (by simp_all) (by simp_all) (fun x hx ↦ ?_)
  rw [Ico_toDual, ← preimage_inter, ← Equiv.image_symm_eq_preimage, mem_image] at hx
  aesop

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
k : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k

Tactic:
rw [eventually_atTop]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
k : ℕ
⊢ ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → ∀ m ≥ b_1, dist (u m) (u b_1) < b k
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ ‖a‖ ≤ 0 ↔ a = 1

Tactic:
← dist_one_right,

Goal state after:
E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ dist a 1 ≤ 0 ↔ a = 1
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
⊢ Icc x y ⊆ s

Tactic:
apply (IsClosed.inter hs isClosed_Icc).Icc_subset_of_forall_mem_nhdsWithin hx.2

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
⊢ ∀ x_1 ∈ s ∩ Ico x y, s ∈ 𝓝[>] x_1
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: ⊢ UniformContinuous (Rat.cast ∘ fun p ↦ p.1 + p.2)

Tactic:
by
    simp only [Function.comp_def, Rat.cast_add]
    exact Real.uniformContinuous_add.comp
      (Rat.uniformContinuous_coe_real.prodMap Rat.uniformContinuous_coe_real)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ limsup (s.piecewise u v) f = (blimsup u f fun x ↦ x ∈ s) ⊔ blimsup v f fun x ↦ x ∉ s

Tactic:
← blimsup_sup_not (p := (· ∈ s))

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ ((blimsup (s.piecewise u v) f fun x ↦ x ∈ s) ⊔ blimsup (s.piecewise u v) f fun x ↦ x ∉ s) =
    (blimsup u f fun x ↦ x ∈ s) ⊔ blimsup v f fun x ↦ x ∉ s
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
⊢ a₁ ∈ s → ∀ y ∈ t, ∀ x ∈ s, ∀ y_1 ∈ t, edist (f a₁ y) (f x y_1) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t

Tactic:
ha₁

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
⊢ ∀ y ∈ t, ∀ x ∈ s, ∀ y_1 ∈ t, edist (f a₁ y) (f x y_1) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ Tendsto Finset.toLeft atTop atTop

Tactic:
intro s

Goal state after:
α : Type u_3
β : Type u_4
s : Set (Finset α)
⊢ s ∈ atTop → s ∈ map Finset.toLeft atTop
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ Tendsto Finset.toRight atTop atTop

Tactic:
intro s

Goal state after:
α : Type u_3
β : Type u_4
s : Set (Finset β)
⊢ s ∈ atTop → s ∈ map Finset.toRight atTop
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

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

pp: case neg
β : Type u_2
L : SummationFilter β
h : ¬L.filter = ⊥
⊢ L.NeBot ∨ L.filter = ⊥

Tactic:
· exact .inr h

Goal state after:
case neg
β : Type u_2
L : SummationFilter β
h : ¬L.filter = ⊥
⊢ L.NeBot ∨ L.filter = ⊥
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L

Tactic:
simp only [HasProd, SummationFilter.comap_filter, tendsto_map'_iff, comp_apply,
    Embedding.coeFn_mk, Function.comp_def]
  refine tendsto_congr fun s ↦ ?_
  rw [s.prod_preimage]
  exact fun x _ h ↦ hf x h

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hf : Multipliable f L
hL : ¬L.NeBot
hfs : (mulSupport fun x ↦ g (f x)).Finite
⊢ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g

Tactic:
simp [tprod_bot hL, finprod_eq_prod _ hfs, ← _root_.map_prod]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Real

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
⊢ dist x y ≤ dist x' y'

Tactic:
refine (dist_pi_le_iff dist_nonneg).2 fun b =>
    (Real.dist_le_of_mem_uIcc ?_ ?_).trans (dist_le_pi_dist x' y' b)

Goal state after:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ x b ∈ uIcc (x' b) (y' b)

case refine_2
ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ y b ∈ uIcc (x' b) (y' b)
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑(Kf * Kg) * edist ((g ∘ f) x) ((g ∘ f) y)

Tactic:
rw [ENNReal.coe_mul, mul_assoc]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑Kf * (↑Kg * edist ((g ∘ f) x) ((g ∘ f) y))
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case coe.top
a✝ b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a : ℝ≥0
ha : ↑a ≠ 0 ∨ ∞ ≠ ∞
hb : ∞ ≠ 0 ∨ ↑a ≠ ∞
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (↑a, ∞)) (𝓝 (↑a * ∞))

Tactic:
simp only [ne_eq, or_false, not_true_eq_false] at ha
      simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : SetRel α α → Set (CauchyFilter α × CauchyFilter α) := fun s ↦ {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
⊢ ((𝓤 α).lift fun s ↦ (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ (𝓤 α).lift' gen

Tactic:
by
        have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val
        simp only [Function.comp, h, mem_map, f]
        exact le_rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ≤ a
⊢ projIcc a b h x = ⟨a, ⋯⟩

Tactic:
simp [projIcc, hx, hx.trans h]

Goal state after:
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

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:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
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:
· push Not at h
      simp only [h, not_true, (pow_pos hr.1 _).not_ge]

Goal state after:
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₄))

Tactic:
refine (dif_pos H).trans_le ?_

Goal state after:
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
⊢ (1 / 2) ^ Nat.find H ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: E : Type u_1
inst✝ : MetricSpace E
x✝¹ y : E
x✝ : x✝¹ ≠ y
⊢ (fun x ↦ dist x y) ∈ {f | LipschitzWith 1 f}

Tactic:
by simp [LipschitzWith.dist_left]

Goal state after:
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: case inr
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))

Tactic:
simp only [← sup'_eq_sup hne]

Goal state after:
case inr
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
hi : Isometry f
h₁ : f 1 = 1
x : E
⊢ ‖f x‖ = ‖x‖

Tactic:
← dist_one_right,

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
hi : Isometry f
h₁ : f 1 = 1
x : E
⊢ dist (f x) 1 = ‖x‖
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ (fun x ↦ c • x) ⁻¹' eball x r = eball (c⁻¹ • x) r

Tactic:
preimage_smul,

Goal state after:
G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ c⁻¹ • eball x r = eball (c⁻¹ • x) r
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ (fun x ↦ c • x) ⁻¹' closedEBall x r = closedEBall (c⁻¹ • x) r

Tactic:
preimage_smul,

Goal state after:
G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ c⁻¹ • closedEBall x r = closedEBall (c⁻¹ • x) r
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x ↦ c • x) ⁻¹' ball x r = ball (c⁻¹ • x) r

Tactic:
preimage_smul,

Goal state after:
G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ c⁻¹ • ball x r = ball (c⁻¹ • x) r
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x ↦ c • x) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r

Tactic:
preimage_smul,

Goal state after:
G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ c⁻¹ • closedBall x r = closedBall (c⁻¹ • x) r
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x ↦ c • x) ⁻¹' sphere x r = sphere (c⁻¹ • x) r

Tactic:
preimage_smul,

Goal state after:
G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ c⁻¹ • sphere x r = sphere (c⁻¹ • x) r
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: β : Type u_5
inst✝¹ : NormedRing β
inst✝ : Nontrivial β
⊢ ‖1‖ ≤ ‖1‖ * ‖1‖

Tactic:
simpa only [mul_one] using norm_mul_le (1 : β) 1

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 G : ι → X → α
f g : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l s
hG : TendstoLocallyUniformlyOn G g l s
hf : ContinuousOn f s
hg : ContinuousOn g s
hg₀ : ∀ x ∈ s, g x ≠ 0
⊢ TendstoLocallyUniformlyOn (F * G⁻¹) (f * g⁻¹) l s

Tactic:
exact hF.mul₀ (hG.inv₀ hg hg₀) hf <| hg.inv₀ hg₀

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
F G : ι → X → α
f g : X → α
l : Filter ι
hF : TendstoLocallyUniformly F f l
hG : TendstoLocallyUniformly G g l
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
hg₀ : ∀ (x : X), g x ≠ 0
⊢ TendstoLocallyUniformly (F * G⁻¹) (f * g⁻¹) l

Tactic:
exact hF.mul₀ (hG.inv₀ hg hg₀) hf <| hg.inv₀ hg₀

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

Goal state before:
pp: case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = 1
⊢ sign (∑ i ∈ s, f i) = 1

Tactic:
sign_eq_one_iff

Goal state after:
case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, 0 < f i
⊢ 0 < ∑ i ∈ s, f i
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (↑a✝).abs = 0 ↔ ↑a✝ = 0

Tactic:
simp only [abs_def, coe_eq_zero, ENNReal.ofReal_eq_zero, abs_nonpos_iff]

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

Goal state before:
pp: ι : Type u_4
s : Finset ι
f : ι → ℝ≥0∞
⊢ ∑ i ∈ s, f i + ∑' (x : ι), (↑s)ᶜ.indicator f x = ∑' (i : ι), f i

Tactic:
sum_eq_tsum_indicator

Goal state after:
ι : Type u_4
s : Finset ι
f : ι → ℝ≥0∞
⊢ ∑' (x : ι), (↑s).indicator f x + ∑' (x : ι), (↑s)ᶜ.indicator f x = ∑' (i : ι), f i
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r' a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, r' x' b

Tactic:
← Filter.EventuallyEq.eq_of_nhdsWithin hfg has

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, r' x' b
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y z : EReal
⊢ x * y * z = x * (y * z)

Tactic:
← sign_eq_and_abs_eq_iff_eq

Goal state after:
x y z : EReal
⊢ (x * y * z).abs = (x * (y * z)).abs ∧ sign (x * y * z) = sign (x * (y * z))
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
⊢ (-a)⁻¹ = -a⁻¹

Tactic:
by
  induction a
  · rw [neg_bot, inv_top, inv_bot, neg_zero]
  · rw [← coe_inv _, ← coe_neg _⁻¹, ← coe_neg _, ← coe_inv (-_)]
    exact EReal.coe_eq_coe_iff.2 _root_.inv_neg
  · rw [neg_top, inv_bot, inv_top, neg_zero]

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

Goal state before:
pp: case coe
a : ℝ
h : ↑a ≤ 0
⊢ a ≤ 0

Tactic:
exact EReal.coe_nonpos.1 h

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
⊢ HasOpenCGraph fun x ↦ f x ∩ g x

Tactic:
by
  have : {x : α × β | x.2 ∈ f x.1 ∩ g x.1} =
      {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1} := by ext; simp
  rw [HasOpenCGraph, this]
  exact IsOpen.inter hf hg

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

Goal state before:
pp: case pos
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ∀ (i : ℕ), P (t i)
⊢ ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) ≤ ∑' (n : ℕ), m (t n)

Tactic:
exact iInf_le_of_le ht (iInf_le_of_le ht_subset le_rfl)

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n ↦ C * r ^ n) (C / (1 - r))
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)

Tactic:
simp only [pow_add, mul_left_comm C, mul_div_right_comm]

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n ↦ C * r ^ n) (C / (1 - r))
⊢ C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ ∀ (a : Set α), μ a ≤ ⨆ (_ : a.Nonempty), m a ↔ μ a ≤ m a

Tactic:
intro s

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ μ s ≤ ⨆ (_ : s.Nonempty), m s ↔ μ s ≤ m s
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ ∀ (a : Set α), μ a ≤ m a ↔ a.Nonempty → μ a ≤ m a

Tactic:
intro s

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ μ s ≤ m s ↔ s.Nonempty → μ s ≤ m s
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
⊢ ∀ (s : Set α), s.Nonempty → ⊤ s ≤ ⊤ s

Tactic:
intro s

Goal state after:
α : Type u_1
s : Set α
⊢ s.Nonempty → ⊤ s ≤ ⊤ s
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
⊢ (comap f) (⨅ i, m i) = ⨅ i, (comap f) (m i)

Tactic:
refine ext_nonempty fun s hs => ?_
  refine ((comap_mono f).map_iInf_le s).antisymm ?_
  simp only [comap_apply, iInf_apply' _ hs, iInf_apply' _ (hs.image _), le_iInf_iff,
    Set.image_subset_iff, preimage_iUnion]
  refine fun t ht => iInf_le_of_le _ (iInf_le_of_le ht <| ENNReal.tsum_le_tsum fun k => ?_)
  exact iInf_mono fun i => (m i).mono (image_preimage_subset _ _)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set α
⊢ IsPiSystem {S}

Tactic:
intro s

Goal state after:
α : Type u_1
S s : Set α
⊢ s ∈ {S} → ∀ t ∈ {S}, (s ∩ t).Nonempty → s ∩ t ∈ {S}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
⊢ IsPiSystem (insert ∅ S)

Tactic:
intro s

Goal state after:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
⊢ s ∈ insert ∅ S → ∀ t ∈ insert ∅ S, (s ∩ t).Nonempty → s ∩ t ∈ insert ∅ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
⊢ IsPiSystem (insert ∅ S)

Tactic:
by
  intro s hs t ht hst
  rcases hs with hs | hs
  · simp [hs]
  · rcases ht with ht | ht
    · simp [ht]
    · exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)

Goal state after: