mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ Homotopic p q → Path.Homotopic (toLoop i p) (toLoop i q)

Tactic:
refine Nonempty.map fun H ↦ ⟨⟨⟨fun t ↦ ⟨homotopyTo i H t, ?_⟩, ?_⟩, ?_, ?_⟩, ?_⟩

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
⊢ (homotopyTo i H) t ∈ Ω^ { j // j ≠ i } X x

case refine_2
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)
⊢ Continuous fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩

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_1 : ↑I),
    { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ?refine_2 }.toFun (0, x_1) =
      (toLoop i p).toContinuousMap x_1

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 := ?refine_2 }.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 := ?refine_2, map_zero_left := ?refine_3,
                    map_one_left := ?refine_4 }.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
inst✝ : TopologicalSpace α
⊢ 𝓝 [] = pure []

Tactic:
by
  rw [nhds_list, List.traverse_nil _]

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

Goal state before:
pp: case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ ↑ε
h_nonempty : A.Nonempty
⊢ externalCoveringNumber ε A ≤ 1

Tactic:
· exact (externalCoveringNumber_eq_one_of_ediam_le h_nonempty hA).le

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
⊢ Tendsto s atTop (𝓝 t)

Tactic:
refine EMetric.tendsto_atTop.2 fun ε εpos => ?_

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, edist (s n) t < ε
Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff

Goal state before:
pp: X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
g : X ≃ₜ ↑KH := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
⊢ ∃ f, Continuous f ∧ Function.Surjective f

Tactic:
obtain ⟨f, hf_continuous, hf_surjective⟩ := exists_retractionCantorSet hKC_closed
    <| Set.Nonempty.preimage (Set.range_nonempty emb) cantorToHilbert_surjective

Goal state after:
X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
g : X ≃ₜ ↑KH := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
⊢ ∃ f, Continuous f ∧ Function.Surjective f
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
s : (b : β) → Set (X b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → X i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → X i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
i : β
hi : x i ≠ y i
⊢ c ≤ edist x y

Tactic:
exact le_trans (le_einfsep_iff.1 (h i) _ (hx _) _ (hy _) hi) (edist_le_pi_edist _ _ i)

Goal state after:
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
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
I :
  (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)) =
    (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y)))
f : X ≃ᵢ ↑(range (kuratowskiEmbedding X))
g : ↑(range (kuratowskiEmbedding Y)) ≃ᵢ Y
⊢ Nonempty (X ≃ᵢ Y)

Tactic:
exact ⟨f.trans <| (cast I e).trans g⟩

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set (Snowflaking X α hα₀ hα₁)
⊢ ediam (⇑toSnowflaking ⁻¹' s) = ediam s ^ α⁻¹

Tactic:
by
  rw [← image_ofSnowflaking_eq_preimage, ediam_image_ofSnowflaking]

Goal state after:
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
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q

Tactic:
let f : X ⊕ Y → ℓ_infty_ℝ := fun x =>
      match x with
      | inl y => Φ y
      | inr z => Ψ z

Goal state after:
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
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (y, r), ⋯⟩

Tactic:
by_cases hx : IsPredPrelimit x
      · obtain ⟨z, hz, hz'⟩ := hx.lt_iff_exists_lt.1 h
        use some z
        simp [some, Prod.Lex.lt_iff, hz', hz]
      obtain ⟨s, hs⟩ := exists_gt (max 0 q)
      rw [max_lt_iff] at hs
      refine ⟨⟨toLex (x, s), ?_⟩, ?_⟩
      · simp [hx, hs.1.le]
      · simp [Prod.Lex.lt_iff, hs.2, h]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ ∀ (a : α) (b : ℚ) (b_1 : (IsSuccPrelimit a → 0 ≤ b) ∧ (IsPredPrelimit a → b ≤ 0)),
    IsOpen (⇑some ⁻¹' Ioi ⟨toLex (a, b), b_1⟩) ∧ IsOpen (⇑some ⁻¹' Iio ⟨toLex (a, b), b_1⟩)

Tactic:
refine fun x q ⟨hx₁, hx₂⟩ ↦ ⟨?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)

case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)
Module: Mathlib.Topology.Order.LawsonTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 ↦ ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen[scott α univ] U}
⊢ IsTopologicalBasis (lawsonBasis α)

Tactic:
rw [lawsonBasis_image2]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 ↦ ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen[scott α univ] U}
⊢ IsTopologicalBasis
    (image2 (fun x x_1 ↦ ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen[scott α univ] U})
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.{w, v} C
inst✝ : HasTerminal C
A : C
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
h : p₀ ∈ unop V
⊢ (if p₀ ∈ unop U then A else ⊤_ C) = if p₀ ∈ unop V then A else ⊤_ C

Tactic:
if_pos h,

Goal state after:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
h : p₀ ∈ unop V
⊢ (if p₀ ∈ unop U then A else ⊤_ C) = A
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
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, p₀ ∉ ↑U :=
  match not_specializes_iff_exists_open.mp h with
  | Exists.intro U ⟨ho, ⟨h₀, hy⟩⟩ => Exists.intro ⟨{ carrier := U, is_open' := ho }, h₀⟩ hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), (skyscraperPresheafCocone p₀ A y).ι.app j ≫ f = c.ι.app j
⊢ f = eqToHom ⋯ ≫ c.ι.app (op h1.choose)

Tactic:
← Category.id_comp f,

Goal state after:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, p₀ ∉ ↑U :=
  match not_specializes_iff_exists_open.mp h with
  | Exists.intro U ⟨ho, ⟨h₀, hy⟩⟩ => Exists.intro ⟨{ carrier := U, is_open' := ho }, h₀⟩ hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), (skyscraperPresheafCocone p₀ A y).ι.app j ≫ f = c.ι.app j
⊢ 𝟙 (skyscraperPresheafCocone p₀ A y).pt ≫ f = eqToHom ⋯ ≫ c.ι.app (op h1.choose)
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' : j = ↑((E q) (Ψ y))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
⊢ ↑((F q).snd ((E q) (Ψ x)) ((E q) (Ψ y))) = min M ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊

Tactic:
by simp only [F, (E q).symm_apply_apply]

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

Goal state before:
pp: X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = fV ⟨x, ⋯⟩
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
wUx : fU ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U' x ⋯)) gU
⊢ ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)

Tactic:
clear wUx

Goal state after:
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = fV ⟨x, ⋯⟩
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
⊢ ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
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
b : β
y : ↑Y
hfy : LowerSemicontinuousOn (fun x ↦ f x ↑y) X
⊢ IsClosed (sublevelLeft X f b ↑y)

Tactic:
rw [← lowerSemicontinuous_restrict_iff, lowerSemicontinuous_iff_isClosed_preimage] at hfy

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
b : β
y : ↑Y
hfy : ∀ (y_1 : β), IsClosed ((X.domRestrict fun x ↦ f x ↑y) ⁻¹' Iic y_1)
⊢ IsClosed (sublevelLeft X f b ↑y)
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Epi (terminalIsTerminal.from A)
U V : (Opens ↑X)ᵒᵖ
r : U ⟶ V
⊢ Epi ((skyscraperSheaf p₀ A).obj.map r)

Tactic:
by_cases h1 : p₀ ∈ unop U

Goal state after:
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Epi (terminalIsTerminal.from A)
U V : (Opens ↑X)ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
⊢ Epi ((skyscraperSheaf p₀ A).obj.map r)

case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Epi (terminalIsTerminal.from A)
U V : (Opens ↑X)ᵒᵖ
r : U ⟶ V
h1 : p₀ ∉ unop U
⊢ Epi ((skyscraperSheaf p₀ A).obj.map r)
Module: Mathlib.Topology.Sion

Goal state before:
pp: case insert.inr
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
s✝ : Set F
t : β
b : F
s : Set F
a✝ : b ∉ s
hs : s.Finite
hrec :
  ∀ {X : Set E},
    X.Nonempty →
      IsCompact X →
        (∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X) →
          (∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y) →
            (∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y) →
              (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y) →
                Convex ℝ X → s ⊆ Y → (∀ x ∈ X, ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
X : Set 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
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun x ↦ f x b) ⁻¹' Iic t
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
have kX' : IsCompact X' := (hfy b hb).isCompact_inter_preimage_Iic kX t

Goal state after:
case insert.inr
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
s✝ : Set F
t : β
b : F
s : Set F
a✝ : b ∉ s
hs : s.Finite
hrec :
  ∀ {X : Set E},
    X.Nonempty →
      IsCompact X →
        (∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X) →
          (∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y) →
            (∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y) →
              (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y) →
                Convex ℝ X → s ⊆ Y → (∀ x ∈ X, ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
X : Set 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
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun x ↦ f x b) ⁻¹' Iic t
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: case intro.refine_2
𝕜 : Type u_1
ι : Type u_2
inst✝²² : NontriviallyNormedField 𝕜
B : Type u_3
inst✝²¹ : TopologicalSpace B
F₁ : Type u_4
inst✝²⁰ : NormedAddCommGroup F₁
inst✝¹⁹ : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst✝¹⁸ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁷ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁵ : NormedAddCommGroup F₂
inst✝¹⁴ : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst✝¹³ : (x : B) → AddCommGroup (E₂ x)
inst✝¹² : (x : B) → Module 𝕜 (E₂ x)
inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁰ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁷ : FiberBundle F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁶ : Finite ι
inst✝⁵ : VectorBundle 𝕜 F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
val✝ : Fintype ι
⊢ ContinuousOn (fun b ↦ ContinuousAlternatingMap.compContinuousLinearMapCLM ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
refine ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM.comp_continuousOn ?_
    exact continuousOn_coordChange 𝕜 e₁' e₁ |>.mono (by mfld_set_tac)

Goal state after:
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝²² : NontriviallyNormedField 𝕜
B : Type u_3
inst✝²¹ : TopologicalSpace B
F₁ : Type u_4
inst✝²⁰ : NormedAddCommGroup F₁
inst✝¹⁹ : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst✝¹⁸ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁷ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁵ : NormedAddCommGroup F₂
inst✝¹⁴ : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst✝¹³ : (x : B) → AddCommGroup (E₂ x)
inst✝¹² : (x : B) → Module 𝕜 (E₂ x)
inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁰ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁷ : FiberBundle F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁶ : Finite ι
inst✝⁵ : VectorBundle 𝕜 F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
⊢ ContinuousOn (continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
cases nonempty_fintype ι
  simp +unfoldPartialApp only [continuousAlternatingMapCoordChange,
    ContinuousLinearEquiv.coe_continuousAlternatingMapCongr, ContinuousLinearEquiv.symm_symm]
  refine .clm_comp ?_ ?_
  · refine map_continuous (ContinuousLinearMap.compContinuousAlternatingMapCLM (ι := ι) 𝕜 F₁ F₂ F₂)
      |>.comp_continuousOn ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)
    mfld_set_tac
  · refine ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM.comp_continuousOn ?_
    exact continuousOn_coordChange 𝕜 e₁' e₁ |>.mono (by mfld_set_tac)

Goal state after: