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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝ : FormallySmooth R P.Ring
this : FormallySmooth P.Ring (Localization M')
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T

Tactic:
haveI : FormallySmooth R Q.Ring := .comp R P.Ring (Localization M')

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝¹ : FormallySmooth R P.Ring
this✝ : FormallySmooth P.Ring (Localization M')
this : FormallySmooth R Q.Ring
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case a.a
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : α
a✝¹ : t ∈ s.biUnion S
x✝ : ι
a✝ : x✝ ∈ s
⊢ 1 = (↑(s.biUnion S)).indicator 1 t

Tactic:
rw [Set.indicator_of_mem ‹_›, Pi.one_apply]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
⊢ ∃ x, IsGLB s x

Tactic:
have hbdd' : BddAbove (-s) := bddAbove_neg.mpr hbdd

Goal state after:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ ∃ x, IsGLB s x
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: f : CauSeq ℝ abs
⊢ ∃ x, f ≈ const abs x

Tactic:
by
  let s := {x : ℝ | const abs x < f}
  have lb : ∃ x, x ∈ s := exists_lt f
  have ub' : ∀ x, f < const abs x → ∀ y ∈ s, y ≤ x := fun x h y yS =>
    le_of_lt <| const_lt.1 <| CauSeq.lt_trans yS h
  have ub : ∃ x, ∀ y ∈ s, y ≤ x := (exists_gt f).imp ub'
  refine ⟨sSup s, ((lt_total _ _).resolve_left fun h => ?_).resolve_right fun h => ?_⟩
  · rcases h with ⟨ε, ε0, i, ih⟩
    refine (csSup_le lb (ub' _ ?_)).not_gt (sub_lt_self _ (half_pos ε0))
    refine ⟨_, half_pos ε0, i, fun j ij => ?_⟩
    rw [sub_apply, const_apply, sub_right_comm, le_sub_iff_add_le, add_halves]
    exact ih _ ij
  · rcases h with ⟨ε, ε0, i, ih⟩
    refine (le_csSup ub ?_).not_gt ((lt_add_iff_pos_left _).2 (half_pos ε0))
    refine ⟨_, half_pos ε0, i, fun j ij => ?_⟩
    rw [sub_apply, const_apply, add_comm, ← sub_sub, le_sub_iff_add_le, add_halves]
    exact ih _ ij

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ ⨅ i, i.maxPowDividing I = ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ (↑(Finite.toFinset ⋯)).Pairwise (IsCoprime on fun i ↦ i.maxPowDividing I)

Tactic:
· ext x
    constructor
    · aesop
    · simp only [Finite.mem_toFinset, mem_mulSupport, one_eq_top, ne_eq, Submodule.mem_iInf]
      intro h i
      by_cases i.maxPowDividing I = ⊤ <;> simp_all

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ (↑(Finite.toFinset ⋯)).Pairwise (IsCoprime on fun i ↦ i.maxPowDividing I)
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✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q✝ : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
⊢ max (p 1) (q 1) = 0

Tactic:
← map_one_eq_zero p,

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q✝ : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
⊢ max (p 1) (q 1) = p 1
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
hb : b ≠ ∞
h : a < b
⊢ a.toNNReal < b.toNNReal

Tactic:
by
  simpa [← ENNReal.coe_lt_coe, hb, h.ne_top]

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ᶜ
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
by_cases H : Disjoint (Icc a b) (ordConnectedSection <| ordSeparatingSet s t)

Goal state after:
case pos
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ᶜ
H : Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

case neg
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ᶜ
H : ¬Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ¬J = 0

Tactic:
exact h_J_ne_zero

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

Goal state before:
pp: case pos
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
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : n = 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

Tactic:
rw [hn, neg_zero, zpow_zero, count_one, neg_zero]

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

Goal state before:
pp: case neg
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
n : ℤ
I : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ count K v (I ^ (-n) * I ^ n) = 0

Tactic:
← zpow_add₀ hI,

Goal state after:
case neg
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
n : ℤ
I : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ count K v (I ^ (-n + n)) = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
ht : b ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
cases b with

Goal state after:
case coe
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inl
a c : ℝ≥0∞
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c

Tactic:
have hc : c ≠ 0 := h0.neg_resolve_left rfl
    simp [div_zero hc]

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x : α
⊢ edist x x < ∞

Tactic:
rw [edist_self]; exact ENNReal.coe_lt_top

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

Goal state before:
pp: case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ (b + 1) ≤ x ^ (a + 1)

Tactic:
apply pow_right_mono₀ hx

Goal state after:
case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ b + 1 ≤ a + 1
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: X : Type u_2
inst✝ : PseudoMetricSpace X
s : Set X
ε : ℝ
hs : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
hε : 0 < ε
t : Finset ↑s
hst : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ⊆ ⋃ i ∈ t, ball (↑i) ε
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x ε

Tactic:
refine ⟨t.map ⟨Subtype.val, Subtype.val_injective⟩, by simp, Finset.finite_toSet _, ?_⟩

Goal state after:
X : Type u_2
inst✝ : PseudoMetricSpace X
s : Set X
ε : ℝ
hs : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
hε : 0 < ε
t : Finset ↑s
hst : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ⊆ ⋃ i ∈ t, ball (↑i) ε
⊢ s ⊆ ⋃ x ∈ ↑(Finset.map { toFun := Subtype.val, inj' := ⋯ } t), ball x ε
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 ((fun x ↦ f ↑x) '' univ)

Tactic:
exact (isSeparable_univ_iff.2 hs.separableSpace).image hf.domRestrict

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
⊢ (fun j ↦ ⨅ i, ⨅ (_ : 0 < j), 𝓟 {a | edist (a.1 i) (a.2 i) < j}) = fun ε ↦
    ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
funext ε

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ ⨅ i, ⨅ (_ : 0 < ε), 𝓟 {a | edist (a.1 i) (a.2 i) < ε} =
    ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}
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
ha : IsLUB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
⊢ b ∈ upperBounds (f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩
  replace ha := ha.inter_Ici_of_mem hx
  have := ha.nhdsWithin_neBot ⟨x, hx, le_rfl⟩
  refine ge_of_tendsto (hb.mono_left (nhdsWithin_mono a (inter_subset_left (t := Ici x)))) ?_
  exact mem_of_superset self_mem_nhdsWithin fun y hy => hf hx hy.1 hy.2

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ IsClosed[inst✝³] (Ico a b) ↔ b ≤ a

Tactic:
refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ico a b)
hab : a < b
⊢ False
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ IsClosed[inst✝³] (Ioc a b) ↔ b ≤ a

Tactic:
refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ioc a b)
hab : a < b
⊢ False
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ IsClosed[inst✝³] (Ioo a b) ↔ b ≤ a

Tactic:
refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ioo a b)
hab : a < b
⊢ False
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_4
inst✝ : (i : Fin (n + 1)) → PseudoMetricSpace (α i)
i : Fin (n + 1)
x y : α i
f g : (j : Fin n) → α (i.succAbove j)
c : ℝ≥0
⊢ nndist (i.insertNth x f) (i.insertNth y g) ≤ c ↔ max (nndist x y) (nndist f g) ≤ c

Tactic:
by simp [nndist_pi_le_iff, i.forall_iff_succAbove]

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

Goal state before:
pp: α : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : x ∉ Ioo y x
ht : (Ioo y x).Nonempty
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ Ioo y x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
exact ⟨u, hu.1, hu.2.2.symm⟩

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
f : ι → F
hf : Surjective f
g : F → E
⊢ ‖g ∘ f‖ = ‖g‖

Tactic:
obtain (h | h) := isEmpty_or_nonempty F
  · have : IsEmpty ι := f.isEmpty
    simp [Subsingleton.elim g 1]
  apply le_antisymm (pi_norm_comp_le' g f)
  obtain ⟨⟨x, h⟩, -⟩ := IsGreatest.pi_norm' g
  obtain ⟨y, rfl⟩ := hf x
  exact h ▸ norm_le_pi_norm' (g ∘ f) y

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

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
⊢ BddBelow sᶜ ∧ BddAbove sᶜ

Tactic:
refine ⟨⟨b, fun x hx ↦ ?_⟩, ⟨a, fun x hx ↦ ?_⟩⟩

Goal state after:
case refine_1
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
⊢ b ≤ x

case refine_2
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
⊢ x ≤ a
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:
by
  rw [continuousOn_iff_continuous_domRestrict] at hf hg
  obtain ⟨b, h⟩ :=
    @intermediate_value_univ₂_eventually₂ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) _ _
      (comap_coe_neBot_of_le_principal hl₁) (comap_coe_neBot_of_le_principal hl₂) _ _ hf hg
      (he₁.comap _) (he₂.comap _)
  exact ⟨b, b.prop, h⟩

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
⊢ BddBelow s

Tactic:
obtain ⟨a, -, has⟩ := hs.exists_isLeast hne

Goal state after:
case inr
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
a : α
has : a ∈ lowerBounds s
⊢ BddBelow s
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x * y‖ ≤ ‖y‖

Tactic:
simpa [h] using norm_mul_le' x y

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x * y‖ ≤ ‖x‖

Tactic:
simpa [h] using norm_mul_le' x y

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

Goal state before:
pp: case inr.inl
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
have Z := A b h'b a h'a

Goal state after:
case inr.inl
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ s
Z : edist b a ≤ ediam s + edist x y + ediam t
⊢ edist a b ≤ ediam s + edist x y + ediam t
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖a⁻¹ * b‖ = ‖a / b‖

Tactic:
← dist_eq_norm_inv_mul,

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a b = ‖a / b‖
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
r : R
n : ℕ
hn : -r ≤ ↑n
⊢ ↑(-↑n) ≤ r

Tactic:
simpa [neg_le] using hn

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 δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
⊢ StrictMono f

Tactic:
intro x y hxy
  let s := min a x
  let t := max b y
  have hsa : s ≤ a := min_le_left a x
  have hbt : b ≤ t := le_max_left b y
  have hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t) := by
    have : Fact (s ≤ t) := ⟨hsa.trans <| hbt.trans' hab.le⟩
    have := Continuous.strictMono_of_inj_boundedOrder' (f := Set.domRestrict (Icc s t) f)
      hf_c.continuousOn.domRestrict hf_i.injOn.injective
    exact this.imp strictMono_domRestrict.mp strictAntiOn_iff_strictAnti.mpr
  have (h : StrictAntiOn f (Icc s t)) : False := by
    have : Icc a b ⊆ Icc s t := Icc_subset_Icc hsa hbt
    replace : StrictAntiOn f (Icc a b) := StrictAntiOn.mono h this
    replace : IsAntichain (· ≤ ·) (Icc a b) :=
      IsAntichain.of_strictMonoOn_antitoneOn hf_mono this.antitoneOn
    exact this.not_lt (left_mem_Icc.mpr (le_of_lt hab)) (right_mem_Icc.mpr (le_of_lt hab)) hab
  replace hf_mono_st : StrictMonoOn f (Icc s t) := hf_mono_st.resolve_right this
  have hsx : s ≤ x := min_le_right a x
  have hyt : y ≤ t := le_max_right b y
  replace : Icc x y ⊆ Icc s t := Icc_subset_Icc hsx hyt
  replace : StrictMonoOn f (Icc x y) := StrictMonoOn.mono hf_mono_st this
  exact this (left_mem_Icc.mpr (le_of_lt hxy)) (right_mem_Icc.mpr (le_of_lt hxy)) hxy

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

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

Tactic:
refine tendsto_atTop.mpr fun s => ?_
  obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
  replace hn : s ≤ (n : ℤ) • r := by simpa
  exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (zsmul_le_zsmul_left hr.le ha)

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
⊢ 0 ≤ m

Tactic:
rw [← Int.lt_add_one_iff, ← zpow_lt_zpow_iff_right h₀, zpow_zero]

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
⊢ 1 < a ^ (m + 1)
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
s : Finset κ
h : ∀ k ∈ s, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ s, u k)

Tactic:
induction s using Finset.cons_induction
  case empty =>
    rw [Finset.sum_empty]
    exact ⟨0, by simp_all only [eventually_map, Pi.zero_apply, eventually_true]⟩
  case cons k₀ s k₀_notin_s ih =>
    simp only [Finset.forall_mem_cons] at *
    simpa only [Finset.sum_cons] using hr _ _ h.1 (ih h.2)

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

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝² : LinearOrder R
inst✝¹ : LinearOrder S
f : R → S
f_incr : Monotone f
inst✝ : F.NeBot
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f

Tactic:
obtain ⟨l, hl⟩ := IsCobounded.frequently_ge cobdd

Goal state after:
R : Type u_5
S : Type u_6
F : Filter R
inst✝² : LinearOrder R
inst✝¹ : LinearOrder S
f : R → S
f_incr : Monotone f
inst✝ : F.NeBot
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
l : R
hl : ∃ᶠ (x : R) in F, l ≤ x
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(↑a✝¹ + ↑a✝) = -↑a✝¹ - ↑a✝

Tactic:
rw [← coe_add, ← coe_neg, ← coe_neg, ← coe_sub, neg_add']

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * ↑K ^ n

Tactic:
rw [iterate_succ, mul_comm]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ edist (f^[n] x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * edist x (f x)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case symm
x✝ y✝ : EReal
h : (x✝ * y✝).toReal = x✝.toReal * y✝.toReal
⊢ (y✝ * x✝).toReal = y✝.toReal * x✝.toReal

Tactic:
| symm h =>

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

Goal state before:
pp: case symm
x✝ y✝ : EReal
h : 0 < x✝ * y✝ ↔ 0 < x✝ ∧ 0 < y✝ ∨ x✝ < 0 ∧ y✝ < 0
⊢ 0 < y✝ * x✝ ↔ 0 < y✝ ∧ 0 < x✝ ∨ y✝ < 0 ∧ x✝ < 0

Tactic:
| symm h =>

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

Goal state before:
pp: α : Type u_3
⊢ Tendsto Finset.powerset atTop atTop

Tactic:
refine tendsto_atTop_atTop.mpr fun t ↦ ⟨t.sup id, fun _ hu _ hv ↦ ?_⟩

Goal state after:
α : Type u_3
t : Finset (Finset α)
x✝¹ : Finset α
hu : t.sup id ⊆ x✝¹
x✝ : Finset α
hv : x✝ ∈ t
⊢ x✝ ∈ x✝¹.powerset
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case symm
x✝ y✝ : EReal
h : x✝ * y✝ = ⊤ ↔ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤
⊢ y✝ * x✝ = ⊤ ↔ y✝ = ⊥ ∧ x✝ < 0 ∨ y✝ < 0 ∧ x✝ = ⊥ ∨ y✝ = ⊤ ∧ 0 < x✝ ∨ 0 < y✝ ∧ x✝ = ⊤

Tactic:
| symm h =>

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

Goal state before:
pp: case coe.top.inl
a✝ : ℝ
hx✝ : 0 ≤ ↑a✝
hx : 0 = ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal

Tactic:
simp [← hx]

Goal state after: