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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
hpos : 0 < r
hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖
x y : E
hne : x ≠ y
⊢ x⁻¹ * y ≠ 1

Tactic:
by simpa [inv_mul_eq_one] using hne

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

Goal state before:
pp: β : Type u_3
f : ℕ → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f atTop l

Tactic:
by
  exact tendsto_comp_val_Ioi_atTop

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

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

Tactic:
simp only [← tendsto_neg_atTop_iff, ← neg_mul] at hf ⊢
  exact hf.atTop_mul_const' hr

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

Goal state before:
pp: α : Type u
s : Set α
x y : α
inst✝ : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ diam (s ∪ t) ≤ diam s + dist x y + diam t

Tactic:
simp only [diam, dist_edist]

Goal state after:
α : Type u
s : Set α
x y : α
inst✝ : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ (ediam (s ∪ t)).toReal ≤ (ediam s).toReal + (edist x y).toReal + (ediam t).toReal
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ cobounded α = cocompact α

Tactic:
nontriviality α

Goal state after:
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
a✝ : Nontrivial α
⊢ cobounded α = cocompact α
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
inst✝ : Nonempty ι
I : ι → Ideal R
hI : ∀ (i : ι), I i ≠ ⊥
⊢ multiplicity p.asIdeal (⨆ i, I i) = ⨅ i, multiplicity p.asIdeal (I i)

Tactic:
have H i : FiniteMultiplicity p.asIdeal (I i) :=
    FiniteMultiplicity.of_prime_left (prime p) <| hI i
  have H' : FiniteMultiplicity p.asIdeal (⨆ i, I i) := by
    refine FiniteMultiplicity.of_prime_left (prime p) ?_
    contrapose! hI
    rw [← bot_eq_zero, iSup_eq_bot] at hI
    exact ⟨Classical.ofNonempty, hI _⟩
  have := emultiplicity_iSup p I
  simp only [H'.emultiplicity_eq_multiplicity, (H _).emultiplicity_eq_multiplicity] at this
  exact_mod_cast this

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
Kg : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t
Kf : ℝ≥0
u : Set β
hu : u ∈ 𝓝 (g x)
hfL : LipschitzOnWith Kf f u
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t

Tactic:
refine ⟨Kf * Kg, t ∩ g⁻¹' u, inter_mem ht (hg.continuous.continuousAt hu), ?_⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
Kg : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t
Kf : ℝ≥0
u : Set β
hu : u ∈ 𝓝 (g x)
hfL : LipschitzOnWith Kf f u
⊢ LipschitzOnWith (Kf * Kg) (f ∘ g) (t ∩ g ⁻¹' u)
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
r : α
hr : limsup (fun i ↦ u i r) cofinite < b
h : c < limsup (fun x ↦ u x r) cofinite
⊢ (Set.Ioo c b).Nonempty

Tactic:
exact ⟨limsup (u · r) cofinite, h, hr⟩

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset α
⊢ ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f (g x) = ∏ b ∈ v', f b

Tactic:
refine ⟨s.image g, fun t ht => ?_⟩

Goal state after:
case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset α
t : Finset β
ht : image g s ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f (g x) = ∏ b ∈ t, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : Preorder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
f : ι → α
a : α
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
hf : HasProd f a L
i : ι
hb : ∀ (j : ι), j ≠ i → 1 ≤ f j
⊢ f i = ∏ i ∈ {i}, f i

Tactic:
rw [prod_singleton]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ∏' (i : ι), f i = 1 ↔ HasProd f 1

Tactic:
hf.hasProd_iff

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ∏' (i : ι), f i = 1 ↔ ∏' (b : ι), f b = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Finite β
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
let : Fintype β := Fintype.ofFinite β
    rw [tprod_eq_prod (s := univ) (fun x hx ↦ (hx (mem_univ x)).elim)]
    simp only [prod_const, Nat.card_eq_fintype_card, Fintype.card]

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

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
⊢ Disjoint (image Nat.cast v') (image Int.negSucc v')

Tactic:
simp only [disjoint_iff_ne, mem_image, ne_eq, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂, not_false_eq_true, implies_true, reduceCtorEq]

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

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
⊢ ∏ x ∈ image Nat.cast v' ∪ image Int.negSucc v', f x = ∏ b ∈ v', f ↑b * f (Int.negSucc b)

Tactic:
· rw [prod_union, prod_image Nat.cast_injective.injOn, prod_image this.injOn,
      prod_mul_distrib]
    simp only [disjoint_iff_ne, mem_image, ne_eq, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂, not_false_eq_true, implies_true, reduceCtorEq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
⊢ ∏' (c : γ), f (g c) = ∏' (b : β), f b

Tactic:
rw [← Function.comp_def]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
⊢ tprod (f ∘ g) = ∏' (b : β), f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
hf : Multipliable f
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
⊢ Multipliable g

Tactic:
obtain ⟨c, hc⟩ := hf

Goal state after:
α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
c : K
hc : HasProd f c
⊢ Multipliable g
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case pos
α : 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:
exact h_closed.mem_of_tendsto hf.hasProd <| .of_forall fun _ => prod_mem fun i _ => h i

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

Goal state before:
pp: β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
⊢ IsCompact (closedBall x₀ r)

Tactic:
have A : IsClosed K := isClosed_closedBall.preimage f_cont

Goal state after:
β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
⊢ IsCompact (closedBall x₀ r)
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
B : Bornology.IsBounded K
⊢ IsCompact (closedBall x₀ r)

Tactic:
have : IsCompact K := isCompact_iff_isClosed_bounded.2 ⟨A, B⟩

Goal state after:
β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
B : Bornology.IsBounded K
this : IsCompact K
⊢ IsCompact (closedBall x₀ r)
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : s ∈ l
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s

Tactic:
have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)

Goal state after:
X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : s ∈ l
this✝ : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
this : ∀ (n : ℕ), W n ∩ s ×ˢ s ∈ l ×ˢ l
⊢ ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝ : SeminormedGroup E
f : α → E
a : Filter α
b : E
⊢ Tendsto f a (𝓝 b) ↔ Tendsto (fun e ↦ ‖(f e)⁻¹ * b‖) a (𝓝 0)

Tactic:
simp only [← dist_eq_norm_inv_mul, ← tendsto_iff_dist_tendsto_zero]

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
M : ℕ
hMl : M ≤ l.length
hMs : IsGreatest s M
⊢ M < l.length + 1

Tactic:
Nat.lt_succ_iff

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
N : β
hN : b N < ε
⊢ ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε

Tactic:
refine ⟨N, fun m hm n hn => ?_⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
N : β
hN : b N < ε
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ edist (s m) (s n) < ε
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: case cons
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✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))

Tactic:
simp only [sup'_cons, hne]

Goal state after:
case cons
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✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
⊢ Tendsto (f a ⊔ s.sup' hne f) l (𝓝 (g a ⊔ s.sup' hne g))
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.mulRight₀ _ (lt_of_le_of_ne ha h)) hs f

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

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz fun x ↦ f x * g x

Tactic:
simpa [← locallyLipschitzOn_univ] using hf.locallyLipschitzOn.mul hg.locallyLipschitzOn

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

Tactic:
obtain ⟨K, ⟨hK1, hK2⟩⟩ := exists_compact_iff_hasCompactMulSupport.mpr hf

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵢ Y
⊢ ratio (Isometry.toDilation ⇑e ⋯) = 1

Tactic:
Isometry.toDilation_ratio

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵢ Y
⊢ 1 = 1
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ (∃ x_1, dist x_1 x ≤ ε ∧ s • x_1 = p) → dist p (s • x) ≤ ‖s‖ * ε

pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ dist p (s • x) ≤ ‖s‖ * ε → ∃ x_1, dist x_1 x ≤ ε ∧ s • x_1 = p

Tactic:
· rintro ⟨y, h1, rfl⟩
    simpa [dist_smul₀] using mul_le_mul_of_nonneg_left h1 (norm_nonneg s)

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ dist p (s • x) ≤ ‖s‖ * ε → ∃ x_1, dist x_1 x ≤ ε ∧ s • x_1 = p
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
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

Tactic:
simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]

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
⊢ z ⟨i, hit⟩ = if h : True ∨ True then (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩ else x i
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case neg
ι : 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
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

Tactic:
simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]

Goal state after:
case neg
ι : 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
⊢ y ⟨i, ⋯⟩ = if h : True ∨ False then (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩ else 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
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

Tactic:
simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]

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
⊢ z ⟨i, hit⟩ = (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case neg
ι : 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
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

Tactic:
simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]

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

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : ↥s) → π ↑i
⊢ s.restrict (updateFinset x s y) = y

Tactic:
rw [restrict_updateFinset_of_subset subset_rfl]
  rfl

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
⊢ (f y.2, F y.1 y.2) ∈ (closedBall 0 (r / 2))ᶜ ×ˢ (closedBall 0 (r / 2))ᶜ

Tactic:
have : r ≤ ‖f y.2‖ := by simp_all [Set.disjoint_left]

Goal state after:
α : 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‖
⊢ (f y.2, F y.1 y.2) ∈ (closedBall 0 (r / 2))ᶜ ×ˢ (closedBall 0 (r / 2))ᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
g : β → α
hg : Function.Surjective g
⊢ MeasurableSpace.map g (MeasurableSpace.comap g m) = m

Tactic:
refine le_antisymm (fun S hS => ?_) le_map_comap

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
g : β → α
hg : Function.Surjective g
S : Set α
hS : MeasurableSet S
⊢ MeasurableSet S
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: α : Type u_6
inst✝¹ : SeminormedRing α
inst✝ : NormSMulClass ℤ α
n : ℤ
⊢ ‖n‖ * ‖1‖ = ↑|n| * ‖1‖

Tactic:
Int.norm_eq_abs,

Goal state after:
α : Type u_6
inst✝¹ : SeminormedRing α
inst✝ : NormSMulClass ℤ α
n : ℤ
⊢ |↑n| * ‖1‖ = ↑|n| * ‖1‖
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ ‖k‖ * ‖e‖ < ‖e‖ ↔ k • e = 0

Tactic:
Int.norm_eq_abs,

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ |↑k| * ‖e‖ < ‖e‖ ↔ k • e = 0