mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : ℝ≥0∞
⊢ recENNReal coe neg_coe ↑x = coe x

Tactic:
suffices ∀ y : EReal, x = y → (recENNReal coe neg_coe y : motive y) ≍ coe x from
    heq_iff_eq.mp (this x rfl)

Goal state after:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : ℝ≥0∞
⊢ ∀ (y : EReal), ↑x = y → recENNReal coe neg_coe y ≍ coe x
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

Tactic:
rcases eq_or_ne (u b) ⊥ with hu | hu

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

case inr
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ limsup u (f ⊔ g) ≤ limsup u f ⊔ limsup u g

Tactic:
simp_rw [limsup_eq, sInf_sup_eq, sup_sInf_eq, mem_ofPred_eq, le_iInf₂_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ ∀ (i : α),
    (∀ᶠ (n : β) in f, u n ≤ i) →
      ∀ (i_1 : α), (∀ᶠ (n : β) in g, u n ≤ i_1) → sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ i ⊔ i_1
Module: Mathlib.Topology.EMetricSpace.Lipschitz

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

Tactic:
refine ⟨max Kf Kg, t₁ ∩ t₂, Filter.inter_mem h₁t h₂t, ?_⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set α
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ LipschitzOnWith (max Kf Kg) (fun x ↦ (f x, g x)) (t₁ ∩ t₂)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
u v : α → β
h : ∃ᶠ (x : α) in ⊥, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ v
⊢ liminf u ⊥ ≤ limsup v ⊥

pp: case inr
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h✝ : f.NeBot
⊢ liminf u f ≤ limsup v f

Tactic:
· exact (frequently_bot h).rec

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h✝ : f.NeBot
⊢ liminf u f ≤ limsup v f
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ⊥ * ↑x✝ = ⊥

Tactic:
bot_mul_coe_of_pos h

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ⊥ = ⊥
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case pos_top
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊤ = -(↑x✝ * ⊤)

Tactic:
coe_mul_top_of_pos h,

Goal state after:
case pos_top
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊤ = -⊤
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i

Tactic:
have : ∀ (j : Subtype p), Nonempty (s j) := fun j ↦ Nonempty.coe_sort (hs j)

Goal state after:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
hb : 0 ≤ b
hc : c ≤ 0
⊢ a * (b - c) = a * b - a * c

Tactic:
rw [sub_eq_add_neg, left_distrib_of_nonneg hb (by simpa)]
  simp [← neg_mul, sub_eq_add_neg]

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 α
f : β → α
a : α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous[inst✝⁴, inst✝²] ⇑g
⊢ HasProd (⇑g ∘ f) (g a) L

Tactic:
have : (g ∘ fun s : Finset β ↦ ∏ b ∈ s, f b) = fun s : Finset β ↦ ∏ b ∈ s, (g ∘ f) b :=
    funext <| map_prod g _
  unfold HasProd
  rw [← this]
  exact (hg.tendsto a).comp hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ⊆ (t₁, t₂).1
ht₂ : (s, s).2 ⊆ (t₁, t₂).2
⊢ ((∏ x ∈ (t₁, t₂).2 \ (s, s).2, f x) * ∏ x ∈ (s, s).2, f x) /
      ((∏ x ∈ (t₁, t₂).1 \ (s, s).1, f x) * ∏ x ∈ (s, s).1, f x) =
    (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b

Tactic:
mul_div_mul_right_eq_div

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ⊆ (t₁, t₂).1
ht₂ : (s, s).2 ⊆ (t₁, t₂).2
⊢ (∏ x ∈ (t₁, t₂).2 \ (s, s).2, f x) / ∏ x ∈ (t₁, t₂).1 \ (s, s).1, f x = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : TopologicalSpace α
f : ι → α
h : Summable fun x ↦ ∏ i ∈ x, f i
⊢ Multipliable fun x ↦ 1 + f x

Tactic:
obtain ⟨a, h⟩ := h

Goal state after:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun x ↦ ∏ i ∈ x, f i) a
⊢ Multipliable fun x ↦ 1 + f x
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx :
  Tendsto (fun x ↦ 1 + ∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
⊢ 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j) = x

Tactic:
rw [ha.tsum_eq]

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx :
  Tendsto (fun x ↦ 1 + ∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
⊢ 1 + a = x
Module: Mathlib.Topology.MetricSpace.Pseudo.Real

Goal state before:
pp: x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ y ∈ uIcc y' x'

Tactic:
by rwa [uIcc_comm]

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

Goal state before:
pp: x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ x ∈ uIcc y' x'

Tactic:
by rwa [uIcc_comm]

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

Goal state before:
pp: α : Type u_3
f : α → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
by
  simp only [← summable_coe, ← tendsto_coe] at hf ⊢
  exact hf.tendsto_cofinite_zero

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

Goal state before:
pp: 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.toUniformSpace = inst✝¹

Tactic:
let I := PseudoMetricSpace.ofPreNNDist d (fun x => hd₀.2 rfl) hd_symm

Goal state after:
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
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
⊢ LipschitzOnWith K f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
by
  have := ENNReal.continuous_const_mul (ENNReal.coe_ne_top (r := K))
  refine fun x hx ↦ le_on_closure (fun y hy ↦ le_on_closure (fun x hx ↦ hf hx hy) ?_ ?_ hx) ?_ ?_
  all_goals fun_prop

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

Goal state before:
pp: 𝓕 : 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 y : E), ‖f (x⁻¹ * y)‖ = ‖x⁻¹ * y‖) ↔ ∀ (x : E), ‖f x‖ = ‖x‖

Tactic:
refine ⟨fun h x => ?_, fun h x y => h _⟩

Goal state after:
𝓕 : 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 : 𝓕
h : ∀ (x y : E), ‖f (x⁻¹ * y)‖ = ‖x⁻¹ * y‖
x : E
⊢ ‖f x‖ = ‖x‖
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
⊢ edist a⁻¹ b⁻¹ = edist a b

Tactic:
rw [← edist_mul_left a, ← edist_mul_right _ _ b, mul_inv_cancel, one_mul, inv_mul_cancel_right,
    edist_comm]

Goal state after:
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
  · contrapose! hx
    simp [hx]
  · have : IsOpen {(0 : 𝕜)} := isOpen_discrete {0}
    simp_rw [Metric.isOpen_singleton_iff, dist_eq_norm, sub_zero] at this
    obtain ⟨ε, εpos, h'⟩ := this
    wlog! h : ‖x‖ < 1 generalizing 𝕜 with H
    · rcases h.eq_or_lt with h | h
      · rw [h]
      replace h := norm_inv x ▸ inv_lt_one_of_one_lt₀ h
      rw [← inv_inj, inv_one, ← norm_inv]
      exact H (by simpa) h' h
    obtain ⟨k, hk⟩ : ∃ k : ℕ, ‖x‖ ^ k < ε := exists_pow_lt_of_lt_one εpos h
    rw [← norm_pow] at hk
    specialize h' _ hk
    simp [hx] at h'

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x}ᶜ

Tactic:
Metric.mem_closure_iff

Goal state after:
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
⊢ ∀ ε > 0, ∃ b ∈ {x}ᶜ, dist x b < ε
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x₁ x₂ : αᵐᵒᵖ
y : α
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0

Tactic:
by
    simpa [mul_sub, dist_eq_norm, mul_comm] using! norm_mul_le y (x₁ - x₂).unop

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

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Finset ι
hf : DependsOn f ↑s
i : ι
y : π i
⊢ DependsOn (fun x ↦ f (Function.update x i y)) ↑(s.erase i)

Tactic:
Function.update_eq_updateFinset,

Goal state after:
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Finset ι
hf : DependsOn f ↑s
i : ι
y : π i
⊢ DependsOn (fun x ↦ f (updateFinset x {i} (uniqueElim y))) ↑(s.erase i)
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: case snd
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
⊢ v.2 = w.2

Tactic:
refine ext (nodup_cons.mp hl).2 fun j hj => ?_

Goal state after:
case snd
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
j : ι
hj : j ∈ is
⊢ TProd.elim v.2 hj = TProd.elim w.2 hj
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
a : IterateMulAct f
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
by ext; apply Nat.succ_mul

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (fun x_1 y ↦ ‖x‖ ≤ dist ((Infinite.natEmbedding 𝕜) x_1 • x) ((Infinite.natEmbedding 𝕜) y • x)) k n

Tactic:
simp only [dist_eq_norm, ← sub_smul, norm_smul]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ ‖x‖ ≤ ‖(Infinite.natEmbedding 𝕜) k - (Infinite.natEmbedding 𝕜) n‖ * ‖x‖
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: case h₁
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋯
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⋯
k : ι
⊢ μ (s k) ≤ M

Tactic:
exact le_iSup (μ ∘ s) k

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type ?u.14
f : ι → OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ ∑' (i : ι), (f i) (⋃ i, s i) ≤ ∑' (b : ι) (a : ℕ), (f b) (s a)

Tactic:
exact ENNReal.tsum_le_tsum fun i => measure_iUnion_le _

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:
sub_nonneg,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddRightMono α
n : ℕ
⊢ 1 / ↑n ≤ 1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬(↑x✝).abs = 0

Tactic:
abs_eq_zero_iff,

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬↑x✝ = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
g : β → ℝ≥0∞
⊢ ∑' (y : β), g y = ∑' (y : β), g (f (surjInv hf y))

Tactic:
by simp only [surjInv_eq hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x

Tactic:
let φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case inl
α : Type u_4
s : Set α
hfin : s.Finite
⊢ ∑' (x : ↑s), 1 = ↑s.encard

pp: case inr
α : Type u_4
s : Set α
hinf : s.Infinite
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Tactic:
· lift s to Finset α using hfin
    simp [tsum_fintype]

Goal state after:
case inr
α : Type u_4
s : Set α
hinf : s.Infinite
⊢ ∑' (x : ↑s), 1 = ↑s.encard
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h
⊢ ∀ i < ⊤, ∃ i', True ∧ Real.toEReal '' Ici i' ⊆ Ici i ∩ {⊤}ᶜ

Tactic:
simp only [EReal.image_coe_Ici, true_and]

Goal state after:
case h
⊢ ∀ i < ⊤, ∃ i', Ico ↑i' ⊤ ⊆ Ici i ∩ {⊤}ᶜ
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed[inst✝¹] (f ⁻¹' Iic y)

Tactic:
rw [lowerSemicontinuous_iff_isOpen_preimage]
  simp only [← isOpen_compl_iff, ← preimage_compl, compl_Iic]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅ ↔ ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩
  · suffices ∀ i ∈ I, IsClosed (s ↓∩ (fun i ↦ f i ⁻¹' Iic c) i) by
      simpa [Set.eq_empty_iff_forall_notMem] using
        ks.elim_finite_subfamily_isClosed_subtype _ this H
    exact fun i hi ↦ lowerSemicontinuous_restrict_iff.mpr (hfi i hi) |>.isClosed_preimage c
  · rw [Set.eq_empty_iff_forall_notMem]
    simp only [mem_inter_iff, mem_iInter, mem_preimage, mem_Iic, not_and, not_forall,
      exists_prop, not_le]
    grind

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

Goal state before:
pp: case e'_6
a : ℝ
⊢ a = a / 2 * (1 - 1 / 2)⁻¹

Tactic:
· norm_num

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

Goal state before:
pp: α : 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
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }

Tactic:
refine ⟨f ∘ Encodable.encode, fun i ↦ f0 _, ?_⟩

Goal state after:
α : 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, HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ UpperSemicontinuous f ↔ ∀ (y : γ), IsClosed[inst✝¹] (f ⁻¹' Ici y)

Tactic:
rw [upperSemicontinuous_iff_isOpen_preimage]
  simp only [← isOpen_compl_iff, ← preimage_compl, compl_Ici]

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

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
f : α ≃ α
Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs
A : Set α
⊢ (inducedOuterMeasure m P0 m0) (⇑f ⁻¹' A) = (inducedOuterMeasure m P0 m0) A

Tactic:
rw [inducedOuterMeasure_eq_iInf _ msU m_mono, inducedOuterMeasure_eq_iInf _ msU m_mono]; symm
    refine f.injective.preimage_surjective.iInf_congr (preimage f) fun s => ?_
    refine iInf_congr_Prop (Pm s) ?_; intro hs
    refine iInf_congr_Prop f.surjective.preimage_subset_preimage_iff ?_
    intro _; exact mm s hs

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

Goal state before:
pp: case mpr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = ∅

Tactic:
use ∅

Goal state after:
case h
α : Type u_1
s : Set α
⊢ (fun x ↦ x ∈ s) ⁻¹' ∅ = ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable fun x ↦ g (Exists.choose ⋯)

Tactic:
simpa only [rangeSplitting] using! hg.comp hf.measurable_rangeSplitting

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ⇑e)
⊢ Measurable f

Tactic:
have : Measurable (f ∘ (e.symm.trans e).toEquiv) := hfe.comp e.symm.measurable
      rwa [coe_toEquiv, symm_trans_self] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
⊢ (A : Set α) ×' MeasurableSet A ∧ F A = A

Tactic:
refine ⟨iInter X, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
⊢ MeasurableSet (iInter X)

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
⊢ F (iInter X) = iInter X