mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (eval (π C J) l) (Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) = (eval C l) x

Tactic:
Products.eval_eq,

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (if ∀ i ∈ ↑l, ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true then 1 else 0) = (eval C l) x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
this : ⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯) = ⇑(eval (π (π C K) J) l)
⊢ ⇑(eval (π (π C K) J) l) ∘ ProjRestrict (π C K) J = ⇑(eval (π C K) l)

Tactic:
← evalFacProp (π C K) J h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
this : ⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯) = ⇑(eval (π (π C K) J) l)
⊢ ⇑(eval (π (π C K) J) l) ∘ ProjRestrict (π C K) J = ⇑(eval (π (π C K) J) l) ∘ ProjRestrict (π C K) J
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
⊢ isGood {fun x ↦ false} nil

Tactic:
intro h

Goal state after:
I : Type u_1
inst✝ : LinearOrder I
h : eval {fun x ↦ false} nil ∈ Submodule.span ℤ (eval {fun x ↦ false} '' {m | m < nil})
⊢ False
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
l : Products I
hl : Products.isGood C l
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1, ∃ (h_1 : Products.isGood (π C fun x ↦ ord I x < a) a_1), eval (π C fun x ↦ ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = eval C ⟨l, hl⟩

Tactic:
contained_eq_proj C o hsC,

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
l : Products I
hl✝ : Products.isGood C l
hl : Products.isGood (π C fun x ↦ ord I x < o) l
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1, ∃ (h_1 : Products.isGood (π C fun x ↦ ord I x < a) a_1), eval (π C fun x ↦ ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = eval C ⟨l, hl✝⟩
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
⊢ (∀ o' < o, P I o') → P I o

Tactic:
intro h

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
⊢ P I o
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case neg
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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
⊢ Products.isGood (π C fun x ↦ ord I x < o) l

Tactic:
intro he

Goal state after:
case neg
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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
⊢ False
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]

Goal state after:
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
⊢ term I ho :: (↑l).tail = term I ho :: ↑l.Tail
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: 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)
⊢ (e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ * (eval C l.Tail) ⟨SwapTrue o ↑x, ⋯⟩ -
      (e C (term I ho)) ⟨↑x, ⋯⟩ * (eval C l.Tail) ⟨↑x, ⋯⟩ =
    (eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)) x

Tactic:
Products.eval_eq,

Goal state after:
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)
⊢ ((e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ * if ∀ i ∈ ↑l.Tail, ↑⟨SwapTrue o ↑x, ⋯⟩ i = true then 1 else 0) -
      (e C (term I ho)) ⟨↑x, ⋯⟩ * (eval C l.Tail) ⟨↑x, ⋯⟩ =
    (eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)) x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: 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)
⊢ ((e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ * if ∀ i ∈ ↑l.Tail, ↑⟨SwapTrue o ↑x, ⋯⟩ i = true then 1 else 0) -
      (e C (term I ho)) ⟨↑x, ⋯⟩ * (eval C l.Tail) ⟨↑x, ⋯⟩ =
    (eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)) x

Tactic:
Products.eval_eq,

Goal state after:
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)
⊢ (((e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ * if ∀ i ∈ ↑l.Tail, ↑⟨SwapTrue o ↑x, ⋯⟩ i = true then 1 else 0) -
      (e C (term I ho)) ⟨↑x, ⋯⟩ * if ∀ i ∈ ↑l.Tail, ↑⟨↑x, ⋯⟩ i = true then 1 else 0) =
    (eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)) x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: 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
⊢ (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true

Tactic:
apply forall_congr

Goal state after:
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
⊢ ∀ (a : I), (a ∈ ↑l.Tail → ↑x a = true) = (a ∈ ↑l.Tail → SwapTrue o (↑x) a = true)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: 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
i : I
⊢ (i ∈ ↑l.Tail → ↑x i = true) = (i ∈ ↑l.Tail → SwapTrue o (↑x) i = true)

Tactic:
apply forall_congr

Goal state after:
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
i : I
⊢ i ∈ ↑l.Tail → (↑x i = true) = (SwapTrue o (↑x) i = true)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
⊢ Products.isGood (C' C ho) (↑l).Tail

Tactic:
intro h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
h : Products.eval (C' C ho) (↑l).Tail ∈ Submodule.span ℤ (Products.eval (C' C ho) '' {m | m < (↑l).Tail})
⊢ False
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this✝ : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
this :
  (Linear_CC' C hsC ho) (Products.eval C ↑l) =
    (Linear_CC' C hsC ho) (m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
⊢ False

Tactic:
← LinearMap.sub_mem_ker_iff,

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this✝ : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
this : (Products.eval C ↑l - m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) ∈ (Linear_CC' C hsC ho).ker
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
⊢ False
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
exact norm_lt_iff_of_compactlySupported h hM

Goal state after:
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋯
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
⊢ a ∈ ⋃ i, closure[inst✝³] {x (i + (k + 1))}

Tactic:
suffices h : closure (x '' Ici (k + 1)) ⊆ ⋃ i, closure {x (i + (k + 1))} from
    h <| mapClusterPt_atTop_iff_forall_mem_closure.1 ha.2 (k + 1)

Goal state after:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
⊢ closure[inst✝³] (x '' Ici (k + 1)) ⊆ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
⊢ LinearIndependent ℤ (eval (C' C ho)) →
    LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) ↦ Products.eval (C' C ho) (↑l).Tail

Tactic:
intro h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
h : LinearIndependent ℤ (eval (C' C ho))
⊢ LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) ↦ Products.eval (C' C ho) (↑l).Tail
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsInducing ⇑(productOfMemOpens X)

Tactic:
convert! inducing_iInf_to_pi fun (u : Opens X) (x : X) => x ∈ u

Goal state after:
case e'_3
X : Type u_1
inst✝ : TopologicalSpace X
⊢ inst✝ = ⨅ i, induced (fun x ↦ x ∈ i) inferInstance
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ 𝓝 l = l.lift' fun s ↦ {l' | s ∈ l'}

Tactic:
simpa only [Function.comp_def, Iic_principal] using nhds_eq l

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

Goal state before:
pp: case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
⊢ x ∈ some '' Metric.eball a r → x ∈ Metric.eball (some a) r

Tactic:
intro h

Goal state after:
case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
h : x ∈ some '' Metric.eball a r
⊢ x ∈ Metric.eball (some a) r
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case mpr
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
⊢ x ∈ Metric.eball (some a) r → x ∈ some '' Metric.eball a r

Tactic:
intro h

Goal state after:
case mpr
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
h : x ∈ Metric.eball (some a) r
⊢ x ∈ some '' Metric.eball a r
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x y : Option α
xy : edist x y = 0
⊢ x = y

Tactic:
cases x

Goal state after:
case none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
y : Option α
xy : edist none y = 0
⊢ none = y

case some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
y : Option α
val✝ : α
xy : edist (some val✝) y = 0
⊢ some val✝ = y
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case hab
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (logSizeBallSeq J hJ a c i).finset

pp: case hba
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ ¬(logSizeBallSeq J hJ a c i).finset ⊆ (logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
· simp [finset_logSizeBallSeq_add_one]

Goal state after:
case hba
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ ¬(logSizeBallSeq J hJ a c i).finset ⊆ (logSizeBallSeq J hJ a c (i + 1)).finset
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ.right
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 3 / 4 ∈ preCantorSet (n + 1)

Tactic:
· -- goal: 3 / 4 ∈ preCantorSet (n + 1)
      -- follows by the inductive hypothesis, since 1 / 4 ∈ preCantorSet n
      exact Or.inr ⟨1 / 4, ih.1, by norm_num⟩

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case cons
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
u✝ : List (Set α)
a✝¹ : α
b✝ : Set α
l₁✝ : List α
l₂✝ : List (Set α)
ht : b✝ ∈ 𝓝 a✝¹
a✝ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l₁✝ l₂✝
ih :
  ∀ (s : Set (List α)), sequence l₂✝ ⊆ s → ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l₁✝ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b✝ :: l₂✝) ⊆ s
u : Set α
hut : u ⊆ b✝
hu : IsOpen[inst✝] u ∧ a✝¹ ∈ u
⊢ ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) (a✝¹ :: l₁✝) v ∧ sequence v ⊆ s

Tactic:
rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩

Goal state after:
case cons
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
u✝ : List (Set α)
a✝¹ : α
b✝ : Set α
l₁✝ : List α
l₂✝ : List (Set α)
ht : b✝ ∈ 𝓝 a✝¹
a✝ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l₁✝ l₂✝
ih :
  ∀ (s : Set (List α)), sequence l₂✝ ⊆ s → ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l₁✝ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b✝ :: l₂✝) ⊆ s
u : Set α
hut : u ⊆ b✝
hu : IsOpen[inst✝] u ∧ a✝¹ ∈ u
v : List (Set α)
hv : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l₁✝ v
hvss : sequence v ⊆ sequence l₂✝
⊢ ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) (a✝¹ :: l₁✝) v ∧ sequence v ⊆ s
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ Tendsto (fun p ↦ p.2.insertIdx (n + 1) p.1) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 ((a' :: l).insertIdx (n + 1) a))

Tactic:
have : 𝓝 a ×ˢ 𝓝 (a'::l) =
        (𝓝 a ×ˢ (𝓝 a' ×ˢ 𝓝 l)).map fun p : α × α × List α => (p.1, p.2.1::p.2.2) := by
      simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]
      simp [-Filter.map_def, Function.comp_def, functor_norm]
    rw [this, tendsto_map'_iff]
    exact
      (tendsto_fst.comp tendsto_snd).cons
        ((@tendsto_insertIdx' _ n l).comp <| tendsto_fst.prodMk <| tendsto_snd.comp tendsto_snd)

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
⊢ Path.Homotopic (toLoop i p) (toLoop i q) → Homotopic p q

Tactic:
by
  refine Nonempty.map fun H ↦ ⟨⟨homotopyFrom i H, ?_, ?_⟩, ?_⟩
  pick_goal 3
  · rintro t y ⟨j, jH⟩
    erw [homotopyFrom_apply]
    obtain rfl | h := eq_or_ne j i
    · simp only [Prod.map_apply, id_eq, funSplitAt_apply, Function.uncurry_apply_pair]
      rw [H.eq_fst]
      exacts [congr_arg p ((Cube.splitAt j).left_inv _), jH]
    · rw [p.2 _ ⟨j, jH⟩]; apply boundary; exact ⟨⟨j, h⟩, jH⟩
  all_goals
    intro
    apply (homotopyFrom_apply _ _ _).trans
    simp only [Prod.map_apply, id_eq, funSplitAt_apply,
      Function.uncurry_apply_pair, ContinuousMap.HomotopyWith.apply_zero,
      ContinuousMap.HomotopyWith.apply_one, ne_eq, Path.coe_toContinuousMap]
    first
    | apply congr_arg p
    | apply congr_arg q
    apply (Cube.splitAt i).left_inv

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

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f = 0 → ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
intro h

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f = 0
⊢ ∀ (x₁ x₂ : X), f x₁ = f x₂
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ (∀ (x₁ x₂ : X), f x₁ = f x₂) → eHolderNorm r f = 0

Tactic:
intro h

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
⊢ eHolderNorm r f = 0
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬c = 0
hf : eHolderNorm r f = ∞
⊢ ¬MemHolder r f

Tactic:
intro h

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬c = 0
hf : eHolderNorm r f = ∞
h : MemHolder r f
⊢ False
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ 0 ≤ dist x y

Tactic:
cases x

Goal state after:
case toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x✝ : X
⊢ 0 ≤ dist (toSnowflaking x✝) y
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ edist x y = ENNReal.ofReal (dist x y)

Tactic:
cases x

Goal state after:
case toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x✝ : X
⊢ edist (toSnowflaking x✝) y = ENNReal.ofReal (dist (toSnowflaking x✝) y)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ dist (ofSnowflaking x) (ofSnowflaking y) = dist x y ^ α⁻¹

Tactic:
cases x

Goal state after:
case toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x✝ : X
⊢ dist (ofSnowflaking (toSnowflaking x✝)) (ofSnowflaking y) = dist (toSnowflaking x✝) y ^ α⁻¹
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
y : ↥(lp (fun n ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam univ + 1 + diam univ
hzy : Ψ z = y
DΦ : diam (range Φ) = diam univ
DΨ : diam (range Ψ) = diam univ
⊢ diam (range Φ) + dist (Φ xX) (Ψ z) + diam (range Ψ) ≤ diam univ + (diam univ + 1 + diam univ) + diam univ

Tactic:
rw [DΦ, DΨ]
          gcongr

Goal state after: