mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ 2⁻¹ ^ n < (↑n)⁻¹

Tactic:
rw [← ENNReal.inv_pow, ENNReal.inv_lt_inv]

Goal state after:
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ ↑n < 2 ^ n
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
hg : ∃ j, g j ≠ ∞
h : ∀ (i j : ι), ∃ k, f k * g k ≤ f i * g j
i j k : ι
hk : f k * g k ≤ f i * g j
⊢ ⨅ i, f i * g i ≤ f i * g j

Tactic:
exact iInf_le_of_le k hk

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

Goal state before:
pp: R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a

Tactic:
by
  simp_rw [← smul_one_mul c (sSup s), ENNReal.mul_sSup, smul_one_mul]

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

Goal state before:
pp: ι : Sort u_3
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ g * iInf h

Tactic:
rw [mul_iInf]

Goal state after:
ι : Sort u_3
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ ⨅ i, g * h i
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
n : ℕ
⊢ True → ∃ x_1 ∈ V n, ∃ a, (x, a) = x_1 ∧ a ∈ iUnion U

Tactic:
_

Goal state after:
ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
n : ℕ
a✝ : True
⊢ ∃ x_1 ∈ V n, ∃ a, (x, a) = x_1 ∧ a ∈ iUnion U
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (c i)
hc₂ : s ⊆ ⋃ i, c i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ i, eball x δ ⊆ c i

Tactic:
by
  simpa only [eball, UniformSpace.ball, preimage_ofPred_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma hs hc₁ hc₂

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
a : α
h : ∀ (b : α), a < b → ∀ᶠ (x : γ) in l, f x < b
d : α
hd : IsGLB (Ioi a) d
H0 : Ioi a = Ici d
⊢ a < d

Tactic:
simp [← Set.mem_Ioi, H0]

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

Goal state before:
pp: case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h✝ : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
t : α
ht : t ∈ Icc a t₁
h : t < t₁
c : α
cA : c ∈ A
tc : t < c
⊢ t ∈ s

Tactic:
apply cA.2

Goal state after:
case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h✝ : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := ⋯
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := ⋯
t₁_mem : t₁ ∈ Icc a b
t : α
ht : t ∈ Icc a t₁
h : t < t₁
c : α
cA : c ∈ A
tc : t < c
⊢ t ∈ Icc a c
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
obtain ⟨K, u, hu, hfu⟩ := hf (h hx)

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
K : ℝ≥0
u : Set α
hu : u ∈ 𝓝[t] x
hfu : LipschitzOnWith K f u
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x✝ : α
hx : x✝ ∈ s
⊢ ∀ ⦃y : α⦄, y ∈ s → edist ((fun x ↦ (f x, g x)) x✝) ((fun x ↦ (f x, g x)) y) ≤ ↑(max Kf Kg) * edist x✝ y

Tactic:
_

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x✝ : α
hx : x✝ ∈ s
y✝ : α
⊢ y✝ ∈ s → edist ((fun x ↦ (f x, g x)) x✝) ((fun x ↦ (f x, g x)) y✝) ≤ ↑(max Kf Kg) * edist x✝ y✝
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: γ : Type u_3
β : Type u_4
f : γ ↪ β
⊢ (unconditional β).comap f = unconditional γ

Tactic:
simp only [unconditional, comap]

Goal state after:
γ : Type u_3
β : Type u_4
f : γ ↪ β
⊢ { filter := Filter.map (fun s ↦ s.preimage ⇑f ⋯) atTop } = { filter := atTop }
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ ∀ (s : Set (Finset ℕ)),
    (∃ a, ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s) → ∃ a, ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s

Tactic:
rintro s ⟨a, ha⟩

Goal state after:
case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ ∀ (s : Set (Finset ℕ)),
    (∃ a, ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s) → ∃ a, ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s

Tactic:
rintro s ⟨a, ha⟩

Goal state after:
case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ l (v x)
hv_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
c : γ
hc : ∀ᶠ (a : α) in f, l (v a) ≤ c
⊢ l (limsup v f) ≤ c

Tactic:
gc _ _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ l (v x)
hv_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
c : γ
hc : ∀ᶠ (a : α) in f, v a ≤ u c
⊢ limsup v f ≤ u c
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ limsup (fun a ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)

Tactic:
have bddmax := IsBoundedUnder.sup h₃ h₄
  have cobddmax := isCoboundedUnder_le_max (v := v) (Or.inl h₁)
  apply le_antisymm
  · refine (limsup_le_iff cobddmax bddmax).2 (fun b hb ↦ ?_)
    have hu := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_left _ _) hb) h₃
    have hv := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_right _ _) hb) h₄
    refine mem_of_superset (inter_mem hu hv) (fun _ ↦ by simp)
  · exact max_le (c := limsup (fun a ↦ max (u a) (v a)) f)
      (limsup_le_limsup (Eventually.of_forall (fun a : α ↦ le_max_left (u a) (v a))) h₁ bddmax)
      (limsup_le_limsup (Eventually.of_forall (fun a : α ↦ le_max_right (u a) (v a))) h₂ bddmax)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
⊢ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f = s.sup' hs fun i ↦ limsup (F i) f

Tactic:
by
  have bddsup := isBoundedUnder_le_finset_sup' hs h₂
  apply le_antisymm
  · have h₃ : ∃ i ∈ s, f.IsCoboundedUnder (· ≤ ·) (F i) := by
      rcases hs with ⟨i, i_s⟩
      use i, i_s
      exact h₁ i i_s
    have cobddsup := isCoboundedUnder_le_finset_sup' hs h₃
    refine (limsup_le_iff cobddsup bddsup).2 (fun b hb ↦ ?_)
    simp only [gt_iff_lt, sup'_lt_iff, eventually_all_finset] at hb ⊢
    exact fun i i_s ↦ eventually_lt_of_limsup_lt (hb i i_s) (h₂ i i_s)
  · apply Finset.sup'_le hs (fun i ↦ limsup (F i) f)
    refine fun i i_s ↦ limsup_le_limsup (Eventually.of_forall (fun a ↦ ?_)) (h₁ i i_s) bddsup
    simp only [le_sup'_iff]
    use i, i_s

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

Goal state before:
pp: case e'_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)

Tactic:
rw [tprod_fintype, Fintype.prod_bool, cond, cond]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
⊢ HasSum (fun i ↦ a₂ / f i) (a₂ * a₁) L ↔ HasSum (1 / f) a₁ L

Tactic:
simpa only [div_eq_mul_inv, one_mul] using! hasSum_mul_left_iff h

Goal state after:
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : IsEmpty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

case inr
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : Nonempty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : (fun x ↦ (f x).toReal) =ᶠ[l] fun x ↦ (g x).toReal
a✝ : α
hfx : f a✝ ≠ ∞
hgx : g a✝ ≠ ∞
⊢ (f a✝).toReal = (g a✝).toReal → f a✝ = g a✝

Tactic:
_

Goal state after:
α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : (fun x ↦ (f x).toReal) =ᶠ[l] fun x ↦ (g x).toReal
a✝¹ : α
hfx : f a✝¹ ≠ ∞
hgx : g a✝¹ ≠ ∞
a✝ : (f a✝¹).toReal = (g a✝¹).toReal
⊢ f a✝¹ = g a✝¹
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝ : SeminormedCommGroup 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_div, ← tendsto_iff_dist_tendsto_zero]

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

Goal state before:
pp: α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ pkg.compare pkg' (pkg'.compare pkg (pkg'.coe a)) = id (pkg'.coe a)

Tactic:
pkg'.compare_coe pkg,

Goal state after:
α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ pkg.compare pkg' (pkg.coe a) = id (pkg'.coe a)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
a_ne_top : a ≠ ∞
⊢ Continuous fun x ↦ a - x

Tactic:
change Continuous (Function.uncurry Sub.sub ∘ (a, ·))

Goal state after:
a : ℝ≥0∞
a_ne_top : a ≠ ∞
⊢ Continuous (uncurry Sub.sub ∘ fun x ↦ (a, x))
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
b : α
f : ↑(Iic b) → β
⊢ range (IicExtend f) = range f

Tactic:
by
  simp only [IicExtend, range_comp f, range_projIic, image_univ]

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

Goal state before:
pp: ⊢ LipschitzWith 1 Real.toNNReal

Tactic:
refine lipschitzWith_iff_dist_le_mul.mpr (fun x y ↦ ?_)

Goal state after:
x y : ℝ
⊢ dist x.toNNReal y.toNNReal ≤ ↑1 * dist x y
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: case refine_1
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
x : E
⊢ (↑K + 1)⁻¹ * ‖x‖ ≤ ‖f x‖

Tactic:
hK.le_mul_norm' (map_one f),

Goal state after:
case refine_1
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
x : E
⊢ (↑K + 1)⁻¹ * (↑K * ‖f x‖) ≤ ‖f x‖
Module: Mathlib.Analysis.Normed.Field.Basic

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

Tactic:
constructor <;> intro hx

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

case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
⊢ ‖x‖ = 1
Module: Mathlib.Analysis.Normed.Group.Bounded

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

Tactic:
NormedGroup.tendsto_nhds_one

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : ∀ ε > 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, ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
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
s : Set α
⊢ diam (⇑f '' s) = ↑(ratio f) * diam s

Tactic:
simp [diam, ediam_image, ENNReal.toReal_mul]

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

Goal state before:
pp: 𝕜 : Type u_4
h : NormedField 𝕜
⊢ DiscreteTopology 𝕜 ∨ Nonempty { h' // h'.toNormedField = h }

Tactic:
by_cases H : ∃ x : 𝕜, x ≠ 0 ∧ ‖x‖ ≠ 1
  · exact Or.inr ⟨(⟨NontriviallyNormedField.ofNormNeOne H, rfl⟩)⟩
  · simp_rw [discreteTopology_iff_isOpen_singleton_zero, Metric.isOpen_singleton_iff, dist_eq_norm,
             sub_zero]
    refine Or.inl ⟨1, zero_lt_one, ?_⟩
    contrapose! H
    refine H.imp ?_
    -- contextual to reuse the `a ≠ 0` hypothesis in the proof of `a ≠ 0 ∧ ‖a‖ ≠ 1`
    simp +contextual [ne_of_lt]

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

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

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : IsEmpty ι
⊢ MeasurableSet (⋃ b, f b)

case inr
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
⊢ MeasurableSet (⋃ b, f b)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: case iUnion
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
f : ℕ → Set α
⊢ (∀ (n : ℕ), MeasurableSet (f n)) → (∀ (n : ℕ), x ∈ f n ↔ y ∈ f n) → (x ∈ ⋃ i, f i ↔ y ∈ ⋃ i, f i)

Tactic:
_

Goal state after:
case iUnion
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
⊢ (∀ (n : ℕ), x ∈ f n ↔ y ∈ f n) → (x ∈ ⋃ i, f i ↔ y ∈ ⋃ i, f i)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
h : y ∈ measurableAtom x
s : Set β
hs : MeasurableSet s
hxs : x ∈ s
⊢ y ∈ s

Tactic:
simp only [measurableAtom, mem_iInter] at h

Goal state after:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
s : Set β
hs : MeasurableSet s
hxs : x ∈ s
h : ∀ (i : Set β), x ∈ i → MeasurableSet i → y ∈ i
⊢ y ∈ s
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
| Measurable fun x ↦ a = f x

Tactic:
1,

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
| fun x ↦ a = f x
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
a : α → ℝ≥0∞
tsum_ne_top : ∑' (i : α), a i ≠ ∞
j : α
⊢ a j < ∞

Tactic:
contrapose! tsum_ne_top with h
  exact ENNReal.tsum_eq_top_of_eq_top ⟨j, top_unique h⟩

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

Goal state before:
pp: case mpr.inl
x y : EReal
h : sign x < sign y
⊢ x ≤ y

Tactic:
exact (sign.monotone.reflect_lt h).le

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Ioo 0 b, c < b' * a

Tactic:
exact exists_lt_mul_left_of_nonneg hb.le hc h

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d dab ↦ ?_

Goal state after:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
⊢ d ≤ c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∃ i, True ∧ ∀ ⦃x : EReal⦄, x ∈ Iio ↑i → ENNReal.ofReal x.toReal = (fun x ↦ ENNReal.ofReal x.toReal) ⊥

Tactic:
simpa [toReal_bot, ENNReal.ofReal_zero, ENNReal.ofReal_eq_zero, true_and] using
      ⟨0, fun _ hx ↦ toReal_nonpos hx.le⟩

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
x : α
⊢ x ∈ s → ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x

Tactic:
_

Goal state after:
case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
x : α
a✝ : x ∈ s
⊢ ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

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

Tactic:
rcases s.eq_empty_or_nonempty with h | h <;> simp [h, Set.not_nonempty_empty]

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

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯ = boundedBy fun s ↦ m (f '' s)

Tactic:
dsimp only [boundedBy]
    congr with s : 1
    rw [image_nonempty]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
i : ℕ
⊢ i ∉ Set.range Encodable.encode → 0 ≤ f i

Tactic:
_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
i : ℕ
a✝ : i ∉ Set.range Encodable.encode
⊢ 0 ≤ f i
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inr
α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

Tactic:
filter_upwards [hg b hb] with x using Or.intro_right _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : IsEmpty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x

case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
⊢ (s ∩ t).Nonempty → s ∩ t ∈ {S}

Tactic:
_

Goal state after:
α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
a✝ : (s ∩ t).Nonempty
⊢ s ∩ t ∈ {S}