mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Tactic.Lint.Simp
Batteries.Tactic.Lint.SimpTheoremInfo.mk.inj : ∀ {hyps : Array Lean.Expr} {lhs rhs : Lean.Expr} {hyps_1 : Array Lean.Expr} {lhs_1 rhs_1 : Lean.Expr},
  { hyps := hyps, lhs := lhs, rhs := rhs } = { hyps := hyps_1, lhs := lhs_1, rhs := rhs_1 } →
    hyps = hyps_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- An open immersion is an iso if the underlying continuous map is epi.  -/
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.to_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] [h' : CategoryTheory.Epi f.hom.base], CategoryTheory.IsIso f
-- Mathlib.Algebra.Group.Basic
neg_ne_zero : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, -a ≠ 0 ↔ a ≠ 0
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.fromSkeleton_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.InducedCategory C Quotient.out}
  (f : X ⟶ Y), (CategoryTheory.fromSkeleton C).map f = f.hom
-- Std.Async.Basic
Std.Async.instMonadAsyncReaderT : {t m : Type → Type} → {n : Type} → [Std.Async.MonadAsync t m] → Std.Async.MonadAsync t (ReaderT n m)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.smul_comp : ∀ {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {S₃ : Type u_6} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11}
  [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂]
  [inst_8 : Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  [inst_10 : Monoid S₃] [inst_11 : DistribMulAction S₃ M₃] [inst_12 : SMulCommClass R₃ S₃ M₃] (a : S₃)
  (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂), (a • g) ∘ₛₗ f = a • g ∘ₛₗ f
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.inv_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : Inv γ] [inst_4 : ContinuousInv γ] (f : C(β, γ)) (g : C(α, β)),
  f⁻¹.comp g = (f.comp g)⁻¹
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteBooleanAlgebra.toCompleteLattice : {α : Type u_1} → [self : CompleteBooleanAlgebra α] → CompleteLattice α
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.AltExpr.mk : {σ : Type} →
  Lean.Syntax → Option Lean.Elab.Term.Do.Var → Lean.Syntax → Array Lean.Syntax → σ → Lean.Elab.Term.Do.AltExpr σ
-- Mathlib.Data.Set.Piecewise
Set.EqOn.piecewise_ite : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] {f f' g : α → β} {t t' : Set α},
  Set.EqOn f g t → Set.EqOn f' g t' → Set.EqOn (s.piecewise f f') g (s.ite t t')
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.forkMap.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A)
  [inst_2 : CategoryTheory.Limits.HasProducts A],
  CategoryTheory.Presheaf.forkMap R P = CategoryTheory.Limits.Pi.lift fun f => P.map (↑f.snd).op
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.children : Lean.Lsp.Ipc.ModuleHierarchy → Array Lean.Lsp.Ipc.ModuleHierarchy
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_sub_sin : ∀ (x y : ℝ), Real.sin x - Real.sin y = 2 * Real.sin ((x - y) / 2) * Real.cos ((x + y) / 2)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.eq_comp_toLinearMap_iff : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₂₃ : R₂ →+* R₃} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂}
  [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f g : M₂ →ₛₗ[σ₂₃] M₃), f ∘ₛₗ ↑e₁₂ = g ∘ₛₗ ↑e₁₂ ↔ f = g
-- Init.Data.String.Lemmas.FindPos
String.offset_posLE_le : ∀ {s : String} {p : String.Pos.Raw}, (s.posLE p).offset ≤ p
-- Batteries.Data.Vector.Lemmas
Vector.scanr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β → β) (init : β) (as : Vector α n),
  Vector.scanr f init as = (Vector.scanrM (fun x1 x2 => pure (f x1 x2)) init as).run
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- Notation for a prefunctor between quivers.  -/
Prefunctor.«term_⥤q_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_pos_of_pos : ∀ {x : ℝ}, 0 < x → ∀ (y : ℝ), 0 < x ^ y
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.instCoeTypeForall : {α : Type u} → Coe (Type v) (α → Type v)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_or : ∀ {v : ℕ} (x y : BitVec v), (x ||| y).toNat = x.toNat ||| y.toNat
-- Mathlib.Data.Set.SymmDiff
Set.symmDiff_eq_empty : ∀ {α : Type u} {s t : Set α}, symmDiff s t = ∅ ↔ s = t
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.toLowerSet_le_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α},
  Topology.WithLowerSet.toLowerSet a ≤ Topology.WithLowerSet.toLowerSet b ↔ a ≤ b
-- Mathlib.RepresentationTheory.Coinduced
Rep.resCoindHomEquiv_apply : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (B : Rep.{max w t, u, w} k H) (A : Rep.{max w t, u, v} k G) (f : Rep.res φ B ⟶ A),
  (Rep.resCoindHomEquiv.{t, u, v, w} φ B A) f = Rep.resCoindToHom φ B A f
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Whether to use the `on_goal n =>` combinator.  -/
Mathlib.Tactic.ClickSuggestions.Context.onGoal : Mathlib.Tactic.ClickSuggestions.Context → Option ℕ
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNonUnitalCommRing : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [IsOrderedCancelAddMonoid Γ] → [inst : NonUnitalCommRing R] → NonUnitalCommRing (HahnSeries Γ R)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.symm : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x y : RingCat.Colimits.Prequotient F) (x_1 : RingCat.Colimits.Relation F x y),
  RingCat.Colimits.Relation.below x_1 → motive x y x_1 → RingCat.Colimits.Relation.below ⋯
-- Mathlib.FieldTheory.Minpoly.Field
/-- Function from `Hom_K(E,L)` to pi type Π (x : basis), roots of min poly of x  -/
minpoly.rootsOfMinPolyPiType : (F : Type u_3) →
  (E : Type u_4) →
    (K : Type u_5) →
      [inst : Field F] →
        [inst_1 : Ring E] →
          [inst_2 : CommRing K] →
            [inst_3 : IsDomain K] →
              [inst_4 : Algebra F E] →
                [inst_5 : Algebra F K] →
                  [inst_6 : FiniteDimensional F E] →
                    (E →ₐ[F] K) → (x : ↑(Set.range ⇑(Module.finBasis F E))) → { l // l ∈ (minpoly F ↑x).aroots K }
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), Function.Injective ⇑f
-- Init.Data.SInt.Lemmas
ISize.toInt16_neg : ∀ (x : ISize), (-x).toInt16 = -x.toInt16
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.erase.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.erase ⟨{ size := size, buckets := buckets }, hm⟩ a =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ =>
      let bkt := buckets[i];
      if Std.DHashMap.Internal.AssocList.contains a bkt = true then
        let buckets' := buckets.uset i Std.DHashMap.Internal.AssocList.nil h;
        ⟨{ size := size - 1, buckets := buckets'.uset i (Std.DHashMap.Internal.AssocList.erase a bkt) ⋯ }, ⋯⟩
      else ⟨{ size := size, buckets := buckets }, hm⟩
-- Mathlib.MeasureTheory.Integral.Pi
MeasureTheory.integrable_comp_eval : ∀ {ι : Type u_2} [inst : Fintype ι] {X : ι → Type u_3} {mX : (i : ι) → MeasurableSpace (X i)}
  {μ : (i : ι) → MeasureTheory.Measure (X i)} {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] {i : ι} {f : X i → E},
  MeasureTheory.Integrable f (μ i) → MeasureTheory.Integrable (fun x => f (x i)) (MeasureTheory.Measure.pi μ)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getKey?_eq_getKey?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  m.getKey? a = m.getKey?ₘ a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.uniqueHomToTrivial.eq_1 : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (A : CategoryTheory.AddMon D),
  A.uniqueHomToTrivial =
    { default := { hom := CategoryTheory.SemiCartesianMonoidalCategory.toUnit A.X, isAddMonHom_hom := ⋯ }, uniq := ⋯ }
-- Mathlib.RingTheory.Coprime.Lemmas
ne_zero_or_ne_zero_of_nat_coprime : ∀ {A : Type u} [inst : CommRing A] [Nontrivial A] {a b : ℕ}, a.Coprime b → ↑a ≠ 0 ∨ ↑b ≠ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
/-- The subdivision functor on simplicial sets.  -/
SSet.sd : CategoryTheory.Functor SSet SSet
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.app_eq_coe : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (η : ApplicativeTransformation F G), η.app = fun {α} => η.app α
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_mul_self_le : ∀ {E : Type u_4} {inst : NonUnitalNormedRing E} {inst_1 : StarRing E} [self : CStarRing E] (x : E),
  ‖x‖ * ‖x‖ ≤ ‖star x * x‖
-- Std.Do.WP.SimpLemmas
Std.Do.WP.get_MonadState : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ : Type u} {Q : Std.Do.PostCond σ ps} [inst : Std.Do.WP m ps]
  [inst_1 : MonadStateOf σ m], (Std.Do.wp get).apply Q = (Std.Do.wp MonadStateOf.get).apply Q
-- Lean.ResolveName
_private.Lean.ResolveName.0.Lean.unresolveNameGlobal?.unresolveNameCore : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] →
            [Lean.AddMessageContext m] →
              Lean.Name → (Lean.Name → m Bool) → Option Lean.MacroScopesView → Lean.Name → OptionT m Lean.Name
-- Mathlib.Order.Interval.Finset.Floor
Nat.cast_mem_Ici_iff : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {a : α} {n : ℕ},
  ↑n ∈ Set.Ici a ↔ n ∈ Set.Ici ⌈a⌉₊
-- Mathlib.Analysis.Analytic.Constructions
hasFPowerSeriesOnBall_const : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {c : F} {e : E},
  HasFPowerSeriesOnBall (fun x => c) (constFormalMultilinearSeries 𝕜 E c) e ⊤
-- Init.Data.Nat.Basic
Nat.zero_lt_of_lt : ∀ {a b : ℕ}, a < b → 0 < b
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.le_mul_inv_iff_mul_le : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] (a b : R) {c : R}, 0 < c → (a ≤ b * c⁻¹ ↔ a * c ≤ b)
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.errSum.eq_1 : ∀ {s : BoundingSieve} (muPlus : ℕ → ℝ),
  BoundingSieve.errSum muPlus = ∑ d ∈ s.prodPrimes.divisors, |muPlus d| * |BoundingSieve.rem d|
-- Mathlib.LinearAlgebra.Basis.MulOpposite
Module.Basis.mulOpposite_repr_eq : ∀ {R : Type u_1} {H : Type u_2} {ι : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid H] [inst_2 : Module R H]
  (b : Module.Basis ι R H), b.mulOpposite.repr = (MulOpposite.opLinearEquiv R).symm ≪≫ₗ b.repr
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiffAt.coordChangeL : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_20 : MemTrivializationAtlas e] [inst_21 : MemTrivializationAtlas e'] {f : M → B} {x : M},
  ContMDiffAt IM IB n f x →
    f x ∈ e.baseSet →
      f x ∈ e'.baseSet →
        ContMDiffAt IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n
          (fun y => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' (f y))) x
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformlyOn.hasProd : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {x : β} {s : Set β}
  [inst_1 : UniformSpace α], HasProdUniformlyOn f g s → x ∈ s → HasProd (fun x_1 => f x_1 x) (g x)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instNontrivial : ∀ {M : Type u_1} [inst : MulOneClass M] [Nontrivial M], Nontrivial (Submonoid M)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_eq_lim_of_equiv : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv]
  {f g : CauSeq β abv}, f ≈ g → f.lim = g.lim
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setAverage_sub_setAverage : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} {s : Set α} [CompleteSpace E],
  μ s ≠ ⊤ → ∀ (f : α → E), ∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ = 0
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.isCancelMul : ∀ {α : Type u} [inst : Add α] [IsCancelAdd α], IsCancelMul (Multiplicative α)
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasPullbacks C}
  {toPrecoverage : CategoryTheory.Precoverage C}
  {has_isos :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X) [CategoryTheory.IsIso f], CategoryTheory.Presieve.singleton f ∈ toPrecoverage.coverings X}
  {pullbacks :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
      ∀ S ∈ toPrecoverage.coverings X, CategoryTheory.Presieve.pullbackArrows f S ∈ toPrecoverage.coverings Y}
  {transitive :
    ∀ ⦃X : C⦄ (S : CategoryTheory.Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y),
      S ∈ toPrecoverage.coverings X →
        (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ toPrecoverage.coverings Y) → S.bind Ti ∈ toPrecoverage.coverings X}
  {toPrecoverage_1 : CategoryTheory.Precoverage C}
  {has_isos_1 :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X) [CategoryTheory.IsIso f], CategoryTheory.Presieve.singleton f ∈ toPrecoverage_1.coverings X}
  {pullbacks_1 :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
      ∀ S ∈ toPrecoverage_1.coverings X, CategoryTheory.Presieve.pullbackArrows f S ∈ toPrecoverage_1.coverings Y}
  {transitive_1 :
    ∀ ⦃X : C⦄ (S : CategoryTheory.Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y),
      S ∈ toPrecoverage_1.coverings X →
        (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ toPrecoverage_1.coverings Y) →
          S.bind Ti ∈ toPrecoverage_1.coverings X},
  { toPrecoverage := toPrecoverage, has_isos := has_isos, pullbacks := pullbacks, transitive := transitive } =
      { toPrecoverage := toPrecoverage_1, has_isos := has_isos_1, pullbacks := pullbacks_1,
        transitive := transitive_1 } →
    toPrecoverage = toPrecoverage_1
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- The map that sends a vector of `E` to the element of the ℤ-lattice spanned by `b` obtained
by rounding down its coordinates on the basis `b`.  -/
ZSpan.floor : {E : Type u_1} →
  {ι : Type u_2} →
    {K : Type u_3} →
      [inst : NormedField K] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace K E] →
            (b : Module.Basis ι K E) →
              [inst_3 : LinearOrder K] →
                [IsStrictOrderedRing K] → [FloorRing K] → [Fintype ι] → E → ↥(Submodule.span ℤ (Set.range ⇑b))
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instLawfulBEq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α], LawfulBEq (Std.ExtHashSet α)
-- Init.Data.BitVec.Bitblast
BitVec.DivModState.Poised.mk : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w},
  BitVec.DivModState.Lawful args qr → 0 < qr.wn → BitVec.DivModState.Poised args qr
-- Mathlib.GroupTheory.Perm.Sign
Equiv.swap.eq_1 : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b : α),
  Equiv.swap a b = { toFun := Equiv.swapCore a b, invFun := Equiv.swapCore a b, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_ofLinearComb : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (C : Set M)
  (nonempty : C.Nonempty) (linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C),
  ↑(Submodule.ofLinearComb C nonempty linearComb) = C
-- Mathlib.Algebra.Opposites
AddOpposite.unop_neg : ∀ {α : Type u_1} [inst : Neg α] (x : αᵃᵒᵖ), AddOpposite.unop (-x) = -AddOpposite.unop x
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_zero : ∀ {α : Sort u_2} (p : Fin 0 → α) (x : α), Fin.snoc p x = fun x_1 => x
-- Mathlib.LinearAlgebra.Finsupp.Pi
LinearMap.splittingOfFunOnFintypeSurjective_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_5}
  [inst_3 : Finite α] (f : M →ₗ[R] α → R) (s : Function.Surjective ⇑f),
  Function.Injective ⇑(f.splittingOfFunOnFintypeSurjective s)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.forget_faithful : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T}, (CategoryTheory.Under.forget X).Faithful
-- Mathlib.Data.List.Induction
List.twoStepInduction_singleton : ∀ {α : Type u_1} {motive : List α → Sort u_2} (x : α) (nil : motive []) (singleton : (x : α) → motive [x])
  (cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)),
  List.twoStepInduction nil singleton cons_cons [x] = singleton x
-- Mathlib.Algebra.Polynomial.Sequence
/-- The `i`-th basis vector is the `i`-th polynomial in the sequence.  -/
Polynomial.Sequence.basis_eq_self : ∀ {R : Type u_1} [inst : Ring R] (S : Polynomial.Sequence R) [inst_1 : IsDomain R]
  (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) (i : ℕ), (S.basis hCoeff) i = ↑S i
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_add_two_sub_fib_add_one : ∀ {n : ℕ}, Nat.fib (n + 2) - Nat.fib (n + 1) = Nat.fib n
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Precoverage.toCoverage.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J J_1 : CategoryTheory.Precoverage C) (e_J : J = J_1)
  [inst_1 : J.HasPullbacks] [inst_2 : J.IsStableUnderBaseChange], J.toCoverage = J_1.toCoverage
-- Lean.Elab.Command
/-- Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function
catches interrupt exceptions as well and thus is intended for use at the top level of elaboration.
Interrupt and abort exceptions are caught but not logged.
 -/
Lean.Elab.Command.withLoggingExceptions : Lean.Elab.Command.CommandElabM Unit → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.unop_ι_app_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g),
  c.unop.ι.app CategoryTheory.Limits.WalkingParallelPair.zero =
    (c.π.app CategoryTheory.Limits.WalkingParallelPair.one).unop
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_8 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  (X : CategoryTheory.Functor Cᵒᵖ D), (J.plusFunctorWhiskerRightIso F).hom.app X = (J.plusCompIso F X).hom
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.invFun_eq_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  e.invFun = ↑e.symm
-- Aesop.Check
Aesop.Check.mk.inj : ∀ {toOption toOption_1 : Lean.Option Bool},
  { toOption := toOption } = { toOption := toOption_1 } → toOption = toOption_1
-- Mathlib.Tactic.Tauto
/-- For each fvar in `fvars`, calls `distribNotAt` and carries along the resulting
renamings.
 -/
Mathlib.Tactic.Tauto.distribNotAux : List Lean.Expr → Lean.MVarId → Lean.MetaM Lean.MVarId
-- Init.Data.SInt.Lemmas
Int16.toInt_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt = (↑n).bmod Int16.size
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.finiteAt_inner : ∀ {a : ℝ} (l : Filter ℝ) {l' : Filter ℝ} [h : intervalIntegral.FTCFilter a l l'] {μ : MeasureTheory.Measure ℝ}
  [MeasureTheory.IsLocallyFiniteMeasure μ], μ.FiniteAtFilter l'
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.fst_zero : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Zero α], (NonemptyInterval.toProd 0).1 = 0
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_le_iff_one_le_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b : α}, a⁻¹ ≤ b ↔ 1 ≤ b * a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {c : ℕ}, (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)).size = 0
-- Mathlib.AlgebraicTopology.SimplicialCategory.Basic
/-- Abbreviation for the enriched composition in a simplicial category.  -/
CategoryTheory.SimplicialCategory.sHomComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.SimplicialCategory C] →
      (K L M : C) →
        CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.SimplicialCategory.sHom K L)
            (CategoryTheory.SimplicialCategory.sHom L M) ⟶
          CategoryTheory.SimplicialCategory.sHom K M
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheafCocone_pt : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C] (y : ↑X),
  (skyscraperPresheafCocone p₀ A y).pt = ⊤_ C
-- Mathlib.SetTheory.Ordinal.Notation
ONote.nf_repr_split' : ∀ {o o' : ONote} {m : ℕ} [o.NF], o.split' = (o', m) → o'.NF ∧ o.repr = Ordinal.omega0 * o'.repr + ↑m