mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitYonedaHomIsoLimitRightOp_π_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor Iᵒᵖ C) (F : CategoryTheory.Functor Cᵒᵖ (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.comp CategoryTheory.yoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))]
  (f : CategoryTheory.Limits.colimit (D.comp CategoryTheory.yoneda) ⟶ F) (i : I),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π (D.rightOp.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitYonedaHomIsoLimitRightOp D F).hom) f) =
    {
      down :=
        (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op (D.obj (Opposite.op i)))))
          ((CategoryTheory.ConcreteCategory.hom
              ((CategoryTheory.Limits.colimit.ι (D.comp CategoryTheory.yoneda) (Opposite.op i)).app
                (Opposite.op (D.obj (Opposite.op i)))))
            (CategoryTheory.CategoryStruct.id (D.obj (Opposite.op i)))) }
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigO_norm_right`. -/
Asymptotics.IsBigO.norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, f =O[l] g' → f =O[l] fun x => ‖g' x‖
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.preadditiveYonedaMap_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v, u₁} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] (X : C) (Y : Cᵒᵖ),
  (CategoryTheory.preadditiveYonedaMap F X).app Y = AddCommGrpCat.ofHom F.mapAddHom
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.Monic.leadingCoeff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → p.leadingCoeff = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app : ∀ {X Y : SSet.Truncated 2}
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))
  (y : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso X Y).hom.app
      (SSet.Truncated.HomotopyCategory.mk x, SSet.Truncated.HomotopyCategory.mk y) =
    CategoryTheory.CategoryStruct.id
      (((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
            (SSet.Truncated.HomotopyCategory.BinaryProduct.functor X Y)).obj
        (SSet.Truncated.HomotopyCategory.mk x, SSet.Truncated.HomotopyCategory.mk y))
-- Lean.LibrarySuggestions.Basic
_private.Lean.LibrarySuggestions.Basic.0.Lean.Expr.FoldRelevantConstantsImpl.fold : {α : Type} → (Lean.Name → α → Lean.MetaM α) → Lean.Expr → α → Lean.Expr.FoldRelevantConstantsImpl.FoldM✝ α
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Non-unital normed commutative ring structure on the product of two non-unital normed
commutative rings, using the sup norm.  -/
Prod.nonUnitalNormedCommRing : {α : Type u_2} →
  {β : Type u_3} → [NonUnitalNormedCommRing α] → [NonUnitalNormedCommRing β] → NonUnitalNormedCommRing (α × β)
-- Mathlib.Logic.Function.Iterate
Function.iterate_succ_apply' : ∀ {α : Type u} (f : α → α) (n : ℕ) (x : α), f^[n.succ] x = f (f^[n] x)
-- Init.Data.Array.Lemmas
Array.isEmpty_push : ∀ {α : Type u_1} {x : α} {xs : Array α}, (xs.push x).isEmpty = false
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeIsoApp.match_1.eq_3 : ∀ (C : Type u_1)
  (motive :
    CategoryTheory.FreeMonoidalCategory C →
      (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C → Sort u_2)
  (X a : CategoryTheory.FreeMonoidalCategory C)
  (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
  (h_1 :
    (a : C) →
      (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
        motive (CategoryTheory.FreeMonoidalCategory.of a) x)
  (h_2 :
    (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
      motive CategoryTheory.FreeMonoidalCategory.unit x)
  (h_3 :
    (X a : CategoryTheory.FreeMonoidalCategory C) →
      (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
        motive (X.tensor a) n),
  (match X.tensor a, n with
    | CategoryTheory.FreeMonoidalCategory.of a, x => h_1 a x
    | CategoryTheory.FreeMonoidalCategory.unit, x => h_2 x
    | X.tensor a, n => h_3 X a n) =
    h_3 X a n
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ringEquivOfRingEquiv_spanSingleton : ∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CommRing S] [inst_3 : 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) (x : K),
  (FractionalIdeal.ringEquivOfRingEquiv K L f) (FractionalIdeal.spanSingleton (nonZeroDivisors R) x) =
    FractionalIdeal.spanSingleton (nonZeroDivisors S) ((IsFractionRing.ringEquivOfRingEquiv f) x)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.toList_insert_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {v : β},
  (Std.DHashMap.Const.toList (m.insert k v)).Perm
    ((k, v) :: List.filter (fun x_2 => decide ¬(k == x_2.1) = true) (Std.DHashMap.Const.toList m))
-- Mathlib.Order.Hom.Bounded
TopHom.top_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : LE β] [inst_2 : OrderTop β] (a : α), ⊤ a = ⊤
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.instSetLike : {α : Type u_2} → [inst : BooleanAlgebra α] → SetLike (BooleanSubalgebra α) α
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_range : ∀ {X Y : SSet} (f : X ⟶ Y), (SSet.Subcomplex.range f).preimage f = ⊤
-- Mathlib.Data.Nat.Factorization.Induction
/-- Given `P 0, P 1` and a way to extend `P a` to `P (p ^ n * a)` for prime `p` not dividing `a`,
we can define `P` for all natural numbers.  -/
Nat.recOnPrimePow : {motive : ℕ → Sort u_1} →
  motive 0 →
    motive 1 → ((a p n : ℕ) → Nat.Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)) → (a : ℕ) → motive a
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.getSimprocs : Lean.CoreM Lean.Meta.Simprocs
-- Std.Data.TreeSet.Basic
/-- Compares two tree sets using Boolean equality on keys.

Returns `true` if the sets contain the same keys, `false` otherwise.
 -/
Std.TreeSet.beq : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → Std.TreeSet α cmp → Bool
-- Mathlib.Tactic.FunProp.FunctionData
/-- Decompose function `f = (← fData.toExpr)` into composition of two functions.  -/
Mathlib.Meta.FunProp.FunctionData.decomposition : Mathlib.Meta.FunProp.FunctionData → Lean.MetaM Mathlib.Meta.FunProp.DecompositionResult
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.xa_mul_a : ∀ {n : ℕ} (i j : ZMod (2 * n)), QuaternionGroup.xa i * QuaternionGroup.a j = QuaternionGroup.xa (i + j)
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.step.match_3.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : Lean.PersistentHashMap.Zipper α β → Sort u_3) (keys : Subarray α)
  (vals : Subarray β) (hsz : Std.Slice.size keys = Std.Slice.size vals) (z' : Lean.PersistentHashMap.Zipper α β)
  (h_1 : Unit → motive Lean.PersistentHashMap.Zipper.done)
  (h_2 :
    (es : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      (z' : Lean.PersistentHashMap.Zipper α β) → motive (Lean.PersistentHashMap.Zipper.consEntries es z'))
  (h_3 :
    (keys : Subarray α) →
      (vals : Subarray β) →
        (hsz : Std.Slice.size keys = Std.Slice.size vals) →
          (z' : Lean.PersistentHashMap.Zipper α β) →
            motive (Lean.PersistentHashMap.Zipper.consCollision keys vals hsz z')),
  (match Lean.PersistentHashMap.Zipper.consCollision keys vals hsz z' with
    | Lean.PersistentHashMap.Zipper.done => h_1 ()
    | Lean.PersistentHashMap.Zipper.consEntries es z' => h_2 es z'
    | Lean.PersistentHashMap.Zipper.consCollision keys vals hsz z' => h_3 keys vals hsz z') =
    h_3 keys vals hsz z'
-- Mathlib.Logic.Basic
forall_and_index' : ∀ {p q : Prop} {r : p → q → Prop}, (∀ (hp : p) (hq : q), r hp hq) ↔ ∀ (h : p ∧ q), r ⋯ ⋯
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceCastAdd : Lean.Meta.Simp.DSimproc
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
LinearMap.IsPerfectCompl.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (p p_1 : M →ₗ[R] N →ₗ[R] R) (e_p : p = p_1) [inst_5 : p.IsPerfPair]
  (U U_1 : Submodule R M),
  U = U_1 → ∀ (V V_1 : Submodule R N), V = V_1 → p.IsPerfectCompl U V = p_1.IsPerfectCompl U_1 V_1
-- Init.Data.Range.Polymorphic.Basic
/-- Checks whether the range contains any value.
This function exists for completeness and always returns false:
The closed lower bound is contained in the range, so
left-closed right-unbounded ranges are never empty.
 -/
Std.Rci.isEmpty : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.Rci α → Bool
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_getKey? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {a : α} {h' : (m.getKey? a).isSome = true}, (m.getKey? a).get h' = m.getKey a ⋯
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forgetToTop
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.instTensorProduct : ∀ (R : Type u) (M : Type v) (N : Type u_1) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [Module.Invertible R M] [Module.Invertible R N],
  Module.Invertible R (TensorProduct R M N)
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.mem_conjGL : ∀ {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {g : GL (Fin 2) ℝ} {x : Matrix.SpecialLinearGroup (Fin 2) ℤ},
  x ∈ CongruenceSubgroup.conjGL Γ g ↔
    ∃ y ∈ Γ,
      Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) y) =
        g * Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) x) * g⁻¹
-- Mathlib.Data.Seq.Basic
Stream'.Seq.Pairwise.cons_elim : ∀ {α : Type u} {R : α → α → Prop} {hd : α} {tl : Stream'.Seq α},
  Stream'.Seq.Pairwise R (Stream'.Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ Stream'.Seq.Pairwise R tl
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.covarianceBilinDual_comm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : BorelSpace E] (L₁ L₂ : StrongDual ℝ E),
  ((ProbabilityTheory.covarianceBilinDual μ) L₁) L₂ = ((ProbabilityTheory.covarianceBilinDual μ) L₂) L₁
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Helper function for reducing homogeneous unary bitvector operators.
 -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.reduceUnary : Lean.Name → ℕ → ({n : ℕ} → BitVec n → BitVec n) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialCosimplicialEquiv_counitIso_inv_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor SimplexCategory Cᵒᵖ)
  (X_1 : SimplexCategory),
  ((CategoryTheory.simplicialCosimplicialEquiv C).counitIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular],
  CategoryTheory.IsCardinalPresentable X κ ↔
    (CategoryTheory.uliftCoyoneda.{t, v₁, u₁}.obj (Opposite.op X)).IsCardinalAccessible κ
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- If `x` is a conjugate root of `0`, then `x = 0`.
 -/
IsConjRoot.eq_zero : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] [IsDomain S] {x : S},
  IsConjRoot K 0 x → x = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `AddMonoidAlgebra.single m r` for `m : M`, `r : R` is the element `rm : R[M]`.  -/
AddMonoidAlgebra.single : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → M → R → AddMonoidAlgebra R M
-- Lean.DocString.Types
/-- No inline content.  -/
Lean.Doc.Inline.empty : {i : Type u_1} → Lean.Doc.Inline i
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₁_hom_comp_i : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).hom
      (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.i =
    CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 1) (groupCohomology.cochainsIso₁ A).hom
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- The `p`-adic valuation of `n!` is equal to the `p`-adic valuation of the factorial of the
largest multiple of `p` below `n`, i.e. `(p * ⌊n / p⌋)!`.  -/
padicValNat_mul_div_factorial : ∀ {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)], padicValNat p (p * (n / p)).factorial = padicValNat p n.factorial
-- Mathlib.CategoryTheory.Shift.Opposite
/-- The category `OppositeShift C A` is the opposite category `Cᵒᵖ` equipped
with the naive shift: `shiftFunctor (OppositeShift C A) n` is `(shiftFunctor C n).op`.  -/
CategoryTheory.OppositeShift : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (A : Type u_3) → [inst_1 : AddMonoid A] → [CategoryTheory.HasShift C A] → Type (max 0 u_1)
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Construct the equivalence class `[f]` of an almost everywhere measurable function `f`, based
on the equivalence relation of being almost everywhere equal.  -/
MeasureTheory.AEEqFun.mk : {α : Type u_1} →
  [inst : MeasurableSpace α] →
    {μ : MeasureTheory.Measure α} →
      {β : Type u_5} → [inst_1 : TopologicalSpace β] → (f : α → β) → MeasureTheory.AEStronglyMeasurable f μ → α →ₘ[μ] β
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.adjoin_rank_le_of_isAlgebraic_right : ∀ {F : Type u_1} [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K)
  [halg : Algebra.IsAlgebraic F ↥L], Module.rank E ↥(IntermediateField.adjoin E ↑L) ≤ Module.rank F ↥L
-- Mathlib.Algebra.Order.Group.DenselyOrdered
add_le_of_forall_lt : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a b c : α},
  (∀ a' < a, ∀ b' < b, a' + b' ≤ c) → a + b ≤ c
-- Init.Data.String.Lemmas.Hashable
String.hash_eq : ∀ {s : String}, hash s = s.hash
-- Lean.Meta.GeneralizeVars
_private.Lean.Meta.GeneralizeVars.0.Lean.Meta.mkGeneralizationForbiddenSet.loop : List Lean.FVarId → Lean.FVarIdSet → Lean.MetaM Lean.FVarIdSet
-- Mathlib.Topology.Order.SuccPred
SuccOrder.accPt_principal : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α]
  {a : α} {s : Set α}, AccPt a (Filter.principal s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Set.Ioo b a).Nonempty
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.ext_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] {S T : NonUnitalStarSubalgebra R A}, S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ T
-- Lean.Data.Json.Basic
Lean.JsonNumber.toString : Lean.JsonNumber → String
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_of_re_neg_of_im_nonneg : ∀ {x : ℂ}, x.re < 0 → 0 ≤ x.im → x.arg = Real.arcsin ((-x).im / ‖x‖) + Real.pi
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.CommShift.commShift_unit : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {adj : F ⊣ G} {A : Type u_3} {inst_2 : AddMonoid A} {inst_3 : CategoryTheory.HasShift C A}
  {inst_4 : CategoryTheory.HasShift D A} {inst_5 : F.CommShift A} {inst_6 : G.CommShift A} [self : adj.CommShift A],
  CategoryTheory.NatTrans.CommShift adj.unit A
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.lTensor_bijective_iff_bijective : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_4}
  {N' : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N] [inst_6 : Module R N']
  (f : N →ₗ[R] N') [Module.FaithfullyFlat R M], Function.Bijective ⇑(LinearMap.lTensor M f) ↔ Function.Bijective ⇑f
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.EquicontinuousOn.continuousOn_of_mem : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {H : Set (X → α)} {S : Set X},
  H.EquicontinuousOn S → ∀ {f : X → α}, f ∈ H → ContinuousOn f S
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
CategoryTheory.Limits.IsTerminal.isTerminalObj.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X : C)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G]
  (l l_1 : CategoryTheory.Limits.IsTerminal X),
  l = l_1 →
    CategoryTheory.Limits.IsTerminal.isTerminalObj G X l = CategoryTheory.Limits.IsTerminal.isTerminalObj G X l_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₁ → (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.inter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A B C : Set E}, IsExtreme 𝕜 A B → IsExtreme 𝕜 A C → IsExtreme 𝕜 A (B ∩ C)
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findFinIdx?.go.match_1.eq_1 : ∀ {α : Type u_1} (l : List α) (motive : (x : List α) → (x_1 : ℕ) → x.length + x_1 = l.length → Sort u_2) (x : ℕ)
  (x_1 : [].length + x = l.length) (h_1 : (x : ℕ) → (x_2 : [].length + x = l.length) → motive [] x x_2)
  (h_2 : (a : α) → (l_1 : List α) → (i : ℕ) → (h : (a :: l_1).length + i = l.length) → motive (a :: l_1) i h),
  (match [], x, x_1 with
    | [], x, x_2 => h_1 x x_2
    | a :: l_1, i, h => h_2 a l_1 i h) =
    h_1 x x_1
-- Mathlib.Order.Lattice
SemilatticeSup.toPartialOrder : {α : Type u} → [self : SemilatticeSup α] → PartialOrder α
-- Mathlib.Algebra.Group.Action.Sum
Sum.FaithfulSMulRight : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul M β] [FaithfulSMul M β],
  FaithfulSMul M (α ⊕ β)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.homOf_ofHom_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G), (CochainComplex.HomComplex.Cocycle.ofHom φ).homOf = φ
-- Init.Data.UInt.Bitwise
UInt64.ofNat_xor : ∀ (a b : ℕ), UInt64.ofNat (a ^^^ b) = UInt64.ofNat a ^^^ UInt64.ofNat b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ ∩ t₂).getKey? k = t₁.getKey? k
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
/-- A function is a conformal map if and only if its differential is a conformal linear map  -/
conformalAt_iff_isConformalMap_fderiv : ∀ {X : Type u_1} {Y : Type u_2} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y] [inst_2 : NormedSpace ℝ X]
  [inst_3 : NormedSpace ℝ Y] {f : X → Y} {x : X}, ConformalAt f x ↔ IsConformalMap (fderiv ℝ f x)
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.divMod.match_1.splitter : (motive : Num × Num → Sort u_1) → (x : Num × Num) → ((q r₁ : Num) → motive (q, r₁)) → motive x
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.fromIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y)
  (f : CategoryTheory.WalkingIso.zero ⟶ CategoryTheory.WalkingIso.one),
  (CategoryTheory.WalkingIso.fromIso e).map f = e.hom
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.map_comp_ιMulti_family : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {I : Type u_4} [inst_5 : LinearOrder I] (v : I → M) (f : M →ₗ[R] N),
  ⇑(exteriorPower.map n f) ∘ exteriorPower.ιMulti_family R n v = exteriorPower.ιMulti_family R n (⇑f ∘ v)
-- Mathlib.Logic.Encodable.Basic
Encodable.surjective_decode_getD : ∀ (α : Type u_3) [inst : Encodable α] (d : α), Function.Surjective fun n => (Encodable.decode n).getD d
-- Batteries.Data.Array.Merge
/-- `O(|xs| * |ys|)`. Merge `xs` and `ys`, which do not need to be sorted. Elements which occur in
both `xs` and `ys` are only added once. If `xs` and `ys` do not contain duplicates, then neither
does the result.
 -/
Array.mergeUnsortedDedup : {α : Type u_1} → [eq : BEq α] → Array α → Array α → Array α
-- Mathlib.Analysis.Complex.Isometry
LinearIsometry.re_apply_eq_re_of_add_conj_eq : ∀ (f : ℂ →ₗᵢ[ℝ] ℂ), (∀ (z : ℂ), z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)) → ∀ (z : ℂ), (f z).re = z.re
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.elabDeclToUnfoldOrTheorem : Lean.Meta.ConfigWithKey →
  Lean.Meta.Origin → Lean.Expr → Bool → Bool → Lean.Elab.Tactic.SimpKind → Lean.MetaM Lean.Elab.Tactic.ElabSimpArgResult
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_erase_eq_iff_not_compare_eq_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).minKey? = t.minKey? ↔ ∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.Algebra.Order.Module.Pointwise
BddBelow.smul_of_nonpos : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : AddCommGroup β]
  [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β] {s : Set β} {a : α},
  a ≤ 0 → BddBelow s → BddAbove (a • s)