mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Coherence
_private.Mathlib.CategoryTheory.Bicategory.Coherence.0.CategoryTheory.FreeBicategory.normalizeAux.match_1.eq_1 : ∀ {B : Type u_2} [inst : Quiver B] {a : B}
  (motive : (x x_1 : B) → Quiver.Path a x → CategoryTheory.FreeBicategory.Hom x x_1 → Sort u_3) (x x_1 : B)
  (p : Quiver.Path a x) (f : x ⟶ x_1)
  (h_1 : (x x_2 : B) → (p : Quiver.Path a x) → (f : x ⟶ x_2) → motive x x_2 p (CategoryTheory.FreeBicategory.Hom.of f))
  (h_2 : (x : B) → (p : Quiver.Path a x) → motive x x p (CategoryTheory.FreeBicategory.Hom.id x))
  (h_3 :
    (x x_2 : B) →
      (p : Quiver.Path a x) →
        (b : B) →
          (f : CategoryTheory.FreeBicategory.Hom x b) →
            (g : CategoryTheory.FreeBicategory.Hom b x_2) → motive x x_2 p (f.comp g)),
  (match x, x_1, p, CategoryTheory.FreeBicategory.Hom.of f with
    | x, x_2, p, CategoryTheory.FreeBicategory.Hom.of f => h_1 x x_2 p f
    | x, .(x), p, CategoryTheory.FreeBicategory.Hom.id .(x) => h_2 x p
    | x, x_2, p, f.comp g => h_3 x x_2 p b f g) =
    h_1 x x_1 p f
-- Mathlib.Order.SuccPred.Basic
WithBot.instSuccOrder : {α : Type u_1} → [inst : Preorder α] → [OrderBot α] → [SuccOrder α] → SuccOrder (WithBot α)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_add : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (f g : ρ.IntertwiningMap σ), Rep.ofHom (f + g) = Rep.ofHom f + Rep.ofHom g
-- Mathlib.Algebra.BigOperators.Ring.Multiset
Multiset.prod_eq_zero : ∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] {s : Multiset M₀}, 0 ∈ s → s.prod = 0
-- Std.Time.Format.Modifier
Std.Time.instReprZoneName : Repr Std.Time.ZoneName
-- Mathlib.Data.FunLike.Group
FunLike.coe_coeMonoidHom' : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : MulOne F] [inst_2 : MulOneClass β]
  [inst_3 : IsOneApply F α β] [inst_4 : IsMulApply F α β], ↑(FunLike.coeMonoidHom F α β) = FunLike.coeMulHom F α β
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.exists : ∀ {α : Type u} {p : WithZero α → Prop}, (∃ x, p x) ↔ p 0 ∨ ∃ a, p ↑a
-- Mathlib.Probability.Independence.Conditional
/-- Two random variables are conditionally independent with respect to `m'` iff the law of
`(id, f, g)` under `μ`, in which the identity is to the space with σ-algebra `m'`, can be written
as a product involving the conditional expectations of `f` and `g` given `m'`.

For a random variable `f`, `(condExpKernel μ m').map f` is the law of the conditional expectation
of `f` given `m'`: almost surely, `(condExpKernel μ m').map f ω s = μ⟦f ⁻¹' s | m'⟧ ω`.  -/
ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'}
  {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'},
  Measurable f →
    Measurable g →
      (ProbabilityTheory.CondIndepFun m' hm' f g μ ↔
        MeasureTheory.Measure.map (fun ω => (ω, f ω, g ω)) μ =
          (μ.trim hm').bind
            ⇑(ProbabilityTheory.Kernel.id.prod
                (((ProbabilityTheory.condExpKernel μ m').map f).prod ((ProbabilityTheory.condExpKernel μ m').map g))))
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits, then `F : C ⥤ D` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfSizeOfOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op] →
            CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.mk.inj : ∀ {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}
  {H : CategoryTheory.Functor C D} {adj₁ : F ⊣ G} {adj₂ : G ⊣ H} {adj₁_1 : F ⊣ G} {adj₂_1 : G ⊣ H},
  { adj₁ := adj₁, adj₂ := adj₂ } = { adj₁ := adj₁_1, adj₂ := adj₂_1 } → adj₁ = adj₁_1 ∧ adj₂ = adj₂_1
-- Mathlib.Data.Finset.Interval
/-- A function `f` from `Finset α` is monotone if and only if `f s ≤ f (insert a s)` for all `s` and
`a ∉ s`.  -/
Finset.monotone_iff_forall_le_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β} [inst_1 : DecidableEq α],
  Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s ≤ f (insert a s)
-- Qq.Macro
Qq.Impl.unquoteExprList : Lean.Expr → Qq.Impl.UnquoteM (List Lean.Expr)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKey?_eq_minEntry?_map_fst : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β}, l.minKey? = Option.map Sigma.fst l.minEntry?
-- Mathlib.Condensed.TopCatAdjunction
CondensedSet.instFaithfulTopCatTopCatToCondensedSet : topCatToCondensedSet.Faithful
-- Init.Grind.AC
Lean.Grind.AC.Var.denote : {α : Sort u} → Lean.Grind.AC.Context α → Lean.Grind.AC.Var → α
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.Hom.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c}
  (homₚ homₚ_1 : (i : ι) → HP.Hₚ i ⟶ HP'.Hₚ i) (e_homₚ : homₚ = homₚ_1) (hom hom_1 : (i : ι) → HP.H i ⟶ HP'.H i)
  (e_hom : hom = hom_1)
  (iso_comm :
    ∀ (i : ι),
      CategoryTheory.CategoryStruct.comp (HP.iso i).hom (TopPair.incl.whiskerLeft (homₚ i)) =
        CategoryTheory.CategoryStruct.comp (hom i) (HP'.iso i).hom)
  (w :
    ∀ (i j : ι),
      CategoryTheory.CategoryStruct.comp (HP.δ i j) (TopPair.proj₂.whiskerLeft (hom j)) =
        CategoryTheory.CategoryStruct.comp (homₚ i) (HP'.δ i j)),
  { homₚ := homₚ, hom := hom, iso_comm := iso_comm, w := w } = { homₚ := homₚ_1, hom := hom_1, iso_comm := ⋯, w := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
contravariant_swap_add_of_contravariant_add : ∀ (N : Type u_2) (r : N → N → Prop) [inst : AddCommSemigroup N] [ContravariantClass N N (fun x1 x2 => x1 + x2) r],
  ContravariantClass N N (Function.swap fun x1 x2 => x1 + x2) r
-- Init.Data.List.MinMaxOn
List.lt_apply_minOn_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β}, b < f (List.minOn f xs h) ↔ ∀ x ∈ xs, b < f x
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] (m m_1 : Std.ExtHashSet α)
  (e_m : m = m_1) (a a_1 : α) (e_a : a = a_1) (h : a ∈ m), m.get a h = m_1.get a_1 ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.comp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (_X _Y _Z : C),
  CategoryTheory.WithInitial.comp = fun f g => CategoryTheory.CategoryStruct.comp f g
-- Lean.Elab.DeclModifiers
Lean.Elab.instInhabitedVisibility : Inhabited Lean.Elab.Visibility
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.containsThenInsert_snd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.containsThenInsert k v).2 = t.insert k v
-- Mathlib.SetTheory.Ordinal.Rank
/-- The rank of an element `a` accessible under a relation `r` is defined recursively as the
smallest ordinal greater than the ranks of all elements below it (i.e. elements `b` such that
`r b a`).  -/
Acc.rank : {α : Type u} → {a : α} → {r : α → α → Prop} → Acc r a → Ordinal.{u}
-- Init.Data.SInt.Lemmas
Int32.toBitVec_toInt64 : ∀ (x : Int32), x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P : CategoryTheory.MorphismProperty C}
  {inst_1 : CategoryTheory.MonoidalCategory C} [self : P.IsMonoidalStable], P.IsMonoidal
-- Init.Data.List.Sublist
List.infix_append_of_infix_left : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁ <:+: l₂ → l₁ <:+: l₂ ++ l₃
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.isoSheafify_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P),
  (CategoryTheory.isoSheafify J hP).hom = CategoryTheory.toSheafify J P
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.mapTermRel_mapTermRel : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1}
  {L'' : FirstOrder.Language} (ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n))
  (fr : (n : ℕ) → L.Relations n → L'.Relations n) (ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n))
  (fr' : (n : ℕ) → L'.Relations n → L''.Relations n) {n : ℕ} (φ : L.BoundedFormula α n),
  FirstOrder.Language.BoundedFormula.mapTermRel ft' fr' (fun x => id)
      (FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun x => id) φ) =
    FirstOrder.Language.BoundedFormula.mapTermRel (fun x => ft' x ∘ ft x) (fun x => fr' x ∘ fr x) (fun x => id) φ
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element that is less than the given element,
panicking if no such element exists.
 -/
Std.ExtTreeSet.getLT! : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeSet α cmp → α → α
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_dvd : ∀ (n : ℕ), n.minFac ∣ n
-- Mathlib.Order.CompleteLattice.Finset
Finset.iSup_biUnion : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice β] [inst_1 : DecidableEq α] (s : Finset γ)
  (t : γ → Finset α) (f : α → β), ⨆ y ∈ s.biUnion t, f y = ⨆ x ∈ s, ⨆ y ∈ t x, f y
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk_himp_mk : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : α) (ha : a ∈ L) (hb : b ∈ L),
  ⟨a, ha⟩ ⇨ ⟨b, hb⟩ = ⟨a ⇨ b, ⋯⟩
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.addUnits_of_val : ∀ {M : Type u_1} [inst : AddMonoid M] {u₁ u₂ : AddUnits M}, AddCommute ↑u₁ ↑u₂ → AddCommute u₁ u₂
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
HomotopyCategory.Pretriangulated.contractible_distinguished : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  (X : HomotopyCategory C (ComplexShape.up ℤ)),
  CategoryTheory.Pretriangulated.contractibleTriangle X ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} [inst_2 : SizeOf B] [inst_3 : SizeOf C] (app : (a : B) → F.obj a ⟶ G.obj a)
  (naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (app a) (G.map f) ⟶ CategoryTheory.CategoryStruct.comp (F.map f) (app b))
  (naturality_naturality :
    autoParam
      (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
        CategoryTheory.CategoryStruct.comp (naturality f) (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)) (naturality g))
      CategoryTheory.Lax.LaxTrans.naturality_naturality._autoParam)
  (naturality_id :
    autoParam
      (∀ (a : B),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a))
            (naturality (CategoryTheory.CategoryStruct.id a)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (app a)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).inv
              (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))))
      CategoryTheory.Lax.LaxTrans.naturality_id._autoParam)
  (naturality_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g))
            (naturality (CategoryTheory.CategoryStruct.comp f g)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (naturality f) (G.map g))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g))
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).inv
                    (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c)))))))
      CategoryTheory.Lax.LaxTrans.naturality_comp._autoParam),
  sizeOf
      { app := app, naturality := naturality, naturality_naturality := naturality_naturality,
        naturality_id := naturality_id, naturality_comp := naturality_comp } =
    1
-- Mathlib.Data.Finset.Defs
/-- **Alias** of `Finset.notMem_mono`. -/
Finset.not_mem_subset : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → ∀ {a : α}, a ∉ t → a ∉ s
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.homFrom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.WithTerminal.homFrom X =
    CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.incl.obj X)
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (a : α), MeasureTheory.Measure.count {a} = 1
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
isBoundedBilinearMap_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G],
  IsBoundedBilinearMap 𝕜 fun p => p.1 ∘SL p.2
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.conv_absolutelyContinuous : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] {μ ν ρ : MeasureTheory.Measure M}
  [ρ.IsAddLeftInvariant] [MeasureTheory.SFinite ν], ν.AbsolutelyContinuous ρ → (μ.conv ν).AbsolutelyContinuous ρ
-- Mathlib.Topology.Defs.Induced
/-- A function `f : X → Y` between topological spaces is inducing if the topology on `X` is induced
by the topology on `Y` through `f`, meaning that a set `s : Set X` is open iff it is the preimage
under `f` of some open set `t : Set Y`.  -/
Topology.IsInducing : {X : Type u_1} → {Y : Type u_2} → [tX : TopologicalSpace X] → [tY : TopologicalSpace Y] → (X → Y) → Prop
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.homeomorphCircle_apply : ∀ {T : ℝ} (hT : T ≠ 0) (x : AddCircle T), (AddCircle.homeomorphCircle hT) x = x.toCircle
-- Init.Data.Fin.Fold
Fin.foldlM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {x : α} [inst : Monad m] [LawfulMonad m] {n : ℕ} {f : α → Fin n → α},
  Fin.foldlM n (fun x i => pure (f x i)) x = pure (Fin.foldl n f x)
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Basis.equivFun_symm_single : ∀ {R : Type u_1} {M : Type u_2} {n : Type u_3} [inst : DecidableEq n] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Finite n] (b : Module.Basis n R M) (i : n), b.equivFun.symm (Pi.single i 1) = b i
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.norm_argSelfAdjoint_le_pi : ∀ {A : Type u_1} [inst : CStarAlgebra A] (u : ↥(unitary A)), ‖Unitary.argSelfAdjoint u‖ ≤ Real.pi
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.SplitInfo.getAnchor : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.GrindM UInt64
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.sum_divisors_selbergTerms_eq_selbergTerms_mul_nu_inv : ∀ {s : BoundingSieve} {d : ℕ},
  d ∣ s.prodPrimes →
    (∑ l ∈ s.prodPrimes.divisors, if l ∣ d then BoundingSieve.selbergTerms l else 0) =
      BoundingSieve.selbergTerms d * (s.nu d)⁻¹
-- Mathlib.Data.Part
Part.mem_assert_iff : ∀ {α : Type u_1} {p : Prop} {f : p → Part α} {a : α}, a ∈ Part.assert p f ↔ ∃ (h : p), a ∈ f h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)},
  List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
    (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a t = true → (List.map Prod.fst l).contains a = false) →
      (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).size = t.size + l.length
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The underlying morphism of a morphism of comonoid objects.  -/
CategoryTheory.Comon.Hom.hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → {M N : CategoryTheory.Comon C} → M.Hom N → (M.X ⟶ N.X)
-- Batteries.Data.Array.Lemmas
Array.forIn_eq_forIn_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (as : Array α) (b : β)
  (f : α → β → m (ForInStep β)), forIn as b f = forIn as.toList b f
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_ofNat' : ∀ (n : ℕ), (UInt16.ofNat n).toBitVec = BitVec.ofNat 16 n
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.instIsAffineHomCompScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsAffineHom f]
  [AlgebraicGeometry.IsAffineHom g], AlgebraicGeometry.IsAffineHom (CategoryTheory.CategoryStruct.comp f g)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.not_mem_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ}, a ∉ Std.DHashMap.emptyWithCapacity c
-- Mathlib.Algebra.Lie.Basic
/-- The inverse function of an equivalence of Lie modules is a left inverse of the underlying
function.  -/
LieModuleEquiv.left_inv : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (self : M ≃ₗ⁅R,L⁆ N),
  Function.LeftInverse self.invFun (↑self.toLieModuleHom).toFun
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.instLeAtTopUnconditional : ∀ (β : Type u_2), (SummationFilter.unconditional β).LeAtTop
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_toUInt8 : ∀ (n : UInt16), n.toUInt8.toUInt64 = n.toUInt64 % 256
-- Lean.Environment
_private.Lean.Environment.0.Lean.VisibilityMap.mk.inj : ∀ {α : Type} {«private» «public» private_1 public_1 : α},
  { «private» := «private», «public» := «public» } = { «private» := private_1, «public» := public_1 } →
    «private» = private_1 ∧ «public» = public_1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- See `Finset.card_nsmul_mono` for a version that works for the empty set.  -/
Finset.Nonempty.card_nsmul_mono : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddCancelMonoid α] {s : Finset α},
  s.Nonempty → Monotone fun n => (n • s).card
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpArgs.zetaDeltaAll : Lean.Elab.Tactic.Grind.DSimpArgs → Bool
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] {g : GL (Fin 2) K},
  g.IsParabolic → ∀ [NeZero 2] {c : OnePoint K}, g • c = c ↔ c = g.parabolicFixedPoint
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Problem.mk.injEq : ∀ (mvarId : Lean.MVarId) (vars : List Lean.Expr) (alts : List Lean.Meta.Match.Alt)
  (examples : List Lean.Meta.Match.Example) (mvarId_1 : Lean.MVarId) (vars_1 : List Lean.Expr)
  (alts_1 : List Lean.Meta.Match.Alt) (examples_1 : List Lean.Meta.Match.Example),
  ({ mvarId := mvarId, vars := vars, alts := alts, examples := examples } =
      { mvarId := mvarId_1, vars := vars_1, alts := alts_1, examples := examples_1 }) =
    (mvarId = mvarId_1 ∧ vars = vars_1 ∧ alts = alts_1 ∧ examples = examples_1)
-- Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Module.Basis.extend.eq_1 : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  (hs : LinearIndepOn K id s), Module.Basis.extend hs = Module.Basis.mk ⋯ ⋯
-- Init.Data.BEq
bne_eq : ∀ {α : Type u_1} [inst : BEq α] {a b : α}, (a != b) = !a == b
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.ιCoproductFrom.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C) {X : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct (P.coproductFromFamily X)] {Y : C} (f f_1 : Y ⟶ X),
  f = f_1 → ∀ (hY : P Y), P.ιCoproductFrom f hY = P.ιCoproductFrom f_1 hY
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.setInterior_map : ∀ {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_4} {P₂ : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂]
  [inst_6 : AddTorsor V₂ P₂] (I : Set k) {n : ℕ} (s : Affine.Simplex k P n) {f : P →ᵃ[k] P₂}
  (hf : Function.Injective ⇑f), Affine.Simplex.setInterior I (s.map f hf) = ⇑f '' Affine.Simplex.setInterior I s
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.check.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (n : ℕ),
      CategoryTheory.Injective S.X₂ →
        (CategoryTheory.HasInjectiveDimensionLT S.X₃ (n + 1) ↔ CategoryTheory.HasInjectiveDimensionLT S.X₁ (n + 2))
-- Init.Data.Bool
Bool.true_xor : ∀ (x : Bool), (true ^^ x) = !x
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Slice.find?_char_eq_some_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  s.find? c = some pos ↔ ∃ (h : pos ≠ s.endPos), pos.get h = c ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), pos'.get ⋯ ≠ c
-- Mathlib.Algebra.Group.Action.Pretransitive
/-- The right regular action of an additive group on itself is transitive.  -/
AddAction.Regular.isPretransitive_addOpposite : ∀ {G : Type u_2} [inst : AddGroup G], AddAction.IsPretransitive Gᵃᵒᵖ G
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.instHasCoproductOppositeOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  [CategoryTheory.Limits.HasProduct Z], CategoryTheory.Limits.HasCoproduct fun x => Opposite.op (Z x)
-- Mathlib.Algebra.Field.Opposite
AddOpposite.op_nnratCast : ∀ {α : Type u_1} [inst : NNRatCast α] (q : ℚ≥0), AddOpposite.op ↑q = ↑q
-- Mathlib.Control.Traversable.Basic
/-- The composition of applicative transformations.  -/
ApplicativeTransformation.comp : {F : Type u → Type v} →
  [inst : Applicative F] →
    {G : Type u → Type w} →
      [inst_1 : Applicative G] →
        {H : Type u → Type s} →
          [inst_2 : Applicative H] →
            ApplicativeTransformation G H → ApplicativeTransformation F G → ApplicativeTransformation F H