mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntryD.eq_2 : ∀ {α : Type u} {β : Type v} (x : α × β) (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.maxEntryD
      (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x =
    (k, v)
-- Mathlib.Order.CompleteLattice.Basic
sSup_univ : ∀ {α : Type u_1} [inst : CompleteLattice α], sSup Set.univ = ⊤
-- Lean.Elab.Match
/-- Try to clear the free variables in `toClear` and auxiliary discriminants, and then execute `k` in the updated local context.
If `type` or another local variables depends on a free variable in `toClear`, then it is not cleared.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.withToClear : {α : Type} → Array Lean.FVarId → Lean.Expr → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.RingTheory.TwoSidedIdeal.Kernel
TwoSidedIdeal.mem_ker : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_3}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) {x : R}, x ∈ TwoSidedIdeal.ker f ↔ f x = 0
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.voluntaryCS : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.Data.PSigma.Order
/-- The lexicographical linear order on a sigma type.  -/
PSigma.Lex.orderBot : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : PartialOrder ι] →
      [inst_1 : OrderBot ι] → [inst_2 : (i : ι) → Preorder (α i)] → [OrderBot (α ⊥)] → OrderBot (Σₗ' (i : ι), α i)
-- Mathlib.Data.Complex.Basic
Complex.sub_conj : ∀ (z : ℂ), z - (starRingEnd ℂ) z = ↑(2 * z.im) * Complex.I
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → k ∈ List.map Prod.fst l → (t.insertMany l).getKey! k' = k
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.reindex_isColimit₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι),
  (c.reindex e).isColimit₁ = c.isColimit₁.whiskerEquivalence (CategoryTheory.Discrete.equivalence e)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.vComp_naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.LaxTrans F G) (θ : CategoryTheory.Lax.LaxTrans G H)
  {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapComp f g))
      (η.vCompNaturality θ (CategoryTheory.CategoryStruct.comp f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.vCompApp θ a) (H.map f) (H.map g)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.vCompNaturality θ f) (H.map g))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f) (η.vCompApp θ b) (H.map g)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (η.vCompNaturality θ g))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.vCompApp θ c)).inv
              (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (η.vCompApp θ c))))))
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
GetElem.getElem.hcongr_8 : ∀ (coll coll' : Type u),
  coll = coll' →
    ∀ (idx idx' : Type v),
      idx = idx' →
        ∀ (elem elem' : Type w),
          elem = elem' →
            ∀ (valid : coll → idx → Prop) (valid' : coll' → idx' → Prop),
              valid ≍ valid' →
                ∀ (self : GetElem coll idx elem valid) (self' : GetElem coll' idx' elem' valid'),
                  self ≍ self' →
                    ∀ (xs : coll) (xs' : coll'),
                      xs ≍ xs' →
                        ∀ (i : idx) (i' : idx'),
                          i ≍ i' → ∀ (h : valid xs i) (h' : valid' xs' i'), h ≍ h' → xs[i] ≍ xs'[i']
-- Init.Data.List.Basic
List.filterMap_nil : ∀ {α : Type u} {β : Type v} {f : α → Option β}, List.filterMap f [] = []
-- Mathlib.Order.Heyting.Basic
CoheytingAlgebra.toGeneralizedCoheytingAlgebra : {α : Type u_4} → [self : CoheytingAlgebra α] → GeneralizedCoheytingAlgebra α
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k k' : α} {f : Option β → Option β} {h : k' ∈ m.alter k f},
  (m.alter k f).getKey k' h = if heq : (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- The cost function comes from the template  -/
ValuedCSP.Term.inΓ : ∀ {D : Type u_1} {C : Type u_2} [inst : AddCommMonoid C] [inst_1 : PartialOrder C] [inst_2 : IsOrderedAddMonoid C]
  {Γ : ValuedCSP D C} {ι : Type u_3} (self : Γ.Term ι), ⟨self.n, self.f⟩ ∈ Γ
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.toMulHom : {R : Type u} →
  {S : Type u₁} →
    [inst : Monoid R] →
      [inst_1 : Monoid S] →
        {φ : R →* S} →
          {A : Type v} →
            {B : Type w} →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : DistribMulAction R A] →
                  [inst_4 : NonUnitalNonAssocSemiring B] → [inst_5 : DistribMulAction S B] → (A →ₛₙₐ[φ] B) → A →ₙ* B
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} {fallback : β k}, m₁.contains k = false → (m₁.inter m₂).getD k fallback = fallback
-- Mathlib.Data.Set.Function
Set.InjOn.image_ssubset_image_iff : ∀ {α : Type u_1} {β : Type u_2} {s s₁ s₂ : Set α} {f : α → β},
  Set.InjOn f s → s₁ ⊆ s → s₂ ⊆ s → (f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂)
-- Mathlib.LinearAlgebra.Determinant
/-- If `M'` is a two-sided inverse for `M` (indexed differently), `det (M * N * M') = det N`.

See `Matrix.det_conj` and `Matrix.det_conj'` for the case when `M' = M⁻¹` or vice versa.  -/
Matrix.det_conj_of_mul_eq_one : ∀ {A : Type u_5} [inst : CommRing A] {m : Type u_6} {n : Type u_7} [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] {M : Matrix m n A} {M' : Matrix n m A} {N : Matrix n n A},
  M * M' = 1 → M' * M = 1 → (M * N * M').det = N.det
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_diff!_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = true →
          Std.DTreeMap.Internal.Impl.Const.get! (m₁.diff! m₂) k = default
-- Mathlib.Topology.Gluing
/-- This is a constructor of `TopCat.GlueData` whose arguments are in terms of elements and
intersections rather than subobjects and pullbacks. Please refer to `TopCat.GlueData.MkCore` for
details.  -/
TopCat.GlueData.mk' : TopCat.GlueData.MkCore → TopCat.GlueData
-- Init.Data.List.Erase
List.eraseIdx_append : ∀ {α : Type u_1} {l l' : List α} {k : ℕ},
  (l ++ l').eraseIdx k = if k < l.length then l.eraseIdx k ++ l' else l ++ l'.eraseIdx (k - l.length)
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.init_neg : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ),
  WittVector.init n (-x) = WittVector.init n (-WittVector.init n x)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.leftFunc_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {X Y : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)} (f : X ⟶ Y),
  CategoryTheory.Arrow.leftFunc.map f = f.left
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instIsStableUnderRetractsOverWeakEquivalences : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts],
  (HomotopicalAlgebra.weakEquivalences (CategoryTheory.Over S)).IsStableUnderRetracts
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_span_finset_le : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  (s : Finset M), Module.rank R ↥(Submodule.span R ↑s) ≤ ↑s.card
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyGT?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGT? k = t₂.getKeyGT? k
-- Mathlib.Topology.Category.Compactum
/-- The functor `compactumToCompHaus` is essentially surjective.  -/
compactumToCompHaus.essSurj : compactumToCompHaus.EssSurj
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_left_strictMono : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftStrictMono M] {a : M},
  0 < a → StrictMono fun x => x • a
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.add : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop} (j : J)
  (x y : ↑(F.obj j)), RingCat.Colimits.Relation.below ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.IsCoreflexivePair.common_retraction : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) [CategoryTheory.IsCoreflexivePair f g],
  ∃ s,
    CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.id A ∧
      CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id A
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- If for a lax monoidal functor `F : V ⥤ W` the canonical function
`(𝟙_ V ⟶ v) → (𝟙_ W ⟶ F.obj v)` is bijective, and `C` is an enriched ordinary category on `V`,
then `F` induces the structure of a `W`-enriched ordinary category on `TransportEnrichment F C`,
i.e. on the same underlying category `C`.  -/
CategoryTheory.TransportEnrichment.enrichedOrdinaryCategory : {V : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u) →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [CategoryTheory.EnrichedOrdinaryCategory V C] →
            {W : Type u''} →
              [inst_4 : CategoryTheory.Category.{v'', u''} W] →
                [inst_5 : CategoryTheory.MonoidalCategory W] →
                  (F : CategoryTheory.Functor V W) →
                    [inst_6 : F.LaxMonoidal] →
                      (e :
                          (v : V) →
                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
                              (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) →
                        (∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
                            (e v) f =
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) →
                          CategoryTheory.EnrichedOrdinaryCategory W (CategoryTheory.TransportEnrichment F C)
-- Mathlib.MeasureTheory.MeasurableSpace.Card
MeasurableSpace.generateMeasurableRec.eq_def : ∀ {α : Type u} (s : Set (Set α)) (i : Ordinal.{u_1}),
  MeasurableSpace.generateMeasurableRec s i =
    have S := ⋃ j, ⋃ (_ : j < i), MeasurableSpace.generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ Set.range fun f => ⋃ n, ↑(f n)
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.mk.injEq : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  (succ : (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j)))
  (map_succ :
    ∀ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (succ j hj x) = x)
  (lift : (j : J) → Order.IsSuccLimit j → ↑(⋯.functor.op.comp F).sections → F.obj (Opposite.op j))
  (map_lift :
    ∀ (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (lift j hj x) =
        ↑x (Opposite.op ⟨i, hi⟩))
  (succ_1 : (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j)))
  (map_succ_1 :
    ∀ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (succ_1 j hj x) = x)
  (lift_1 : (j : J) → Order.IsSuccLimit j → ↑(⋯.functor.op.comp F).sections → F.obj (Opposite.op j))
  (map_lift_1 :
    ∀ (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (lift_1 j hj x) =
        ↑x (Opposite.op ⟨i, hi⟩)),
  ({ succ := succ, map_succ := map_succ, lift := lift, map_lift := map_lift } =
      { succ := succ_1, map_succ := map_succ_1, lift := lift_1, map_lift := map_lift_1 }) =
    (succ = succ_1 ∧ lift = lift_1)
-- Init.Tactics
/-- Start the stateful proof mode of `Std.Do.SPred`.
This will transform a stateful goal of the form `H ⊢ₛ T` into `⊢ₛ H → T`
upon which `mintro` can be used to re-introduce `H` and give it a name.
It is often more convenient to use `mintro` directly, which will
try `mstart` automatically if necessary.
 -/
Lean.Parser.Tactic.mstartMacro : Lean.ParserDescr
-- Mathlib.Order.Hom.Bounded
OrderIsoClass.toBotHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : LE α] [inst_2 : OrderBot α]
  [inst_3 : PartialOrder β] [inst_4 : OrderBot β] [OrderIsoClass F α β], BotHomClass F α β
-- Mathlib.Control.Fold
Monoid.Foldl.ofFreeMonoid : {α β : Type u} → (β → α → β) → FreeMonoid α →* Monoid.Foldl β
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.hole.sizeOf_spec : ∀ (mvarId : Lean.MVarId), sizeOf (Lean.Elab.InfoTree.hole mvarId) = 1 + sizeOf mvarId
-- Init.Data.Ord.Basic
Ordering.isEq_gt : Ordering.gt.isEq = false
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_sup_le_inf_aux_right : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  (Filter.blimsup u f fun x => p x ∧ q x) ≤ Filter.blimsup u f q
-- Lean.Meta.DiscrTree.Util
/-- Apply a monadic function to the array of values at each node in a `DiscrTree`.  -/
Lean.Meta.DiscrTree.Trie.mapArraysM : {m : Type → Type} →
  [Monad m] → {α β : Type} → Lean.Meta.DiscrTree.Trie α → (Array α → m (Array β)) → m (Lean.Meta.DiscrTree.Trie β)
-- Mathlib.Data.Finset.Sum
Finset.disjSum_eq_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (α ⊕ β)},
  s.disjSum t = u ↔ s = u.toLeft ∧ t = u.toRight
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.preconnectedSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  PreconnectedSpace (TopologicalSpace.NonemptyCompacts α) ↔ PreconnectedSpace α
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.freeOn_not_isLoop : ∀ {α : Type u_1} (E : Set α) (e : α), ¬(Matroid.freeOn E).IsLoop e
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddZeroClass : {α : Type u_1} → [AddZeroClass α] → AddZeroClass (Colex α)
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T S : E →ₗ[𝕜] E}, T.IsSymmetric → S.IsSymmetric → (T - S).IsSymmetric
-- Mathlib.MeasureTheory.Order.Lattice
/-- **Alias** of `AEMeasurable.inf`. -/
AEMeasurable.inf' : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → M} [inst_1 : Min M] [MeasurableInf₂ M], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f ⊓ g) μ
-- Lean.Elab.ConfigEval.Types
/-- The expected type to use when elaborating a term for use with this `EvalExpr` instance.
If present, the expression will be coerced to this type.
 -/
Lean.Elab.ConfigEval.EvalExpr.expectedType? : (α : Type) → [self : Lean.Elab.ConfigEval.EvalExpr α] → Option Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- `BirdDet.birdDet n A` computes the determinant of the `n × n` matrix whose
entries are stored in row-major order in `A`.  -/
BirdDet.det_eq_birdDet : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Array R) (hA : A.size = n * n),
  (Matrix.ofArray A hA).det = BirdDet.birdDet n A
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.intervalIntegrable_of_integral_ne_zero : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ}, ∫ (x : ℝ) in a..b, f x ∂μ ≠ 0 → IntervalIntegrable f μ a b
-- Mathlib.Tactic.Widget.StringDiagram
/-- The penrose variable associated with a strand.  -/
Mathlib.Tactic.Widget.StringDiagram.Strand.toPenroseVar : Mathlib.Tactic.Widget.StringDiagram.Strand → Mathlib.Tactic.Widget.StringDiagram.PenroseVar
-- Mathlib.Order.Filter.AtTopBot.Field
/-- The function `fun x ↦ f x * r` tends to negative infinity along a nontrivial filter
if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity.  -/
Filter.tendsto_mul_const_atBot_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔
    0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.atTop
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_eq_iInter : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X},
  (Convexity.convexHull R) s = ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : Convexity.IsConvexSet R t), t
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getValueCast?.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)),
  (match [] with
    | [] => h_1 ()
    | ⟨k, v⟩ :: l => h_2 k v l) =
    h_1 ()
-- Mathlib.Algebra.Algebra.Defs
RingHom.smul_toAlgebra : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (i : R →+* S) (r : R) (s : S),
  have x := i.toAlgebra;
  r • s = i r * s
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves binary biproducts if it preserves the binary biproduct of `X` and `Y`
for all `X` and `Y`.  -/
CategoryTheory.Limits.PreservesBinaryBiproducts.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D}
  {F : CategoryTheory.Functor C D} {inst_4 : F.PreservesZeroMorphisms}
  [self : CategoryTheory.Limits.PreservesBinaryBiproducts F] {X Y : C},
  CategoryTheory.Limits.PreservesBinaryBiproduct X Y F
-- Mathlib.Analysis.Calculus.TangentCone.Real
/-- If a subset of a real vector space contains an open segment, then the direction of this
segment belongs to the positive tangent cone at its endpoints.  -/
sub_mem_posTangentConeAt_of_openSegment_subset : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousSMul ℝ E]
  {s : Set E} {x y : E}, openSegment ℝ x y ⊆ s → y - x ∈ tangentConeAt NNReal s x
-- Mathlib.Algebra.Order.CauSeq.BigOperators
IsCauSeq.geo_series_const : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] [Archimedean α] (a : α)
  {x : α}, |x| < 1 → IsCauSeq abs fun m => ∑ n ∈ Finset.range m, a * x ^ n
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.Integrable.comp_mul_left : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : Group G] [MeasurableMul G] {f : G → F} [μ.IsMulLeftInvariant],
  MeasureTheory.Integrable f μ → ∀ (g : G), MeasureTheory.Integrable (fun t => f (g * t)) μ
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonLeanClientCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.LeanClientCapabilities
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone is a limit cone if and only if the corresponding bicone is a limit cone.  -/
CategoryTheory.Limits.BinaryBicone.toBiconeIsLimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (b : CategoryTheory.Limits.BinaryBicone X Y) →
          CategoryTheory.Limits.IsLimit b.toBicone.toCone ≃ CategoryTheory.Limits.IsLimit b.toCone
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeUsingDefaultPrio.synthesizePending : List Lean.MVarId → Lean.Elab.TermElabM Bool
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkDoneProgressBegin : Lean.ToJson Lean.Lsp.WorkDoneProgressBegin
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictMonoOn_toDual_comp_iff`. -/
StrictAntiOn.dual_right : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn f s → StrictMonoOn (⇑OrderDual.toDual ∘ f) s
-- Mathlib.LinearAlgebra.Ray
/-- A vector is in the same ray as a positive multiple of one it is in the same ray as.  -/
SameRay.pos_smul_right : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x y : M} {S : Type u_5} [inst_5 : CommSemiring S]
  [inst_6 : PartialOrder S] [inst_7 : Algebra S R] [inst_8 : Module S M] [SMulPosMono S R] [IsScalarTower S R M]
  {a : S}, SameRay R x y → 0 < a → SameRay R x (a • y)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k : α} (h : t.WF),
  Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.filter f t) k =
    ((Std.DTreeMap.Raw.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.Topology.Homeomorph.Lemmas
/-- An equivalence between topological spaces is a homeomorphism iff it is continuous in both
directions.  -/
Equiv.isHomeomorph_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y),
  IsHomeomorph ⇑e ↔ Continuous ⇑e ∧ Continuous ⇑e.symm
-- Mathlib.Topology.Algebra.UniformConvergence
/-- If `G` is a uniform group, then `α →ᵤ G` is a uniform group as well.  -/
instIsUniformGroupUniformFun : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : UniformSpace G] [IsUniformGroup G],
  IsUniformGroup (UniformFun α G)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.pos_size_of_mem : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] {x : α} {t : Ordnode α}, t.Sized → x ∈ t → 0 < t.size
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.unitOfList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, Std.DTreeMap.Const.unitOfList [k] cmp = ∅.insertIfNew k ()
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_le_card_of_surjective : ∀ {α : Type u} {β : Type v} [Finite α] (f : α → β), Function.Surjective f → Nat.card β ≤ Nat.card α