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

Goal state before:
pp: case refine_2
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
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
⊢ Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer ⋯))

Tactic:
let F : P.ker →ₗ[P.Ring] RingHom.ker fQ := f.mapKer rfl

Goal state after:
case refine_2
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
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
⊢ Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer ⋯))
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case hs
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
this : (⋃ i ∈ s, S i).indicator 1 a = 1
i : ι
hi : i ∈ s
⊢ s.Nonempty

Tactic:
exact ⟨i, hi⟩

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : ¬t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

Tactic:
obtain rfl := not_nonempty_iff_eq_empty.1 ht
        simp

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

Goal state before:
pp: r : ℝ
⊢ r = 0 ∨ ∃ x, 0 < x ∧ (r = ↑x ∨ r = -↑x)

Tactic:
obtain ⟨x, hx⟩ := nnreal_dichotomy r

Goal state after:
r : ℝ
x : ℝ≥0
hx : r = ↑x ∨ r = -↑x
⊢ r = 0 ∨ ∃ x, 0 < x ∧ (r = ↑x ∨ r = -↑x)
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ a.toReal ≤ b.toReal ↔ a ≤ b

Tactic:
lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  norm_cast

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ a.toReal < b.toReal ↔ a < b

Tactic:
lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  norm_cast

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : αᵒᵈ
⊢ (x ∈ range fun x ↦ ⋯.some) ↔ x ∈ ⇑ofDual ⁻¹' range fun x ↦ ⋯.some

Tactic:
simp only [mem_range, Subtype.exists, mem_preimage, OrderDual.exists, dual_ordConnectedComponent,
    ofDual_toDual]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : αᵒᵈ
⊢ (∃ a, ∃ (h : a ∈ s), ⋯.some = x) ↔ ∃ a, ∃ (h : a ∈ s), ⋯.some = ofDual x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x.toENNReal ≠ 0 ↔ 0 < x

Tactic:
simp [toENNReal_eq_zero_iff.not]

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

Goal state before:
pp: case inl
x : EReal
hx : 0 ≤ x
⊢ ↑x.toENNReal = max 0 x

Tactic:
coe_toENNReal hx,

Goal state after:
case inl
x : EReal
hx : 0 ≤ x
⊢ x = max 0 x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ a / ∞ = 0

Tactic:
by rw [div_eq_mul_inv, inv_top, mul_zero]

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

Goal state before:
pp: a b c : ℝ≥0∞
h : a ≤ b / c
⊢ a * c ≤ b

Tactic:
by
  rw [← inv_inv c]
  exact div_le_of_le_mul h

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

Goal state before:
pp: case refine_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ↑(Iic 1)
this : 1 ≤ (↑x)⁻¹
⊢ ↑((fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) ((fun x ↦ ((↑x)⁻¹ - 1)⁻¹) x)) = ↑x

Tactic:
simp only [inv_inv, tsub_add_cancel_of_le this]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist z x = edist z y

Tactic:
edist_comm z x,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist z y
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑y ^ n ≤ ↑x

pp: case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑x < ↑y ^ (n + 1)

Tactic:
· rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]

Goal state after:
case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑x < ↑y ^ (n + 1)
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
⊢ ∃ ε' > 0, eball y ε' ⊆ eball x ε

Tactic:
have : 0 < ε - edist y x := by simpa using h

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
this : 0 < ε - edist y x
⊢ ∃ ε' > 0, eball y ε' ⊆ eball x ε
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)

Tactic:
· rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]

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

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α✝
α : Type ?u.9
B : Bornology α
m : PseudoMetricSpace α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
s : Set α
⊢ Bornology.IsBounded s ↔ sᶜ ∈ {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}

Tactic:
rw [isBounded_iff, mem_ofPred_eq, compl_compl]

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 := ⋯ }
⊢ p' ∈ s

Tactic:
simpa [p', s, Ideal.dvd_iff_le] using le_sup_left.trans 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₁ : J * K ≤ J * p
⊢ False

Tactic:
replace H₁ := hK.trans_le H₁ (Ideal.mem_span_singleton_self _)

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
⊢ False
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ Ici a ⊆ closure[inst✝³] (Ioi a)

Tactic:
← sdiff_subset_closure_iff,

Goal state after:
case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ Ici a \ Ioi a ⊆ closure[inst✝³] (Ioi a)
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)

Tactic:
← sdiff_subset_closure_iff,

Goal state after:
case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ Icc a b \ Ioo a b ⊆ closure[inst✝³] (Ioo a b)
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : sᶜᶜ ∈ cobounded α
⊢ s ∈ Filter.atTop

Tactic:
← isBounded_def,

Goal state after:
α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : IsBounded sᶜ
⊢ s ∈ Filter.atTop
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
⊢ ((∃ i, True ∧ Iic i ⊆ sᶜᶜ) ∧ ∃ i, True ∧ Ici i ⊆ sᶜᶜ) → sᶜᶜ ∈ cobounded α

Tactic:
← isBounded_def,

Goal state after:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
⊢ ((∃ i, True ∧ Iic i ⊆ sᶜᶜ) ∧ ∃ i, True ∧ Ici i ⊆ sᶜᶜ) → IsBounded sᶜ
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝⁴ : Bornology α
inst✝³ : LinearOrder α
inst✝² : IsOrderBornology α
inst✝¹ : NoMaxOrder α
inst✝ : OrderBot α
s : Set α
⊢ (∃ i, True ∧ Ici i ⊆ sᶜᶜ) → sᶜᶜ ∈ cobounded α

Tactic:
← isBounded_def,

Goal state after:
α : Type u_1
inst✝⁴ : Bornology α
inst✝³ : LinearOrder α
inst✝² : IsOrderBornology α
inst✝¹ : NoMaxOrder α
inst✝ : OrderBot α
s : Set α
⊢ (∃ i, True ∧ Ici i ⊆ sᶜᶜ) → IsBounded sᶜ
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ x✝
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

Tactic:
refine ⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩

Goal state after:
case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝¹ : Set α
hs : x✝¹ ∈ atBot
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ x✝¹
x✝ : α
hx : x✝ ∈ (Icc t ⊤)ᶜ
⊢ x✝ ∈ x✝¹
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖

Tactic:
rw [dist_eq_norm_inv_mul, Set.apply_mulIndicator_symmDiff norm_inv']
  simp only [Set.mulIndicator, mul_ite, mul_one]
  split_ifs <;> simp

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

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

Tactic:
rw [mem_ball, dist_eq_norm_inv_mul]

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 (toDual b) (toDual a))
x : αᵒᵈ
hx : x ∈ ⇑ofDual ⁻¹' s ∩ Ico (toDual b) (toDual a)
⊢ (⇑ofDual ⁻¹' s ∩ Ioc x (toDual a)).Nonempty

Tactic:
rw [Ico_toDual, ← preimage_inter, ← Equiv.image_symm_eq_preimage, mem_image] at hx

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))
x : αᵒᵈ
hx : ∃ x_1 ∈ s ∩ Ioc a b, ofDual.symm x_1 = x
⊢ (⇑ofDual ⁻¹' s ∩ Ioc x (toDual a)).Nonempty
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
⊢ tᶜ ∩ Ioc z y ∈ 𝓝[>] z

Tactic:
← nhdsWithin_Ioc_eq_nhdsGT hz.2

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
⊢ tᶜ ∩ Ioc z y ∈ 𝓝[Ioc z y] z
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
s : Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
c : α
h : ∃ r, (closedBall c r)ᶜ ⊆ s
⊢ s ∈ cocompact α

Tactic:
rcases h with ⟨r, h⟩
  rw [Filter.mem_cocompact]
  exact ⟨closedBall c r, isCompact_closedBall c r, h⟩

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

Goal state before:
pp: case cons
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (∀ i ∈ s✝, f i < g i) → ∑ i ∈ s✝, f i < ∑ i ∈ s✝, g i
Hlt : ∀ i ∈ cons a✝ s✝ h✝, f i < g i
⊢ ∑ i ∈ cons a✝ s✝ h✝, f i < ∑ i ∈ cons a✝ s✝ h✝, g i

Tactic:
simp only [Finset.sum_cons, forall_mem_cons] at Hlt ⊢

Goal state after:
case cons
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (∀ i ∈ s✝, f i < g i) → ∑ i ∈ s✝, f i < ∑ i ∈ s✝, g i
Hlt : f a✝ < g a✝ ∧ ∀ x ∈ s✝, f x < g x
⊢ f a✝ + ∑ i ∈ s✝, f i < g a✝ + ∑ i ∈ s✝, g i
Module: Mathlib.Order.Filter.IsBounded

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

Tactic:
choose! m hm using h
  use sup' s hs m
  simp only [eventually_map] at hm ⊢
  rw [← eventually_all_finset s] at hm
  refine hm.mono fun a h ↦ ?_
  simp only [sup'_le_iff]
  exact fun i i_s ↦ le_trans (h i i_s) (le_sup' m i_s)

Goal state after:
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
⊢ limsup u f = limsup v f

Tactic:
by
  rw [limsup_eq]
  congr with b
  exact eventually_congr (h.mono fun x hx => by simp [hx])

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ f (limsup (fun n ↦ (⇑f)^[n] a) atTop) = limsup (fun n ↦ (⇑f)^[n] a) atTop

Tactic:
limsup_eq_iInf_iSup_of_nat',

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ f (⨅ n, ⨆ i, (⇑f)^[i + n] a) = ⨅ n, ⨆ i, (⇑f)^[i + n] a
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 : α
this : c ≤ u n0 r
⊢ b < ⨆ i, u i r

Tactic:
exact hb.trans_le (this.trans (le_iSup_iff.mpr fun b a ↦ a n0))

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < δ
hδ : ↑δ * ↑(3 * K) < ε / 2
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε

Tactic:
rw [← ENNReal.coe_pos] at δpos

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
s : Set α
hs : Dense s
ha : ∀ a ∈ s, Continuous[inst✝¹, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] fun y ↦ f (a, y)
hb : ∀ (b : β), LipschitzWith K fun x ↦ f (x, b)
⊢ Continuous[instTopologicalSpaceProd, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
simp only [← continuousOn_univ, ← univ_prod_univ, ← lipschitzOnWith_univ] at *
  exact continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith f (subset_univ _)
    hs.closure_eq.ge K ha fun b _ => hb b

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

Goal state before:
pp: γ : Type u_3
β : Type u_4
f : γ ↪ β
⊢ (unconditional β).comap f = unconditional γ

Tactic:
classical
  simp only [unconditional, comap]
  congr 1 with s
  simp only [mem_map, mem_atTop_sets, mem_preimage]
  constructor <;> rintro ⟨t, ht⟩
  · refine ⟨t.preimage f (by simp), fun x hx ↦ ?_⟩
    simpa [Finset.union_eq_right.mpr hx] using ht (t ∪ x.map f) t.subset_union_left
  · exact ⟨_, fun b hb ↦ ht _ (Finset.map_subset_iff_subset_preimage.mp hb)⟩

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ c * (a + b) = c * a + c * b

Tactic:
nth_rewrite 1 [EReal.mul_comm]; nth_rewrite 2 [EReal.mul_comm]; nth_rewrite 3 [EReal.mul_comm]
  exact right_distrib_of_nonneg ha hb

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

Goal state before:
pp: n : ℕ
x : EReal
⊢ n • x = ↑n * x

Tactic:
induction n with
  | zero => rw [zero_smul, Nat.cast_zero, zero_mul]
  | succ n ih =>
    rw [succ_nsmul, ih, Nat.cast_succ]
    convert! (EReal.right_distrib_of_nonneg _ _).symm <;> simp

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

Goal state before:
pp: ⊢ comap Real.toNNReal atTop ≤ atTop

Tactic:
refine (atTop_basis_Ioi' 0).ge_iff.2 fun a ha ↦ ?_

Goal state after:
a : ℝ
ha : 0 < a
⊢ Set.Ioi a ∈ comap Real.toNNReal atTop
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Metric.ediam univ = Metric.ediam univ

Tactic:
by
  rw [← h.range_eq_univ, h.isometry.ediam_range]

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
m n : ℕ
x✝¹ x✝ : (Fin m → α) × (Fin n → α)
⊢ edist ((Fin.appendEquiv m n).toFun x✝¹) ((Fin.appendEquiv m n).toFun x✝) = edist x✝¹ x✝

Tactic:
simp_rw [Fin.appendEquiv, Fin.edist_append_eq_max_edist, Prod.edist_eq]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst✝¹] s
⊢ ∃ ia, (a ∉ ia ∧ IsClosed[inst✝²] ia) ∧ ∀ x ∈ iaᶜ, f x ∈ sᶜ

Tactic:
refine ⟨closure (f ⁻¹' s), ⟨mt ?_ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst✝¹] s
⊢ a ∈ closure[inst✝²] (f ⁻¹' s) → b ∈ s
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case mpr
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n ≤ ε

Tactic:
· obtain ⟨n, hn⟩ := h ε hε
    exact ⟨n, hn.le⟩

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

Goal state before:
pp: α : Type uα
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝³ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ pkg'.extend f (pkg'.coe (g a)) = (f ∘ g) a

Tactic:
pkg'.extend_coe hf

Goal state after:
α : Type uα
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝³ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ f (g a) = (f ∘ g) a
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case pos
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
H : x = 0
⊢ x ^ n ≠ 0 ∨ x ≠ ∞

Tactic:
simp only [H, zero_ne_top, Ne, or_true, not_false_iff]

Goal state after: