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

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n✝ n : ℕ
ih :
  (p : Fin (n + 1) → X) →
    (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) →
      ((k : Fin n) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)
p : Fin (n + 1 + 1) → X
F G : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
H : (k : Fin (n + 1)) → (F k).Homotopy (G k)
⊢ (concat p F).Homotopy (concat p G)

Tactic:
concat_succ,

Goal state after:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n✝ n : ℕ
ih :
  (p : Fin (n + 1) → X) →
    (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) →
      ((k : Fin n) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)
p : Fin (n + 1 + 1) → X
F G : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
H : (k : Fin (n + 1)) → (F k).Homotopy (G k)
⊢ ((concat (p ∘ castSucc) fun k ↦ F k.castSucc).trans (F (last n))).Homotopy (concat p G)
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s

Tactic:
by
  rw [UniformSpace.mem_nhds_iff]
  constructor
  · rintro ⟨V, V_in, V_sub⟩
    rw [IsUltraUniformity.hasBasis.mem_iff'] at V_in
    obtain ⟨U, ⟨U_in, U_sym, U_trans⟩, U_sub⟩ := V_in
    refine ⟨U, U_in, U_sym, U_trans, (UniformSpace.ball_mono U_sub _).trans V_sub⟩
  · rintro ⟨V, V_in, _, _, V_sub⟩
    exact ⟨V, V_in, V_sub⟩

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

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
⊢ ∃ v,
    IsOpen v ∧
      closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : Fintype ι
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₁)
inst✝¹² : (x : B) → TopologicalSpace (E₁ x)
inst✝¹¹ : FiberBundle F₁ E₁
inst✝¹⁰ : VectorBundle 𝕜 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✝² : VectorBundle 𝕜 F₂ E₂
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
b : B
⊢ IsInducing (↑(continuousAlternatingMap 𝕜 ι (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) ∘ TotalSpace.mk b)

Tactic:
by
    simp only [Function.comp_def, continuousAlternatingMap_apply, isInducing_const_prod]
    let L₁ : E₁ b ≃L[𝕜] F₁ :=
      (trivializationAt F₁ E₁ b).continuousLinearEquivAt 𝕜 b
        (mem_baseSet_trivializationAt _ _ _)
    let L₂ : E₂ b ≃L[𝕜] F₂ :=
      (trivializationAt F₂ E₂ b).continuousLinearEquivAt 𝕜 b
        (mem_baseSet_trivializationAt _ _ _)
    convert! (L₁.continuousAlternatingMapCongr L₂).toHomeomorph.isInducing
    ext f
    simp [Trivialization.linearMapAt_def_of_mem _ (mem_baseSet_trivializationAt _ _ _), L₁, L₂,
      Function.comp_def, mem_baseSet_trivializationAt]

Goal state after: