mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
inst : IsReduced (L ⊗[K] L)
⊢ 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1

Tactic:
exact sub_eq_zero.mp (IsNilpotent.eq_zero ⟨_, this⟩)

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
⊢ ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Bijective ⇑(awayMap (algebraMap R S) r')

Tactic:
obtain ⟨r, hrp, hr⟩ := Localization.exists_awayMap_injective_of_localRingHom_injective hRS H.1

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
⊢ ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Bijective ⇑(awayMap (algebraMap R S) r')
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a

Tactic:
calc
    ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a
      = ∑ a, f a - ∑ a ∈ s.biUnion S, f a := by
      rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
    _ = ∑ t ∈ s.powerset.filter (¬ ·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a
          + ∑ t ∈ s.powerset.filter (·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a := by
      simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq',
        sub_eq_add_neg, pow_succ]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a := sum_filter_not_add_sum_filter ..

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
⊢ sSup (s * t⁻¹) = sSup s * (sInf t)⁻¹

Tactic:
sSup_mul,

Goal state after:
M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
⊢ sSup s * sSup t⁻¹ = sSup s * (sInf t)⁻¹
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨅ x, 0 = 0

Tactic:
· exact ciInf_const

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: n : ℤ
⊢ ↑n.natAbs = ↑(nnabs ↑n)

Tactic:
Nat.cast_natAbs,

Goal state after:
n : ℤ
⊢ ↑|n| = ↑(nnabs ↑n)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q f g : NonarchAddGroupNorm E
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by obtain ⟨⟨⟨_, _⟩, _, _⟩, _⟩ := f; cases g; congr

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case inr.inl
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
hbx : b ≤ x
⊢ x ∈ ⊥

Tactic:
exact ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt

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

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < c → c < b → a ≠ ∞
⊢ a * (b - c) = a * b - a * c

Tactic:
simp only [mul_comm a]
  exact ENNReal.sub_mul h

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

Goal state before:
pp: ⊢ StrictAnti Inv.inv

Tactic:
intro a b h

Goal state after:
a b : ℝ≥0∞
h : a < b
⊢ b⁻¹ < a⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ y ≠ 0

Tactic:
simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ x ∈ ball y ε ↔ y ∈ ball x ε

Tactic:
rw [mem_ball', mem_ball]

Goal state after:
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Type u_2
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
x : ι
hxs : x ∈ s
⊢ f x = ↑(f x).toNNReal

Tactic:
rw [Real.coe_toNNReal _ (hf x hxs)]

Goal state after:
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Type u_2
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
x : ι
hxs : x ∈ s
⊢ f x = ↑(f x).toNNReal

Tactic:
rw [Real.coe_toNNReal _ (hf x hxs)]

Goal state after:
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_4
f : ι → ℕ
⊢ ↑(⨅ i, f i) = ⨅ i, ↑(f i)

Tactic:
obtain hι | hι := isEmpty_or_nonempty ι
  · simp [iInf_empty]
  apply eq_of_forall_le_iff
  simp [le_ciInf_iff, ← Nat.ceil_le]

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

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
⊢ ∃ᶠ (x : X) in Filter.comap (Prod.mk x) (𝓤 X), x ∈ iUnion U

Tactic:
frequently_comap,

Goal state after:
ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
⊢ ∃ᶠ (b : X × X) in 𝓤 X, ∃ a, (x, a) = b ∧ a ∈ iUnion U
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = 0 ↔ ↑(nndist x y) = 0

Tactic:
NNReal.coe_eq_zero

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = 0 ↔ nndist x y = 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: a b : ℝ≥0
⊢ a ≤ b + nndist a b

Tactic:
suffices (a : ℝ) ≤ (b : ℝ) + dist a b by
    rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]
  rw [← sub_le_iff_le_add']
  exact le_of_abs_le (dist_eq a b).ge

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu
  have : Iic ε ∈ 𝓝 (0 : ℝ) := Iic_mem_nhds εpos
  filter_upwards [this] with _ hr using Subset.trans (closedBall_subset_closedBall hr) hε

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

Goal state before:
pp: case neg
α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsClosed[inst✝¹] s
h₁ : s.Nonempty
h₂ : ¬BddBelow s
⊢ IsClosed[inst✝¹] ↑(upperClosure s)

Tactic:
exact upperClosure_eq_bot h₂ ▸ isClosed_univ

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
g : ι → E
f : F → ι
⊢ ‖g ∘ f‖ ≤ ‖g‖

Tactic:
rw [pi_norm_le_iff_of_nonneg' (by positivity)]
  exact fun x ↦ norm_le_pi_norm' g (f x)

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

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
b : ι
⊢ ‖single i y b‖₊ = single i ‖y‖₊ b

Tactic:
refine Pi.apply_single (fun i (x : G i) ↦ ‖x‖₊) ?_ i y b

Goal state after:
ι : Type u_1
G : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
b : ι
⊢ ∀ (i : ι), ‖0‖₊ = 0
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
m : β
hm : m > sSup (f '' Ioo y x)
w✝ : α
hy : y < w✝
hx : w✝ < x
w : α
hw : w ∈ Ioo y x
⊢ f w < m

Tactic:
exact (le_csSup h_bdd (mem_image_of_mem _ hw)).trans_lt hm

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
f : Filter α
hf : Cauchy f
⊢ ∃ x, f ≤ nhds x

Tactic:
obtain ⟨t, t_fset, ht⟩ : ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < 1 :=
      (Metric.cauchy_iff.1 hf).2 1 zero_lt_one
    rcases hf.1.nonempty_of_mem t_fset with ⟨x, xt⟩
    have : closedBall x 1 ∈ f := mem_of_superset t_fset fun y yt => (ht y yt x xt).le
    rcases (isCompact_iff_totallyBounded_isComplete.1 (isCompact_closedBall x 1)).2 f hf
        (le_principal_iff.2 this) with
      ⟨y, -, hy⟩
    exact ⟨y, hy⟩

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
h : b ∈ closedBall a r
⊢ ‖a‖ + ‖b⁻¹ * a‖ ≤ ‖a‖ + r

Tactic:
by simp [mem_closedBall_iff_norm_inv_mul_le.1 h]

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this : IsClosed[instTopologicalSpace] (⇑ofDual ⁻¹' (s ∩ Icc a b))
⊢ toDual a ∈ ⇑ofDual ⁻¹' s

Tactic:
rw [preimage_inter, ← Icc_toDual] at this

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this : IsClosed[instTopologicalSpace] (⇑ofDual ⁻¹' s ∩ Icc (toDual b) (toDual a))
⊢ toDual a ∈ ⇑ofDual ⁻¹' s
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ edist a b = ‖a⁻¹ * b‖ₑ

Tactic:
rw [edist_dist, dist_eq_norm_inv_mul, ofReal_norm']

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
⊢ StrictMonoOn f (Icc a b)

Tactic:
have : Fact (a ≤ b) := ⟨hab⟩
  refine StrictMono.of_domRestrict ?_
  set g : Icc a b → δ := Set.domRestrict (Icc a b) f
  have hgab : g ⊥ ≤ g ⊤ := by aesop
  exact Continuous.strictMono_of_inj_boundedOrder (f := g) hf_c.domRestrict hgab hf_i.injective

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
⊢ Dense ↑S

Tactic:
by
  cases subsingleton_or_nontrivial G
  · refine fun x => _root_.subset_closure ?_
    rw [Subsingleton.elim x 1]
    exact one_mem S
  refine dense_of_exists_between fun a b hlt => ?_
  rcases hS (b / a) (one_lt_div'.2 hlt) with ⟨g, hgS, hg0, hg⟩
  rcases (existsUnique_add_zpow_mem_Ioc hg0 1 a).exists with ⟨m, hm⟩
  rw [one_mul] at hm
  refine ⟨g ^ m, zpow_mem hgS _, hm.1, hm.2.trans_lt ?_⟩
  rwa [lt_div_iff_mul_lt'] at hg

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

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) t a
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Tactic:
rcases isBot_or_exists_lt t with tbot | ⟨t', ht'⟩

Goal state after:
case inl
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) t a
tbot : IsBot t
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

case inr
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t

Tactic:
rcases hg x with ⟨Kg, t, ht, hgL⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
Kg : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case inr.refine_1
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b < c
r : α
⊢ b < ⨆ i, u i r

Tactic:
have : c ≤ u n0 r := (h_anti n0).le_of_tendsto (h_all n0) r

Goal state after:
case inr.refine_1
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b < c
r : α
this : c ≤ u n0 r
⊢ b < ⨆ i, u i r
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
a b : EReal
c : ℝ
h : a ≤ b + ↑c
⊢ a - ↑c ≤ b

Tactic:
| coe c =>

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ blimsup s cofinite p = {x | {n | p n ∧ x ∈ s n}.Infinite}

Tactic:
by
  simp only [blimsup_eq, eventually_cofinite, not_forall, sInf_eq_sInter, exists_prop]
  ext x
  refine ⟨fun h => ?_, fun hx t h => ?_⟩ <;> contrapose h
  · simp only [mem_sInter, mem_ofPred_eq, not_forall, exists_prop]
    exact ⟨{x}ᶜ, by simpa using h, by simp⟩
  · exact hx.mono fun i hi => ⟨hi.1, fun hit => h (hit hi.2)⟩

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

Goal state before:
pp: x y : EReal
⊢ (∀ (z : ℝ), x < ↑z → y ≤ ↑z) ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ WithBot.le_of_forall_lt_iff_le.1 ?_, fun h _ x_z ↦ h.trans x_z.le⟩
  rw [WithTop.forall]
  aesop

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

Goal state before:
pp: ⊢ ∀ {a b : EReal}, a * b = 0 → a = 0 ∨ b = 0

Tactic:
intro a b h

Goal state after:
a b : EReal
h : a * b = 0
⊢ a = 0 ∨ b = 0
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ x ≤ limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a

Tactic:
by
  refine ⟨fun h _ h' ↦ (frequently_lt_of_lt_limsup h₁ (h'.trans_le h)).mono fun _ ↦ le_of_lt, ?_⟩
  rw [← forall_lt_iff_le]
  intro h y y_x
  obtain ⟨z, y_z, z_x⟩ := exists_between y_x
  exact y_z.trans_le (le_limsup_of_frequently_le (h z z_x) h₂)

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

Goal state before:
pp: a b : EReal
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
rcases lt_trichotomy a 0 with (h | h | h)

Goal state after:
case inl
a b : EReal
h : a < 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

case inr.inl
a b : EReal
h : a = 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

case inr.inr
a b : EReal
h : 0 < a
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
a b c : ℝ≥0∞
⊢ (↑a + ↑b) * ↑c = ↑a * ↑c + ↑b * ↑c

Tactic:
| coe c =>

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
l : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f

Tactic:
exact IsBounded.isBoundedUnder f_decr bdd_above

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
⊢ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f = s.sup' hs fun i ↦ limsup (F i) f

Tactic:
have bddsup := isBoundedUnder_le_finset_sup' hs h₂
  apply le_antisymm
  · have h₃ : ∃ i ∈ s, f.IsCoboundedUnder (· ≤ ·) (F i) := by
      rcases hs with ⟨i, i_s⟩
      use i, i_s
      exact h₁ i i_s
    have cobddsup := isCoboundedUnder_le_finset_sup' hs h₃
    refine (limsup_le_iff cobddsup bddsup).2 (fun b hb ↦ ?_)
    simp only [gt_iff_lt, sup'_lt_iff, eventually_all_finset] at hb ⊢
    exact fun i i_s ↦ eventually_lt_of_limsup_lt (hb i i_s) (h₂ i i_s)
  · apply Finset.sup'_le hs (fun i ↦ limsup (F i) f)
    refine fun i i_s ↦ limsup_le_limsup (Eventually.of_forall (fun a ↦ ?_)) (h₁ i i_s) bddsup
    simp only [le_sup'_iff]
    use i, i_s

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

Goal state before:
pp: case e'_6
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ finprod (L.support.mulIndicator fun b ↦ f b) = ∏ b ∈ ⋯.toFinset, f b

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]

Goal state after:
case e'_6
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ ∏ i ∈ ⋯.toFinset, L.support.mulIndicator (fun b ↦ f b) i = ∏ b ∈ ⋯.toFinset, f b

case e'_6.h
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ mulSupport (L.support.mulIndicator fun b ↦ f b) ⊆ ↑⋯.toFinset
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommMonoid α
inst✝⁶ : Preorder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderClosedTopology α
f : ι → α
a : α
inst✝² : L.NeBot
inst✝¹ : L.LeAtTop
inst✝ : MulRightStrictMono α
hf : HasProd f a L
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
⊢ f j * f i = ∏ k ∈ {j, i}, f k

Tactic:
Finset.prod_pair hij

Goal state after:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommMonoid α
inst✝⁶ : Preorder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderClosedTopology α
f : ι → α
a : α
inst✝² : L.NeBot
inst✝¹ : L.LeAtTop
inst✝ : MulRightStrictMono α
hf : HasProd f a L
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
⊢ f j * f i = f j * f i
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 α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hf : Multipliable f L
hL : ¬L.NeBot
⊢ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g

Tactic:
by_cases hfs : (mulSupport fun x ↦ g (f x)).Finite
        · simp [tprod_bot hL, finprod_eq_prod _ hfs, ← _root_.map_prod]
        · exact ⟨1, by simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]⟩

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 : ¬Multipliable f L
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
rwa [tprod_eq_one_of_not_multipliable hf]

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

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝³ : CommGroupWithZero K
inst✝² : TopologicalSpace K
f g : α → K
L : SummationFilter α
inst✝¹ : ContinuousInv₀ K
inst✝ : ContinuousMul K
a b : K
hf : HasProd f a L
hg : HasProd g b L
hb : b ≠ 0
⊢ HasProd (fun x ↦ f x / g x) (a / b) L

Tactic:
simp only [div_eq_mul_inv]
  exact hf.mul <| hg.inv₀ hb

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

Goal state before:
pp: case he
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ (-1) ^ (2 * k) * f (2 * k)

Tactic:
simp only [even_two, Even.mul_right, Even.neg_pow, one_pow, one_mul]
    exact hf.comp_injective (mul_right_injective₀ (two_ne_zero' ℕ))

Goal state after: