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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (s.domRestrict fst)) (a, b).1 ∧ IsLUB (snd '' s) (a, b).2
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))

Tactic:
← range_domRestrict

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (s.domRestrict fst)) (a, b).1 ∧ IsLUB (range (s.domRestrict snd)) (a, b).2
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
exact ENNReal.ofReal_add_le

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ (map u (f ⊓ 𝓟 {x | p x})).limsSup = (map u (map Subtype.val (comap Subtype.val f))).limsSup

Tactic:
map_comap_setCoe_val

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ (map u (f ⊓ 𝓟 {x | p x})).limsSup = (map u (f ⊓ 𝓟 {x | p x})).limsSup
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, u i ≤ a
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
b : α
hb : ∀ᶠ (n : ι) in f, b ≤ u n
⊢ b ≤ a

Tactic:
obtain ⟨n, hna, hbn⟩ := (hu.and_eventually hb).exists

Goal state after:
α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, u i ≤ a
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
b : α
hb : ∀ᶠ (n : ι) in f, b ≤ u n
n : ι
hna : u n ≤ a
hbn : b ≤ u n
⊢ b ≤ a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inl
x : ℝ≥0
⊢ ↑↑x = ↑↑(↑x).toNNReal - ↑↑(-↑x).toNNReal

Tactic:
Real.toNNReal_of_nonpos (neg_nonpos.mpr x.coe_nonneg),

Goal state after:
case inl
x : ℝ≥0
⊢ ↑↑x = ↑↑(↑x).toNNReal - ↑↑0
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ a ⊔ liminf u f = liminf (fun x ↦ a ⊔ u x) f

Tactic:
simp only [liminf_eq_iSup_iInf]
  rw [sup_comm, biSup_sup (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
  simp_rw [iInf₂_sup_eq, sup_comm (a := a)]

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

Goal state before:
pp: case bot
a b : EReal
h : a ≤ ⊥
⊢ a - ⊥ ≤ b

Tactic:
le_bot_iff

Goal state after:
case bot
a b : EReal
h : a = ⊥
⊢ a - ⊥ ≤ b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
h : a < b + c
⊢ a < c + b

Tactic:
by rwa [add_comm]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : ↑{i | q i}
⊢ x ∈ u ((fun i ↦ g (b ↑i) ⋯) i)

Tactic:
exact hg' (b i) (hl.mem_of_mem i.2)

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

Goal state before:
pp: case a
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
⊢ ∀ c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a}), c < liminf f F

Tactic:
intro c

Goal state after:
case a
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : S
⊢ c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a}) → c < liminf f F
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
⊢ d ∈ {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}

Tactic:
rcases hd with ⟨e, ⟨he, fe_eq_d⟩⟩
      filter_upwards [he] with x hx using (fe_eq_d.symm ▸ f_decr hx)

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a₁ : α
inst✝¹ : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : ¬b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

Tactic:
· simp only [h, update_of_ne, if_false, Ne, one_mul, not_false_iff]

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

Goal state before:
pp: case e_a
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
⊢ (∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) = ∏ x ∈ u1 ∩ u2, f x

Tactic:
refine (prod_subset_one_on_sdiff inter_subset_union ?_ ?_).symm

Goal state after:
case e_a.refine_1
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
⊢ ∀ x ∈ (u1 ∪ u2) \ (u1 ∩ u2), (if x = 0 then f 0 else 1) = 1

case e_a.refine_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
⊢ ∀ x ∈ u1 ∩ u2, f x = if x = 0 then f 0 else 1
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
a : G
⊢ HasProd (fun x ↦ f ↑x) a ↔ HasProd f (a * f 0)

Tactic:
by
  simp [hasProd_pnat_iff_hasProd_succ, hasProd_nat_add_iff]

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
α : Fin 2 → Type u_3
inst✝ : (i : Fin 2) → PseudoEMetricSpace (α i)
x hx : (i : Fin 2) → α i
⊢ edist ((piFinTwoEquiv α).toFun x) ((piFinTwoEquiv α).toFun hx) = edist x hx

Tactic:
by simp [edist_pi_def, Fin.univ_succ, Prod.edist_eq]

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case h
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
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
set L := zipWith d (x::l) (l ++ [y])

Goal state after:
case h
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])
⊢ d x y ≤ 2 * L.sum
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedGroup E
⊢ comap norm (𝓝 0) = 𝓝 1

Tactic:
simpa only [dist_one_right] using nhds_comap_dist (1 : E)

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

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
γ : Type uγ
inst✝ : UniformSpace γ
pkg'' : AbstractCompletion.{vγ, uγ} γ
e : α ≃ᵤ β
⊢ pkg.map pkg' ⇑e ∘ pkg'.map pkg ⇑e.symm = id

Tactic:
simp [map_comp _ _ _ e.uniformContinuous e.symm.uniformContinuous]

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

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous[inst✝².toTopologicalSpace, inst✝¹] f
⊢ (∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))) → ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

Tactic:
by
  intro h
  have (x : α) : (pkg.isDenseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by
    simp only [Function.comp_apply, compare_coe, IsDenseInducing.extend_eq _ cont_f]
  apply (IsDenseInducing.extend_unique (AbstractCompletion.isDenseInducing _) this
    (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous)).symm
  apply IsDenseInducing.continuous_extend
  exact fun a ↦ ⟨(pkg.isDenseInducing.extend f) a, h a⟩

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

Goal state before:
pp: n : ℕ
⊢ Continuous fun a ↦ a ^ n

Tactic:
induction n with
  | zero => simp [continuous_const]
  | succ n IH =>
    simp_rw [pow_add, pow_one, continuous_iff_continuousAt]
    intro x
    refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_ <;> by_cases H : x = 0
    · simp only [H, zero_ne_top, Ne, or_true, not_false_iff]
    · exact Or.inl fun h => H (eq_zero_of_pow_eq_zero h)
    · simp only [H, pow_eq_top_iff, zero_ne_top, false_or, not_true, Ne,
        not_false_iff, false_and]
    · simp only [H, true_or, Ne, not_false_iff]

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

Goal state before:
pp: case neg
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous fun x ↦ x - a

Tactic:
show (fun x => x - a) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨x, a⟩ by rfl

Goal state after:
case neg
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous ((fun p ↦ p.1 - p.2) ∘ fun x ↦ (x, a))
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
a b : E
⊢ dist (b * a) b = ‖a‖

Tactic:
by
  rw [dist_comm, dist_self_mul_right]

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂

Tactic:
simp only [edist_nndist]
  norm_cast
  apply nndist_mul_mul_le

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

Goal state before:
pp: α : Type u_6
β : Type u_7
F : Type u_5
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : dist x y ≠ 0
hr : dist (f x) (f y) = ↑r * dist x y
⊢ ↑(nndist (f x) (f y)) = ↑(r * nndist x y)

Tactic:
coe_nndist,

Goal state after:
α : Type u_6
β : Type u_7
F : Type u_5
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : dist x y ≠ 0
hr : dist (f x) (f y) = ↑r * dist x y
⊢ dist (f x) (f y) = ↑(r * nndist x y)
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
r : ℝ≥0
hr : r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
x y : α
⊢ ↑(nndist (f x) (f y)) = ↑(r * nndist x y)

Tactic:
coe_nndist,

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
r : ℝ≥0
hr : r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
x y : α
⊢ dist (f x) (f y) = ↑(r * nndist x y)
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst✝ : NonUnitalSeminormedRing β
x y : α × β
⊢ max (‖x.1‖ * ‖y.1‖) (‖x.2‖ * ‖y.2‖) = max (‖x.1‖ * ‖y.1‖) (‖y.2‖ * ‖x.2‖)

Tactic:
by simp [mul_comm]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ∀ (s : Set α), s = ∅ ∨ s = univ → sᶜ = ∅ ∨ sᶜ = univ

Tactic:
by simp +contextual [or_imp]

Goal state after:
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
x : E
hx : x ∈ AddSubgroup.zmultiples e
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' ball 0 ‖e‖ ↔ ⟨x, hx⟩ ∈ {0}

Tactic:
obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx

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, hx⟩ ∈ Subtype.val ⁻¹' ball 0 ‖e‖ ↔ ⟨k • e, hx⟩ ∈ {0}
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, hx⟩ = 0

Tactic:
Subtype.ext_iff,

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, hx⟩ = ↑0
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
⊢ Tendsto (⇑(algebraMap 𝕜 𝕜')) (cobounded 𝕜) (cobounded 𝕜')

Tactic:
intro c

Goal state after:
𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
⊢ c ∈ cobounded 𝕜' → c ∈ map (⇑(algebraMap 𝕜 𝕜')) (cobounded 𝕜)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ ⋃ i, t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (iUnionLift t f htf T hT ⁻¹' s)

Tactic:
preimage_iUnionLift

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ ⋃ i, t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (inclusion hT ⁻¹' ⋃ i, inclusion ⋯ '' f i ⁻¹' s)
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ ((restrict s) m) u ≤ ((restrict t) m') u

Tactic:
by
  simp only [restrict_apply]
  exact (hm _).trans (m'.mono <| inter_subset_inter_right _ h)

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) = pos
⊢ sign (∑ i ∈ s, f i) = pos

Tactic:
pos_eq_one,

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, sign (f i) = 1
⊢ sign (∑ i ∈ s, f i) = 1
Module: Mathlib.Data.Sign.Basic

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

Tactic:
cases t
  · simp_rw [zero_eq_zero, sign_eq_zero_iff] at h ⊢
    exact Finset.sum_eq_zero h
  · simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h ⊢
    exact Finset.sum_neg h hs
  · simp_rw [pos_eq_one, sign_eq_one_iff] at h ⊢
    exact Finset.sum_pos h hs

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddRightMono α
n : ℕ
⊢ 0 ≤ 1 - 1 / ↑n

Tactic:
by
  rw [sub_nonneg, one_div]
  exact cast_inv_le_one n

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

Goal state before:
pp: x : EReal
⊢ ↑x.abs * ↑(sign x) = x

Tactic:
by
  rw [EReal.mul_comm, EReal.sign_mul_abs]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
⊢ SemicontinuousAt r x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝 x, ¬r x' y) → ¬r x y

Tactic:
simp only [← not_eventually, not_imp_not, SemicontinuousAt]

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

Goal state before:
pp: case pos
β : Type u_2
f : β → ℝ≥0
h : Summable f
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Tactic:
← ENNReal.coe_tsum h,

Goal state after:
case pos
β : Type u_2
f : β → ℝ≥0
h : Summable f
⊢ ∑' (b : β), f b = (↑(tsum f)).toNNReal
Module: Mathlib.Data.EReal.Inv

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

Tactic:
induction a

Goal state after:
case bot
⊢ (-⊥)⁻¹ = -⊥⁻¹

case coe
a✝ : ℝ
⊢ (-↑a✝)⁻¹ = -(↑a✝)⁻¹

case top
⊢ (-⊤)⁻¹ = -⊤⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case pos_bot
x : ℝ
x_pos : 0 < x
⊢ 0 = (↑x)⁻¹ * 0

Tactic:
mul_zero

Goal state after:
case pos_bot
x : ℝ
x_pos : 0 < x
⊢ 0 = 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case neg_bot
x : ℝ
x_neg : x < 0
⊢ 0 = (↑x)⁻¹ * 0

Tactic:
mul_zero

Goal state after:
case neg_bot
x : ℝ
x_neg : x < 0
⊢ 0 = 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h : a ≤ 0
⊢ a⁻¹ ≤ 0

Tactic:
cases a with
  | bot => simp
  | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]; exact EReal.coe_nonpos.1 h

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousAt f x
gmon : Monotone g
⊢ LowerSemicontinuousAt (g ∘ f) x

Tactic:
simp only [← lowerSemicontinuousWithinAt_univ_iff] at hf ⊢
  exact hg.comp_lowerSemicontinuousWithinAt hf gmon

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

Goal state before:
pp: case pos
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto (fun n ↦ 1) atTop (𝓝 0)
⊢ False

Tactic:
exact zero_ne_one <| tendsto_nhds_unique h tendsto_const_nhds

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ CauchySeq f

Tactic:
refine cauchySeq_of_edist_le_geometric 2⁻¹ C ?_ hC hu

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ 2⁻¹ < 1
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
⊢ (boundedBy m) s = (OuterMeasure.ofFunction m m_empty) s

Tactic:
have : (fun s : Set α => ⨆ _ : s.Nonempty, m s) = m := by
    ext1 t
    rcases t.eq_empty_or_nonempty with h | h <;> simp [h, Set.not_nonempty_empty, m_empty]

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
this : (fun s ↦ ⨆ (_ : s.Nonempty), m s) = m
⊢ (boundedBy m) s = (OuterMeasure.ofFunction m m_empty) s
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set (OuterMeasure α)
s : Set α
h : m.Nonempty
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), sInfGen m (t n) =
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)

Tactic:
iSup_sInfGen_nonempty h

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋂ x, dissipate s x ⊆ ⋂ x, s x

Tactic:
simp_rw [subset_def, dissipate_def, mem_iInter]

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β), (∀ (i i_1 : α), i_1 ≤ i → x ∈ s i_1) → ∀ (i : α), x ∈ s i
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋂ x, s x ⊆ ⋂ x, dissipate s x

Tactic:
simp_rw [subset_def, dissipate_def, mem_iInter]

Goal state after:
case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β), (∀ (i : α), x ∈ s i) → ∀ (i i_1 : α), i_1 ≤ i → x ∈ s i_1
Module: Mathlib.MeasureTheory.PiSystem

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

Tactic:
intro s h_s t h_t _

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}
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ s ∪ t =ᵐ[μ] t ↔ μ (s \ t) = 0

Tactic:
by
  simp [eventuallyLE_antisymm_iff, ae_le_set, union_sdiff_right,
    sdiff_eq_empty.2 Set.subset_union_right]

Goal state after: