mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coset.Basic
AddMonoidHom.fiberEquivKer_apply : ∀ {α : Type u_1} [inst : AddGroup α] {H : Type u_2} [inst_1 : AddGroup H] (f : α →+ H) (a : α) (g : ↑(⇑f ⁻¹' {f a})),
  ↑((f.fiberEquivKer a) g) = -a + ↑g
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ.eq_1 : ∀ {n : ℕ} (i : Fin (n + 2)), SimplexCategory.δ i = SimplexCategory.mkHom i.succAboveOrderEmb.toOrderHom
-- Init.PropLemmas
if_false_left : ∀ {p q : Prop} [h : Decidable p], (if p then False else q) ↔ ¬p ∧ q
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableWithinAt_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {s : Set M} {z : M} {f : M → E'}, MDiffAt[s] (-f) z ↔ MDiffAt[s] f z
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_inter_Ici : ∀ {α : Type u_1} [inst : SemilatticeSup α] (b a c : α), Set.Ico b a ∩ Set.Ici c = Set.Ico (b ⊔ c) a
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.starAddMonoid : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddMonoid β] →
          [inst_3 : ContinuousAdd β] → [inst_4 : StarAddMonoid β] → [ContinuousStar β] → StarAddMonoid C(α, β)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectR_mapComp_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b_1 c : C} (f : a ⟶ b_1) (g : b_1 ⟶ c),
  ((CategoryTheory.Bicategory.Prod.sectR b C).mapComp f g).hom =
    CategoryTheory.Prod.mkHom (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id b)).inv
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g))
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getEntry!_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α}
  [inst_1 : Inhabited ((a : α) × β a)],
  Std.DHashMap.Internal.AssocList.getEntry! a l = Std.Internal.List.getEntry! a l.toList
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.brecOn.go : {motive : Turing.ToPartrec.Code → Sort u} →
  (t : Turing.ToPartrec.Code) →
    ((t : Turing.ToPartrec.Code) → Turing.ToPartrec.Code.below t → motive t) → motive t ×' Turing.ToPartrec.Code.below t
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.proetalePrecoverage_le_precoverage_weaklyEtale : AlgebraicGeometry.Scheme.proetalePrecoverage ≤
  CategoryTheory.MorphismProperty.precoverage @AlgebraicGeometry.WeaklyEtale
-- Mathlib.Data.List.Duplicate
List.Duplicate.mono_sublist : ∀ {α : Type u_1} {l : List α} {x : α} {l' : List α}, List.Duplicate x l → l.Sublist l' → List.Duplicate x l'
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- The boundary map is only nonzero if `c.Rel i j`.  -/
TopPair.HomologyPretheory.shape_δ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (self : TopPair.HomologyPretheory C c) (i j : ι), ¬c.Rel i j → self.δ i j = 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, k ∉ m₁ → (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback
-- Mathlib.Order.Hom.WithTopBot
WithBot.toDualTopEquiv_bot : ∀ {α : Type u_1} [inst : LE α], WithBot.toDualTopEquiv ⊥ = ⊥
-- Init.Data.Array.Lemmas
Array.all_push : ∀ {α : Type u_1} {xs : Array α} {a : α} {p : α → Bool}, (xs.push a).all p = (xs.all p && p a)
-- Mathlib.Order.Monotone.Defs
Monotone.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β}, Monotone g → Antitone f → Antitone (g ∘ f)
-- Init.Data.Array.DecidableEq
_private.Init.Data.Array.DecidableEq.0.Array.isEqvAux.eq_1 : ∀ {α : Type u} (xs ys : Array α) (hsz : xs.size = ys.size) (p : α → α → Bool) (x_2 : 0 ≤ xs.size),
  xs.isEqvAux ys hsz p 0 x_2 = true
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.coe_comap : ∀ {α : Type u} {β : Type v} {m : α → β} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m ∈ u),
  ↑(u.comap inj large) = Filter.comap m ↑u
-- Mathlib.Algebra.GradedMonoid
/-- An element `a : R` is said to be homogeneous if there is some `i : ι` such that `a ∈ A i`.  -/
SetLike.IsHomogeneousElem : {ι : Type u_1} → {R : Type u_2} → {S : Type u_3} → [SetLike S R] → (ι → S) → R → Prop
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_eq_single_one_one_iff`. -/
SkewMonoidAlgebra.toFinsupp_eq_single_one_one_iff : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k] {a : SkewMonoidAlgebra k G},
  (a.coeff = fun₀ | 1 => 1) ↔ a = 1
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonian.getVertEquiv_symm_apply : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} (hp : p.IsHamiltonian) (a_1 : α),
  hp.getVertEquiv.symm a_1 = hp.supportGetEquiv.invFun a_1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments_performRupCheck_base_case : ∀ {rupHints : Array ℕ} {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (f_assignments_size : f.assignments.size = n) (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f' = (f.performRupCheck rupHints).1 →
    ∀ (f'_assignments_size : f'.assignments.size = n)
      (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
      (derivedLits_arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))),
      derivedLits_arr = { toList := derivedLits } →
        f.DerivedLitsInvariant f_assignments_size f'.assignments f'_assignments_size derivedLits →
          (∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]) →
            f.ClearInsertInductionMotive f_assignments_size derivedLits_arr 0 f'.assignments
-- Mathlib.Data.Finset.Option
Finset.eraseNone_none : ∀ {α : Type u_1}, Finset.eraseNone {none} = ∅
-- Aesop.Forward.PremiseIndex
Aesop.PremiseIndex.mk.inj : ∀ {toNat toNat_1 : ℕ}, { toNat := toNat } = { toNat := toNat_1 } → toNat = toNat_1
-- Mathlib.Computability.RegularExpressions
RegularExpression.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (P : RegularExpression α),
  RegularExpression.map g (RegularExpression.map f P) = RegularExpression.map (g ∘ f) P
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.closedInterior_face_subset_closedInterior : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] [ZeroLEOneClass k] {n : ℕ} (s : Affine.Simplex k P n)
  {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1), (s.face h).closedInterior ⊆ s.closedInterior
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instHasDistribNeg : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : Mul R] →
      [inst_2 : HasDistribNeg R] → [inst_3 : ContinuousMul R] → [ContinuousNeg R] → HasDistribNeg (SeparationQuotient R)
-- Mathlib.Data.Fintype.Sets
Set.toFinset_univ : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Fintype ↑Set.univ], Set.univ.toFinset = Finset.univ
-- Init.Data.SInt.Lemmas
ISize.lt_of_lt_of_le : ∀ {a b c : ISize}, a < b → b ≤ c → a < c
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.coe_symm_toNatLinearEquiv : ∀ {M : Type u_5} {M₂ : Type u_7} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] (e : M ≃+ M₂),
  ⇑e.toNatLinearEquiv.symm = ⇑e.symm
-- Mathlib.Order.Heyting.Hom
HeytingHom.instPartialOrder : {α : Type u_2} →
  {β : Type u_3} → [inst : HeytingAlgebra α] → [inst_1 : HeytingAlgebra β] → PartialOrder (HeytingHom α β)
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.induction_on_of_compact : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {s : Set 𝕜} [CompactSpace ↑s] {p : C(↑s, 𝕜) → Prop},
  (∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)) →
    p (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) →
      p (star (ContinuousMap.restrict s (ContinuousMap.id 𝕜))) →
        (∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)) →
          (∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)) →
            (∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in nhds f, p g) → p f) → ∀ (f : C(↑s, 𝕜)), p f
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithTop.coe_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : Preorder α] [inst_1 : SupSet α] (f : ι → α),
  BddAbove (Set.range f) → ↑(⨆ i, f i) = ⨆ i, ↑(f i)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingEquiv.subsemiringMap_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (e : R ≃+* S) (s : Subsemiring R)
  (x : ↥s), ↑((e.subsemiringMap s) x) = e ↑x
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.bounded : {α : Type} → Std.CloseableChannel.Bounded✝ α → Std.CloseableChannel.Flavors α
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.coeff_injective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f), Function.Injective ⇑h.coeff
-- Aesop.Forward.State.ApplyGoalDiff
_private.Aesop.Forward.State.ApplyGoalDiff.0.Aesop.ForwardState.applyGoalDiff.addHyp : Aesop.LocalRuleSet → Lean.FVarId → Aesop.ForwardState → Aesop.BaseM Aesop.ForwardState
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
EuclideanGeometry.angle_smul_left_of_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₄ : P} (p₃ : P) {r : ℝ},
  0 < r → r • (p₄ -ᵥ p₂) = p₁ -ᵥ p₂ → EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₂ p₃
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.isCardinalFiltered_under : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ] (j₀ : J), CategoryTheory.IsCardinalFiltered (CategoryTheory.Under j₀) κ
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddRightCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddRightCancelMonoid α],
  Lex.instAddRightCancelMonoid = { toAddMonoid := Lex.instAddMonoid, toIsRightCancelAdd := ⋯ }
-- Mathlib.Topology.Sion
/-- `sublevelLeft` is parameterwise monotone  -/
_private.Mathlib.Topology.Sion.0.Sion.monotone_sublevelLeft : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β} {u v : β}
  (y : ↑Y), u ≤ v → Sion.sublevelLeft✝ X f u ↑y ⊆ Sion.sublevelLeft✝ X f v ↑y
-- Std.Data.HashMap.Lemmas
/-- Simpler variant of `getD_filterMap` when `LawfulBEq` is available.  -/
Std.HashMap.getD_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α]
  {f : α → β → Option γ} {k : α} {fallback : γ},
  (Std.HashMap.filterMap f m).getD k fallback = (m[k]?.bind (f k)).getD fallback
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.Rewrites.below : {T : Type u_1} →
  {N : Type u_2} →
    {r : ContextFreeRule T N} →
      {motive : (a a_1 : List (Symbol T N)) → r.Rewrites a a_1 → Prop} →
        {a a_1 : List (Symbol T N)} → r.Rewrites a a_1 → Prop
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.valuationIdeal.congr_simp : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v v_1 : Valuation (RatFunc K) Γ} (e_v : v = v_1) [inst_2 : v.IsNontrivial] [inst_3 : Valuation.IsTrivialOn K v]
  (hle : v RatFunc.X ≤ 1), RatFunc.valuationIdeal hle = RatFunc.valuationIdeal ⋯
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.instNonemptyEdgeLabeling : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Nonempty K], Nonempty (G.EdgeLabeling K)
-- Aesop.Frontend.Extension
Aesop.Frontend.modifyGetGlobalRuleSet : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      [MonadLiftT IO m] →
        [MonadLiftT Lean.CoreM m] →
          [Lean.MonadEnv m] → {α : Type} → Aesop.RuleSetName → (Aesop.GlobalRuleSet → α × Aesop.GlobalRuleSet) → m α
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.full_univ : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C], CategoryTheory.Subgroupoid.full Set.univ = ⊤
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.Bool.bne_to_beq : ∀ (a b : Bool), (a != b) = !a == b
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- **Alias** of `LinearOrderedCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete`. -/
LinearOrderedCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] (g : G),
  ({x | x ≤ g}.WellFoundedOn fun x1 x2 => x1 > x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.isJointlySurjectivePreserving : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.NonnegCoeffs.below : {motive : (a : Lean.Grind.CommRing.Poly) → a.NonnegCoeffs → Prop} →
  {a : Lean.Grind.CommRing.Poly} → a.NonnegCoeffs → Prop
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.rightInv.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E),
  p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.decay_add_le_aux : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (k n : ℕ) (f g : SchwartzMap E F) (x : E),
  ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑g) x‖
-- Mathlib.Order.CompleteLattice.Basic
Prod.swap_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst_1 : SupSet β] (s : Set (α × β)),
  (sSup s).swap = sSup (Prod.swap '' s)
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State.fType : Lean.Elab.Tactic.ElimApp.State✝ → Lean.Expr
-- Mathlib.Order.Atoms
isCoatomistic_dual_iff_isAtomistic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α], IsCoatomistic αᵒᵈ ↔ IsAtomistic α
-- Mathlib.Algebra.Polynomial.Basic
/-- `monomial s a` is the monomial `a * X^s`  -/
Polynomial.monomial : {R : Type u} → [inst : Semiring R] → ℕ → R →ₗ[R] Polynomial R
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.limitConeLift_toFunctor : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat)
  (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Cat.HasLimits.limitConeLift F s).toFunctor =
    {
      obj :=
        ⇑(CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects)
              { pt := ↑s.pt, π := { app := fun j => TypeCat.ofHom (s.π.app j).toFunctor.obj, naturality := ⋯ } })),
      map := fun {X Y} f =>
        CategoryTheory.Limits.Types.Limit.mk
          (CategoryTheory.Cat.HasLimits.homDiagram
            ((CategoryTheory.ConcreteCategory.hom
                (CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects)
                  { pt := ↑s.pt, π := { app := fun j => TypeCat.ofHom (s.π.app j).toFunctor.obj, naturality := ⋯ } }))
              X)
            ((CategoryTheory.ConcreteCategory.hom
                (CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects)
                  { pt := ↑s.pt, π := { app := fun j => TypeCat.ofHom (s.π.app j).toFunctor.obj, naturality := ⋯ } }))
              Y))
          (fun j =>
            CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
              (CategoryTheory.CategoryStruct.comp ((s.π.app j).toFunctor.map f) (CategoryTheory.eqToHom ⋯)))
          ⋯,
      map_id := ⋯, map_comp := ⋯ }
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_rci : ∀ {α : Type u_1} {xs : List α} {lo : ℕ}, Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = List.drop lo xs
-- Init.Data.List.Lemmas
List.filter_cons_of_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, ¬p a = true → List.filter p (a :: l) = List.filter p l
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Var
Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go_get : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (a curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ)
  (hidx : idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).vec.get idx ⋯ = (s.get idx hidx).cast ⋯
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.single_eq_zero_iff : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommGroup (β i)] (p : ENNReal) (i : ι)
  {a : β i}, PiLp.single p i a = 0 ↔ a = 0
-- Init.Data.List.Basic
List.isEqv_nil_nil : ∀ {α : Type u} {eqv : α → α → Bool}, [].isEqv [] eqv = true
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp'.eq_1 : ∀ (C : Type u) (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) (a : C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C (CategoryTheory.FreeMonoidalCategory.of a) x =
    CategoryTheory.Iso.refl
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.FreeMonoidalCategory.inclusionObj x)
        (CategoryTheory.FreeMonoidalCategory.of a))
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
AEMeasurable.nnnorm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} {μ : MeasureTheory.Measure β},
  AEMeasurable f μ → AEMeasurable (fun a => ‖f a‖₊) μ
-- Mathlib.Algebra.Module.Basic
map_inv_intCast_smul : ∀ {M : Type u_3} {M₂ : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] {F : Type u_5}
  [inst_2 : FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7) [inst_4 : DivisionRing R]
  [inst_5 : DivisionRing S] [inst_6 : Module R M] [inst_7 : Module S M₂] (z : ℤ) (x : M), f ((↑z)⁻¹ • x) = (↑z)⁻¹ • f x
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.toOuterMeasure_pure_apply : ∀ {α : Type u_1} (a : α) (s : Set α), (PMF.pure a).toOuterMeasure s = if a ∈ s then 1 else 0
-- Mathlib.Computability.Primrec.List
Primcodable.list : {α : Type u_1} → [Primcodable α] → Primcodable (List α)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.contLinear_map_vsub : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] [inst_11 : TopologicalSpace W] [inst_12 : IsTopologicalAddTorsor Q]
  (f : P →ᴬ[R] Q) (p₁ p₂ : P), f.contLinear (p₁ -ᵥ p₂) = f p₁ -ᵥ f p₂
-- Mathlib.Analysis.Convex.MetricSpace
/-- **Alias** of `Convexity.dist_iConvexComb_le`.

---

`dist(∑ tᵢ xᵢ, ∑ tᵢ yᵢ) ≤ ∑ tᵢ dist(xᵢ, yᵢ)`  -/
Convexity.dist_convexCombination_right_le : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] {ι : Type u_3}
  (f : Convexity.StdSimplex ℝ ι) (x y : ι → X),
  dist (Convexity.iConvexComb f x) (Convexity.iConvexComb f y) ≤ Convexity.iConvexComb f fun i => dist (x i) (y i)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsId'App_hom_naturality_assoc : ∀ {R : Type u₁} [inst : Ring R] (f : R →+* R) (hf : f = RingHom.id R) {M N : ModuleCat R} (φ : M ⟶ N) {Z : ModuleCat R}
  (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map φ)
      (CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf N).hom h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf M).hom
      (CategoryTheory.CategoryStruct.comp φ h)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_mono_set_of_nonneg : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f : ι → N} [AddLeftMono N],
  (∀ (x : ι), 0 ≤ f x) → Monotone fun s => ∑ x ∈ s, f x
-- Aesop.Forward.Match.Types
/-- Premises that appear in the rule's conclusion. This is a property of the
rule, but we include it here because it's used to check whether two matches
are equivalent.  -/
Aesop.Match.conclusionDeps : Aesop.Match → Array Aesop.PremiseIndex
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
GrpCat.binaryProductLimitCone_isLimit_lift : ∀ (G H : GrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)),
  (G.binaryProductLimitCone H).isLimit.lift t =
    GrpCat.ofHom
      ((GrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod
        (GrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
-- Mathlib.CategoryTheory.Generator.Basic
/-- For a category `C` and an object `G : C`, `G` is a detector of `C` if
the functor `C(G, -)` reflects isomorphisms.

While `IsDetector G : Prop` is the proposition that `G` is a detector of `C`,
an `HasDetector C : Prop` is the proposition that such a detector exists.
Note that `HasDetector C` is a proposition. It does not designate a favored detector
and merely asserts the existence of one.
 -/
CategoryTheory.HasDetector : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- Multiplication by a nonzero element `a` on the right, as a `Dilation` of a ring with a strictly
multiplicative norm.  -/
Dilation.mulRight : {α : Type u_1} → [inst : NonUnitalNormedRing α] → [NormMulClass α] → (a : α) → a ≠ 0 → α →ᵈ α
-- Mathlib.NumberTheory.Height.NumberField
/-- A number field `K` satisfies the **Northcott property**:
The set of elements of bounded logarithmic height is finite.  -/
NumberField.finite_setOfPred_logHeight₁_le : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B : ℝ), {x | Height.logHeight₁ x ≤ B}.Finite
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFieldRedeclInfo.sizeOf_spec : ∀ (i : Lean.Elab.FieldRedeclInfo), sizeOf (Lean.Elab.Info.ofFieldRedeclInfo i) = 1 + sizeOf i
-- Mathlib.Data.List.Indexes
List.mapIdx_eq_ofFn : ∀ {α : Type u} {β : Type v} (l : List α) (f : ℕ → α → β), List.mapIdx f l = List.ofFn fun i => f (↑i) (l.get i)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveCombine.inj : ∀ {c₁ c₂ c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveCombine c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveCombine c₁_1 c₂_1 →
    c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Data.Sigma.Lex
Sigma.Lex.mono_left : ∀ {ι : Type u_1} {α : ι → Type u_2} {r₁ r₂ : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop},
  (∀ (a b : ι), r₁ a b → r₂ a b) → ∀ {a b : (i : ι) × α i}, Sigma.Lex r₁ s a b → Sigma.Lex r₂ s a b
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_neg_distrib : ∀ {ι : Type u_1} {G : Type u_5} {s : Finset ι} [inst : SubtractionCommMonoid G] (f : ι → G),
  ∑ x ∈ s, -f x = -∑ x ∈ s, f x
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.toSSetObjEdgeEquiv_apply_hom : ∀ {X : TopCat} {x y : ↑X} (e : SSet.Edge (TopCat.toSSetObj₀Equiv.symm x) (TopCat.toSSetObj₀Equiv.symm y)),
  (TopCat.toSSetObjEdgeEquiv e).hom = TopCat.toSSetObj₁Equiv e.edge