mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ ((homotopyTo i✝ H) t) y = x

Tactic:
homotopyTo_apply,

Goal state after:
case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ H (t.1, (Cube.insertAt i✝) (t.2, y)) = x
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case inr
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h : ofDigits a = ofDigits b
n1 : ℕ
h1 : ∀ n < n1, a n = b n
h2 : a n1 ≠ b n1
this :
  ∀ {a b : ℕ → Fin 3},
    (∀ (n : ℕ), a n ≠ 1) →
      (∀ (n : ℕ), b n ≠ 1) → ofDigits a = ofDigits b → (∀ n < n1, a n = b n) → a n1 ≠ b n1 → a n1 = 0 ∧ b n1 = 2 → False
h3 : ¬(a n1 = 0 ∧ b n1 = 2)
⊢ False

pp: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h : ofDigits a = ofDigits b
h1 : ∀ n < n1, a n = b n
h2 : a n1 ≠ b n1
h3 : a n1 = 0 ∧ b n1 = 2
⊢ False

Tactic:
· exact this hb ha h.symm (fun n hn ↦ (h1 n hn).symm) h2.symm (by grind)

Goal state after:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h : ofDigits a = ofDigits b
h1 : ∀ n < n1, a n = b n
h2 : a n1 ≠ b n1
h3 : a n1 = 0 ∧ b n1 = 2
⊢ False
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ ((homotopyTo i H) (0, x✝)) y✝ = ((toLoop i p) x✝) y✝

pp: case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (x_1 : ↑I),
    { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x_1) =
      (toLoop i q).toContinuousMap x_1

pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ?refine_4 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1

Tactic:
homotopyTo_apply,

Goal state after:
case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = ((toLoop i p) x✝) y✝

case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (x_1 : ↑I),
    { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x_1) =
      (toLoop i q).toContinuousMap x_1

case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ?refine_4 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ ((homotopyTo i H) (1, x✝)) y✝ = ((toLoop i q) x✝) y✝

pp: case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1

Tactic:
homotopyTo_apply,

Goal state after:
case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((1, x✝).1, (Cube.insertAt i) ((1, x✝).2, y✝)) = ((toLoop i q) x✝) y✝

case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology α
⊢ DiscreteTopology (List α)

Tactic:
by
  rw [discreteTopology_iff_nhds]; intro l; induction l <;> simp [*, nhds_cons]

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝² : Add R
inst✝¹ : Zero R
inst✝ : Preorder R
d : PseudoMetric X R
ε : R
⊢ ∀ (a b : X), (a, b) ∈ {xy | d xy.1 xy.2 < ε} → (b, a) ∈ {xy | d xy.1 xy.2 < ε}

Tactic:
simp [d.symm]

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝² : Add R
inst✝¹ : Zero R
inst✝ : LE R
d : PseudoMetric X R
ε : R
⊢ ∀ (a b : X), (a, b) ∈ {xy | d xy.1 xy.2 ≤ ε} → (b, a) ∈ {xy | d xy.1 xy.2 ≤ ε}

Tactic:
simp [d.symm]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ ContinuousAt (eraseIdx i) ⟨l, hl⟩

Tactic:
by
    rw [ContinuousAt, Vector.eraseIdx, tendsto_subtype_rng]
    simp only [Vector.eraseIdx_val]
    exact Tendsto.comp List.tendsto_eraseIdx continuousAt_subtype_val

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 j : N
f g : ↑(Ω^ N X x)
⊢ ⟦transAt i f g⟧ = ⟦transAt j f g⟧

Tactic:
simp_rw [← fromLoop_trans_toLoop]

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f g : ↑(Ω^ N X x)
⊢ ⟦fromLoop i (Path.trans (toLoop i f) (toLoop i g))⟧ = ⟦fromLoop j (Path.trans (toLoop j f) (toLoop j g))⟧
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty { s // s ⊆ A ∧ IsCover ε A s }
C : { s // s ⊆ A ∧ IsCover ε A s }
hC : (↑C).encard = ⨅ x, (↑x).encard
⊢ ∃ a, (a ⊆ A ∧ IsCover ε A a) ∧ a.Finite

Tactic:
exact ⟨C', ⟨hC'_subset, hC'_cover⟩, hC'_fin⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = packingNumber ε A

Tactic:
by
  rcases Set.eq_empty_or_nonempty A with hA | hA
  · simp [hA, packingNumber]
  have : Nonempty { s : Set X // s ⊆ A ∧ IsSeparated ε s } := by
    obtain ⟨a, ha⟩ := hA
    exact ⟨⟨{a}, by simp [ha], by simp⟩⟩
  let h_exists := ENat.exists_eq_iSup_of_lt_top
    (f := fun C : { s : Set X // s ⊆ A ∧ IsSeparated ε s } ↦ (C : Set X).encard)
  simp_rw [packingNumber] at h ⊢
  simp_rw [iSup_subtype, iSup_and] at h_exists
  specialize h_exists h.lt_top
  obtain ⟨C, hC⟩ := h_exists
  refine ⟨C, C.2.1, ?_, C.2.2, ?_⟩
  · refine Set.encard_ne_top_iff.mp ?_
    rwa [hC]
  · rw [hC]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep ≠ ∞

Tactic:
by
  contrapose! hs
  exact subsingleton_of_einfsep_eq_top hs

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
hs : s.offDiag = ∅
⊢ (↑s).infsep = 0

Tactic:
← Finset.not_nonempty_iff_eq_empty

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
hs : ¬s.offDiag.Nonempty
⊢ (↑s).infsep = 0
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: X✝ : Type u_1
inst✝ : TopologicalSpace X✝
L : Locale
X : TopCat
u : ↑(Opposite.unop (topToLocale.obj X))
⊢ IsOpen (localePointOfSpacePoint ↑X ⁻¹' {x | x u})

Tactic:
simpa using! u.2

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

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ dist x (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z) = dist x y + dist y z

Tactic:
y.toGHSpace_rep,

Goal state after:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ dist x y + dist y (toGHSpace Z) = dist x y + dist y z
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: X : TopCat
p₀ : ↑X
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : Abelian C
inst✝ : HasColimits C
⊢ (Presheaf.stalkFunctor C p₀).Additive

Tactic:
dsimp [Presheaf.stalkFunctor]
  have : ((Functor.whiskeringLeft _ _ C).obj (OpenNhds.inclusion p₀).op).Additive := ⟨by cat_disch⟩
  infer_instance

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ ((OpenNhds.inclusion p₀).op ⋙ 𝓕).map inc ≫ f.app ((OpenNhds.inclusion p₀).op.obj V) ≫ eqToHom ⋯ =
    (f.app ((OpenNhds.inclusion p₀).op.obj U) ≫ eqToHom ⋯) ≫ ((Functor.const (OpenNhds p₀)ᵒᵖ).obj c).map inc

Tactic:
by
          dsimp only [Functor.const_obj_map, Functor.const_obj_obj, Functor.comp_map,
            Functor.comp_obj, Functor.op_obj, skyscraperPresheaf_obj]
          rw [Category.comp_id, ← Category.assoc, comp_eqToHom_iff, Category.assoc,
            eqToHom_trans, f.naturality, skyscraperPresheaf_map]
          have hV : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop := V.unop.2
          simp only [dif_pos hV]

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X✝ : TopCat
p₀ : ↑X✝
inst✝³ : (U : Opens ↑X✝) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
h : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j✝)
⊢ (X.germ ((OpenNhds.inclusion p₀).obj (unop j✝)) p₀ ⋯ ≫ 𝟙 (X.stalk p₀) ≫ eqToHom ⋯) ≫
      colimit.ι ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) j✝ ≫
        (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝

Tactic:
simp [skyscraperPresheafStalkOfSpecializes]
      rfl

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

Goal state before:
pp: δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
⊢ j = ↑((E q) (Ψ y))

Tactic:
simp only [j, Ψ, Equiv.apply_symm_apply, Fin.val_cast]

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case neg
X✝ : TopCat
p₀ : ↑X✝
inst✝³ : (U : Opens ↑X✝) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
h : p₀ ∉ (OpenNhds.inclusion p₀).obj (unop j✝)
⊢ (⋯ ▸ terminalIsTerminal).from (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j✝)))) ≫
      colimit.ι ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) j✝ ≫
        (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝

Tactic:
· simp only [skyscraperPresheafStalkOfSpecializes, colimit.isoColimitCocone_ι_hom,
        skyscraperPresheafCoconeOfSpecializes_pt, skyscraperPresheafCoconeOfSpecializes_ι_app,
        Functor.comp_obj, Functor.op_obj, skyscraperPresheaf_obj, Functor.const_obj_obj]
      rw [comp_eqToHom_iff]
      apply ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext

Goal state after:
Module: Mathlib.Topology.Sheaves.EtaleSpace

Goal state before:
pp: case h
X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
y : ↥U
g : ToType (F.stalk x)
V : Opens ↑X
f : ToType (F.obj (op V))
hyV : ↑y ∈ V
hgf : (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑y ⋯)) f
W : Opens ↑X
hyW : ↑y ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW : (ConcreteCategory.hom (F.map ιWU.op)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.map ιWV.op)) f
z : ↥U
hz : z ∈ Subtype.val ⁻¹' ↑W
⊢ (ConcreteCategory.hom (F.germ W (↑z) hz)) ((ConcreteCategory.hom (F.map ιWU.op)) (surjInv ⋯ g)) =
    (ConcreteCategory.hom (F.germ V ↑z ⋯)) f

Tactic:
hW,

Goal state after:
case h
X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
y : ↥U
g : ToType (F.stalk x)
V : Opens ↑X
f : ToType (F.obj (op V))
hyV : ↑y ∈ V
hgf : (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑y ⋯)) f
W : Opens ↑X
hyW : ↑y ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW : (ConcreteCategory.hom (F.map ιWU.op)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.map ιWV.op)) f
z : ↥U
hz : z ∈ Subtype.val ⁻¹' ↑W
⊢ (ConcreteCategory.hom (F.germ W (↑z) hz)) ((ConcreteCategory.hom (F.map ιWV.op)) f) =
    (ConcreteCategory.hom (F.germ V ↑z ⋯)) f
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
⊢ j = ↑((E q) (Ψ y))

Tactic:
simp only [j, Ψ, Equiv.apply_symm_apply, Fin.val_cast]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
⊢ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g ≤ max (⨆ x, ⨅ y, g (inl x, inr y)) (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g

Tactic:
← le_max_right

Goal state after:
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
⊢ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
⊢ False

Tactic:
let J2 := φ ⁻¹' (setOfPred_sublevelLeft_subset X Y f t t' y2 y1)

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
J2 : Set ↑(segment ℝ ↑y1 ↑y2) := ⇑φ ⁻¹' setOfPred_sublevelLeft_subset X Y f t t' y2 y1
⊢ False
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
p : Fin (n + 2) → X
F : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
⊢ concat p F = (concat (p ∘ castSucc) fun k ↦ F k.castSucc).trans (F (last n))

Tactic:
rw [concat, dfoldl_succ_last]
  rfl

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : E → F
η_mem : ∀ x ∈ X, η x ∈ Y
η_max : ∀ x ∈ X, IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn (fun x ↦ f x (η x)) X
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
obtain ⟨a, ha, ha'⟩ : ∃ a ∈ X, IsMinOn (fun x ↦ f x (η x)) X a := hlsc.exists_isMinOn ne_X kX

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : E → F
η_mem : ∀ x ∈ X, η x ∈ Y
η_max : ∀ x ∈ X, IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn (fun x ↦ f x (η x)) X
a : E
ha : a ∈ X
ha' : IsMinOn (fun x ↦ f x (η x)) X a
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b