mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: case cons
head✝ : ℝ → ℝ
tail✝ : List (ℝ → ℝ)
⊢ Sorted 0

Tactic:
| cons =>

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: case cons
head✝ : ℝ → ℝ
tail✝ : List (ℝ → ℝ)
⊢ zero.Approximates

Tactic:
| cons =>

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case cons.cons.cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
x✝¹ : α
s✝¹ : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = Seq.cons x✝¹ s✝¹
x✝ : α
s✝ : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = Seq.cons x✝ s✝
this : (Seq.cons x✝¹ s✝¹).head = (Seq.cons x✝ s✝).head
⊢ (Seq.cons x✝ s✝).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s_tl))
      (match (Seq.cons x✝¹ s✝¹).destruct with
      | none => none
      | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
| cons =>

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case cons.cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl t : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = t
x✝ : α
s✝ : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = Seq.cons x✝ s✝
this : (Seq.cons x✝ s✝).head = t.head
⊢ t.destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s_tl))
      (match (Seq.cons x✝ s✝).destruct with
      | none => none
      | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
| cons =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
⊢ zero.FundamentalSequenceProp zero.fundamentalSequence

Tactic:
exact rfl

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) exps) basis).prod) =ᶠ[atTop] fun a ↦
        (List.zipWith (fun exp b ↦ b a ^ exp) exps basis).prod⁻¹
basis : Basis
h_basis : WellFormedBasis basis
⊢ (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) (exp :: exps)) basis).prod) =ᶠ[atTop] fun a ↦
    (List.zipWith (fun exp b ↦ b a ^ exp) (exp :: exps) basis).prod⁻¹

Tactic:
cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono
      intro x ⟨h_pos, ih⟩
      simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]
      grind [Real.rpow_neg h_pos.le]

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: s : S
⊢ S.decode s.encode = s

Tactic:
induction s with

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
⊢ ∃ m, n = m ^ q

Tactic:
have hf0 : f 0 = 0 := by simpa [hq.ne'] using congr($hf 0)

Goal state after:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
hf0 : f 0 = 0
⊢ ∃ m, n = m ^ q
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h₁
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ xs₀ ~ xs₁

Tactic:
rwa [← hxs, h₀, h₁] at hperm

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
f : InjectiveFunction α
⊢ Injective f.apply

Tactic:
obtain ⟨xs, hperm, hnodup⟩ := f
  generalize h₀ : List.map Sigma.fst xs = xs₀
  generalize h₁ : xs.map (@id ((Σ _ : α, α) → α) <| @Sigma.snd α fun _ : α => α) = xs₁
  dsimp [id] at h₁
  have hxs : xs = TotalFunction.List.toFinmap' (xs₀.zip xs₁) := by
    rw [← h₀, ← h₁, List.toFinmap']; clear h₀ h₁ xs₀ xs₁ hperm hnodup
    induction xs with
    | nil => simp only [List.zip_nil_right, List.map_nil]
    | cons xs_hd xs_tl xs_ih =>
      simp only [Sigma.eta, List.zip_cons_cons,
        List.map, List.cons_inj_right]
      exact xs_ih
  revert hperm hnodup
  rw [hxs]; intro hperm hnodup
  apply InjectiveFunction.applyId_injective
  · rwa [← h₀, hxs, hperm.nodup_iff]
  · rwa [← hxs, h₀, h₁] at hperm

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

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
h : EquicontinuousAt (fun f ↦ ⇑↑f) 1
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
replace h := equicontinuous_of_equicontinuousAt_one _ h
  obtain ⟨W, hWo, hWV, hWc⟩ := local_compact_nhds hV
  let S1 : Set (X →* Y) := {f | Set.MapsTo f U W}
  let S2 : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo f U W}
  let S3 : Set C(X, Y) := (↑) '' S2
  let S4 : Set (X → Y) := (↑) '' S3
  replace h : Equicontinuous ((↑) : S1 → X → Y) :=
    h.comp (Subtype.map _root_.id fun f hf ↦ hf.mono_right hWV)
  have hS4 : S4 = (↑) '' S1 := by
    ext
    constructor
    · rintro ⟨-, ⟨f, hf, rfl⟩, rfl⟩
      exact ⟨f, hf, rfl⟩
    · rintro ⟨f, hf, rfl⟩
      exact ⟨⟨f, h.continuous ⟨f, hf⟩⟩, ⟨⟨f, h.continuous ⟨f, hf⟩⟩, hf, rfl⟩, rfl⟩
  replace h : Equicontinuous ((↑) : S3 → X → Y) := by
    rw [equicontinuous_iff_range, ← Set.image_eq_range] at h ⊢
    rwa [← hS4] at h
  replace hS4 : S4 = Set.pi U (fun _ ↦ W) ∩ Set.range ((↑) : (X →* Y) → (X → Y)) := by
    simp_rw [hS4, Set.ext_iff, Set.mem_image, S1, Set.mem_ofPred_eq]
    exact fun f ↦ ⟨fun ⟨g, hg, hf⟩ ↦ hf ▸ ⟨hg, g, rfl⟩, fun ⟨hg, g, hf⟩ ↦ ⟨g, hf ▸ hg, hf⟩⟩
  replace hS4 : IsClosed S4 :=
    hS4.symm ▸ (isClosed_set_pi (fun _ _ ↦ hWc.isClosed)).inter (MonoidHom.isClosed_range_coe X Y)
  have hS2 : (interior S2).Nonempty := by
    let T : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo f U (interior W)}
    have h1 : T.Nonempty := ⟨1, fun _ _ ↦ mem_interior_iff_mem_nhds.mpr hWo⟩
    have h2 : T ⊆ S2 := fun f hf ↦ hf.mono_right interior_subset
    have h3 : IsOpen T := isOpen_induced (ContinuousMap.isOpen_setOfPred_mapsTo hU isOpen_interior)
    exact h1.mono (interior_maximal h2 h3)
  exact TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group
    ⟨⟨S2, (isInducing_toContinuousMap X Y).isCompact_iff.mpr
      (ArzelaAscoli.isCompact_of_equicontinuous S3 hS4.isCompact h)⟩, hS2⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
⊢ ∃ V, Disjoint (a • ↑V) (b • ↑V)

Tactic:
obtain ⟨V, hV⟩ := is_nonarchimedean v (open_v.mem_nhds mem_v)

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : ↑V ⊆ v
⊢ ∃ V, Disjoint (a • ↑V) (b • ↑V)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ ↑(map n i) '' sphere 0 1 ∪ ↑(map n i) '' ball 0 1 = closedCell n i

Tactic:
closedCell,

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ ↑(map n i) '' sphere 0 1 ∪ ↑(map n i) '' ball 0 1 = ↑(map n i) '' closedBall 0 1
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ closedCell n j ⊆ closure[t] (openCell n j)

Tactic:
closedCell,

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ↑(map n j) '' closedBall 0 1 ⊆ closure[t] (openCell n j)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
j : cell C 0
⊢ closedCell 0 j = {↑(map 0 j) ![]}

Tactic:
simp [closedCell, Matrix.empty_eq]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x z : cell C 0
h : (fun x ↦ ↑(map 0 x) ![]) x = (fun x ↦ ↑(map 0 x) ![]) z
hne : ¬x = z
⊢ ↑(map 0 x) ![] ∈ openCell 0 x ∧ ↑(map 0 x) ![] ∈ openCell 0 z

Tactic:
by simp [openCell_zero_eq_singleton, h]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
⊢ ∃ x y, cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y

Tactic:
obtain ⟨f, h⟩ := cellFrontier_subset_finite_closedCell 1 e
  simp only [RelCWComplex.cellFrontier_one_eq, image_pair, Order.lt_one_iff, iUnion_iUnion_eq_left,
    RelCWComplex.closedCell_zero_eq_singleton, pair_subset_iff, mem_iUnion, mem_singleton_iff,
    exists_prop] at h
  obtain ⟨⟨u, hu, hun1⟩, v, hv, hv1⟩ := h
  use u, v
  simp [RelCWComplex.cellFrontier_one_eq, image_pair, RelCWComplex.closedCell_zero_eq_singleton,
    hun1, hv1, pair_comm]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = false
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

pp: case true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = true
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Tactic:
· rw [hx, ne_eq, Bool.not_eq_false] at ha
    refine ⟨1 - (e (π C (· ∈ s)) a), ⟨one_sub_e_mem_of_false _ _ ha hx, ?_⟩⟩
    rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]

Goal state after:
case true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = true
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ ∀ (i : I), x i ≠ false → J i

Tactic:
exact (hh · x h)

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ D ∪ ⋃ n, ⋃ j, openCell n j = C

Tactic:
suffices D ∪ ⋃ n, ⋃ (j : cell C n), openCell n j =
      D ∪ ⋃ (m : ℕ) (_ : m < (⊤ : ℕ∞)) (j : cell C m), closedCell m j by
    simpa [union] using this

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ D ∪ ⋃ n, ⋃ j, openCell n j = D ∪ ⋃ m, ⋃ (_ : ↑m < ⊤), ⋃ j, closedCell m j
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Bijective (range_equiv_smaller_toFun C o)

Tactic:
dsimp +unfoldPartialApp [range_equiv_smaller_toFun]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Bijective fun x ↦ ⟨(πs C o) ↑x, ⋯⟩
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
⊢ ↑l = term I ho :: ↑l.Tail

Tactic:
rw [← List.cons_head!_tail hl, hlh]
  simp [Tail]

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

Goal state before:
pp: X✝ Y✝ Z✝ : UniformSpaceCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ⇑(ConcreteCategory.hom (ConcreteCategory.ofHom ⟨Completion.map ⇑(f ≫ g).hom', ⋯⟩).hom) =
    ⇑(ConcreteCategory.hom
        (ConcreteCategory.ofHom ⟨Completion.map ⇑f.hom', ⋯⟩ ≫ ConcreteCategory.ofHom ⟨Completion.map ⇑g.hom', ⋯⟩).hom)

Tactic:
by
    exact (Completion.map_comp g.hom.property f.hom.property).symm

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
i : I
hi : i ∈ ↑l.Tail ∧ SwapTrue o (↑x) i ≠ true
⊢ False

Tactic:
← hi' i hi.1

Goal state after:
case pos
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
i : I
hi : i ∈ ↑l.Tail ∧ ↑x i ≠ true
⊢ False
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) [] (term I ho :: ↑(↑l).Tail)

Tactic:
exact List.Lex.nil

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ 𝓝 (⨅ i, f i) = ⨅ i, 𝓝 (f i)

Tactic:
simp only [nhds_eq]

Goal state after:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (⨅ i, f i).lift' (Iic ∘ 𝓟) = ⨅ i, (f i).lift' (Iic ∘ 𝓟)
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ uniformity (Set α) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | hausdorffEDist p.1 p.2 < ε}

Tactic:
refine le_antisymm
      (le_iInf₂ fun ε hε => Filter.le_principal_iff.mpr ?_)
      (uniformity_basis_edist.lift' monotone_hausdorffEntourage |>.ge_iff.mpr fun ε hε =>
        Filter.mem_iInf_of_mem ε <| Filter.mem_iInf_of_mem hε fun _ =>
        mem_hausdorffEntourage_of_hausdorffEDist_lt)
    obtain ⟨δ, hδ, hδε⟩ := exists_between hε
    filter_upwards [Filter.mem_lift' (uniformity_basis_edist_le.mem_of_mem hδ)]
      with _ h using hδε.trans_le' <| hausdorffEDist_le_of_mem_hausdorffEntourage h

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ 0 < externalCoveringNumber ε A ↔ A.Nonempty

Tactic:
← not_iff_not

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < externalCoveringNumber ε A ↔ ¬A.Nonempty
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ 0 < coveringNumber ε A ↔ A.Nonempty

Tactic:
← not_iff_not

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < coveringNumber ε A ↔ ¬A.Nonempty
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ 0 < packingNumber ε A ↔ A.Nonempty

Tactic:
← not_iff_not

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < packingNumber ε A ↔ ¬A.Nonempty
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) ∅
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) ∅
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g ∅

pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
· exact ⟨0, LipschitzWith.const' 0, by simp⟩

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ y ∈ maximalSeparatedSet ε A, (x, y) ∉ {x | edist x.1 x.2 ≤ ↑ε}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
this : C ⊆ A ∧ IsSeparated (↑ε) C
⊢ False

Tactic:
refine absurd (encard_le_of_isSeparated this.1 this.2 h) ?_

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ y ∈ maximalSeparatedSet ε A, (x, y) ∉ {x | edist x.1 x.2 ≤ ↑ε}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
this : C ⊆ A ∧ IsSeparated (↑ε) C
⊢ ¬C.encard ≤ (maximalSeparatedSet ε A).encard
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ∞
C : ℝ≥0
hC : HolderWith C r f
⊢ edist (f x₁) (f x₂) / edist x₁ x₂ ^ ↑r ≤ ↑C

Tactic:
ENNReal.div_le_iff h₁ h₂

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ∞
C : ℝ≥0
hC : HolderWith C r f
⊢ edist (f x₁) (f x₂) ≤ ↑C * edist x₁ x₂ ^ ↑r
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ 0 < s.einfsep.toReal ↔ 0 < s.einfsep ∧ s.einfsep < ∞

Tactic:
ENNReal.toReal_pos_iff

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x y z : Snowflaking X α hα₀ hα₁
⊢ edist (ofSnowflaking x) (ofSnowflaking z) ^ α ≤
    edist (ofSnowflaking x) (ofSnowflaking y) ^ α + edist (ofSnowflaking y) (ofSnowflaking z) ^ α

Tactic:
edist_triangle x.ofSnowflaking y.ofSnowflaking z.ofSnowflaking,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x y z : Snowflaking X α hα₀ hα₁
⊢ (edist (ofSnowflaking x) (ofSnowflaking y) + edist (ofSnowflaking y) (ofSnowflaking z)) ^ α ≤
    edist (ofSnowflaking x) (ofSnowflaking y) ^ α + edist (ofSnowflaking y) (ofSnowflaking z) ^ α
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case h
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
x : X
hx : x ∈ ⇑toSnowflaking ⁻¹' s
y : X
hy : y ∈ ⇑toSnowflaking ⁻¹' s
⊢ dist x y ≤ (dist x y ^ α) ^ α⁻¹

Tactic:
Real.rpow_rpow_inv (by positivity) hα₀.ne'

Goal state after:
case h
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
x : X
hx : x ∈ ⇑toSnowflaking ⁻¹' s
y : X
hy : y ∈ ⇑toSnowflaking ⁻¹' s
⊢ dist x y ≤ dist x y
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ closure[instTopologicalSpace] {toLowerSet b} ⊆ closure[instTopologicalSpace] {toLowerSet a} ↔ a ≤ b

Tactic:
IsLowerSet.closure_singleton,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ici (toLowerSet b) ⊆ Ici (toLowerSet a) ↔ a ≤ b
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
a : α
inst✝ : IsScott α univ
⊢ Iic a ⊆ closure[inst✝¹] {a}

Tactic:
by
    rw [← LowerSet.coe_Iic, ← lowerClosure_singleton]
    apply lowerClosure_subset_closure

Goal state after:
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : PseudoEpimorphism α β
f' : α → β
h : f' = ⇑f
⊢ ∀ ⦃a : α⦄ ⦃b : β⦄, (f.copy f' h).toFun a ≤ b → ∃ c, a ≤ c ∧ (f.copy f' h).toFun c = b

Tactic:
simpa only [h.symm, toFun_eq_coe] using! f.exists_map_eq_of_map_le'

Goal state after:
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
f : EsakiaHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ ⦃a : α⦄ ⦃b : β⦄, (f.copy f' h).toFun a ≤ b → ∃ c, a ≤ c ∧ (f.copy f' h).toFun c = b

Tactic:
simpa only [h.symm, toFun_eq_coe] using! f.exists_map_eq_of_map_le'

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
T : Set α
S : Set ↑T
⊢ hull T (sInf (⇑OrderDual.toDual ⁻¹' ⇑OrderDual.ofDual ⁻¹' Subtype.val '' S)) = hull T (kernel S)

Tactic:
← preimage_comp,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
T : Set α
S : Set ↑T
⊢ hull T (sInf (⇑OrderDual.ofDual ∘ ⇑OrderDual.toDual ⁻¹' Subtype.val '' S)) = hull T (kernel S)
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
T : Set α
S : Set ↑T
⊢ hull T (sInf (id (Subtype.val '' S))) = hull T (kernel S)

Tactic:
id_eq

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
T : Set α
S : Set ↑T
⊢ hull T (sInf (Subtype.val '' S)) = hull T (kernel S)