mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.arrowEquiv_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C),
  CategoryTheory.ComposableArrows.arrowEquiv.symm f = CategoryTheory.ComposableArrows.mk₁ f.hom
-- Mathlib.Computability.NFA
NFA.disjoint_evalFrom_reverse_iff : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {x : List α} {S S' : Set σ},
  Disjoint S (M.reverse.evalFrom S' x) ↔ Disjoint S' (M.evalFrom S x.reverse)
-- Lean.Meta.Match.Match
/-- Return true if the given (sub-)problem has been solved.  -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isDone : Lean.Meta.Match.Problem → Bool
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGTD.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α fun x => β) (fallback : α × β),
  Std.DTreeMap.Internal.Impl.Const.getEntryGTD k t fallback =
    (Std.DTreeMap.Internal.Impl.Const.getEntryGT? k t).getD fallback
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.eraseMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (l : List α), (t₁.eraseMany l).Equiv (t₂.eraseMany l)
-- Mathlib.NumberTheory.Height.Basic
_private.Mathlib.NumberTheory.Height.Basic.0.Height.hasFiniteMulSupport_max_nonarchAbsVal : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K),
  Function.HasFiniteMulSupport fun v => max (↑v x) 1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq c = Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq c_1 → c = c_1
-- Init.Data.Option.Instances
Option.instForIn'InferInstanceMembershipOfMonad : {m : Type u_1 → Type u_2} → {α : Type u_3} → [Monad m] → ForIn' m (Option α) α inferInstance
-- Mathlib.Logic.Equiv.Defs
/-- Equivalence between `Fin 2` and `Bool`.  -/
finTwoEquiv : Fin 2 ≃ Bool
-- Mathlib.Logic.Unique
PUnit.default_eq_unit : default = PUnit.unit
-- Std.Time.Zoned.Database.TzIf
/-- The array of transition times in seconds since the epoch.
 -/
Std.Time.TimeZone.TZif.TZifV1.transitionTimes : Std.Time.TimeZone.TZif.TZifV1 → Array ℤ
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.linearMapAt.congr_simp : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e_1 : Bundle.Trivialization F Bundle.TotalSpace.proj) (e_e : e = e_1) [inst_8 : Bundle.Trivialization.IsLinear R e]
  (b : B), Bundle.Trivialization.linearMapAt R e b = Bundle.Trivialization.linearMapAt R e_1 b
-- Mathlib.Data.Sum.Order
Sum.Lex.toLex_lt_toLex : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : α ⊕ β},
  toLex a < toLex b ↔ Sum.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) a b
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- On sites with a terminal object, the global sections functor is isomorphic to the functor
of sections on that object.  -/
CategoryTheory.Sheaf.ΓNatIsoSheafSections : {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] →
            [inst_3 : CategoryTheory.Limits.HasTerminal C] →
              {T : C} →
                CategoryTheory.Limits.IsTerminal T →
                  (CategoryTheory.Sheaf.Γ J A ≅ (CategoryTheory.sheafSections J A).obj (Opposite.op T))
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.instInhabitedBicone : (J : Type u₁) → Inhabited (CategoryTheory.Bicone J)
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The restriction of a topological representation along a monoid homomorphism.  -/
TopRep.res : {k : Type u} →
  [inst : TopologicalSpace k] →
    [inst_1 : Ring k] →
      {G : Type v} → [inst_2 : Group G] → {H : Type u_1} → [inst_3 : Monoid H] → (H →* G) → TopRep k G → TopRep k H
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The bijection `WalkingMultispan J ≃ J.L ⊕ J.R`.  -/
CategoryTheory.Limits.WalkingMultispan.equiv : (J : CategoryTheory.Limits.MultispanShape) → CategoryTheory.Limits.WalkingMultispan J ≃ J.L ⊕ J.R
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.hasKernel : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C},
  (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) →
    ∀ {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃}
      {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)},
      CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles →
        ∀ {K Q : A} {α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q}
          {γ : ι.obj Q ⟶ (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj (ι.obj K))},
          CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
            ∀ [ι.Full] [inst_8 : CategoryTheory.Preadditive A] [ι.Faithful], CategoryTheory.Limits.HasKernel f₁
-- Mathlib.NumberTheory.ModularForms.Basic
CuspFormClass.holo : ∀ {F : Type u_2} {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} {inst : FunLike F UpperHalfPlane ℂ}
  [self : CuspFormClass F Γ k] (f : F), MDiff ⇑f
-- Mathlib.Order.Bounds.Image
bddBelow_range_prod : ∀ {ι : Sort x} {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {F : ι → α × β},
  BddBelow (Set.range F) ↔ BddBelow (Set.range (Prod.fst ∘ F)) ∧ BddBelow (Set.range (Prod.snd ∘ F))
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `(M', f : M ⟶ M')` satisfies universal property of localized module, there is a canonical
map `LocalizedModule S M ⟶ M'`.
 -/
IsLocalizedModule.fromLocalizedModule' : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        {M' : Type u_3} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M'] →
              [inst_3 : Module R M] →
                [inst_4 : Module R M'] → (f : M →ₗ[R] M') → [IsLocalizedModule S f] → LocalizedModule S M → M'
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.withFor : {α : Type} → Lean.Elab.Term.Do.ToCodeBlock.M α → Lean.Elab.Term.Do.ToCodeBlock.M α
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` reflects isomorphisms and we can lift a single colimit cocone to a colimit cocone, then
`F` creates limits. Note that unlike `createsColimitOfReflectsIso`, to apply this result it is
necessary to know that `K ⋙ F` actually has a colimit.  -/
CategoryTheory.createsColimitOfReflectsIso' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.ReflectsIsomorphisms] →
                  {c : CategoryTheory.Limits.Cocone (K.comp F)} →
                    (hc : CategoryTheory.Limits.IsColimit c) →
                      CategoryTheory.LiftsToColimit K F c hc → CategoryTheory.CreatesColimit K F
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedCodeDecl.default : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.CodeDecl pu
-- Std.Do.PostCond
Std.Do.ExceptConds.fst_true : ∀ {ε : Type u} {ps : Std.Do.PostShape}, Std.Do.ExceptConds.true.1 = fun _ε => ⌜True⌝
-- Mathlib.Probability.Density
MeasureTheory.HasPDF.aemeasurable' : ∀ {Ω : Type u_1} {E : Type u_2} {inst : MeasurableSpace E} {m : MeasurableSpace Ω} {X : Ω → E}
  {ℙ : MeasureTheory.Measure Ω} (μ : autoParam (MeasureTheory.Measure E) MeasureTheory.HasPDF._auto_1)
  [self : MeasureTheory.HasPDF X ℙ μ], AEMeasurable X ℙ
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedCategory.id_def : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] (𝒳 : CategoryTheory.BasedCategory 𝒮),
  CategoryTheory.CategoryStruct.id 𝒳 = CategoryTheory.BasedFunctor.id 𝒳
-- Mathlib.Combinatorics.Graph.Subgraph
/-- `H ≤i G` (`Graph.IsInducedSubgraph`) is a subgraph of `G` such that every link of `G`
involving two vertices of `H` is also a link of `H`.  -/
Graph.IsInducedSubgraph : {α : Type u_1} → {β : Type u_2} → Graph α β → Graph α β → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.InitialMonoClass.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (∀ {I : C} (X : C) (hI : CategoryTheory.Limits.IsInitial I), CategoryTheory.Mono (hI.to X)) →
    CategoryTheory.Limits.InitialMonoClass C
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.filterMap_eq_filterMapₘ : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β)
  (f : (a : α) → β a → Option (δ a)), Std.DHashMap.Internal.Raw₀.filterMap f m = m.filterMapₘ f
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Partial order on the set of groupoids, given by inclusion of the members of the groupoid.  -/
StructureGroupoid.partialOrder : {H : Type u_1} → [inst : TopologicalSpace H] → PartialOrder (StructureGroupoid H)
-- Mathlib.Order.Types.Defs
/-- `ω` is the first infinite order type, defined as the order type of `ℕ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `ω` in identifiers is `omega0`. -/
OrderType.omega0 : OrderType.{u_1}
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functorialityCompFunctoriality.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₅, u₅} E] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D)
  (H : CategoryTheory.Functor D E),
  CategoryTheory.Limits.Cocone.functorialityCompFunctoriality F G H =
    CategoryTheory.NatIso.ofComponents'
      (fun x =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.Limits.Cocone.functoriality F G).comp
                (CategoryTheory.Limits.Cocone.functoriality (F.comp G) H)).obj
            x))
      ⋯
-- Mathlib.Data.Multiset.AddSub
/-- The sum of two multisets is the lift of the list append operation.
This adds the multiplicities of each element,
i.e. `count a (s + t) = count a s + count a t`.  -/
Multiset.add : {α : Type u_1} → Multiset α → Multiset α → Multiset α
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_factorial_lt_of_ne_zero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {n : ℕ}, n ≠ 0 → padicValNat p n.factorial < n
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjHomologySelfIso_inv_homologyι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) {Z : C} (h : ((HomologicalComplex.single C c j).obj A).opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).inv
      (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).homologyι j) h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom h
-- Mathlib.GroupTheory.PGroup
isPGroup_iff_card_dvd_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Finite G], IsPGroup p G ↔ ∃ n, Nat.card G ∣ p ^ n
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.id_toContinuousLinearMap : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E],
  LinearIsometry.id.toContinuousLinearMap = ContinuousLinearMap.id R E
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.Types.isIso_colimitPointwiseProductToProductColimit : ∀ {α : Type u} {I : α → Type u} [inst : (i : α) → CategoryTheory.SmallCategory (I i)]
  [∀ (i : α), CategoryTheory.IsFiltered (I i)] (F : (i : α) → CategoryTheory.Functor (I i) (Type u)),
  CategoryTheory.IsIso (CategoryTheory.Limits.colimitPointwiseProductToProductColimit F)
-- Mathlib.Algebra.Group.End
Equiv.Perm.sigmaCongrRight_inv : ∀ {α : Type u_7} {β : α → Type u_8} (F : (a : α) → Equiv.Perm (β a)),
  (Equiv.Perm.sigmaCongrRight F)⁻¹ = Equiv.Perm.sigmaCongrRight fun a => (F a)⁻¹
-- Init.Control.Lawful.MonadLift.Lemmas
monadLift_seqRight : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β),
  monadLift (x *> y) = monadLift x *> monadLift y
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_coe_sort_eq_attach : ∀ {ι : Type u_1} {M : Type u_3} (s : Finset ι) [inst : AddCommMonoid M] (f : ↥s → M), ∑ i, f i = ∑ i ∈ s.attach, f i
-- Mathlib.Data.Set.Image
Set.image_union_image_compl_eq_range : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} (f : α → β), f '' s ∪ f '' sᶜ = Set.range f
-- Mathlib.Algebra.Notation.Indicator
Set.mem_range_mulIndicator : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {r : M} {s : Set α} {f : α → M},
  r ∈ Set.range (s.mulIndicator f) ↔ r = 1 ∧ s ≠ Set.univ ∨ r ∈ f '' s
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat),
  (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).inverse =
    CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.mem_sets : ∀ {α : Type u_1} {s : Set α} {B : FilterBasis α}, s ∈ B.sets ↔ s ∈ B
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.freeMap_map : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {X Y : TopCat} (f : X ⟶ Y) (v : ↑X →₀ R),
  (CategoryTheory.ConcreteCategory.hom (TopModuleCat.freeMap R f)) v = Finsupp.mapDomain (⇑(TopCat.Hom.hom f)) v
-- Mathlib.Order.TypeTags
WithBot.coe : {α : Type u_1} → Coe α (WithBot α)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.associated_num_inv : ∀ {K : Type u} [inst : Field K] {x : RatFunc K}, x ≠ 0 → Associated x⁻¹.num x.denom
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.one_trans : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), LinearIsometryEquiv.trans 1 e = e
-- Mathlib.Tactic.Translate.GuessName
Mathlib.Tactic.GuessName.GuessNameData.mk : Std.HashMap String (List String) → Std.HashMap String String → Mathlib.Tactic.GuessName.GuessNameData
-- Mathlib.Data.Finset.Max
Finset.max_insert : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α} {s : Finset α}, (insert a s).max = max (↑a) s.max
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_modify_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k : α} {f : β k → β k}, (m.modify k f).getKey! k = if k ∈ m then k else default
-- Mathlib.Analysis.Calculus.Deriv.Prod
hasDerivAt_pi : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_1} {E' : ι → Type u_2}
  [inst_1 : (i : ι) → NormedAddCommGroup (E' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i}
  {φ' : (i : ι) → E' i}, HasDerivAt φ φ' x ↔ ∀ (i : ι), HasDerivAt (fun x => φ x i) (φ' i) x
-- Mathlib.CategoryTheory.MarkovCategory.Positive
/-- Markov category where copy is natural given deterministic composition of morphisms.  -/
CategoryTheory.PositiveCategory : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type (max u v)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.map.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] (M : Subgroup H)
  [inst_2 : M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M),
  QuotientGroup.map N M f h = QuotientGroup.lift N ((QuotientGroup.mk' M).comp f) ⋯
-- Mathlib.Algebra.Quaternion
Quaternion.coe_starAe : ∀ {R : Type u_3} [inst : CommRing R], ⇑Quaternion.starAe = MulOpposite.op ∘ star
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.leibniz_lie : ∀ {R : Type u} {X : Type v} [inst : CommRing R] (a b c : FreeNonUnitalNonAssocAlgebra R X),
  FreeLieAlgebra.Rel R X (a * (b * c)) (a * b * c + b * (a * c))
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.ext_iff : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {x y : C ≌ D},
  x = y ↔ x.functor = y.functor ∧ x.inverse = y.inverse ∧ x.unitIso ≍ y.unitIso ∧ x.counitIso ≍ y.counitIso
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_erase!_eq_iff_not_compare_maxKeyD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k fallback : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        ((Std.DTreeMap.Internal.Impl.erase! k t).maxKeyD fallback = t.maxKeyD fallback ↔
          ¬compare k (t.maxKeyD fallback) = Ordering.eq)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_insert_one : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.closure (insert 1 s) = Subgroup.closure s
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.destruct_join.aux.match_1.splitter : {α : Type u_1} →
  (motive : Option (Stream'.WSeq α × Stream'.WSeq (Stream'.WSeq α)) → Sort u_2) →
    (x : Option (Stream'.WSeq α × Stream'.WSeq (Stream'.WSeq α))) →
      (Unit → motive none) →
        ((s : Stream'.WSeq α) → (S : Stream'.WSeq (Stream'.WSeq α)) → motive (some (s, S))) → motive x
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.instSMul : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] → [inst_3 : Module R M] → [inst_4 : Module R N] → SMul R (TensorProduct R M N)
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- Given two smooth maps into the same fibers of a Riemannian bundle,
their scalar product is smooth.  -/
ContMDiff.inner_bundle : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (x : B) → NormedAddCommGroup (E x)] [inst_9 : (x : B) → InnerProductSpace ℝ (E x)]
  [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E] {EM : Type u_6} [inst_12 : NormedAddCommGroup EM]
  [inst_13 : NormedSpace ℝ EM] {HM : Type u_7} [inst_14 : TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM}
  {M : Type u_8} [inst_15 : TopologicalSpace M] [inst_16 : ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB n F E]
  {b : M → B} {v w : (x : M) → E (b x)},
  (ContMDiff IM (IB.prod (modelWithCornersSelf ℝ F)) n fun m => ⟨b m, v m⟩) →
    (ContMDiff IM (IB.prod (modelWithCornersSelf ℝ F)) n fun m => ⟨b m, w m⟩) →
      ContMDiff IM (modelWithCornersSelf ℝ ℝ) n fun b_1 => inner ℝ (v b_1) (w b_1)
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.maximal_ideal_unique : ∀ (R : Type u_1) [inst : CommSemiring R] [IsLocalRing R], ∃! I, I.IsMaximal
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instFibrationP₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition]
  [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [HomotopicalAlgebra.IsFibrant A] [P.IsGood],
  HomotopicalAlgebra.Fibration P.p₁
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.transEquiv_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (f' : β ≃ γ) (a : γ),
  ↑(e.transEquiv f').symm a = ↑e.symm (f'.symm a)
-- Lean.Util.MonadCache
Lean.MonadCache.mk : {α β : Type} → {m : Type → Type} → (α → m (Option β)) → (α → β → m Unit) → Lean.MonadCache α β m
-- Mathlib.Geometry.Euclidean.Incenter
/-- The insphere of a simplex.  -/
Affine.Simplex.insphere : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] → {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → EuclideanGeometry.Sphere P
-- Lean.Server.Utils
/-- Prefixes all written outputs with `pre`.  -/
Lean.IO.FS.Stream.withPrefix : IO.FS.Stream → String → IO.FS.Stream
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instHasTerminalElemCarrierObjPartOrdEmbIsCardinalFilteredValSetPropSet : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (S : Subtype J.PropSet),
  CategoryTheory.Limits.HasTerminal ↑↑S
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_snd : ∀ (K : Type u_1) [inst : Field K] (x : NumberField.mixedEmbedding.realMixedSpace K) (w : { w // w.IsComplex }),
  ((NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace K) x).2 w = (x.2 w).2
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  {F : CategoryTheory.Functor C V}
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution U F] {G : CategoryTheory.Functor C V}
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution U G] (f : F ⟶ G),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id U) f)
      (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U G).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U F).hom f
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symm_apply_eq : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) {x : N} {y : M}, e.symm x = y ↔ x = e y