mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Sat.FromLRAT
/-- Build the main proof of `⊢ ctx.proof []` using the LRAT proof trace.

* `arr`: The input CNF
* `ctx`: The abbreviated formula, a constant like `foo.ctx_1`
* `ctx'`: The definitional expansion of the formula, a tree of `Fmla.and` nodes
* `steps`: The input LRAT proof trace
 -/
Mathlib.Tactic.Sat.buildProof : Array (Array ℤ) → Lean.Expr → Lean.Expr → Array Mathlib.Tactic.Sat.LRATStep → Lean.MetaM Lean.Expr
-- Init.Internal.Order.Basic
Lean.Order.fun_sup_is_sup : ∀ {α : Sort u} {β : α → Sort v} [inst : (x : α) → Lean.Order.CompleteLattice (β x)] (c : ((x : α) → β x) → Prop),
  Lean.Order.is_sup c (Lean.Order.fun_sup c)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.RankFinite.mk : ∀ {α : Type u_1} {M : Matroid α}, (∃ B, M.IsBase B ∧ B.Finite) → M.RankFinite
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Auxiliary definition for `costructuredArrowToOverEquivalence`.  -/
CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.inverse : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D T) →
          {X : T} →
            (Y : CategoryTheory.Over X) →
              CategoryTheory.Functor (CategoryTheory.CostructuredArrow F Y.left)
                (CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.toOver F X) Y)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} {z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n}, z₁ = z₂ ↔ ↑z₁ = ↑z₂
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.IterM.step_intermediateDropWhile.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : true = true → motive true) (h_2 : true = false → motive false),
  (match hP : true with
    | true => h_1 hP
    | false => h_2 hP) =
    h_1 ⋯
-- Mathlib.Algebra.Order.UpperLower
lowerClosure_vadd : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] (s : Set α) (a : α),
  lowerClosure (a +ᵥ s) = a +ᵥ lowerClosure s
-- Init.Data.Rat.Lemmas
Rat.den_mul : ∀ (a b : ℚ), (a * b).den = a.den * b.den / (a.num * b.num).natAbs.gcd (a.den * b.den)
-- Mathlib.Data.Set.Restrict
/-- Restrict codomain of a function `f` to a set `s`. Same as `Subtype.coind` but this version
has codomain `↥s` instead of `Subtype s`.  -/
Set.codRestrict : {α : Type u_1} → {ι : Sort u_5} → (f : ι → α) → (s : Set α) → (∀ (x : ι), f x ∈ s) → ι → ↑s
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.mk_toWord : ∀ {α : Type u_1} [inst : DecidableEq α] {x : FreeAddGroup α}, FreeAddGroup.mk x.toWord = x
-- Lean.LibrarySuggestions.SineQuaNon
/-- Combine two trigger maps, taking the sorted union of the triggered theorems for each symbol.
If one map is much larger than the other, it should be the first argument.
 -/
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.combineTriggers : Lean.NameMap (List (Lean.Name × Float)) →
  Lean.NameMap (List (Lean.Name × Float)) → Lean.NameMap (List (Lean.Name × Float))
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance between two sets is the smallest nonnegative `r` such that each set is
included in the `r`-neighborhood of the other. If there is no such `r`, it is defined to
be `0`, arbitrarily.  -/
Metric.hausdorffDist : {α : Type u} → [PseudoMetricSpace α] → Set α → Set α → ℝ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {outWidth : ℕ} [inst_2 : SizeOf α]
  {w : ℕ} (x : aig.RefVec w) (h : outWidth = w * w),
  sizeOf { w := w, x := x, h := h } = 1 + sizeOf w + sizeOf x + sizeOf h
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_eq_add_fract_mul : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] [inst_3 : FloorRing α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a b = a + Int.fract ((b - a) / p) * p
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : Option β → Option β},
  t.alter k f ≠ ∅ → ((t.alter k f).minKey! = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Mathlib.Data.Set.Insert
Set.instLawfulSingleton : ∀ {α : Type u_1}, LawfulSingleton α (Set α)
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_re_zero_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), RCLike.re (inner 𝕜 0 x) = 0
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.comp_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {X Y Z : CategoryTheory.Span Wₗ Wᵣ c c'} (φ : X.Hom Y) (φ' : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp φ φ').hom = CategoryTheory.CategoryStruct.comp φ.hom φ'.hom
-- Mathlib.CategoryTheory.Subobject.Comma
/-- Every subobject of a structured arrow can be projected to a subobject of the underlying
object.  -/
CategoryTheory.StructuredArrow.projectSubobject : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T : CategoryTheory.Functor C D} →
            [CategoryTheory.Limits.HasFiniteLimits C] →
              [CategoryTheory.Limits.PreservesFiniteLimits T] →
                {A : CategoryTheory.StructuredArrow S T} → CategoryTheory.Subobject A → CategoryTheory.Subobject A.right
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.notConvergentSeq_measurableSet : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β] {n : ℕ} {j : ι}
  {f : ι → α → β} {g : α → β} [inst_1 : Preorder ι] [Countable ι],
  (∀ (n : ι), Measurable fun a => edist (f n a) (g a)) → MeasurableSet (MeasureTheory.Egorov.notConvergentSeq f g n j)
-- Mathlib.Analysis.Calculus.VectorField
/-- The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric
second derivative. Version in a complete space. One could also give a version avoiding
completeness but requiring that `f` is a local diffeomorphism.  -/
VectorField.pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  [CompleteSpace E] {f : E → F} {V W : F → F} {x : E} {t : Set F},
  IsSymmSndFDerivWithinAt 𝕜 f s x →
    ContDiffWithinAt 𝕜 2 f s x →
      DifferentiableWithinAt 𝕜 V t (f x) →
        DifferentiableWithinAt 𝕜 W t (f x) →
          UniqueDiffOn 𝕜 s →
            x ∈ s →
              Set.MapsTo f s t →
                VectorField.pullbackWithin 𝕜 f (VectorField.lieBracketWithin 𝕜 V W t) s x =
                  VectorField.lieBracketWithin 𝕜 (VectorField.pullbackWithin 𝕜 f V s)
                    (VectorField.pullbackWithin 𝕜 f W s) s x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.canonical_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.LeftHomologyData.canonical S).π = S.homologyπ
-- Mathlib.Data.List.Count
List.countP_erase : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (p : α → Bool) (l : List α) (a : α),
  List.countP p (l.erase a) = List.countP p l - if a ∈ l ∧ p a = true then 1 else 0
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] [inst_5 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (q : Submodule K (Module.Dual K ↥H))
  (hq : ∀ (i : ↥LieSubalgebra.root), q ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection i)),
  ↑(LieAlgebra.IsKilling.invtSubmoduleToLieIdeal q hq) = ↑(⨆ α, LieAlgebra.IsKilling.sl2SubmoduleOfRoot ⋯)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.cgf_const' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsFiniteMeasure μ],
  μ ≠ 0 → ∀ (c : ℝ), ProbabilityTheory.cgf (fun x => c) μ t = Real.log (μ.real Set.univ) + t * c
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.coe_sSup_apply' : ∀ {E : Type u_3} [inst : AddGroup E] {s : Set (AddGroupSeminorm E)},
  BddAbove s → ∀ {x : E}, (sSup s) x = sSup ((fun x_1 => x_1 x) '' s)
-- Mathlib.Order.Directed
IsMin.isBot : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [IsCodirectedOrder α], IsMin a → IsBot a
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.zero_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f : X → E}, MeasureTheory.VectorMeasure.Integrable 0 f
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.topologicalClosure_mono : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : Star A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A] [inst_5 : ContinuousStar A] [inst_6 : ContinuousConstSMul R A]
  [inst_7 : IsSemitopologicalSemiring A] {s t : NonUnitalStarSubalgebra R A},
  s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- Weaker version of the **monotone convergence theorem**.  -/
MeasureTheory.lintegral_iSup_ae : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
  (∀ (n : ℕ), Measurable (f n)) →
    (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a) → ∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
-- Init.Data.Array.BinSearch
/-- Binary search for an element equivalent to `k` in the sorted array `as`. Returns `true` if the
element is found, or `false` otherwise.

The array `as` must be sorted according to the comparison operator `lt`, which should be a total
order.

The optional parameters `lo` and `hi` determine the region of the array indices to be searched. Both
are inclusive, and default to searching the entire array.
 -/
Array.binSearchContains : {α : Type} → (as : Array α) → α → (α → α → Bool) → optParam ℕ 0 → optParam ℕ (as.size - 1) → Bool
-- Lean.Server.FileWorker.InlayHints
Lean.Elab.InlayHintInfo.toLspInlayHint : Lean.FileMap → Lean.Elab.InlayHintInfo → IO Lean.Lsp.InlayHint
-- Mathlib.Data.Multiset.Dedup
/-- **Alias** of the reverse direction of `Multiset.dedup_eq_self`. -/
Multiset.Nodup.dedup : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s.Nodup → s.dedup = s
-- Mathlib.Topology.Homeomorph.Defs
HomeomorphClass.map_continuous : ∀ {F : Type u_5} {A : outParam (Type u_6)} {B : outParam (Type u_7)} {inst : TopologicalSpace A}
  {inst_1 : TopologicalSpace B} {h : EquivLike F A B} [self : HomeomorphClass F A B] (f : F), Continuous ⇑f
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.exact : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p q : Path x₀ x₁},
  Path.Homotopic.Quotient.mk p = Path.Homotopic.Quotient.mk q → p.Homotopic q
-- Init.Data.BitVec.Lemmas
BitVec.toFin_zero : ∀ {w : ℕ}, BitVec.toFin 0 = 0
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_3.eq_3 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : (CategoryTheory.WithInitial C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3)
  (x :
    Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
      Opposite.unop (Opposite.op CategoryTheory.WithInitial.star))
  (x_1 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star)
  (h_1 :
    (x y : C) →
      (f :
          Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of y)) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of x))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of x) ⟶ Opposite.op (CategoryTheory.WithInitial.of y)) →
          motive (Opposite.op (CategoryTheory.WithInitial.of x)) (Opposite.op (CategoryTheory.WithInitial.of y)) f x_2)
  (h_2 :
    (a : C) →
      (x :
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of a))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of a) ⟶ Opposite.op CategoryTheory.WithInitial.star) →
          motive (Opposite.op (CategoryTheory.WithInitial.of a)) (Opposite.op CategoryTheory.WithInitial.star) x x_2)
  (h_3 :
    (x :
        Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star)) →
      (x_2 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star) →
        motive (Opposite.op CategoryTheory.WithInitial.star) (Opposite.op CategoryTheory.WithInitial.star) x x_2),
  (match Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_1 with
    | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_2 =>
      h_1 x y f x_2
    | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_2 a x x_2
    | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_3 x x_2) =
    h_3 x x_1
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- A *strong FE-pair* is a weak FE-pair in which `f₀` and `g₀` are zero.  -/
IsStrongFEPair : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → Prop
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_subset_Ioc_left : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₁ ≤ a₂ → Set.Ioc a₂ b ⊆ Set.Ioc a₁ b
-- Mathlib.Order.Interval.Set.Basic
/-- If `a ≤ b`, then `(-∞, a) ⊆ (-∞, b]`. In preorders, this is just an implication. If you need
the equivalence in dense linear orders, use `Iio_subset_Iic_iff`.  -/
Set.Iio_subset_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → Set.Iio a ⊆ Set.Iic b
-- Mathlib.Topology.Order.OrderClosed
Icc_mem_nhdsLT_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b c : α},
  b ∈ Set.Ioc a c → Set.Icc a c ∈ nhdsWithin b (Set.Iio b)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instInhabitedSimpTheorems : Inhabited Lean.Meta.SimpTheorems
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- **Alias** of `WithSeminorms.continuous_normedSpace_rng`. -/
Seminorm.cont_withSeminorms_normedSpace : ∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {ι : Type u_9} [inst : AddCommGroup E] [inst_1 : NormedField 𝕝]
  [inst_2 : Module 𝕝 E] [inst_3 : NormedField 𝕝₂] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_4 : RingHomIsometric τ₁₂] (F : Type u_11)
  [inst_5 : SeminormedAddCommGroup F] [inst_6 : NormedSpace 𝕝₂ F] [inst_7 : TopologicalSpace E] {p : ι → Seminorm 𝕝 E},
  WithSeminorms p → ∀ (f : E →ₛₗ[τ₁₂] F), (∃ s C, (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p) → Continuous ⇑f
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.hom_hom_rightUnitor : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R},
  ModuleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = ↑(TensorProduct.rid R ↑M)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
Unitary.inner_map_map : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] (u : ↥(unitary (H →L[𝕜] H))) (x y : H), inner 𝕜 (↑u x) (↑u y) = inner 𝕜 x y
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
IsIntegralClosure.isLocalization_of_isSeparable : ∀ (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (L : Type u_3) [inst_4 : Field L] (C : Type u_4) [inst_5 : CommRing C] [inst_6 : Algebra K L] [inst_7 : Algebra A L]
  [IsScalarTower A K L] [inst_9 : Algebra C L] [IsIntegralClosure C A L] [inst_11 : Algebra A C] [IsScalarTower A C L]
  [IsDomain A] [Algebra.IsSeparable K L], IsLocalization (Algebra.algebraMapSubmonoid C (nonZeroDivisors A)) L
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.isOpen_image_iff_of_subset_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X}, s ⊆ e.source → (IsOpen (↑e '' s) ↔ IsOpen s)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.equiv_iff_keysArray_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.DTreeMap α (fun x => Unit) cmp},
  t₁.Equiv t₂ ↔ t₁.keysArray = t₂.keysArray
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.equiv_of_beq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap α β cmp} [inst : (k : α) → BEq (β k)]
  [inst_1 : Std.LawfulEqCmp cmp] [Std.TransCmp cmp] [∀ (k : α), LawfulBEq (β k)], (m₁ == m₂) = true → m₁.Equiv m₂
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.opensRange_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g],
  AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.CategoryStruct.comp f g) =
    (AlgebraicGeometry.Scheme.Hom.opensFunctor g).obj (AlgebraicGeometry.Scheme.Hom.opensRange f)
-- Mathlib.Algebra.Field.Defs
/-- Every nonzero element of a group with zero is invertible.  -/
Semifield.mul_inv_cancel : ∀ {K : Type u_2} [self : Semifield K] (a : K), a ≠ 0 → a * a⁻¹ = 1
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimitCore.funext : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  (self : c.IsColimitCore) {T : Type w₂} {f g : c.pt → T}, (∀ (j : J), f ∘ c.ι j = g ∘ c.ι j) → f = g
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.lt_iff_exists : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LT a b ↔ ∃ n, Std.PRange.succMany? (n + 1) a = some b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (f : x ⟶ y) (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).map f).fst.app X_1 =
    ψ.left.map (f.fst.app X_1)
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.value : Lean.Elab.PreDefinition → Lean.Expr
-- Init.Data.SInt.Lemmas
Int64.toInt8_ofNat' : ∀ {n : ℕ}, (Int64.ofNat n).toInt8 = Int8.ofNat n
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_eq : ∀ (a b : UInt32), a.toUInt16 = b.toUInt16 ↔ a % 65536 = b % 65536
-- Mathlib.Order.Lex
/-- A type synonym to equip a type with its lexicographic order.  -/
Colex : Type u_2 → Type u_2
-- Mathlib.Data.Int.GCD
Nat.xgcdAux.eq_1 : ∀ (t : ℕ),
  t.xgcdAux =
    Nat.strongRec (motive := fun x => ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
      (fun n ih s t r' s' t' =>
        match n, ih with
        | 0, ih => (r', s', t')
        | k.succ, ih =>
          have q := r' / k.succ;
          ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
      t
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ratio_ne_zero : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F), Dilation.ratio f ≠ 0
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- We define the global sections functor as the right-adjoint of the constant sheaf functor
whenever it exists.  -/
CategoryTheory.Sheaf.Γ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          [inst_2 : CategoryTheory.HasWeakSheafify J A] →
            [CategoryTheory.HasGlobalSectionsFunctor J A] → CategoryTheory.Functor (CategoryTheory.Sheaf J A) A
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- A quiver `HasInvolutiveReverse` if reversing twice is the identity.  -/
Quiver.HasInvolutiveReverse : (V : Type u_2) → [Quiver V] → Type (max u_2 v)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The "forward" image of a subgroupoid under a functor injective on objects  -/
CategoryTheory.Subgroupoid.map : {C : Type u} →
  [inst : CategoryTheory.Groupoid C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Groupoid D] →
        (φ : CategoryTheory.Functor C D) →
          Function.Injective φ.obj → CategoryTheory.Subgroupoid C → CategoryTheory.Subgroupoid D
-- Mathlib.Algebra.FreeMonoid.Basic
/-- Embeds an element of `α` into `FreeAddMonoid α` as a singleton list.  -/
FreeAddMonoid.of : {α : Type u_1} → α → FreeAddMonoid α
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- Auxiliary lemma for tangent spaces: the derivative of a coordinate change between two charts is
`C^n` on its source.  -/
contDiffOn_fderiv_coord_change : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I (n + 1) M] (i j : ↑(atlas H M)),
  ContDiffOn 𝕜 n (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (Set.range ↑I))
    (((↑i).extend I).symm.trans ((↑j).extend I)).source
-- Mathlib.Data.Holor
Holor.slice_unitVec_mul : ∀ {α : Type} {d : ℕ} {ds : List ℕ} [inst : Semiring α] {i j : ℕ} (hid : i < d) (x : Holor α ds),
  ((Holor.unitVec d j).mul x).slice i hid = if i = j then x else 0
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
ZMod.χ₄_nat_eq_if_mod_four : ∀ (n : ℕ), ZMod.χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_map : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix n n R) {S : Type u_4} [inst_3 : CommSemiring S] (f : R →+* S),
  Matrix.detp s (A.map ⇑f) = f (Matrix.detp s A)
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.digitsAux0.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_eq : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α],
  ProbabilityTheory.IsMeasurableRatCDF f →
    ∀ (a : α) (r : ℚ), ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a ↑r = f a r