mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
ε : ℝ
ε0 : ε > 0
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2
n : ℕ
hn : n ≥ N
⊢ sSup (S n) < ε

Tactic:
refine lt_of_le_of_lt (csSup_le ⟨_, S0m _⟩ ?_) (half_lt_self ε0)

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
ε : ℝ
ε0 : ε > 0
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2
n : ℕ
hn : n ≥ N
⊢ ∀ b ∈ S n, b ≤ ε / 2
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
⊢ ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖ ↔ ‖x‖ ≤ ‖y‖

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by gcongr⟩

Goal state after:
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
h : ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖
⊢ ‖x‖ ≤ ‖y‖
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
⊢ map (algebraMap S R) p = ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S

Tactic:
by
  have h : map (algebraMap S R) p ≠ 0 := map_ne_bot_of_ne_bot hp
  rw [← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h]
  let hF : Fintype {v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} :=
    (finite_factors h).fintype
  rw [finprod_eq_finsetProd_of_mulSupport_subset
    (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset), ← Finset.prod_set_coe,
    ← Finset.prod_set_coe]
  · let _ : Fintype {v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p} := hF
    refine Fintype.prod_equiv (equivPrimesOver _ hp) _ _ fun ⟨v, _⟩ ↦ ?_
    have : v.asIdeal.LiesOver p := by rwa [Ideal.liesOver_iff_dvd_map v.2.ne_top]
    simp [maxPowDividing_eq_pow_multiset_count _ h, ramificationIdx_eq_factors_count p v h]
  · intro v hv
    simpa [maxPowDividing, Function.mem_mulSupport, IsPrime.ne_top _,
      Associates.count_ne_zero_iff_dvd h (irreducible v)] using hv

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
s : Set α
hs : x ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ x ∈ s ∩ ball x 1 ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ ball x 1)

Tactic:
by aesop (add safe apply IsOpen.inter)

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedCommGroup α
n : ℤ
a : α
⊢ ‖a ^ n‖ ≤ ‖n‖ * ‖a‖

Tactic:
by
  rcases n.eq_nat_or_neg with ⟨n, rfl | rfl⟩ <;> simpa [Int.norm_natCast] using norm_pow_le_mul_norm

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) cofinite f
⊢ BddAbove (range f)

Tactic:
by
  rcases hf with ⟨b, hb⟩
  have : Nonempty β := ⟨b⟩
  rw [← image_univ, ← union_compl_self { x | f x ≤ b }, image_union, bddAbove_union]
  exact ⟨⟨b, forall_mem_image.2 fun x => id⟩, (hb.image f).bddAbove⟩

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop f
⊢ BddAbove (range f)

Tactic:
by
  rw [← Nat.cofinite_eq_atTop] at hf
  exact hf.bddAbove_range_of_cofinite

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (s.sup' hs fun i ↦ F i a) c
a : α
h : ∀ b ∈ s, F b a ≤ c
⊢ F i a ≤ c

Tactic:
exact h i i_s

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

Goal state before:
pp: x : EReal
h_top : x ≠ ⊤
h_bot : x ≠ ⊥
⊢ x - x = 0

Tactic:
by
  cases x <;> simp_all [← coe_sub]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∀ (x : α), x ≤ f.limsSup
this : OrderTop α := { top := f.limsSup, le_top := htop }
⊢ ClusterPt f.limsSup f

Tactic:
exact nhds_top_basis.clusterPt_iff_frequently |>.mpr fun a => frequently_lt_of_lt_limsSup hc

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

Goal state before:
pp: case top
y : ℝ≥0
h_le : ↑y ≤ ∞
⊢ ↑(∞ - ↑y) = ↑∞ - ↑↑y

Tactic:
simp [coe_nnreal_eq_coe_real]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
z : β
z_x : z < x
hz : ∀ (z_1 : β), z_1 ≤ z ∨ x ≤ z_1
⊢ ∃ᶠ (i : α) in f, x ≤ u i

Tactic:
exact (h z z_x).mono <| fun w hw ↦ (or_iff_right (not_le_of_gt hw)).1 (hz (u w))

Goal state after:
Module: Mathlib.Logic.Encodable.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C (⋃ b ∈ none, f b)

Tactic:
by
    simp only [Option.mem_def, iUnion_of_empty, iUnion_empty, reduceCtorEq]
    apply H0

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

Goal state before:
pp: case neg
α : Type u_3
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h✝ : Nonempty α
h : ¬IsDirectedOrder α
⊢ Tendsto Finset.Iic atTop atTop

Tactic:
· obtain h := Filter.atTop_neBot_iff.not.mpr (fun h' ↦ h h'.2)
    simp [not_ne_iff.mp <| Filter.neBot_iff.not.mp h]

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

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

Tactic:
coe_mul_bot_of_neg (neg_neg_of_pos h)

Goal state after:
case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ ⊤ = ⊤
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : 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)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
j : Subtype p
Hj : j ∈ m
⊢ liminfReparam f s p j ∈ m

pp: case neg
α : 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)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
j : Subtype p
Hj : j ∉ m
⊢ liminfReparam f s p j ∈ m

Tactic:
· simpa only [m, liminfReparam, if_pos Hj] using Hj

Goal state after:
case neg
α : 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)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
j : Subtype p
Hj : j ∉ m
⊢ liminfReparam f s p j ∈ m
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case succ
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ ↑n * x + x = (↑n + 1) * x

Tactic:
convert! (EReal.right_distrib_of_nonneg _ _).symm

Goal state after:
case e'_2.e'_6
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ x = 1 * x

case succ.convert_4
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ 0 ≤ ↑n

case succ.convert_5
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ 0 ≤ 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
⊢ HasProd f (∏'[L] (b : β), f b) L

Tactic:
rw [tprod_def, dif_pos ha]
  split_ifs with h h'
  · convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
    · simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
      simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
      rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
      · exact Finset.prod_congr rfl (by simp_all)
      · simp
    · grind [Set.Finite.mem_toFinset, mem_mulSupport]
    · exact h.1
  · exact h'
  · exact ha.choose_spec

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
hf : ¬(mulSupport f).Finite
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
rwa [tprod_bot hL, finprod_of_infinite_mulSupport hf]

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

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

Tactic:
rw [prod_union, prod_image Nat.cast_injective.injOn, prod_image this.injOn,
      prod_mul_distrib]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : i ∈ ⋃ d, s d
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
⊢ ∏' (d : γ), (s d).mulIndicator f i = f i

Tactic:
by
  obtain ⟨j, hj⟩ := Set.mem_iUnion.mp hi
  rw [← tprod_subtype_eq_of_mulSupport_subset (s := {j})]
  · aesop
  · exact Set.mulSupport_subset_subsingleton_of_disjoint_on_mulSupport f hs i j hj

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:
by
  cases isEmpty_or_nonempty ι
  · simp [hn]
  · exact iSup_pow hf _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
⊢ comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (𝓤 α)

Tactic:
grw [← hf.comap_uniformity_le]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
⊢ comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (comap (Prod.map f f) (𝓤 β))
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
m : α → ℝ≥0∞
f : Filter α
h : ∀ (n : ℕ), ∀ᶠ (a : α) in f, ↑n < m a
x : ℝ≥0
n : ℕ
hn : x < ↑n
x✝ : α
⊢ ↑x < ↑n

Tactic:
by rwa [← ENNReal.coe_natCast, coe_lt_coe]

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 : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.map pkg' f (pkg.coe a) = g (pkg.coe a)

Tactic:
change pkg.extend (ι' ∘ f) _ = _

Goal state after:
α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (pkg'.coe ∘ f) (pkg.coe a) = g (pkg.coe a)
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Tactic:
by
  let f := fun s : SetRel α α =>
        { p : CauchyFilter α × CauchyFilter α | s ∈ (p.2.val ×ˢ p.1.val : Filter (α × α)) }
  have h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f := by
    delta gen
    simp [f, map_lift'_eq, monotone_ofPred, Filter.monotone_mem, Function.comp_def,
      image_swap_eq_preimage_swap]
  have h₂ : (𝓤 α).lift' f ≤ (𝓤 α).lift' gen :=
    uniformity_lift_le_swap
      (monotone_principal.comp
        (monotone_ofPred fun p => @Filter.monotone_mem _ (p.2.val ×ˢ p.1.val)))
      (by
        have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val
        simp only [Function.comp, h, mem_map, f]
        exact le_rfl)
  exact h₁.trans_le h₂

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

Goal state before:
pp: a : ℝ≥0∞
a_ne_top : a ≠ ∞
⊢ Continuous (uncurry Sub.sub ∘ fun x ↦ (a, x))

Tactic:
refine continuousOn_sub.comp_continuous (.prodMk_right a) fun x => ?_

Goal state after:
a : ℝ≥0∞
a_ne_top : a ≠ ∞
x : ℝ≥0∞
⊢ (a, x) ∈ {p | p ≠ (∞, ∞)}
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
⊢ ∃ a,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
      ‖(j (a 0))⁻¹ * b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

Tactic:
obtain ⟨v, sum_v, v_in, hv₀, hv_pos⟩ := controlled_prod_of_mem_closure hb b_pos

Goal state after:
E : Type u_4
F : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
v_in : ∀ (n : ℕ), v n ∈ j.range
hv₀ : ‖(v 0)⁻¹ * b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
⊢ ∃ a,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
      ‖(j (a 0))⁻¹ * b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f y + C * edist x y ≤ f y + ε

Tactic:
grw [← hδ.le]

Goal state after:
case refine_1
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f y + C * edist x y ≤ f y + C * ↑δ
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f x + C * edist y x ≤ f x + ε

Tactic:
grw [← hδ.le]

Goal state after:
case refine_2
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f x + C * edist y x ≤ f x + C * ↑δ
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f g : α → ℝ
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (max Kf Kg) fun x ↦ max (f x) (g x)

Tactic:
by
  simpa only [(· ∘ ·), one_mul] using! lipschitzWith_max.comp (hf.prodMk hg)

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
⊢ liminf (fun i ↦ (u i).toReal) f = (liminf u f).toReal

Tactic:
liminf_congr aux,

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
⊢ liminf (fun a ↦ b.truncateToReal (u a)) f = (liminf u f).toReal
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤
  · exact ratio_of_trivial hf.toDilation h
  · obtain ⟨x, y, h₁, h₂⟩ := h
    exact ratio_unique h₁ h₂ (by simp [hf x y]) |>.symm

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a‖ + ‖a * (1 - b)‖ ≤ ‖c - a‖ + ‖a‖ * ‖1 - b‖

Tactic:
gcongr; exact norm_mul_le ..

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

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π ↑i_1
j : ι
hj : j = i
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j

Tactic:
cases hj

Goal state after:
case pos.refl
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π ↑i_1
⊢ updateFinset x {i} y i = update x i (y ⟨i, ⋯⟩) i
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

Tactic:
cases hj

Goal state after:
case pos.refl
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
⊢ update x i y i = updateFinset x {i} (uniqueElim y) i
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ r⁻¹ * (ε * r ^ 2) * r⁻¹ = ε

Tactic:
by field_simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rw [map_def]; by_cases h : b ∈ s <;> simp [h]

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 𝕜'
hc : c ∈ cobounded 𝕜'
⊢ ⇑(algebraMap 𝕜 𝕜') ⁻¹' c ∈ cobounded 𝕜

Tactic:
rw [← isCobounded_def, ← isBounded_compl_iff, isBounded_iff_forall_norm_le] at hc ⊢

Goal state after:
𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
hc : ∃ C, ∀ x ∈ cᶜ, ‖x‖ ≤ C
⊢ ∃ C, ∀ x ∈ (⇑(algebraMap 𝕜 𝕜') ⁻¹' c)ᶜ, ‖x‖ ≤ C
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst✝⁵ : NormedField 𝕜✝
inst✝⁴ : SeminormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜✝ 𝕜'
𝕜 : Type ?u.15
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : NormedAlgebra ℝ 𝕜
q : ℚ
x : 𝕜
⊢ ‖q • x‖ ≤ ‖q‖ * ‖x‖

Tactic:
← smul_one_smul ℝ q x,

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst✝⁵ : NormedField 𝕜✝
inst✝⁴ : SeminormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜✝ 𝕜'
𝕜 : Type ?u.15
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : NormedAlgebra ℝ 𝕜
q : ℚ
x : 𝕜
⊢ ‖(q • 1) • x‖ ≤ ‖q‖ * ‖x‖
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₂
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ ⋂ y ∈ (measurableAtom x)ᶜ, s y ⊆ measurableAtom x

Tactic:
· apply compl_subset_compl.1
      intro z hz
      simp only [compl_iInter, mem_iUnion, mem_compl_iff, exists_prop]
      exact ⟨z, hz, (hs z hz).2.2⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ mβ ≤ MeasurableSpace.map Prod.fst (MeasurableSpace.map f m)

Tactic:
MeasurableSpace.map_comp

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ mγ ≤ MeasurableSpace.map Prod.snd (MeasurableSpace.map f m)

Tactic:
MeasurableSpace.map_comp

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ f ⁻¹' s = ⋃ y, ((fun x ↦ f (x, y)) ⁻¹' s) ×ˢ measurableAtom y

Tactic:
ext1 ⟨x, y⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ (x, y) ∈ f ⁻¹' s ↔ (x, y) ∈ ⋃ y, ((fun x ↦ f (x, y)) ⁻¹' s) ×ˢ measurableAtom y
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
H : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop
n : ℕ
hn : c < ∑ i ∈ range n, f i
⊢ False

Tactic:
exact lt_irrefl _ (hn.trans_le (h n))

Goal state after: