mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q)

Tactic:
sub_eq_iff_eq_add',

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b = φ ↑(f P) + ∑ Q ∈ f.support \ {P}, φ ↑(f Q)
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : α
⊢ y ∈ s.ordConnectedComponent x ↔ x ∈ s.ordConnectedComponent y

Tactic:
by
  rw [mem_ordConnectedComponent, mem_ordConnectedComponent, uIcc_comm]

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

Goal state before:
pp: a : ℝ≥0∞
⊢ ∞ * a = if a = 0 then 0 else ∞

Tactic:
by convert! WithTop.top_mul' a

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
this : c < y
⊢ c ∈ Icc x y

Tactic:
exact ⟨hx.2.le, this.le⟩

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

Goal state before:
pp: ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : IsCodirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ f _k + g _k ≤ f i + g j

Tactic:
gcongr <;> apply_rules

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

Goal state before:
pp: ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i + g j ≤ f _k + g _k

Tactic:
gcongr <;> apply_rules

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

Goal state before:
pp: y : ℝ
⊢ Real.toEReal ⁻¹' Iio ↑y = Iio y

Tactic:
change (WithBot.some ∘ WithTop.some) ⁻¹' (Iio (WithBot.some (WithTop.some y))) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio]

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

Goal state before:
pp: m n : ℕ
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
← coe_coe_eq_natCast,

Goal state after:
m n : ℕ
⊢ ↑↑(m * n) = ↑m * ↑n
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ ↑↑(m * n) = ↑m * ↑n

Tactic:
← coe_coe_eq_natCast,

Goal state after:
m n : ℕ
⊢ ↑↑(m * n) = ↑↑m * ↑n
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ ↑↑(m * n) = ↑↑m * ↑n

Tactic:
← coe_coe_eq_natCast,

Goal state after:
m n : ℕ
⊢ ↑↑(m * n) = ↑↑m * ↑↑n
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ count K v ↑v.asIdeal = 1

Tactic:
have hv : (v.asIdeal : FractionalIdeal R⁰ K) ≠ 0 := coeIdeal_ne_zero.mpr v.ne_bot
  have h_self : (v.asIdeal : FractionalIdeal R⁰ K) =
      spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal := by
    rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]
  have hv_irred : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible
  rw [count_well_defined K v hv h_self, Associates.count_self hv_irred,
    Ideal.span_singleton_one, ← Ideal.one_eq_top, Associates.mk_one, Associates.factors_one,
    Associates.count_zero hv_irred, ofNat_zero, sub_zero, ofNat_one]

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

Goal state before:
pp: a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a⁻¹⁻¹ = a

Tactic:
by_cases a = 0

Goal state after:
case pos
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h✝ : a = 0
⊢ a⁻¹⁻¹ = a

case neg
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h✝ : ¬a = 0
⊢ a⁻¹⁻¹ = a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ ↑x✝⁻¹ < (↑a)⁻¹

Tactic:
← coe_inv ha,

Goal state after:
case coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ ↑x✝⁻¹ < ↑a⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ∞
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b

Tactic:
rw [← @ENNReal.mul_le_mul_iff_right _ a _ hr₀ hr₁, ← mul_assoc, ENNReal.mul_inv_cancel hr₀ hr₁,
    one_mul]

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

Goal state before:
pp: a b c : ℝ≥0∞
hc : c < a * b
⊢ ∃ a' < a, c < a' * b

Tactic:
by
  obtain ⟨a', hc, ha'⟩ := exists_between (ENNReal.div_lt_of_lt_mul hc)
  exact ⟨_, ha', (ENNReal.div_lt_iff (.inl <| by rintro rfl; simp at *)
    (.inr <| by rintro rfl; simp at *)).1 hc⟩

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

Goal state before:
pp: α : Type u_2
m m' : EMetricSpace α
h : m.toEDist = m'.toEDist
⊢ m = m'

Tactic:
cases m

Goal state after:
case mk
α : Type u_2
m' : EMetricSpace α
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h : { toPseudoEMetricSpace := toPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ }.toEDist = m'.toEDist
⊢ { toPseudoEMetricSpace := toPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ } = m'
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
m m' : WeakPseudoEMetricSpace α
h : m.toEDist = m'.toEDist
⊢ m = m'

Tactic:
cases m

Goal state after:
case mk
α : Type u_2
inst✝ : TopologicalSpace α
m' : WeakPseudoEMetricSpace α
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le✝ : (uniformSpaceOfEDist edist edist_self✝ edist_comm✝ edist_triangle✝).toTopologicalSpace ≤ inst✝
topology_eq_on_restrict✝ :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
h :
  { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ }.toEDist =
    m'.toEDist
⊢ { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ } =
    m'
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (f ⁻¹' s)

Tactic:
rw [isOpen_iff] at hs ⊢

Goal state after:
α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
⊢ ∀ x ∈ f ⁻¹' s, ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
m m' : WeakEMetricSpace α
h : m.toEDist = m'.toEDist
⊢ m = m'

Tactic:
cases m

Goal state after:
case mk
α : Type u_2
inst✝ : TopologicalSpace α
m' : WeakEMetricSpace α
toWeakPseudoEMetricSpace✝ : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h :
  { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ }.toEDist =
    m'.toEDist
⊢ { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ } = m'
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: α : Type u_3
m m' : MetricSpace α
h : m.toDist = m'.toDist
⊢ m = m'

Tactic:
cases m

Goal state after:
case mk
α : Type u_3
m' : MetricSpace α
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist = m'.toDist
⊢ { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ } = m'
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inr
a : ℝ≥0
ha : a ≠ 0
⊢ (↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹

Tactic:
← coe_inv ha,

Goal state after:
case coe.inr
a : ℝ≥0
ha : a ≠ 0
⊢ (↑a⁻¹).toNNReal = (↑a).toNNReal⁻¹
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ IsUniformInducing f ∧ Function.Injective f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
and_comm,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ Function.Injective f ∧ IsUniformInducing f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this✝³ : UniformSpace α := pseudoMetrizableSpaceUniformity α
this✝² : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
this✝¹ : SeparableSpace ↑s
this✝ : SecondCountableTopology ↑s
this : IsInducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)
⊢ IsSeparable (f ⁻¹' s)

Tactic:
have := this.secondCountableTopology

Goal state after:
β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this✝⁴ : UniformSpace α := pseudoMetrizableSpaceUniformity α
this✝³ : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
this✝² : SeparableSpace ↑s
this✝¹ : SecondCountableTopology ↑s
this✝ : IsInducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)
this : SecondCountableTopology ↑(f ⁻¹' s)
⊢ IsSeparable (f ⁻¹' s)
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case inr.inl.mk
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
fst✝ : α
snd✝ : β
⊢ closedBall (fst✝, snd✝) 0 = closedBall fst✝ 0 ×ˢ closedBall snd✝ 0

Tactic:
closedBall_prod_same

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : (𝓝[s ∩ Ici x] a).NeBot
⊢ f x ≤ b

Tactic:
refine ge_of_tendsto (hb.mono_left (nhdsWithin_mono a (inter_subset_left (t := Ici x)))) ?_

Goal state after:
α : Type u_1
γ : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : (𝓝[s ∩ Ici x] a).NeBot
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Ici x] a, f x ≤ f c
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ dist (Pi.single i a) (Pi.single j b) = max (dist a 0) (dist b 0)

Tactic:
simp only [dist_nndist, nndist_single_single i j a b h, NNReal.coe_max]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
β : Type u_3
inst✝² : LinearOrder β
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
v : ℕ → β
hu : StrictMono (f ∘ v)
huyxf : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x ∩ range f
hlim : Tendsto (f ∘ v) atTop (𝓝 x)
huyx : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x
hv : ∀ (n : ℕ), f (v n) = (f ∘ v) n
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
exact ⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, huyx, hlim⟩

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

Goal state before:
pp: case inl
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
f : ι → F
hf : Surjective f
g : F → E
h : IsEmpty F
⊢ ‖g ∘ f‖ = ‖g‖

Tactic:
have : IsEmpty ι := f.isEmpty

Goal state after:
case inl
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
f : ι → F
hf : Surjective f
g : F → E
h : IsEmpty F
this : IsEmpty ι
⊢ ‖g ∘ f‖ = ‖g‖
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
⊢ {x | x ∈ s ∧ ¬ContinuousWithinAt f s x} ⊆
    {x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x} ∪ {x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x}

Tactic:
refine compl_subset_compl.1 ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
⊢ ({x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x} ∪ {x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x})ᶜ ⊆
    {x | x ∈ s ∧ ¬ContinuousWithinAt f s x}ᶜ
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : BddBelow (range g)
⊢ f (⨅ i, g i) = ⨆ i, f (g i)

Tactic:
rw [iInf, Antitone.map_csInf_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]

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

Goal state before:
pp: X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x ∈ s, f x = g x

Tactic:
continuousOn_iff_continuous_domRestrict

Goal state after:
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst✝²] (s.domRestrict f)
hg : Continuous[instTopologicalSpaceSubtype, inst✝²] (s.domRestrict g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x ∈ s, f x = g x
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : l₁.NeBot
inst✝ : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ ∃ x ∈ s, f x = g x

Tactic:
continuousOn_iff_continuous_domRestrict

Goal state after:
X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : l₁.NeBot
inst✝ : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst✝³] (s.domRestrict f)
hg : Continuous[instTopologicalSpaceSubtype, inst✝³] (s.domRestrict g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ ∃ x ∈ s, f x = g x
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inr.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst✝] u
left✝ : IsOpen[inst✝¹] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
⊢ sSup (f x' '' K) < z

Tactic:
rw [hK.sSup_lt_iff_of_continuous h0K
        (show Continuous (f x') from hf.comp <| .prodMk_right x').continuousOn]

Goal state after:
case inr.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst✝] u
left✝ : IsOpen[inst✝¹] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
⊢ ∀ x ∈ K, f x' x < z
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (f '' [[a, b]])

Tactic:
rw [h.image_uIcc_eq_Icc]

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (f '' [[a, b]])

Tactic:
rw [h.image_uIcc_eq_Icc]

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ |n|‖ = ‖a ^ n‖

Tactic:
by
  rcases le_total 0 n with hn | hn <;> simp [hn, abs_of_nonneg, abs_of_nonpos]

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

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
⊢ UniformCauchySeqOn F atTop s → ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε

Tactic:
intro h ε hε
    let u := { a : α × α | dist a.fst a.snd < ε }
    have hu : u ∈ 𝓤 α := Metric.mem_uniformity_dist.mpr ⟨ε, hε, by simp [u]⟩
    rw [← Filter.eventually_atTop_prod_self' (p := fun m =>
      ∀ x ∈ s, dist (F m.fst x) (F m.snd x) < ε)]
    specialize h u hu
    rw [prod_atTop_atTop_eq] at h
    exact h.mono fun n h x hx => h x hx

Goal state after:
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}
R : ℝ
hR : ∀ (m n : ℕ), dist (s m) (s n) < R
N : ℕ
⊢ ∀ y ∈ S N, y ≤ R

Tactic:
rintro _ ⟨⟨m, n⟩, _, rfl⟩

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}
R : ℝ
hR : ∀ (m n : ℕ), dist (s m) (s n) < R
N m n : ℕ
left✝ : (m, n) ∈ {p | p.1 ≥ N ∧ p.2 ≥ N}
⊢ (fun p ↦ dist (s p.1) (s p.2)) (m, n) ≤ R
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a * b ∈ ball a r ↔ ‖b‖ < r

Tactic:
rw [mem_ball_iff_norm'']
  simp

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

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ r * f x) l atTop

Tactic:
refine tendsto_atTop.2 fun b => ?_
  obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
  rw [nsmul_eq_mul'] at hn
  filter_upwards [tendsto_atTop.1 hf (n * max b 0)] with x hx
  calc
    b ≤ 1 * max b 0 := by
    { rw [one_mul]
      exact le_max_left _ _ }
    _ ≤ r * n * max b 0 := by gcongr
    _ = r * (n * max b 0) := by rw [mul_assoc]
    _ ≤ r * f x := by gcongr

Goal state after: