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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
⊢ g.symm.symm (g.symm (limsup (fun x ↦ g (u x)) f)) ≤ g (limsup u f)

Tactic:
g.symm_symm

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
⊢ g (g.symm (limsup (fun x ↦ g (u x)) f)) ≤ g (limsup u f)
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Fintype β
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ HasProd f (∏ b, f b) L

Tactic:
by
  simpa using hasProd_fintype_support f L

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

Goal state before:
pp: α : 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' : β
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

Tactic:
by_cases h : b' = b

Goal state after:
case pos
α : 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'

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'
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
this : Multipliable (f ∘ Subtype.val)
⊢ Multipliable (f ∘ Subtype.val)

Tactic:
rwa [hs.coe_toFinset] at this

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

Goal state before:
pp: κ : Type u_4
γ : Type u_5
inst✝⁶ : CommGroup γ
inst✝⁵ : PartialOrder γ
inst✝⁴ : IsOrderedMonoid γ
inst✝³ : UniformSpace γ
inst✝² : IsUniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∀ c ∉ Set.range fun a ↦ ↑a, 1 ≤ f c

Tactic:
simp only [Subtype.range_coe_subtype, Set.ofPred_mem_eq, h, implies_true]

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

Goal state before:
pp: κ : Type u_4
γ : Type u_5
inst✝⁶ : CommGroup γ
inst✝⁵ : PartialOrder γ
inst✝⁴ : IsOrderedMonoid γ
inst✝³ : UniformSpace γ
inst✝² : IsUniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∏' (b : ↑β), f ↑b ≤ ∏' (a : κ), f a

Tactic:
apply Multipliable.tprod_le_tprod_of_inj _
    (Subtype.coe_injective)
    (by simp only [Subtype.range_coe_subtype, Set.ofPred_mem_eq, h, implies_true])
    (by simp only [le_refl, implies_true])
    (by apply hf.subtype)

Goal state after:
κ : Type u_4
γ : Type u_5
inst✝⁶ : CommGroup γ
inst✝⁵ : PartialOrder γ
inst✝⁴ : IsOrderedMonoid γ
inst✝³ : UniformSpace γ
inst✝² : IsUniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ Multipliable fun a ↦ f a
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
hf : f 0 = 1
n : ℕ
hn : n ∈ mulSupport f
⊢ n ∈ Set.range PNat.val

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | h

Goal state after:
case inl
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
hf : f 0 = 1
hn : 0 ∈ mulSupport f
⊢ 0 ∈ Set.range PNat.val

case inr
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
hf : f 0 = 1
n : ℕ
hn : n ∈ mulSupport f
h : n > 0
⊢ n ∈ Set.range PNat.val
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
by
  by_cases hn : n = 0
  · simp [hn]
  · exact iSup_pow_of_ne_zero hn _

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

Goal state before:
pp: ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
by
  by_cases hn : n = 0
  · simp [hn]
  · exact iSup_pow_of_ne_zero hn _

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

Goal state before:
pp: ⊢ ⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Iio a)

Tactic:
simp [pos_iff_ne_zero, Iio]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ Tendsto (fun t ↦ ∏ a ∈ bs, ∏ s ∈ t.preimage (Sigma.mk a) ⋯, f ⟨a, s⟩) atTop (𝓝 (∏ b ∈ bs, g b))

Tactic:
refine tendsto_finsetProd _ fun b _ ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
b : β
x✝ : b ∈ bs
⊢ Tendsto (fun t ↦ ∏ s ∈ t.preimage (Sigma.mk b) ⋯, f ⟨b, s⟩) atTop (𝓝 (g b))
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst✝¹.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
⊢ Tendsto (fun t ↦ ∏ a ∈ t0, ∏ s ∈ t.preimage (Sigma.mk a) ⋯, f ⟨a, s⟩) atTop (𝓝 (∏ b ∈ t0, g b))

Tactic:
refine tendsto_finsetProd _ fun b _ ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst✝¹.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
b : β
x✝ : b ∈ t0
⊢ Tendsto (fun t ↦ ∏ s ∈ t.preimage (Sigma.mk b) ⋯, f ⟨b, s⟩) atTop (𝓝 (g b))
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_1
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n ≤ ε

Tactic:
obtain ⟨n, hn⟩ := h ε hε

Goal state after:
case refine_1
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : ∀ n_1 ≥ n, f n_1 ≤ ε
⊢ ∃ n, f n ≤ ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_2
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
obtain ⟨n, hn⟩ := h ε hε

Goal state after:
case refine_2
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : β
hn : f n ≤ ε
⊢ ∃ N, ∀ n ≥ N, f n ≤ ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case mp
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n < ε

Tactic:
obtain ⟨n, hn⟩ := h (min 1 (ε / 2))
      (lt_min_iff.mpr ⟨zero_lt_one, (ENNReal.div_pos_iff.mpr ⟨hε.ne', by finiteness⟩)⟩)

Goal state after:
case mp
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
⊢ ∃ n, f n < ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case mpr
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n ≤ ε

Tactic:
obtain ⟨n, hn⟩ := h ε hε

Goal state after:
case mpr
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n < ε
⊢ ∃ n, f n ≤ ε
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id

Tactic:
have uc := pkg.uniformContinuous_compare pkg'

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

Goal state before:
pp: α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ Tendsto (fun a ↦ ma a / mb a) f (𝓝 (a / b))

Tactic:
apply Tendsto.mul hma _ (tendsto_inv_iff.2 hmb) _ <;> simp [ha, hb]

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

Goal state before:
pp: case refine_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a : Completion α
⊢ Completion.extension (lift' coe') (Completion.map SeparationQuotient.mk a) = a

Tactic:
· refine induction_on a
      (isClosed_eq (continuous_extension.comp continuous_map) continuous_id) fun a ↦ ?_
    rw [map_coe uniformContinuous_mk, extension_coe (uniformContinuous_lift' _),
      lift'_mk (uniformContinuous_coe _)]

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

Goal state before:
pp: t : ℝ≥0∞
t_ne_top : t ≠ ∞
x : ℝ≥0∞
⊢ t.truncateToReal x ≤ t.toReal

Tactic:
rw [truncateToReal]
  gcongr
  exact min_le_left t x

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ x ∈ s,
        ∀ y ∈ s,
          dist x y ≤ δ → dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) x) (Function.uncurry (fun x1 x2 ↦ x1 • x2) y) ≤ ε

Tactic:
intro ε

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
⊢ ε > 0 →
    ∃ δ > 0,
      ∀ x ∈ s,
        ∀ y ∈ s,
          dist x y ≤ δ → dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) x) (Function.uncurry (fun x1 x2 ↦ x1 • x2) y) ≤ ε
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ dist (f x) (f y) = ↑(ratio f) * dist x y

Tactic:
simp only [dist_nndist, nndist_eq, NNReal.coe_mul]

Goal state after:
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 : ∀ ε > 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)‖ < ε

Tactic:
intro ε

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.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: ⊢ LipschitzWith 2 (toReal ∘ fun p ↦ p.1 - p.2)

Tactic:
have : Isometry (Prod.map ((↑) : ℝ≥0 → ℝ) ((↑) : ℝ≥0 → ℝ)) :=
    NNReal.isometry_coe.prodMap NNReal.isometry_coe

Goal state after:
this : Isometry (Prod.map toReal toReal)
⊢ LipschitzWith 2 (toReal ∘ fun p ↦ p.1 - p.2)
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε

Tactic:
intro ε

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
⊢ ε > 0 → ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ y, ‖y‖ < 1 ∧ y ≠ 0
⊢ ∀ (a : 𝕜), ‖a‖ < 1 ∧ a ≠ 0 → a ≠ 0 ∧ ‖a‖ ≠ 1

Tactic:
simp +contextual [ne_of_lt]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x ↦ b)
a : α
⊢ a ∈ s ↔ a ∈ (s.indicator fun x ↦ b) ⁻¹' {0}ᶜ

Tactic:
simp [NeZero.ne b]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet s

Tactic:
rw [← biUnion_of_singleton s]
  exact .biUnion hs fun b _ => .singleton b

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

Goal state before:
pp: 𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
s : ℝ
hs : ∀ x ∈ cᶜ, ‖x‖ ≤ s
x : 𝕜
hx : x ∈ (⇑(algebraMap 𝕜 𝕜') ⁻¹' c)ᶜ
⊢ ‖x‖ ≤ s

Tactic:
by simpa using hs (algebraMap 𝕜 𝕜' x) hx

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

Goal state before:
pp: G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ‖(↑n)⁻¹‖ * ‖f (n • x)‖ < ‖(↑n)⁻¹‖ * C

Tactic:
gcongr
      · simpa [pos_iff_ne_zero]
      · refine hC _ <| norm_nsmul_le.trans_lt ?_
        simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
t : β
ht : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1

Tactic:
exact ⟨sub_nonneg.2 ht.2, (sub_le_self_iff _).2 ht.1⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
ht' : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩
f : ↑(⋃ i, t i) → β := iUnionLift t g' ht' (⋃ i, t i) ⋯
hfm : Measurable f
i : ι
x : α
hx : x ∈ t i
⊢ (fun x ↦ if hx : x ∈ ⋃ i, t i then f ⟨x, hx⟩ else g default x) x = g i x

Tactic:
simp only [dif_pos (mem_iUnion.2 ⟨i, hx⟩)]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
ht' : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩
f : ↑(⋃ i, t i) → β := iUnionLift t g' ht' (⋃ i, t i) ⋯
hfm : Measurable f
i : ι
x : α
hx : x ∈ t i
⊢ f ⟨x, ⋯⟩ = g i x
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
h : Continuous[inst✝², inst✝¹] ⇑(algebraMap R A)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ p.1 • p.2

Tactic:
simp only [Algebra.smul_def]

Goal state after:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
h : Continuous[inst✝², inst✝¹] ⇑(algebraMap R A)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ (algebraMap R A) p.1 * p.2
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_zero
⊢ (⊤ * 0).abs = ⊤.abs * EReal.abs 0

Tactic:
| top_zero =>

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

Goal state before:
pp: case top_zero
⊢ sign (⊤ * 0) = sign ⊤ * sign 0

Tactic:
| top_zero =>

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

Goal state before:
pp: x : ℝ
⊢ ↑(sign x) * ↑|x| = ↑x

Tactic:
← coe_coe_sign,

Goal state after:
x : ℝ
⊢ ↑↑(sign x) * ↑|x| = ↑x
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
by
  have f_ne_top : ∀ n, f n ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top hf
  have h_f_coe : f = fun n => ((f n).toNNReal : ENNReal) :=
    funext fun n => (coe_toNNReal (f_ne_top n)).symm
  rw [h_f_coe, ← @coe_zero, tendsto_coe]
  exact NNReal.tendsto_cofinite_zero_of_summable (summable_toNNReal_of_tsum_ne_top hf)

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

Goal state before:
pp: case top_zero
⊢ (⊤ * 0)⁻¹ = ⊤⁻¹ * 0⁻¹

Tactic:
| top_zero =>

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf : Summable f
⊢ ∑' (i : α), ↑(f i).toNNReal ≠ ∞

Tactic:
ENNReal.tsum_coe_ne_top_iff_summable

Goal state after:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun i ↦ (f i).toNNReal
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
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x

Tactic:
refine ⟨a, ha, fun x hx ↦ le_of_not_gt fun hxa ↦ ?_⟩

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)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
⊢ False
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : ∑' (i : ℕ), ↑(d i) ≠ ∞
⊢ CauchySeq f

Tactic:
ENNReal.tsum_coe_ne_top_iff_summable

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable d
⊢ CauchySeq f
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ ∀ (ε : ℝ≥0), 0 < ε → ∑' (i : ℕ), μ (s i) < ∞ → μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε

Tactic:
intro ε

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
⊢ 0 < ε → ∑' (i : ℕ), μ (s i) < ∞ → μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ((comap f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f '' s)

Tactic:
rw [comap_apply]
    apply ofFunction_le

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
⊢ (c • fun s ↦ ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs) <;> simp [*]

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

Goal state before:
pp: k : ℕ
hn : 0 < k.succ
⊢ (∏ i ∈ Finset.range k.succ, ↑(i + 1)) * (∏ _k ∈ Finset.range k.succ, (↑k + 1))⁻¹ ≤ (↑k + 1)⁻¹

Tactic:
← Finset.prod_inv_distrib,

Goal state after:
k : ℕ
hn : 0 < k.succ
⊢ (∏ i ∈ Finset.range k.succ, ↑(i + 1)) * ∏ x ∈ Finset.range k.succ, (↑k + 1)⁻¹ ≤ (↑k + 1)⁻¹
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inter
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s✝ t✝ : Set α
h_s✝ : generatePiSystem S s✝
h_t✝ : generatePiSystem S t✝
h_nonempty : (s✝ ∩ t✝).Nonempty
h_s : s✝ ∈ S
h_u : t✝ ∈ S
⊢ s✝ ∩ t✝ ∈ S

Tactic:
| inter _ _ h_nonempty h_s h_u =>

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inter
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s✝ t✝ : Set α
h_s✝ : generatePiSystem S s✝
h_t✝ : generatePiSystem S t✝
h_nonempty : (s✝ ∩ t✝).Nonempty
h_s : s✝ ∈ generatePiSystem T
h_u : t✝ ∈ generatePiSystem T
⊢ s✝ ∩ t✝ ∈ generatePiSystem T

Tactic:
| inter _ _ h_nonempty h_s h_u =>

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

Goal state before:
pp: α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
⊢ m s h ≤ extend m s

Tactic:
simp only [extend, le_iInf_iff]
  intro
  rfl

Goal state after: