mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Category.FinPartOrd
/-- The equivalence between `FinPartOrd` and itself induced by `OrderDual` both ways.  -/
FinPartOrd.dualEquiv : FinPartOrd ≌ FinPartOrd
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
CategoryTheory.Presheaf.coconeCompShrinkYonedaHomEquiv_apply_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] {F : CategoryTheory.Functor J Cᵒᵖ}
  {c' : CategoryTheory.Limits.Cocone (F.leftOp.comp CategoryTheory.shrinkYoneda.{w, v, u})}
  (hc' : CategoryTheory.Limits.IsColimit c') {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : c'.pt ⟶ P) (j : J),
  ↑((CategoryTheory.Presheaf.coconeCompShrinkYonedaHomEquiv hc') f) j =
    CategoryTheory.shrinkYonedaEquiv (CategoryTheory.CategoryStruct.comp (c'.ι.app (Opposite.op j)) f)
-- Mathlib.Topology.Maps.Basic
IsOpenMap.range_mem_nhds : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → ∀ (x : X), Set.range f ∈ nhds (f x)
-- Aesop.Script.Step
Aesop.Script.LazyStep : Type
-- Init.Data.Array.Lemmas
Array.swapAt!.eq_1 : ∀ {α : Type u} (xs : Array α) (i : ℕ) (v : α),
  xs.swapAt! i v =
    if h : i < xs.size then xs.swapAt i v h
    else
      have this := { default := (v, xs) };
      panicWithPosWithDecl "Init.Data.Array.Basic" "Array.swapAt!" 438 4
        (String.Internal.append (String.Internal.append "index " (toString i)) " out of bounds")
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The chosen wedge is limiting.  -/
CategoryTheory.Limits.ChosenEndsOfShape.isEnd : {J : Type u_3} →
  {inst : CategoryTheory.Category.{v_3, u_3} J} →
    {C : Type u_4} →
      {inst_1 : CategoryTheory.Category.{v_4, u_4} C} →
        [self : CategoryTheory.Limits.ChosenEndsOfShape J C] →
          (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.ChosenEndsOfShape.wedge F)
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- Composition of two temperate growth functions is of temperate growth.  -/
Function.HasTemperateGrowth.comp : ∀ {D : Type u_4} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup D] [inst_5 : NormedSpace ℝ D]
  {g : E → F} {f : D → E},
  Function.HasTemperateGrowth g → Function.HasTemperateGrowth f → Function.HasTemperateGrowth (g ∘ f)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuous_coe : Continuous ENNReal.ofNNReal
-- Mathlib.RingTheory.Ideal.Prime
Ideal.IsPrime.pow_mem_iff_mem : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsPrime → ∀ {r : α} (n : ℕ), 0 < n → (r ^ n ∈ I ↔ r ∈ I)
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalParen : Lean.Elab.Tactic.Tactic
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instToJsonDiagnosticSeverity : Lean.ToJson Lean.Lsp.DiagnosticSeverity
-- Init.Data.UInt.Basic
/-- Bitwise right shift for word-sized unsigned integers. Usually accessed via the `>>>` operator.

This function is overridden at runtime with an efficient implementation.
 -/
USize.shiftRight : USize → USize → USize
-- Mathlib.LinearAlgebra.InvariantBasisNumber
invariantBasisNumber_of_rankCondition : ∀ (R : Type u) [inst : Semiring R] [RankCondition R], InvariantBasisNumber R
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.equivalence_unitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Idempotents.DoldKan.equivalence.unitIso = CategoryTheory.Idempotents.DoldKan.ε
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I),
  (I.multiforkEquivPiFork.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.Analysis.Normed.Group.Basic
norm_inv' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), ‖a⁻¹‖ = ‖a‖
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.Paths.liftNatTrans_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {V : Type u₁} [inst_1 : Quiver V]
  {F G : CategoryTheory.Functor (CategoryTheory.Paths V) C} (α_app : (v : V) → F.obj v ⟶ G.obj v)
  (α_nat :
    ∀ {X Y : V} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp (F.map f.toPath) (α_app Y) =
        CategoryTheory.CategoryStruct.comp (α_app X) (G.map f.toPath))
  (v : V), (CategoryTheory.Paths.liftNatTrans α_app α_nat).app v = α_app v
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeSet_univ_card : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype ↑G.edgeSet], Finset.univ.card = G.edgeFinset.card
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Two vectors with equal norms are equal if and only if they have zero angle between them.  -/
Orientation.eq_iff_oangle_eq_zero_of_norm_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, ‖x‖ = ‖y‖ → (x = y ↔ o.oangle x y = 0)
-- Mathlib.RingTheory.MatrixAlgebra
/-- `Matrix.kronecker` as a ⋆-algebra equivalence, when the two arguments are tensored.  -/
Matrix.kroneckerStarAlgEquiv : (m : Type u_2) →
  (n : Type u_3) →
    (R : Type u_5) →
      [inst : CommSemiring R] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq n] →
            [inst_3 : Fintype m] →
              [inst_4 : DecidableEq m] →
                [inst_5 : StarRing R] → TensorProduct R (Matrix m m R) (Matrix n n R) ≃⋆ₐ[R] Matrix (m × n) (m × n) R
-- Lean.Level
_private.Lean.Level.0.Lean.Level.isIMax.match_1.eq_1 : ∀ (motive : Lean.Level → Sort u_1) (a a_1 : Lean.Level) (h_1 : (a a_2 : Lean.Level) → motive (a.imax a_2))
  (h_2 : (x : Lean.Level) → motive x),
  (match a.imax a_1 with
    | a.imax a_2 => h_1 a a_2
    | x => h_2 x) =
    h_1 a a_1
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.equivOfIsColimit_symm_apply : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.CofanTypes F}
  (hc : CategoryTheory.Functor.CoconeTypes.IsColimit c) (i : C) (x : F i),
  (CategoryTheory.Limits.CofanTypes.equivOfIsColimit hc).symm (c.inj i x) = ⟨i, x⟩
-- Mathlib.Order.Interval.Set.Disjoint
iUnion_Iic_of_not_bddAbove_range : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {f : ι → α}, ¬BddAbove (Set.range f) → ⋃ i, Set.Iic (f i) = Set.univ
-- Init.Data.String.Defs
String.Slice.instDecidableEqPos : {s : String.Slice} → DecidableEq s.Pos
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_eq_zero_of_remainder : ∀ {p r : ℕ} (i : ℕ), ¬p ∣ r → (p * i + r).factorization p = 0
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.mk_mem_sparsePairs : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  (P : Finpartition A) (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] (u v : Finset α) (ε : 𝕜),
  (u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ↑(G.edgeDensity u v) < ε
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodPUnit.eq_1 : ∀ (M : Type u_1) [inst : Monoid M], MulEquiv.coprodPUnit M = Monoid.Coprod.fst.toMulEquiv Monoid.Coprod.inl ⋯ ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
          k ∈ List.map Sigma.fst l →
            ∀ {h' : (↑(m.insertMany l)).contains k' = true}, (↑(m.insertMany l)).getKey k' h' = k
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.sInf_of_bot_mem : ∀ {α : Type u_1} [inst : LE α] [inst_1 : InfSet α] {s : Set (WithBot α)}, ⊥ ∈ s → sInf s = ⊥
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Aut.instGroup : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X : C) → Group (CategoryTheory.Aut X)
-- Mathlib.Topology.LocallyConstant.Basic
/-- A locally constant function is constant on any preconnected set.  -/
IsLocallyConstant.apply_eq_of_isPreconnected : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyConstant f → ∀ {s : Set X}, IsPreconnected s → ∀ {x y : X}, x ∈ s → y ∈ s → f x = f y
-- Mathlib.Order.Disjoint
Complementeds.coe_bot : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α], ↑⊥ = ⊥
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.nat_add_neg : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {f : ℤ → M},
  Summable f → Summable fun n => f ↑n + f (-↑n)
-- Std.Time.Format.DateFormat
Std.Time.DayPeriodSymbols.mk : String → String → String → String → Std.Time.DayPeriodSymbols
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
_private.Mathlib.CategoryTheory.Limits.Types.Coproducts.0.CategoryTheory.Limits.WalkingPair.swap.match_1.splitter : (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) →
  (x : CategoryTheory.Limits.WalkingPair) →
    (Unit → motive CategoryTheory.Limits.WalkingPair.left) →
      (Unit → motive CategoryTheory.Limits.WalkingPair.right) → motive x
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvectorUnitary_coe : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {n : Type u_4} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian),
  ↑hA.eigenvectorUnitary = (EuclideanSpace.basisFun n 𝕜).toBasis.toMatrix ⇑hA.eigenvectorBasis.toBasis
-- Mathlib.Data.Set.Lattice
Set.iUnion_congr_of_surjective : ∀ {α : Type u_1} {ι : Sort u_5} {ι₂ : Sort u_7} {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂),
  Function.Surjective h → (∀ (x : ι), g (h x) = f x) → ⋃ x, f x = ⋃ y, g y
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Product of two continuous linear equivalences. The map comes from `Equiv.prodCongr`.  -/
ContinuousLinearEquiv.prodCongr : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          {M₂ : Type u_5} →
            [inst_3 : TopologicalSpace M₂] →
              [inst_4 : AddCommMonoid M₂] →
                {M₃ : Type u_6} →
                  [inst_5 : TopologicalSpace M₃] →
                    [inst_6 : AddCommMonoid M₃] →
                      {M₄ : Type u_7} →
                        [inst_7 : TopologicalSpace M₄] →
                          [inst_8 : AddCommMonoid M₄] →
                            [inst_9 : Module R₁ M₁] →
                              [inst_10 : Module R₁ M₂] →
                                [inst_11 : Module R₁ M₃] →
                                  [inst_12 : Module R₁ M₄] → (M₁ ≃L[R₁] M₂) → (M₃ ≃L[R₁] M₄) → (M₁ × M₃) ≃L[R₁] M₂ × M₄
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_inj : ∀ {a b : UInt32}, a.toBitVec = b.toBitVec ↔ a = b
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.toListRev_iter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap α β},
  m.iter.toListRev = m.toList.reverse
-- Mathlib.Order.Lattice
/-- Pointwise supremum of two antitone functions is an antitone function.  -/
Antitone.sup : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeSup β] {f g : α → β},
  Antitone f → Antitone g → Antitone (f ⊔ g)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Copy of a `ContinuousLinearMap` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
ContinuousLinearMap.copy : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] →
                        [inst_7 : Module R₂ M₂] → (f : M₁ →SL[σ₁₂] M₂) → (f' : M₁ → M₂) → f' = ⇑f → M₁ →SL[σ₁₂] M₂
-- Aesop.Builder.Tactic
Aesop.RuleBuilder.tacticIMode : Option Aesop.IndexingMode → Aesop.IndexingMode
-- Mathlib.Algebra.Quaternion
Quaternion.coe_normSq_add : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R),
  ↑(Quaternion.normSq (a + b)) = ↑(Quaternion.normSq a) + a * star b + b * star a + ↑(Quaternion.normSq b)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.median_restrict : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1))
  (S : AffineSubspace k P) (hS : affineSpan k (Set.range s.points) ≤ S),
  AffineSubspace.map S.subtype ((s.restrict S hS).median i) = s.median i
-- Mathlib.Algebra.Order.Module.Defs
instPosSMulMonoNatOfIsOrderedAddMonoid : ∀ {M : Type u_3} [inst : PartialOrder M] [inst_1 : AddCommMonoid M] [IsOrderedAddMonoid M], PosSMulMono ℕ M
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mem_restrictScalars : ∀ (K : Type u_1) {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] [inst_5 : Algebra L' L] [inst_6 : IsScalarTower K L' L]
  {E : IntermediateField L' L} {x : L}, x ∈ IntermediateField.restrictScalars K E ↔ x ∈ E
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonLeanServerCapabilities : Lean.FromJson Lean.Lsp.LeanServerCapabilities
-- Mathlib.Order.Filter.Prod
Filter.inf_prod : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β} {f₁ f₂ : Filter α}, (f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- An additive submagma of a cancellative additive magma inherits cancellation.  -/
AddMemClass.isCancelAdd : ∀ {M : Type u_1} {A : Type u_3} [inst : Add M] [inst_1 : SetLike A M] [hA : AddMemClass A M] [IsCancelAdd M] (S : A),
  IsCancelAdd ↥S
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.toPrepartition : {ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.TaggedPrepartition I → BoxIntegral.Prepartition I
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.eq_of_eq : ∀ {α : Type u_1} {a a' b b' : α} [inst : Add α] [IsRightCancelAdd α], a = b → a' + b = b' + a → a' = b'
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.mopFunctor_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.mopFunctor C) X Y = (β_ { unmop := X } { unmop := Y }).inv
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_of_contains_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β}, (t.insert k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Mathlib.Data.Nat.Prime.Defs
_private.Mathlib.Data.Nat.Prime.Defs.0.Nat.minFacProp : ℕ → ℕ → Prop
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsShortComplex_X₂ : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{w, u, v} k G) (S : Subgroup G)
  [inst_2 : S.Normal], (A.coinvariantsShortComplex S).X₂ = A
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
/-- Mapping a walk to its own subgraph and then to `G[w.support]` is the same as inducing the walk
to its support.  -/
SimpleGraph.Walk.map_mapToSubgraph_eq_induce_id : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v),
  SimpleGraph.Walk.map { toFun := fun v_1 => ⟨↑v_1, ⋯⟩, map_rel' := ⋯ } w.mapToSubgraph =
    SimpleGraph.Walk.induce (fun x => List.Mem x w.support) w ⋯
-- Mathlib.LinearAlgebra.Dimension.Finrank
Module.lt_rank_of_lt_finrank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  n < Module.finrank R M → ↑n < Module.rank R M
-- Init.WF
Prod.Lex.right' : ∀ {β : Type v} (rb : β → β → Prop) {a₂ : ℕ} {b₂ : β} {a₁ : ℕ} {b₁ : β},
  a₁ ≤ a₂ → rb b₁ b₂ → Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂)
-- Mathlib.CategoryTheory.Monad.Types
/-- A lawful `Control.Monad` gives a category theory `Monad` on the category of types.
 -/
CategoryTheory.ofTypeMonad : (m : Type u → Type u) → [inst : Monad m] → [LawfulMonad m] → CategoryTheory.Monad (Type u)
-- Mathlib.Topology.Sheaves.Flasque
TopCat.Presheaf.IsCompatible.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type u_4} (U : ι → TopologicalSpace.Opens ↑X)
  (sf : (i : ι) → CategoryTheory.ToType (F.obj (Opposite.op (U i)))),
  F.IsCompatible U sf =
    ∀ (i j : ι),
      (CategoryTheory.ConcreteCategory.hom (F.map ((U i).infLELeft (U j)).op)) (sf i) =
        (CategoryTheory.ConcreteCategory.hom (F.map ((U i).infLERight (U j)).op)) (sf j)
-- Mathlib.Topology.Sets.BaseChangeNhds
TopologicalSpace.Compacts.baseChangeOpenNhds_comp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K L M : TopologicalSpace.Compacts α} (h : K ⟶ L) (k : L ⟶ M)
  (U : ↑M.openNhds),
  TopologicalSpace.Compacts.baseChangeOpenNhds (CategoryTheory.CategoryStruct.comp h k) U =
    TopologicalSpace.Compacts.baseChangeOpenNhds h (TopologicalSpace.Compacts.baseChangeOpenNhds k U)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isAffineOpen_bot : ∀ (X : AlgebraicGeometry.Scheme), AlgebraicGeometry.IsAffineOpen ⊥
-- Init.MetaTypes
Lean.Meta.TransparencyMode.noConfusionType : Sort v✝ → Lean.Meta.TransparencyMode → Lean.Meta.TransparencyMode → Sort v✝
-- Init.Data.Nat.Basic
Nat.sub_self : ∀ (n : ℕ), n - n = 0
-- Mathlib.Order.Interval.Set.Basic
IsMax.Ici_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, IsMax a → Set.Ici a = {a}
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgHomClass.toBialgHom.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] [inst_7 : FunLike F A B] [inst_8 : BialgHomClass F R A B] (f f_1 : F),
  f = f_1 → ↑f = ↑f_1
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- If `f : R ≃+* S` is a ring isomorphism and `I : Submodule R K` is fractional with respect to
`R⁰`, then `I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap`
is fractional with respect to `S⁰`.

Do not confuse with `IsFractional.map`.  -/
IsFractional.mapEquiv : ∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [IsDomain R] [inst_2 : CommRing S]
  [IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K] [inst_7 : Algebra S L]
  [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] (f : R ≃+* S) {I : Submodule R K},
  IsFractional (nonZeroDivisors R) I →
    IsFractional (nonZeroDivisors S) (Submodule.map (↑(IsFractionRing.semilinearEquivOfRingEquiv K L f)) I)
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.corec.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: β))
  (x : β), MvQPF.Cofix.corec g x = Quot.mk MvQPF.Mcongr (MvQPF.corecF g x)
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instMin : {α : Type u} → [inst : Group α] → Min (GroupTopology α)
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
/-- A `LieAdmissibleRing` is a `NonUnitalNonAssocRing` such that the canonical bracket
`⁅x, y⁆ := x * y - y * x` turns it into a `LieRing`. This is expressed by an associator identity.  -/
LieAdmissibleRing : Type u_1 → Type u_1
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.div_mul : ∀ {R : Type u} [inst : EuclideanDomain R] {x y z : R}, y ∣ x → y * z ∣ x → x / (y * z) = x / y / z
-- Init.Data.Array.Extract
Array.popWhile_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {p : β → Bool} {as : Array α},
  Array.popWhile p (Array.filterMap f as) = Array.filterMap f (Array.popWhile (fun a => Option.all p (f a)) as)
-- Mathlib.Topology.EMetricSpace.PairReduction
/-- If `(V, t, r)` is a `logSizeBallStruct` then `logSizeBallStruct.smallBall`
is `{x ∈ V | d(t, x) ≤ (r - 1)c}`.  -/
PairReduction.logSizeBallStruct.smallBall : {T : Type u_1} → [PseudoEMetricSpace T] → PairReduction.logSizeBallStruct T → ENNReal → Finset T
-- Mathlib.Analysis.Normed.Group.Basic
mem_sphere_iff_norm_inv_mul_eq : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a b : E} {r : ℝ}, b ∈ Metric.sphere a r ↔ ‖b⁻¹ * a‖ = r
-- Mathlib.Data.Set.Finite.Lattice
Set.Finite.sUnion : ∀ {α : Type u} {s : Set (Set α)}, s.Finite → (∀ t ∈ s, t.Finite) → (⋃₀ s).Finite
-- Init.Data.SInt.Lemmas
Int16.toNat_toInt : ∀ (x : Int16), x.toInt.toNat = x.toNatClampNeg
-- Init.Data.UInt.Lemmas
UInt16.toUSize_le : ∀ {a b : UInt16}, a.toUSize ≤ b.toUSize ↔ a ≤ b
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- Auxiliary definition for `desc`.  -/
ComplexShape.Embedding.AreComplementary.desc' : {ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} →
          {c₂ : ComplexShape ι₂} →
            {e₁ : c₁.Embedding c} →
              {e₂ : c₂.Embedding c} →
                (ac : e₁.AreComplementary e₂) →
                  {X : ι → Type u_5} →
                    ((i₁ : ι₁) → X (e₁.f i₁)) → ((i₂ : ι₂) → X (e₂.f i₂)) → (i : ι₁ ⊕ ι₂) → X (ac.equiv i)
-- Mathlib.Analysis.Real.Sqrt
NNReal.one_le_sqrt : ∀ {x : NNReal}, 1 ≤ NNReal.sqrt x ↔ 1 ≤ x
-- Init.CbvSimproc
Lean.Parser.Attr.cbvSimprocBuiltinAttr : Lean.ParserDescr
-- Mathlib.Control.Applicative
Functor.Comp.seq_pure : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F]
  [LawfulApplicative G] {α β : Type v} (f : Functor.Comp F G (α → β)) (x : α), f <*> pure x = (fun g => g x) <$> f
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.alter_eq_alterₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α) (f : Option β → Option β),
  Std.DHashMap.Internal.Raw₀.Const.alter m a f = Std.DHashMap.Internal.Raw₀.Const.alterₘ m a f
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.mk.inj : ∀ {R : Type u} {inst : Ring R} {inst_1 : TopologicalSpace R} {toModuleCat : ModuleCat R}
  {topologicalSpace : TopologicalSpace ↑toModuleCat} {isTopologicalAddGroup : IsTopologicalAddGroup ↑toModuleCat}
  {continuousSMul : ContinuousSMul R ↑toModuleCat} {toModuleCat_1 : ModuleCat R}
  {topologicalSpace_1 : TopologicalSpace ↑toModuleCat_1}
  {isTopologicalAddGroup_1 : IsTopologicalAddGroup ↑toModuleCat_1} {continuousSMul_1 : ContinuousSMul R ↑toModuleCat_1},
  { toModuleCat := toModuleCat, topologicalSpace := topologicalSpace, isTopologicalAddGroup := isTopologicalAddGroup,
        continuousSMul := continuousSMul } =
      { toModuleCat := toModuleCat_1, topologicalSpace := topologicalSpace_1,
        isTopologicalAddGroup := isTopologicalAddGroup_1, continuousSMul := continuousSMul_1 } →
    toModuleCat = toModuleCat_1 ∧ topologicalSpace ≍ topologicalSpace_1
-- Lean.Parser.Basic
Lean.Parser.identNoAntiquot : Lean.Parser.Parser