mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
j✝ : Discrete (ι × ι)
⊢ (𝟙 (F.obj (op (iSup U))) ≫ Pi.lift fun b ↦ F.map (coconeιApp U (Pairwise.pair b.1 b.2)).op) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    ((Pi.lift fun i ↦ F.map (leSupr U i).op) ≫
        Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝

Tactic:
simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
                Category.assoc]

Goal state after:
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
j✝ : Discrete (ι × ι)
⊢ F.map (coconeιApp U (Pairwise.pair j✝.as.1 j✝.as.2)).op =
    F.map (leSupr U j✝.as.1).op ≫ F.map ((U j✝.as.1).infLELeft (U j✝.as.2)).op
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X n)
inst✝ : ∀ (n : ℕ), Nonempty (X n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
x✝ : ℕ
⊢ 0 < d x✝

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ IsUltraUniformity X

Tactic:
refine .mk_of_hasBasis (h.hasBasis.inf h'.hasBasis) ?_ ?_

Goal state after:
case refine_1
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsSymm (id i.1 ∩ id i.2)

case refine_2
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsTrans (id i.1 ∩ id i.2)
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)
⊢ ∀
    e ∈
      {e |
        ∃ e₁ e₂,
          ∃ (x : MemTrivializationAtlas e₁) (x_1 : MemTrivializationAtlas e₂), e = continuousAlternatingMap 𝕜 ι e₁ e₂},
    ∀
      e' ∈
        {e |
          ∃ e₁ e₂,
            ∃ (x : MemTrivializationAtlas e₁) (x_1 : MemTrivializationAtlas e₂),
              e = continuousAlternatingMap 𝕜 ι e₁ e₂},
      ∃ f,
        ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧
          ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F₁ [⋀^ι]→L[𝕜] F₂), (f b) v = (↑e' { proj := b, snd := e.symm b v }).2

Tactic:
rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩ _ ⟨e₁', e₂', he₁', he₂', rfl⟩
    exact ⟨continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂',
      continuousOn_continuousAlternatingMapCoordChange,
      continuousAlternatingMapCoordChange_apply⟩

Goal state after: