mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Slice
String.Slice.SplitIterator.instIteratorIdSubslice.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] {pat : ρ}
  [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ] {s : String.Slice},
  String.Slice.SplitIterator.instIteratorIdSubslice =
    {
      IsPlausibleStep := fun x x_1 =>
        match x, x_1 with
        | { internalState := String.Slice.SplitIterator.operating currPos s_1 },
          Std.IterStep.yield { internalState := String.Slice.SplitIterator.operating currPos_1 s' } out =>
          s'.IsPlausibleSuccessorOf s_1
        | { internalState := String.Slice.SplitIterator.operating currPos s_1 },
          Std.IterStep.yield { internalState := String.Slice.SplitIterator.atEnd } out => True
        | { internalState := String.Slice.SplitIterator.operating currPos s_1 },
          Std.IterStep.skip { internalState := String.Slice.SplitIterator.operating currPos_1 s' } =>
          s'.IsPlausibleSuccessorOf s_1
        | { internalState := String.Slice.SplitIterator.operating currPos s },
          Std.IterStep.skip { internalState := String.Slice.SplitIterator.atEnd } => False
        | { internalState := String.Slice.SplitIterator.operating currPos s }, Std.IterStep.done => True
        | { internalState := String.Slice.SplitIterator.atEnd }, Std.IterStep.yield it out => False
        | { internalState := String.Slice.SplitIterator.atEnd }, Std.IterStep.skip it => False
        | { internalState := String.Slice.SplitIterator.atEnd }, Std.IterStep.done => True,
      step := fun x =>
        match x with
        | { internalState := String.Slice.SplitIterator.operating currPos searcher } =>
          match h : searcher.step with
          | ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =>
            have slice := s.subslice! currPos startPos;
            let nextIt := { internalState := String.Slice.SplitIterator.operating endPos searcher' };
            pure (Std.Shrink.deflate ⟨Std.IterStep.yield nextIt slice, ⋯⟩)
          | ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =>
            pure
              (Std.Shrink.deflate
                ⟨Std.IterStep.skip { internalState := String.Slice.SplitIterator.operating currPos searcher' }, ⋯⟩)
          | ⟨Std.IterStep.skip searcher', hps⟩ =>
            pure
              (Std.Shrink.deflate
                ⟨Std.IterStep.skip { internalState := String.Slice.SplitIterator.operating currPos searcher' }, ⋯⟩)
          | ⟨Std.IterStep.done, property⟩ =>
            have slice := s.subsliceFrom currPos;
            pure
              (Std.Shrink.deflate ⟨Std.IterStep.yield { internalState := String.Slice.SplitIterator.atEnd } slice, ⋯⟩)
        | { internalState := String.Slice.SplitIterator.atEnd } => pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩) }
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Functor.copyObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (obj : C → D) (e : (X : C) → F.obj X ≅ obj X),
  F.copyObj obj e =
    { obj := obj,
      map := fun {X Y} f =>
        CategoryTheory.CategoryStruct.comp (e X).inv (CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- An auxiliary lemma for `Basis.le_span`.

If `R` satisfies the rank condition,
then for any finite basis `b : Basis ι R M`,
and any finite spanning set `w : Set M`,
the cardinality of `ι` is bounded by the cardinality of `w`.
 -/
Basis.le_span'' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [RankCondition R]
  {ι : Type u_2} [inst_4 : Fintype ι] (b : Module.Basis ι R M) {w : Set M} [inst_5 : Fintype ↑w],
  Submodule.span R w = ⊤ → Fintype.card ι ≤ Fintype.card ↑w
-- Init.Data.BitVec.Decidable
BitVec.forall_zero_iff : ∀ {P : BitVec 0 → Prop}, (∀ (v : BitVec 0), P v) ↔ P 0#0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqParam.beq : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Param pu → Lean.Compiler.LCNF.Param pu → Bool
-- Mathlib.Data.Vector.Basic
List.Vector.get_replicate : ∀ {α : Type u_1} {n : ℕ} (a : α) (i : Fin n), (List.Vector.replicate n a).get i = a
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux1.eq_1 : ∀ {α : Type u} (l : List (Computation α)) (S : Stream'.WSeq (Computation α)),
  Computation.parallel.aux1✝ (l, S) =
    Computation.rmap
      (fun l' =>
        match Stream'.Seq.destruct S with
        | none => (l', Stream'.Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))
      (Computation.parallel.aux2✝ l)
-- Init.Data.Int.Order
Int.sign_eq_neg_one_iff_neg : ∀ {a : ℤ}, a.sign = -1 ↔ a < 0
-- Mathlib.Analysis.Normed.Ring.Basic
ULift.seminormedRing : {α : Type u_2} → [SeminormedRing α] → SeminormedRing (ULift.{u_5, u_2} α)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.congr_symm_tmul : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] [inst_13 : AddCommMonoid Q]
  [inst_14 : Module R Q] (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q),
  (TensorProduct.AlgebraTensorModule.congr f g).symm (p ⊗ₜ[R] q) = f.symm p ⊗ₜ[R] g.symm q
-- Init.Data.SInt.Lemmas
ISize.toInt_inj : ∀ {x y : ISize}, x.toInt = y.toInt ↔ x = y
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.isoInv_pullback_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (Z : CategoryTheory.Over Y),
  ((CategoryTheory.ChosenPullbacksAlong.pullback f.inv).obj Z).left = Z.left
-- Lean.Elab.Term.TermElabM
/-- Wraps the given action for use in `BaseIO.asTask` etc., discarding its final state except for
`logSnapshotTask` tasks, which are reported as part of the returned tree. The given cancellation
token, if any, should be stored in a `SnapshotTask` for the server to trigger it when the result is
no longer needed.
 -/
Lean.Elab.Term.wrapAsyncAsSnapshot : {α : Type} →
  (α → Lean.Elab.TermElabM Unit) →
    Option IO.CancelToken →
      autoParam String Lean.Elab.Term.wrapAsyncAsSnapshot._auto_1 →
        Lean.Elab.TermElabM (α → BaseIO Lean.Language.SnapshotTree)
-- Mathlib.Tactic.Sat.FromLRAT
/-- The clause expression of type `Clause`  -/
Mathlib.Tactic.Sat.Clause.expr : Mathlib.Tactic.Sat.Clause → Lean.Expr
-- Mathlib.Algebra.Group.Nat.Hom
AddMonoidHom.ext_nat : ∀ {A : Type u_2} [inst : AddZeroClass A] {f g : ℕ →+ A}, f 1 = g 1 → f = g
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
_private.Mathlib.Algebra.ContinuedFractions.Computation.Translations.0.Option.getD.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match none with
    | some x => h_1 x
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_toReal_coe_eq_self_iff : ∀ {θ : ℝ}, |(↑θ).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ Real.pi
-- Mathlib.MeasureTheory.Measure.Lebesgue.Complex
/-- Measurable equivalence between `ℂ` and `ℝ × ℝ`.  -/
Complex.measurableEquivRealProd : ℂ ≃ᵐ ℝ × ℝ
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {km fallback : α},
  t.max? = some km → t.getD km fallback = km
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
CategoryTheory.Under.instHasColimitsOfSizeOfHasWidePushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} [CategoryTheory.Limits.HasWidePushouts C],
  CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, max u v} (CategoryTheory.Under B)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.divModByMonicAux.congr_simp : ∀ {R : Type u} [inst : Ring R] (_p _p_1 : Polynomial R),
  _p = _p_1 → ∀ {q q_1 : Polynomial R} (e_q : q = q_1) (a : q.Monic), _p.divModByMonicAux a = _p_1.divModByMonicAux ⋯
-- Init.Data.List.Sublist
List.infix_append' : ∀ {α : Type u_1} (l₁ l₂ l₃ : List α), l₂ <:+: l₁ ++ (l₂ ++ l₃)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
summable_of_hasFiniteSupport : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [L.HasSupport], Function.HasFiniteSupport f → Summable f L
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The Gram operator T†T is a positive operator.  -/
LinearMap.re_inner_adjoint_mul_self_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (x : E), 0 ≤ RCLike.re (inner 𝕜 x ((LinearMap.adjoint T * T) x))
-- Mathlib.RingTheory.Norm.Basic
Algebra.norm_eq_of_ringEquiv : ∀ {A : Type u_8} {B : Type u_9} {C : Type u_10} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Ring C]
  [inst_3 : Algebra A C] [inst_4 : Algebra B C] (e : A ≃+* B),
  (algebraMap B C).comp ↑e = algebraMap A C → ∀ (x : C), e ((Algebra.norm A) x) = (Algebra.norm B) x
-- Mathlib.Order.SuccPred.Archimedean
instIsPredArchimedeanOrderDualOfIsSuccArchimedean : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α], IsPredArchimedean αᵒᵈ
-- Mathlib.Algebra.Group.Pi.Units
MulEquiv.val_piUnits_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (f : ((i : ι) → M i)ˣ) (i : ι),
  ↑(MulEquiv.piUnits f i) = ↑f i
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `IsCancelAdd` across an `Equiv`  -/
Equiv.isCancelAdd : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Add β] [IsCancelAdd β], IsCancelAdd α
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.one_spec_asOver_spec : ∀ {R A : CommRingCat} [inst : Bialgebra ↑R ↑A],
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (AlgebraicGeometry.algSpec R))
      (CategoryTheory.Over.homMk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom ↑R ↑A))) ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A family `f` of parallel morphisms has a wide coequalizer if the diagram `parallelFamily f` has
a colimit.  -/
CategoryTheory.Limits.HasWideCoequalizer : {J : Type w} → {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (J → (X ⟶ Y)) → Prop
-- Mathlib.Topology.Inseparable
IsCompact.of_subset_of_specializes : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X},
  IsCompact s → t ⊆ s → (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) → IsCompact t
-- Lean.Meta.Tactic.Grind.PropagateInj
_private.Lean.Meta.Tactic.Grind.PropagateInj.0.Lean.Meta.Grind.getInvFor? : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Option (Lean.Expr × Lean.Expr))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α}, k ∉ m₂ → Std.DHashMap.Const.get! (m₁.inter m₂) k = default
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_le_minKey_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (cmp (t.minKey ⋯) ((t.erase k).minKey he)).isLE = true
-- Mathlib.Algebra.Quaternion
Quaternion.imI_sub : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R), (a - b).imI = a.imI - b.imI
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The product of two `C^n` open partial homeomorphisms is `C^n`.  -/
contDiffGroupoid_prod : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {E' : Type u_5} {H' : Type u_6}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : TopologicalSpace H']
  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {e : OpenPartialHomeomorph H H}
  {e' : OpenPartialHomeomorph H' H'},
  e ∈ contDiffGroupoid n I → e' ∈ contDiffGroupoid n I' → e.prod e' ∈ contDiffGroupoid n (I.prod I')
-- Mathlib.Order.Category.LinOrd
LinOrd.hom_comp : ∀ {X Y Z : LinOrd} (f : X ⟶ Y) (g : Y ⟶ Z),
  LinOrd.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (LinOrd.Hom.hom g).comp (LinOrd.Hom.hom f)
-- Mathlib.Topology.Separation.Basic
isOpen_setOfPred_eventually_nhdsWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {p : X → Prop},
  IsOpen {x | ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, p y}
-- Mathlib.Order.Basic
/-- **Alias** of `Decidable.lt_or_eq_of_le`. -/
LE.le.lt_or_eq_dec : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α} [DecidableLE α], a ≤ b → a < b ∨ a = b
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_add_self_mul : ∀ {a b c : ℤ}, a ∣ b + a * c ↔ a ∣ b
-- Mathlib.Data.Set.Piecewise
Set.piecewise_preimage : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] (f g : α → β) (t : Set β),
  s.piecewise f g ⁻¹' t = s.ite (f ⁻¹' t) (g ⁻¹' t)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedEntry : Inhabited Lean.Meta.Grind.Entry
-- Init.Data.List.Find
List.findIdx_singleton : ∀ {α : Type u_1} {a : α} {p : α → Bool}, List.findIdx p [a] = if p a = true then 0 else 1
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.normUnit_X : ∀ {R : Type u} [inst : CommRing R] [inst_1 : NoZeroDivisors R] [inst_2 : NormalizationMonoid R],
  normUnit Polynomial.X = 1
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.functorCategoryHasLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Functor K C)
-- Mathlib.Data.DFinsupp.WellFounded
Pi.Lex.wellFounded : ∀ {ι : Type u_1} {α : ι → Type u_2} (r : ι → ι → Prop) {s : (i : ι) → α i → α i → Prop} [IsStrictTotalOrder ι r]
  [Finite ι], (∀ (i : ι), WellFounded (s i)) → WellFounded (Pi.Lex r fun {i} => s i)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.prod_eq_top_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] [Nonempty M] [Nonempty N] {s : AddSubsemigroup M}
  {t : AddSubsemigroup N}, s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤
-- Aesop.Stats.Basic
Aesop.RuleStatsTotals.compareByTotalElapsed : Aesop.RuleStatsTotals → Aesop.RuleStatsTotals → Ordering
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_symm_apply : ∀ {F : Type u} [inst : Field F] (W : WeierstrassCurve.Jacobian F) [inst_1 : DecidableEq F] (a : W.toAffine.Point),
  (WeierstrassCurve.Jacobian.Point.toAffineAddEquiv W).symm a = WeierstrassCurve.Jacobian.Point.fromAffine a
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
/-- The canonical natural transformation from
`(whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B` to
`presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F`.  -/
CategoryTheory.toPresheafToSheafCompComposeAndSheafify : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u_1} →
        {B : Type u_2} →
          [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} B] →
              (F : CategoryTheory.Functor A B) →
                [inst_3 : CategoryTheory.HasWeakSheafify J B] →
                  [inst_4 : CategoryTheory.HasWeakSheafify J A] →
                    ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B) ⟶
                      (CategoryTheory.presheafToSheaf J A).comp (CategoryTheory.Sheaf.composeAndSheafify J F)
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry induces an isometric isomorphism between the source space and the
range of the isometry.  -/
Isometry.isometryEquivOnRange : {α : Type u} →
  {β : Type v} →
    [inst : EMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → {f : α → β} → Isometry f → α ≃ᵢ ↑(Set.range f)
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.mk.injEq : ∀ (stx : Lean.Syntax) (mpState : Lean.Parser.ModuleParserState) (cmdState : Lean.Elab.Command.State)
  (stx_1 : Lean.Syntax) (mpState_1 : Lean.Parser.ModuleParserState) (cmdState_1 : Lean.Elab.Command.State),
  ({ stx := stx, mpState := mpState, cmdState := cmdState } =
      { stx := stx_1, mpState := mpState_1, cmdState := cmdState_1 }) =
    (stx = stx_1 ∧ mpState = mpState_1 ∧ cmdState = cmdState_1)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.entails.trans' : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ⊢ₛ Q) → (P ∧ Q ⊢ₛ R) → P ⊢ₛ R
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {Ω₀ Ω : C} {truth : Ω₀ ⟶ Ω}
  {mono_truth : autoParam (CategoryTheory.Mono truth) CategoryTheory.Subobject.Classifier.mono_truth._autoParam}
  {χ₀ : (U : C) → U ⟶ Ω₀} {χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω}
  {isPullback :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (χ₀ U) (χ m) truth}
  {uniq :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] {χ₀' : U ⟶ Ω₀} {χ' : X ⟶ Ω},
      CategoryTheory.IsPullback m χ₀' χ' truth → χ' = χ m}
  {Ω₀_1 Ω_1 : C} {truth_1 : Ω₀_1 ⟶ Ω_1}
  {mono_truth_1 : autoParam (CategoryTheory.Mono truth_1) CategoryTheory.Subobject.Classifier.mono_truth._autoParam}
  {χ₀_1 : (U : C) → U ⟶ Ω₀_1} {χ_1 : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω_1}
  {isPullback_1 :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (χ₀_1 U) (χ_1 m) truth_1}
  {uniq_1 :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] {χ₀' : U ⟶ Ω₀_1} {χ' : X ⟶ Ω_1},
      CategoryTheory.IsPullback m χ₀' χ' truth_1 → χ' = χ_1 m},
  { Ω₀ := Ω₀, Ω := Ω, truth := truth, mono_truth := mono_truth, χ₀ := χ₀, χ := χ, isPullback := isPullback,
        uniq := uniq } =
      { Ω₀ := Ω₀_1, Ω := Ω_1, truth := truth_1, mono_truth := mono_truth_1, χ₀ := χ₀_1, χ := χ_1,
        isPullback := isPullback_1, uniq := uniq_1 } →
    Ω₀ = Ω₀_1 ∧ Ω = Ω_1 ∧ truth ≍ truth_1 ∧ χ₀ ≍ χ₀_1 ∧ χ ≍ χ_1
-- Mathlib.Logic.Basic
/-- **Alias** of `not_congr`. -/
Iff.not : ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hurwitzZetaEven_apply_zero : ∀ (a : UnitAddCircle), HurwitzZeta.hurwitzZetaEven a 0 = if a = 0 then -1 / 2 else 0
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedPreElabHeaderResult : Inhabited Lean.Elab.Command.PreElabHeaderResult
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.Walk.IsCircuit.egirth_le_length : ∀ {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a}, w.IsCircuit → G.egirth ≤ ↑w.length
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_roc_eq_mkSlice_rcc : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rcc.Sliceable.mkSlice xs (lo + 1)...=hi
-- Init.Core
instTransIff : Trans Iff Iff Iff
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.hasPullback_op_iff_hasPushout : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.Limits.HasPullback f.op g.op ↔ CategoryTheory.Limits.HasPushout f g
-- Batteries.Data.List.Lemmas
List.findIdxNth.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (xs : List α) (n : ℕ), List.findIdxNth p xs n = List.findIdxNth.go p xs n 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Real.sinc_apply : ∀ {x : ℝ}, Real.sinc x = if x = 0 then 1 else Real.sin x / x
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
IsStrictlyPositive.isUnit_cfcSqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A),
  autoParam (IsStrictlyPositive a) IsStrictlyPositive.isUnit_cfcSqrt._auto_1 → IsUnit (CFC.sqrt a)
-- Lean.Compiler.IR.Basic
/-- Store `y` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1.
This operation is not part of λPure is only used during optimization.  -/
Lean.IR.FnBody.set : Lean.IR.VarId → ℕ → Lean.IR.Arg → Lean.IR.FnBody → Lean.IR.FnBody
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst.injEq : ∀ (n n_1 : ℕ),
  (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n = Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n_1) = (n = n_1)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- The symmetric difference of two `iSup`s is at most the `iSup` of the symmetric differences.  -/
iSup_symmDiff_iSup_le : ∀ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {f g : ι → α},
  symmDiff (⨆ i, f i) (⨆ i, g i) ≤ ⨆ i, symmDiff (f i) (g i)
-- Mathlib.Order.Filter.NAry
Filter.le_map₂_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β} {h : Filter γ},
  h ≤ Filter.map₂ m f g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → Set.image2 m s t ∈ h
-- Mathlib.Data.Set.Subset
Set.image_val_sUnion : ∀ {α : Type u_2} {A : Set α} {T : Set (Set ↑A)}, Subtype.val '' ⋃₀ T = ⋃₀ {x | ∃ B ∈ T, Subtype.val '' B = x}
-- Mathlib.GroupTheory.Transfer
/-- The transfer transversal. Contains elements of the form `g ^ k • g₀` for fixed choices
of representatives `g₀` of fixed choices of representatives `q₀` of `⟨g⟩`-orbits in `G ⧸ H`.  -/
Subgroup.transferTransversal : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → G → H.LeftTransversal
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An orbit of a normal subgroup is a block  -/
AddAction.IsBlock.orbit_of_normal : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {N : AddSubgroup G} [N.Normal] (a : X),
  AddAction.IsBlock G (AddAction.orbit (↥N) a)
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.instQuotientSubgroupOfFinite : ∀ {G : Type u_1} [inst : Group G] [Finite G] [IsZGroup G] (H : Subgroup G) [inst_3 : H.Normal], IsZGroup (G ⧸ H)
-- Mathlib.LinearAlgebra.Matrix.Cartan
/-- The Cartan matrix of type Cₙ (rank n, corresponding to sp(2n)).  -/
CartanMatrix.C : (n : ℕ) → Matrix (Fin n) (Fin n) ℤ
-- Mathlib.Analysis.Matrix.Order
/-- The partial order on matrices given by `A ≤ B := (B - A).PosSemidef`.  -/
Matrix.instPartialOrder : {𝕜 : Type u_1} → {n : Type u_2} → [RCLike 𝕜] → PartialOrder (Matrix n n 𝕜)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instModule : {R : Type u_1} →
  {S : Type u_2} → [inst : Semiring R] → [inst_1 : AddCommMonoid S] → [Module R S] → Module R (ArithmeticFunction S)
-- Mathlib.Data.Set.Image
Set.disjoint_image_inl_image_inr : ∀ {α : Type u_1} {β : Type u_2} {u : Set α} {v : Set β}, Disjoint (Sum.inl '' u) (Sum.inr '' v)
-- Init.Data.SInt.Bitwise
Int8.not_xor : ∀ {a b : Int8}, ~~~a ^^^ b = ~~~(a ^^^ b)
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.aeval_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : ℕ) {A : Type u_5} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] (f : σ → A) (φ : MvPolynomial σ R),
  (MvPolynomial.aeval f) ((MvPolynomial.expand p) φ) = (MvPolynomial.aeval (f ^ p)) φ
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.precoverage_top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C], ⊤.precoverage = ⊤