mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι → α
H : ∃ j, s ↑j = ∅
⊢ liminf f v =
    if ∃ j, s ↑j = ∅ then sSup univ
    else if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i

Tactic:
if_pos H

Goal state after:
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 : ι → α
H : ∃ j, s ↑j = ∅
⊢ liminf f v = sSup univ
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 : α
g : γ → α
e : ↑(mulSupport f) ≃ ↑(mulSupport g)
he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x
this : (g ∘ Subtype.val) ∘ ⇑e = f ∘ Subtype.val
⊢ HasProd f a ↔ HasProd g a

Tactic:
rw [← hasProd_subtype_mulSupport, ← this, e.hasProd_iff, hasProd_subtype_mulSupport]

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 : β → α
L : SummationFilter β
inst✝⁵ : CommMonoid γ
inst✝⁴ : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst✝³ : FunLike G α γ
inst✝² : MonoidHomClass G α γ
inst✝¹ : FunLike G' γ α
inst✝ : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous[inst✝⁶, inst✝⁴] ⇑g
hg' : Continuous[inst✝⁴, inst✝⁶] ⇑g'
hinv : LeftInverse ⇑g' ⇑g
h : Multipliable (⇑g ∘ f) L
⊢ Multipliable f L

Tactic:
by
    have := h.map _ hg'
    rwa [← Function.comp_assoc, hinv.id] at this

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

Goal state before:
pp: case pos
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
⊢ g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)

Tactic:
by_cases h : Multipliable f L

Goal state after:
case pos
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : Multipliable f L
⊢ g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)

case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
⊢ g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)

Tactic:
by_cases hL : L.NeBot
  · by_cases h : Multipliable f L
    · exact h.map_tprod g hge.continuous
    · rw [tprod_eq_one_of_not_multipliable h, tprod_eq_one_of_not_multipliable, map_one]
      contrapose h
      -- need to show `g ∘ f` multipliable implies `g` multipliable
      simp only [Multipliable, HasProd] at h ⊢
      obtain ⟨b, hb⟩ := h
      obtain ⟨a, ha⟩ : b ∈ Set.range g :=
        hge.isClosed_range.mem_of_tendsto hb (.of_forall <| by simp [← _root_.map_prod])
      use a
      simp [hge.tendsto_nhds_iff, Function.comp_def, ha, hb]
  · simpa [tprod_bot hL] using
      (MonoidHomClass.toMonoidHom g).map_finprod_of_injective hge.injective _

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁵ : CommMonoidWithZero α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : ZeroLEOneClass α
inst✝¹ : PosMulMono α
inst✝ : ClosedIciTopology α
f : ι → α
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∏'[L] (x : ι), f x

Tactic:
by_cases h : Multipliable f L

Goal state after:
case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁵ : CommMonoidWithZero α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : ZeroLEOneClass α
inst✝¹ : PosMulMono α
inst✝ : ClosedIciTopology α
f : ι → α
hf : ∀ (i : ι), 0 ≤ f i
h : Multipliable f L
⊢ 0 ≤ ∏'[L] (x : ι), f x

case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁵ : CommMonoidWithZero α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : ZeroLEOneClass α
inst✝¹ : PosMulMono α
inst✝ : ClosedIciTopology α
f : ι → α
hf : ∀ (i : ι), 0 ≤ f i
h : ¬Multipliable f L
⊢ 0 ≤ ∏'[L] (x : ι), f x
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : ι → α
x : α
hfx : HasProd f x
⊢ HasProd (fun x ↦ |f x|) |x|

Tactic:
by
  simpa only [HasProd, ← abs_prod] using hfx.abs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)
⊢ HasProd (fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a) (∏ i ∈ s, a i)

Tactic:
exact hasProd_prod hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
s : Finset β
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ ∏ x ∈ s, f x = ∏'[L] (x : β), (↑s).mulIndicator f x

Tactic:
by
  rw [tprod_eq_prod' (Set.mulSupport_mulIndicator_subset),
      Finset.prod_mulIndicator_subset _ Finset.Subset.rfl]

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
f : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
hf : Summable f L
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
f : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
hf : ¬Summable f L
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

Tactic:
· rw [SemiconjBy, ← hf.tsum_mul_right a, ← hf.tsum_mul_left b, tsum_congr h]

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
f : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
hf : ¬Summable f L
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ (if h : Multipliable (f ∘ g) then
      if (unconditional γ).HasSupport ∧ (mulSupport (f ∘ g)).Finite then finprod (Set.univ.mulIndicator (f ∘ g))
      else if HasProd (f ∘ g) 1 then 1 else Exists.choose ⋯
    else 1) =
    if h : Multipliable fun b ↦ f b then
      if True ∧ (mulSupport fun b ↦ f b).Finite then finprod (Set.univ.mulIndicator fun b ↦ f b)
      else if HasProd (fun b ↦ f b) 1 then 1 else Exists.choose ⋯
    else 1

Tactic:
show (unconditional γ).HasSupport by infer_instance,

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ (if h : Multipliable (f ∘ g) then
      if True ∧ (mulSupport (f ∘ g)).Finite then finprod (Set.univ.mulIndicator (f ∘ g))
      else if HasProd (f ∘ g) 1 then 1 else Exists.choose ⋯
    else 1) =
    if h : Multipliable fun b ↦ f b then
      if True ∧ (mulSupport fun b ↦ f b).Finite then finprod (Set.univ.mulIndicator fun b ↦ f b)
      else if HasProd (fun b ↦ f b) 1 then 1 else Exists.choose ⋯
    else 1
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 β
hs : Pairwise (Disjoint on s)
f : β → α
i : β
⊢ (⋃ d, s d).mulIndicator f i = ∏' (d : γ), (s d).mulIndicator f i

Tactic:
exact mulIndicator_iUnion_of_pairwise_disjoint_on_mulSupport s f (pairwise_disjoint_mono hs
    <| fun _ _ hi ↦ hi.1) i

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
ys : ℕ → Y
xs : ℕ → X
xs_in_K : ∀ (n : ℕ), xs n ∈ K
fxs_eq_ys : ∀ (n : ℕ), f (xs n) = ys n
a : X
a_in_K : a ∈ K
phi : ℕ → ℕ
phi_mono : StrictMono phi
xs_phi_lim : Tendsto (xs ∘ phi) atTop (𝓝 a)
⊢ ∃ a ∈ f '' K, ∃ φ, StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)

Tactic:
refine ⟨f a, mem_image_of_mem f a_in_K, phi, phi_mono, ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
ys : ℕ → Y
xs : ℕ → X
xs_in_K : ∀ (n : ℕ), xs n ∈ K
fxs_eq_ys : ∀ (n : ℕ), f (xs n) = ys n
a : X
a_in_K : a ∈ K
phi : ℕ → ℕ
phi_mono : StrictMono phi
xs_phi_lim : Tendsto (xs ∘ phi) atTop (𝓝 a)
⊢ Tendsto (ys ∘ phi) atTop (𝓝 (f a))
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
L : Tendsto (fun t ↦ ∏ p ∈ t with p.fst ∈ t0, f p) atTop (𝓝 (∏ b ∈ t0, g b))
t : Finset ((b : β) × γ b)
tv : ∏ p ∈ t with p.fst ∈ t0, f p ∈ v
st : s ⊆ t
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
refine ⟨{p ∈ t | p.1 ∈ t0}, fun x hx ↦ ?_, vu tv⟩

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
L : Tendsto (fun t ↦ ∏ p ∈ t with p.fst ∈ t0, f p) atTop (𝓝 (∏ b ∈ t0, g b))
t : Finset ((b : β) × γ b)
tv : ∏ p ∈ t with p.fst ∈ t0, f p ∈ v
st : s ⊆ t
x : (b : β) × γ b
hx : x ∈ s
⊢ x ∈ {p ∈ t | p.fst ∈ t0}
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:
intro a
    change pkg.extend (ι' ∘ f) _ = _
    simp_rw [Function.comp_def, h, ← comp_apply (f := g)]
    rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]

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

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Filter α
hf : Cauchy f
f' : CauchyFilter α := ⟨f, hf⟩
this : map pureCauchy f ≤ (𝓤 (CauchyFilter α)).lift' (preimage (Prod.mk f'))
⊢ map pureCauchy f ≤ 𝓝 f'

Tactic:
simpa [nhds_eq_uniformity]

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

Goal state before:
pp: case neg
a : ℝ≥0∞
a_infty : ¬a = ∞
x : ℝ≥0∞
⊢ (x, a) ∈ {p | p ≠ (∞, ∞)}

Tactic:
simp only [a_infty, Ne, mem_ofPred_eq, Prod.mk_inj, and_false, not_false_iff]

Goal state after:
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
v : ℕ → F
sum_v : Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
hv₀ : ‖(v 0)⁻¹ * b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
g : ℕ → E
hg : ∀ (n : ℕ), j (g n) = v n
⊢ ‖(j (g 0))⁻¹ * b‖ < f 0

Tactic:
simpa [hg 0] using hv₀

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
⊢ (∃ b, (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)) →
    ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε

Tactic:
rintro ⟨b, ⟨b_bound, b_lim⟩⟩ ε εpos
    have : ∀ᶠ n in atTop, b n < ε := b_lim.eventually (gt_mem_nhds εpos)
    rcases this.exists with ⟨N, hN⟩
    refine ⟨N, fun m hm n hn => ?_⟩
    calc edist (s m) (s n) ≤ b N := b_bound m n N hm hn
    _ < ε := hN

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

Goal state before:
pp: 𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ ≤ 1

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
⊢ ‖0‖ ≤ 1

case inr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
⊢ ‖x‖ ≤ 1
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ edist (f x) (f y) = ↑1 * edist x y

Tactic:
rcases DilationClass.edist_eq' f with ⟨r, hne, hr⟩

Goal state after:
case pos
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
r : ℝ≥0
hne : r ≠ 0
hr : ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y
⊢ edist (f x) (f y) = ↑1 * edist x y
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: case inl
α : 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
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : A ≤ 0
⊢ A * ‖f i‖ * ‖g i‖ < ε

pp: case inr
α : 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
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ A * ‖f i‖ * ‖g i‖ < ε

Tactic:
· exact (mul_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonpos_of_nonneg hA <| norm_nonneg' _) <|
      norm_nonneg' _).trans_lt ε₀

Goal state after:
case inr
α : 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
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ A * ‖f i‖ * ‖g i‖ < ε
Module: Mathlib.Algebra.Order.AddTorsor

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ ¬b • d ≤ a • d

Tactic:
by_contra hbad

Goal state after:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
⊢ False
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α✝ : Type u_2
β : Type u_3
ι✝ : Type u_4
ι : Type u_5
α : ι → Type u_6
inst✝⁴ : Nonempty ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedAddCommGroup (α i)
inst✝¹ : (i : ι) → One (α i)
inst✝ : ∀ (i : ι), NormOneClass (α i)
⊢ ‖1‖ = 1

Tactic:
simpa [Pi.norm_def] using Finset.sup_const Finset.univ_nonempty 1

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

Goal state before:
pp: x : ℝ≥0
⊢ |↑x| = ↑x

Tactic:
x.abs_eq

Goal state after:
x : ℝ≥0
⊢ ↑x = ↑x
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : ↥s) → π ↑i
⊢ s.restrict (updateFinset x s y) = y

Tactic:
rw [restrict_updateFinset_of_subset subset_rfl]

Goal state after:
ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : ↥s) → π ↑i
⊢ restrict₂ ⋯ y = y
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
i : Bool
⊢ MeasurableSet (bif i then s₁ else s₂)

Tactic:
cases i

Goal state after:
case false
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif false then s₁ else s₂)

case true
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif true then s₁ else s₂)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s

Tactic:
measurableSet_iSup

Goal state after:
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ GenerateMeasurable {s | ∃ i, MeasurableSet s} s ↔ MeasurableSet s
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: α : Type u_6
inst✝¹ : SeminormedRing α
inst✝ : NormSMulClass ℤ α
n : ℤ
⊢ ‖↑n‖ = ↑|n| * ‖1‖

Tactic:
by
  rw [← zsmul_one, norm_smul, Int.norm_eq_abs, Int.cast_abs]

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 ∘ f) m

Tactic:
exact hf₁

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

Goal state before:
pp: α : Type u_1
s t : Set α
m : OuterMeasure α
⊢ ((restrict s) m) t = m (t ∩ s)

Tactic:
simp [restrict, inter_comm t]

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

Goal state before:
pp: case nil
δ : Type u_4
X : δ → Type u_6
inst✝ : (i : δ) → MeasurableSpace (X i)
s : (i : δ) → Set (X i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod [] s)

Tactic:
exact MeasurableSet.univ

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsSemitopologicalSemiring A
inst✝ : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(map (↑f) s).topologicalClosure = ↑⊤

Tactic:
simp only [Subalgebra.topologicalClosure_coe, coe_top, ← dense_iff_closure_eq,
    Subalgebra.coe_map] at hs ⊢

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsSemitopologicalSemiring A
inst✝ : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : Dense ↑s
⊢ Dense (⇑↑f '' ↑s)
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
r' : α → β → Prop
h : SemicontinuousWithinAt r s x
h' : SemicontinuousWithinAt r' s x
⊢ SemicontinuousWithinAt (r ⊔ r') s x

Tactic:
by
  intro b hab
  obtain hb | hb' := hab
  · exact (h b hb).mono fun _ hx ↦ Or.inl hx
  · exact (h' b hb').mono fun _ hx ↦ Or.inr hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
r' : α → β → Prop
h : SemicontinuousAt r x
h' : SemicontinuousAt r' x
⊢ SemicontinuousAt (r ⊔ r') x

Tactic:
by
  intro b hab
  obtain hb | hb' := hab
  · exact (h b hb).mono fun _ hx ↦ Or.inl hx
  · exact (h' b hb').mono fun _ hx ↦ Or.inr hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ LowerHemicontinuousWithinAt f s x ↔ ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
rw [lowerHemicontinuousWithinAt_iff, compl_surjective.forall]
  simp only [isOpen_compl_iff]
  refine forall₂_congr fun t ht ↦ ?_
  rw [← not_imp_not]
  simp [not_nonempty_iff_eq_empty, ← disjoint_iff_inter_eq_empty, disjoint_compl_right_iff_subset]

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

Goal state before:
pp: x : EReal
⊢ ⊥ < x⁻¹

Tactic:
cases x with

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

Goal state before:
pp: x : EReal
⊢ x⁻¹ < ⊤

Tactic:
cases x with

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

Goal state before:
pp: case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab✝¹ : d < a * b
d0 : 0 ≤ d
a' : EReal
aa' : a' ∈ Ioo 0 a
dab✝ : d < a' * b
b' : EReal
bb' : b' ∈ Ioo 0 b
dab : d < a' * b'
⊢ d ≤ c

Tactic:
exact dab.le.trans (h a' aa' b' bb')

Goal state after:
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)
⊢ μ ∅ = 0

Tactic:
by
      rw [← nonpos_iff_eq_zero]
      exact (iInf_le_of_le fun _ => ∅) <| iInf_le_of_le (empty_subset _) <| by simpa

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Semiring 𝕜
inst✝² : Algebra ℚ≥0 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℚ≥0 𝕜
⊢ Tendsto (⇑(algebraMap ℚ≥0 𝕜) ∘ fun n ↦ (↑n)⁻¹) atTop (𝓝 0)

Tactic:
convert! (continuous_algebraMap ℚ≥0 𝕜).continuousAt.tendsto.comp tendsto_inv_atTop_nhds_zero_nat
  rw [map_zero]

Goal state after: