mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_2
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
⊢ (this ⋯) 1 = 0

Tactic:
change (1 : S) ⊗ₜ[P] KaehlerDifferential.D R P 1 = 0; simp

Goal state after:
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
⊢ Algebra.IsSeparable K L

Tactic:
have := finite_of_free (R := K) (S := L)

Goal state after:
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
this : Module.Finite K L
⊢ Algebra.IsSeparable K L
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
⊢ ¬minpoly K ((algebraMap A Q.ResidueField) x) ^ 2 ∣ p

Tactic:
have : Algebra.FiniteType K A := .of_surjective _ hp₂
  have := Algebra.FormallyUnramified.finite_of_free K (Localization.AtPrime Q)
  have : IsField (Localization.AtPrime Q) :=
    have := IsArtinianRing.of_finite K (Localization.AtPrime Q)
    have := Algebra.FormallyUnramified.isReduced_of_field K (Localization.AtPrime Q)
    IsArtinianRing.isField_of_isReduced_of_isLocalRing _
  let := this.toField
  set q := minpoly K (algebraMap A Q.ResidueField x)
  have : algebraMap A (Localization.AtPrime Q) (aeval x q) = 0 := by
    apply (algebraMap (Localization.AtPrime Q) Q.ResidueField).injective
    rw [← IsScalarTower.algebraMap_apply, ← aeval_algebraMap_apply, minpoly.aeval, map_zero]
  obtain ⟨⟨m, hm⟩, hm'⟩ := (IsLocalization.map_eq_zero_iff Q.primeCompl _ _).mp this
  obtain ⟨m, rfl⟩ := hp₂ m
  simp_rw [← map_mul, ← AlgHom.coe_toRingHom, ← AlgHom.toRingHom_eq_coe, ← RingHom.mem_ker,
    ← hp₁, Ideal.mem_span_singleton] at hm'
  rw [pow_two]
  rintro H
  have := (mul_dvd_mul_iff_right (minpoly.ne_zero (Algebra.IsIntegral.isIntegral _))).mp
    (H.trans hm')
  rw [minpoly.dvd_iff, aeval_algebraMap_apply, Q.algebraMap_residueField_eq_zero] at this
  exact hm this

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
⊢ (Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker =
    (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
refine le_antisymm ?_ (liftBaseChange_range_le Q P)

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
⊢ (Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker ≤
    (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)).range
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mpr
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h✝ : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
x : A
h : ∀ i ∈ S, x ∈ i.maxPowDividing (span {a})
⊢ ∀ (i : HeightOneSpectrum A), x ∈ i.maxPowDividing (span {a})

Tactic:
i

Goal state after:
case mpr
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h✝ : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
x : A
h : ∀ i ∈ S, x ∈ i.maxPowDividing (span {a})
i : HeightOneSpectrum A
⊢ x ∈ i.maxPowDividing (span {a})
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R), ¬i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
⊢ ∀ (i : HeightOneSpectrum R), x ∈ i.maxPowDividing I

Tactic:
i

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R), ¬i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
⊢ x ∈ i.maxPowDividing I
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: ι : Type u_2
f : ι → ℝ≥0∞
hf : ∀ (x : ι), f x ≠ ∞
⊢ (fun x ↦ ↑x) ∘ ENNReal.toNNReal ∘ f = f

Tactic:
by
  ext x
  simp [coe_toNNReal (hf x)]

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 ∈ [[y, x]]

Tactic:
rw [uIcc_of_ge (hx.2.trans this).le]

Goal state after:
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
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
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝 a

Tactic:
← nhdsLE_sup_nhdsGE,

Goal state after:
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
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a ⊔ 𝓝[≥] a
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ a, ⨅ a', f a + g a' = ⨅ i, f i + iInf g

Tactic:
add_iInf

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
κ : Sort u_2
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ ⨅ i, f i + iInf g

Tactic:
add_iInf

Goal state after:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
κ : Sort u_2
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ ⨅ i, ⨅ b, f i + g b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe
a✝ : ℝ
hx : ↑a✝ ≤ 0
⊢ (↑a✝).toReal ≤ 0

Tactic:
exact toReal_coe _ ▸ EReal.coe_nonpos.mp hx

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

Goal state before:
pp: case mpr
x : EReal
⊢ (∀ (y : ℝ), x < ↑y) → x = ⊥

Tactic:
contrapose!
    intro h
    exact ⟨x.toReal, coe_toReal_le h⟩

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α × β
⊢ max (edist x.1 y.1) (edist x.2 y.2) = max (edist y.1 x.1) (edist y.2 x.2)

Tactic:
simp [edist_comm]

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

Goal state before:
pp: case pos
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

pp: case neg
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
· simp [hf]

Goal state after:
case neg
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
⊢ ⨆ b ∈ s, c • 1 * b = ⨆ a ∈ s, c • a

Tactic:
smul_one_mul

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
⊢ ∃ y ∈ s, dist x y < ε

Tactic:
have : (ball x ε).Nonempty := by simp [hε]
  simpa only [mem_ball'] using hs.exists_mem_open isOpen_ball this

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

Goal state before:
pp: ι : Sort u_3
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ g * iSup h ≤ a

Tactic:
rw [mul_iSup]
  exact ciSup_le' H

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
⊢ ∀ (i : Subtype (Membership.mem s)), a p' ∈ J * (↑i).asIdeal

Tactic:
rintro ⟨q, hq⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
q : HeightOneSpectrum R
hq : q ∈ s
⊢ a p' ∈ J * (↑⟨q, hq⟩).asIdeal
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable (f '' s)

Tactic:
rw [image_eq_range, ← image_univ]
  exact (isSeparable_univ_iff.2 hs.separableSpace).image hf.domRestrict

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
hs : s.Nonempty
⊢ ∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s

Tactic:
by
  rcases hs with ⟨a', ha'⟩
  intro h
  rcases (ha.1 ha').eq_or_lt with (rfl | ha'a)
  · exact h.self_of_nhdsWithin le_rfl ha'
  · rcases (mem_nhdsLE_iff_exists_Ioc_subset' ha'a).1 h with ⟨b, hba, hb⟩
    rcases ha.exists_between hba with ⟨b', hb's, hb'⟩
    exact hb hb' hb's

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

Goal state before:
pp: γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
x : α
hx : x ∈ upperBounds (f '' S)
⊢ x ∈ upperBounds (closure[inst✝³] (f '' S))

Tactic:
i

Goal state after:
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
x : α
hx : x ∈ upperBounds (f '' S)
i : α
⊢ i ∈ closure[inst✝³] (f '' S) → i ≤ x
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
⊢ IsOrderBornology α ↔ inst✝² = orderBornology

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun s ↦ by rw [h, orderBornology_isBounded]⟩⟩

Goal state after:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : IsOrderBornology α
⊢ inst✝² = orderBornology
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:
rw [continuousOn_iff_continuous_domRestrict] at hf hg

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:
rw [continuousOn_iff_continuous_domRestrict] at hf hg

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: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
⊢ ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs')
  · obtain ⟨a', ha'⟩ := exists_gt a
    exact ⟨a', ha', fun _ a ↦ a.elim⟩
  · obtain ⟨x, hx, hx'⟩ := hs.exists_isMinOn hs' hf
    exact ⟨f x, hf' x hx, hx'⟩

Goal state after:
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
h : map (algebraMap S R) p ≠ 0
⊢ map (algebraMap S R) p = ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S

Tactic:
← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h

Goal state after:
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
h : map (algebraMap S R) p ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (algebraMap S R) p) =
    ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S
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 δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
⊢ StrictMono f

Tactic:
intro a b hab

Goal state after:
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
⊢ f a < f b
Module: Mathlib.Topology.Bornology.Real

Goal state before:
pp: r : ℝ
⊢ BddAbove (closedBall 0 r)

Tactic:
obtain hr | hr := le_or_gt 0 r <;> simp [closedBall_zero_eq_Icc, *]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
h_mono : Monotone f
h_dense : DenseRange f
a : α
⊢ closure[inst✝²] (f '' univ) ∈ 𝓝 (f a)

Tactic:
simp only [image_univ, h_dense.closure_eq, univ_mem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ b ∈ upperBounds (u '' {a | u a ≤ b})

Tactic:
rintro _ ⟨a, ha, rfl⟩; exact ha

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

Goal state before:
pp: x y : EReal
⊢ ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Tactic:
by
  simp [bot_lt_iff_ne_bot]

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

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ ∅, u k)

Tactic:
rw [Finset.sum_empty]

Goal state after:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f 0
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x V
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)

Tactic:
use U + V

Goal state after:
case h
α : Type u_5
f : Filter α
R : Type u_6
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x V
⊢ ∀ᶠ (x : R) in map (u + v) f, (fun x1 x2 ↦ x1 ≤ x2) x (U + V)
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
c : α
hcs : c ∈ s
bc : b < c
bca : c ≤ a
⊢ ∀ᶠ (b_1 : { x // x ∈ s }) in atTop, b < ↑b_1

Tactic:
lift c to s using hcs

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
c : { x // x ∈ s }
bc : b < ↑c
bca : ↑c ≤ a
⊢ ∀ᶠ (b_1 : { x // x ∈ s }) in atTop, b < ↑b_1
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ sInf {a | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f

Tactic:
congr with b

Goal state after:
β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
⊢ (∀ᶠ (n : α) in f, u n ≤ b) ↔ ∀ᶠ (n : β) in map v f, n ≤ b
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, f.limsSup < x
hbot : ∀ (x : α), f.limsSup ≤ x
this : OrderBot α := { bot := f.limsSup, bot_le := hbot }
⊢ ClusterPt f.limsSup f

Tactic:
refine nhds_bot_basis.clusterPt_iff_frequently |>.mpr fun a h => ?_

Goal state after:
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, f.limsSup < x
hbot : ∀ (x : α), f.limsSup ≤ x
this : OrderBot α := { bot := f.limsSup, bot_le := hbot }
a : α
h : ⊥ < a
⊢ ∃ᶠ (x : α) in f, x ∈ Set.Iio a
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ limsup u f \ a = limsup (fun b ↦ u b \ a) f

Tactic:
simp only [limsup_eq_iInf_iSup, _root_.sdiff_eq]
  rw [biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
  simp_rw [inf_comm, inf_iSup₂_eq, inf_comm]

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

Goal state before:
pp: case top.coe.inl
a✝ : ℝ
h✝ : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
h : ↑a✝ < 0
⊢ ⊤ * ↑a✝ ≠ 0

Tactic:
simp [EReal.top_mul_of_pos, EReal.top_mul_of_neg, h]

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

Goal state before:
pp: case top.coe.inr
a✝ : ℝ
h✝ : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
h : 0 < ↑a✝
⊢ ⊤ * ↑a✝ ≠ 0

Tactic:
simp [EReal.top_mul_of_pos, EReal.top_mul_of_neg, h]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg.H
α : 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 = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∃ j, BddBelow (range fun i ↦ f ↑i)

Tactic:
· push Not at H'
    exact H'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b : β
⊢ HasProd (fun n ↦ if n = b then 1 else f n) (a / f b) L

Tactic:
convert! hf.update b 1 using 1
  · ext n
    rw [Function.update_apply]
  · rw [div_mul_eq_mul_div, one_mul]

Goal state after: