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

Goal state before:
pp: case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ↑j = 0 ∨ (insertAt i) (t₀, t) ↑j = 1

Tactic:
funSplitAt_symm_apply,

Goal state after:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (if h : ↑j = i then (t₀, t).1 else (t₀, t).2 ⟨↑j, ⋯⟩) = 0 ∨ (if h : ↑j = i then (t₀, t).1 else (t₀, t).2 ⟨↑j, ⋯⟩) = 1
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case h
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 y : ↑I
yH : y ∈ {0, 1}
y✝ : { j // j ≠ i } → ↑I
⊢ (Cube.insertAt i) ((t, y).2, y✝) i = 0 ∨ (Cube.insertAt i) ((t, y).2, y✝) i = 1

Tactic:
funSplitAt_symm_apply,

Goal state after:
case h
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 y : ↑I
yH : y ∈ {0, 1}
y✝ : { j // j ≠ i } → ↑I
⊢ (if h : i = i then ((t, y).2, y✝).1 else ((t, y).2, y✝).2 ⟨i, ⋯⟩) = 0 ∨
    (if h : i = i then ((t, y).2, y✝).1 else ((t, y).2, y✝).2 ⟨i, ⋯⟩) = 1
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : hausdorffEDist s t < δ
⊢ (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 < δ}

Tactic:
rw [hausdorffEDist, max_lt_iff] at h

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
⊢ (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 < δ}
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ ∃ x₀, J = {x₀}

Tactic:
by
      rw [← Finset.card_eq_one]
      refine le_antisymm ?_ ?_
      · suffices (#J : ENNReal) ≤ 1 by norm_cast at this
        refine hJ_card.trans ?_
        conv_rhs => rw [← one_pow n]
        exact ENNReal.pow_le_pow_left ha1
      · rwa [Finset.one_le_card, ← Finset.nonempty_coe_sort]

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

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist x ↑t + hausdorffEDist ↑t ↑s ≤ infEDist y ↑t + edist x y + hausdorffEDist ↑t ↑s

Tactic:
gcongr; apply infEDist_le_infEDist_add_edist

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

Goal state before:
pp: α : 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
⊢ ∀ (n : ℕ), B n ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: case refine_2
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
⊢ ⨅ x, (↑x).encard = coveringNumber ε A

Tactic:
simp_rw [iInf_subtype, iInf_and]

Goal state after:
case refine_2
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
⊢ ⨅ i, ⨅ (_ : i ⊆ A), ⨅ (_ : IsCover ε A i), i.encard = coveringNumber ε A
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
D s : ℝ≥0
A : Set X
hs : s ≤ r
hA : ∀ ⦃x : X⦄, x ∈ A → ∀ ⦃y : X⦄, y ∈ A → edist x y ≤ ↑D
hf : ∃ C, HolderWith C r (A.domRestrict f)
⊢ ∃ C, HolderWith C s (A.domRestrict f)

Tactic:
let := PseudoEMetricSpace.toPseudoMetricSpace
    fun x y : A ↦ ne_top_of_le_ne_top ENNReal.coe_ne_top (hA x.2 y.2)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
D s : ℝ≥0
A : Set X
hs : s ≤ r
hA : ∀ ⦃x : X⦄, x ∈ A → ∀ ⦃y : X⦄, y ∈ A → edist x y ≤ ↑D
hf : ∃ C, HolderWith C r (A.domRestrict f)
this : PseudoMetricSpace ↑A := PseudoEMetricSpace.toPseudoMetricSpace ⋯
⊢ ∃ C, HolderWith C s (A.domRestrict f)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 ∈ s →
      ∀ (y : α), y = x ∨ y ∈ s → x_1 ≠ y → ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist x_1 y ∨ s.einfsep ≤ edist x_1 y

Tactic:
rintro y (rfl | hy) z (rfl | hz) hyz

Goal state after:
case inl.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
z : α
hyz : z ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z z ∨ s.einfsep ≤ edist z z

case inl.inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y_1 ∈ s, ⨅ (_ : y ≠ y_1), edist y y_1 ≤ edist y z ∨ s.einfsep ≤ edist y z

case inr.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist y z ∨ s.einfsep ≤ edist y z

case inr.inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
y : α
hy : y ∈ s
z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist y z ∨ s.einfsep ≤ edist y z
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
hs : ¬s.Nontrivial
⊢ d ≤ dist x y

Tactic:
· rw [not_nontrivial_iff] at hs
    rw [hs.infsep_zero] at hd
    exact le_trans hd dist_nonneg

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
D : Set (Set α)
inst✝ : Preorder α
s t : Set α
hs :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
ht :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ t → ∃ b ∈ d, Ici b ∩ d ⊆ t
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hd₃ : IsLUB d a
ha : a ∈ s ∩ t
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t

Tactic:
by
    obtain ⟨b₁, hb₁d, hb₁ds⟩ := hs hd₀ hd₁ hd₂ hd₃ ha.1
    obtain ⟨b₂, hb₂d, hb₂dt⟩ := ht hd₀ hd₁ hd₂ hd₃ ha.2
    obtain ⟨c, hcd, hc⟩ := hd₂ b₁ hb₁d b₂ hb₂d
    exact ⟨c, hcd, fun e ⟨hce, hed⟩ ↦ ⟨hb₁ds ⟨hc.1.trans hce, hed⟩, hb₂dt ⟨hc.2.trans hce, hed⟩⟩⟩

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✝⁵ : FunLike F α β
inst✝⁴ : PartialOrder α
inst✝³ : OrderTop α
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : PseudoEpimorphismClass F α β
f : F
⊢ f ⊤ = ⊤

Tactic:
let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ <| f ⊤)

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁵ : FunLike F α β
inst✝⁴ : PartialOrder α
inst✝³ : OrderTop α
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : PseudoEpimorphismClass F α β
f : F
b : α
h : ⊤ ≤ b ∧ f b = ⊤
⊢ f ⊤ = ⊤
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨s_x, hs_x : ((stalkFunctor C x).map T) s_x = t_x⟩ := hT x t_x

Goal state after:
case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
s_x : CC ((stalkFunctor C x).obj ℱ)
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) s_x = t_x
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
i : ι
⊢ res F U ≫ limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) { as := i } = F.map (leSupr U i).op

Tactic:
rw [res, limit.lift_π, Fan.mk_π_app]

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint hZ_irred.genericPoint Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
hi_cmpt : IsCompact i
⊢ hZ_irred.genericPoint ∈ i

Tactic:
rw [hη.mem_open_set_iff (by grind [hB.prop, constructibleTopologySubbasis]), Set.inter_comm]

Goal state after:
case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint hZ_irred.genericPoint Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
hi_cmpt : IsCompact i
⊢ (i ∩ Z).Nonempty
Module: Mathlib.Topology.UniformSpace.Dini

Goal state before:
pp: case eq_bot
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
h : atTop = ⊥
⊢ TendstoLocallyUniformly F f atTop

pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
⊢ TendstoLocallyUniformly F f atTop

Tactic:
case eq_bot => simp [h, tendstoLocallyUniformly_iff_forall_tendsto]

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
⊢ TendstoLocallyUniformly F f atTop
Module: Mathlib.Topology.UniformSpace.Dini

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e ↦ ‖F e x - f x‖) atTop (𝓝 0)
n : ι
hn : ‖F n x - f x‖ < ε
⊢ ∀ᶠ (n_1 : ι) in atTop, ∀ y ∈ {y | ‖F n y - f y‖ < ε}, ‖F n_1 y - f y‖ < ε

Tactic:
filter_upwards [eventually_ge_atTop n] with m hnm z hz

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e ↦ ‖F e x - f x‖) atTop (𝓝 0)
n : ι
hn : ‖F n x - f x‖ < ε
m : ι
hnm : n ≤ m
z : α
hz : ‖F n z - f z‖ < ε
⊢ ‖F m z - f z‖ < ε
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: X : Type u_1
this : UniformSpace X := ⊤
⊢ IsUltraUniformity X

Tactic:
have := Filter.hasBasis_top (α := (X × X))

Goal state after:
X : Type u_1
this✝ : UniformSpace X := ⊤
this : ⊤.HasBasis (fun x ↦ True) fun x ↦ Set.univ
⊢ IsUltraUniformity X
Module: Mathlib.Topology.UniformSpace.Uniformizable

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
c u : Set X
IsThickeningcu : IsThickening c u
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ IsThickening c v ∧ IsThickening (closure v) u

Tactic:
obtain ⟨x, uc, s, huc, ucu, rfl, hn, hs⟩ := IsThickeningcu
  obtain ⟨(ds : SetRel X X), hdsu, hdso, -, hdsd⟩ := comp_open_symm_mem_uniformity_sets hs
  have ho : IsOpen (ds ○ uc ○ ds) := (hdso.relComp huc).relComp hdso
  have hsub := calc ds ○ (ds ○ uc ○ ds) ○ ds
    _ = (ds ○ ds) ○ uc ○ (ds ○ ds) := by simp [comp_assoc]
    _ ⊆ s ○ uc ○ s := comp_subset_comp (comp_subset_comp_left hdsd) hdsd
  replace hsub := (ball_mono hsub x).trans hn
  have : ds.IsRefl := id_subset_iff.1 (refl_le_uniformity hdsu)
  refine ⟨ball x (ds ○ uc ○ ds), isOpen_ball x ho, ?_, subset_trans ?_ hsub,
      ⟨x, uc, ds, huc, ucu, rfl, subset_rfl, hdsu⟩,
      ⟨x, ds ○ uc ○ ds, ds, ho, mem_of_superset ucu (right_subset_comp.trans left_subset_comp),
        rfl, hsub, hdsu⟩⟩ <;>
  · refine closure_ball_subset.trans (ball_mono ?_ x)
    rw [closure_eq_inter_uniformity]
    exact iInter₂_subset_of_subset ds hdsu (by simp [comp_assoc])

Goal state after:
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: