mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- The oriented angles at a point `p'` in their intersection between `p` and its orthogonal
projections onto two affine subspaces (typically lines, for this version of the lemma) are equal
if `p` is equidistant to the two subspaces.  -/
EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [inst_4 : Fact (Module.finrank ℝ V = 2)] [inst_5 : Module.Oriented ℝ V (Fin 2)]
  {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} (hp'₁ : p' ∈ s₁) (hp'₂ : p' ∈ s₂),
  ↑((EuclideanGeometry.orthogonalProjection s₁) p) ≠ ↑((EuclideanGeometry.orthogonalProjection s₂) p) →
    dist p ↑((EuclideanGeometry.orthogonalProjection s₁) p) = dist p ↑((EuclideanGeometry.orthogonalProjection s₂) p) →
      EuclideanGeometry.oangle (↑((EuclideanGeometry.orthogonalProjection s₁) p)) p' p =
        EuclideanGeometry.oangle p p' ↑((EuclideanGeometry.orthogonalProjection s₂) p)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
continuousMultilinearCurryFin1_symm_apply : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (f : G →L[𝕜] G')
  (v : Fin 1 → G), ((continuousMultilinearCurryFin1 𝕜 G G').symm f) v = f (v 0)
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.isHomogeneous_X : ∀ {σ : Type u_1} (R : Type u_3) [inst : CommSemiring R] (i : σ), (MvPolynomial.X i).IsHomogeneous 1
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `le_of_antisymmRel_of_le`. -/
AntisymmRel.trans_le : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → b ≤ c → a ≤ c
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddLECancellable.withTop : ∀ {α : Type u} [inst : Add α] {a : α} [inst_1 : LE α], AddLECancellable a → AddLECancellable ↑a
-- Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
/-- If `C` has (small) wide equalizers and a weakly initial object, then it has an initial object.

The initial object is constructed as the wide equalizer of all endomorphisms on the given weakly
initial object.
 -/
CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWideEqualizers C] {T : C},
  (∀ (X : C), Nonempty (T ⟶ X)) → CategoryTheory.Limits.HasInitial C
-- Init.Data.Char.Ordinal
Char.ofOrdinal_le_of_le : ∀ {f g : Fin Char.numCodePoints}, f ≤ g → Char.ofOrdinal f ≤ Char.ofOrdinal g
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.ofSet_target : ∀ {α : Type u_1} (s : Set α), (PartialEquiv.ofSet s).target = s
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_eq_lsub : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}),
  (Ordinal.type WellOrderingRel).blsub (Ordinal.bfamilyOfFamily f) = Ordinal.lsub f
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.toMapFactorizationData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          HomotopicalAlgebra.CofibrantBrownFactorization f →
            (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.order_le_of_coeff_ne_zero : ∀ {R : Type u_3} [inst : Zero R] {Γ : Type u_5} [inst_1 : Zero Γ] [inst_2 : LinearOrder Γ] {x : HahnSeries Γ R} {g : Γ},
  x.coeff g ≠ 0 → x.order ≤ g
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.toEquiv_eq_codRestrict_restrict : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β),
  ⇑e.toEquiv = Set.codRestrict (e.source.domRestrict ↑e) e.target ⋯
-- Init.Data.Array.Lemmas
Array.anyM.eq_1 : ∀ {α : Type u} {m : Type → Type w} [inst : Monad m] (p : α → m Bool) (as : Array α) (start stop : ℕ),
  Array.anyM p as start stop =
    if h : stop ≤ as.size then (fun stop h => Array.anyM.loop p as stop h start) stop h
    else (fun stop h => Array.anyM.loop p as stop h start) as.size ⋯
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.ofList_singleton : ∀ {α : Type u_1} (x : α), FreeAddMonoid.ofList [x] = FreeAddMonoid.of x
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The pullback cone obtained from the pushout cone associated to a
commutative square in the opposite category identifies to the cone associated
to the flipped square.  -/
CategoryTheory.CommSq.coconeUnop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z : Cᵒᵖ} →
      {f : W ⟶ X} →
        {g : W ⟶ Y} → {h : X ⟶ Z} → {i : Y ⟶ Z} → (p : CategoryTheory.CommSq f g h i) → p.cocone.unop ≅ ⋯.cone
-- Mathlib.Order.RelIso.Basic
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because `RelIso` defines custom coercions other than the ones given by `DFunLike`.  -/
RelIso.Simps.apply : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → α → β
-- Mathlib.Order.BooleanAlgebra.Set
Set.disjoint_compl_right_iff_subset : ∀ {α : Type u_1} {s t : Set α}, Disjoint s tᶜ ↔ s ⊆ t
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.instLinearOrderFiniteElement : (K : Type u_1) →
  [inst : LinearOrder K] →
    [inst_1 : Field K] → [inst_2 : IsOrderedRing K] → LinearOrder (ArchimedeanClass.FiniteElement K)
-- Mathlib.Topology.Order.Category.AlexDisc
alexDiscEquivPreord_unitIso : alexDiscEquivPreord.unitIso =
  CategoryTheory.NatIso.ofComponents (fun X => AlexDisc.Iso.mk (id (homeoWithUpperSetTopologyorderIso ↑X.toTopCat)))
    @alexDiscEquivPreord._proof_3
-- Mathlib.MeasureTheory.Measure.ResolventTransform
MeasureTheory.hasDerivAt_resolventTransform : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [HereditarilyLindelofSpace 𝕜] [CompleteSpace 𝕜]
  [inst_3 : MeasurableSpace 𝕜] [BorelSpace 𝕜] [inst_5 : RCLike A] [inst_6 : NormedAlgebra 𝕜 A]
  {μ : MeasureTheory.Measure 𝕜} [MeasureTheory.IsFiniteMeasure μ],
  ∀ a ∉ ⇑(algebraMap 𝕜 A) '' μ.support,
    HasDerivAt (MeasureTheory.resolventTransform μ) (∫ (x : 𝕜), resolvent a x ^ 2 ∂μ) a
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentHom.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentHom✝ D =
    LinearMap.liftBaseChange S
      (Algebra.Extension.Cotangent.map (Algebra.Generators.PresentationOfFreeCotangent.Aux.fhom✝ D).toExtensionHom)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- `PseudoEMetricSpace` instance on the product of two pseudoemetric spaces, using the
`L^p` pseudoedistance, and having as uniformity the product uniformity.  -/
WithLp.instProdPseudoEMetricSpace : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) →
      [hp : Fact (1 ≤ p)] → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → PseudoEMetricSpace (WithLp p (α × β))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasDerivWithinAt.sinh : ∀ {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Real.sinh (f x)) (Real.cosh (f x) * f') s x
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasNegAssignment.eq_1 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.hasNegAssignment = false
-- Mathlib.Data.Set.Pairwise.Lattice
Equiv.setCongr.congr_simp : ∀ {α : Type u_3} {s t : Set α} (h : s = t), Equiv.setCongr h = Equiv.setCongr h
-- Init.Data.BitVec.Lemmas
/-- If `y ≤ x`, then the subtraction `(x - y)` does not overflow.
Thus, `(x - y).toNat = x.toNat - y.toNat`
 -/
BitVec.toNat_sub_of_le : ∀ {n : ℕ} {x y : BitVec n}, y ≤ x → (x - y).toNat = x.toNat - y.toNat
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
_private.Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic.0.ProfiniteAddGrp.Hom.mk.injEq : ∀ {A B : ProfiniteAddGrp.{u}} (hom' hom'_1 : ↑A.toProfinite.toTop →ₜ+ ↑B.toProfinite.toTop),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Use the axiom of choice to extract a right adjoint from an `IsLeftAdjoint` instance.  -/
CategoryTheory.Bicategory.getRightAdjoint : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} → (f : a ⟶ b) → [CategoryTheory.Bicategory.IsLeftAdjoint f] → CategoryTheory.Bicategory.RightAdjoint f
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_inv : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] (d : D),
  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).inv =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv)
      (CategoryTheory.Functor.OplaxLeftLinear.δₗ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.algebraMap_eq_zero_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : R),
  (algebraMap R (TensorAlgebra R M)) x = 0 ↔ x = 0
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictWidthInfty.eq_1 : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)), 𝒢.strictWidthInfty = if h : DiscreteTopology ↥𝒢.strictPeriods then |⋯.choose| else 0
-- Lean.Data.Lsp.Internal
/-- Full name of the declaration that matches the query.  -/
Lean.Lsp.LeanIdentifier.decl : Lean.Lsp.LeanIdentifier → Lean.Name
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_alter!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)} {hc : k ∈ Std.DTreeMap.Internal.Impl.alter! k f t},
      (Std.DTreeMap.Internal.Impl.alter! k f t).getKey k hc = k
-- Init.Data.Vector.Lemmas
Vector.replicate_inj : ∀ {n : ℕ} {α : Type u_1} {a b : α}, Vector.replicate n a = Vector.replicate n b ↔ n = 0 ∨ a = b
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.ninePointCircle_center : ∀ {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 : ℕ} (s : Affine.Simplex ℝ P n),
  s.ninePointCircle.center = ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter
-- Init.Data.SInt.Basic
instToStringInt32 : ToString Int32
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] {U V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ}
  (i : U ⟶ V) {Z : C}
  (h :
    Y.presheaf.obj
        (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj (Opposite.unop V))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (X.presheaf.map i)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f (Opposite.unop V))
        h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f (Opposite.unop U))
      (CategoryTheory.CategoryStruct.comp
        (Y.presheaf.map ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).op.map i)) h)
-- Mathlib.Combinatorics.Hindman
Hindman.FS.tail' : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M) (m : M), Hindman.FS a.tail m → Hindman.FS a m
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
      (CategoryTheory.Limits.codiag A))
  [inst_2 : CategoryTheory.Limits.HasTerminal C] [HomotopicalAlgebra.IsFibrant A]
  [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition],
  HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.Cylinder.ofFactorizationData h).I
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.closure_nsmul : ∀ {M : Type u_3} [inst : AddMonoid M] {s : Set M} {n : ℕ},
  0 ∈ s → n ≠ 0 → AddSubmonoid.closure (n • s) = AddSubmonoid.closure s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (assign : α → Bool) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ)
  (hidx1 : idx < w),
  curr ≤ idx →
    ⟦assign,
        { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance curr hcurr s).aig,
          ref :=
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance curr hcurr s).vec.get idx
              hidx1 }⟧ =
      if hidx : idx < distance then false else ⟦assign, { aig := aig, ref := input.get (idx - distance) ⋯ }⟧
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.RingCat.Colimits.descFunLift.match_1.eq_3 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (motive : RingCat.Colimits.Prequotient F → Sort u_2)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (RingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive RingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive RingCat.Colimits.Prequotient.one)
  (h_4 : (x : RingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : RingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : RingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match RingCat.Colimits.Prequotient.one with
    | RingCat.Colimits.Prequotient.of j x => h_1 j x
    | RingCat.Colimits.Prequotient.zero => h_2 ()
    | RingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_3 ()
-- Mathlib.Order.Category.Lat
Lat.dualEquiv_inverse : Lat.dualEquiv.inverse = Lat.dual
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.tendsto_coe : ∀ {α : Type u_2} {f : Filter α} {m : α → NNReal} {x : NNReal},
  Filter.Tendsto (fun a => ↑(m a)) f (nhds ↑x) ↔ Filter.Tendsto m f (nhds x)
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inrCompAssociator_inv_app_down_down : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : E),
  ((CategoryTheory.sum.inrCompAssociator C D E).inv.app X).down.down = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.Order.IsLUB
IsGLB.isGLB_of_tendsto : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : Preorder γ] [inst_4 : TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ},
  MonotoneOn f s → IsGLB s a → s.Nonempty → Filter.Tendsto f (nhdsWithin a s) (nhds b) → IsGLB (f '' s) b
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.of_sub_right : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, (s - t).Nonempty → t.Nonempty
-- Mathlib.Algebra.Order.Field.Basic
StrictMono.div_const : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α]
  {β : Type u_4} [inst_4 : Preorder β] {f : β → α}, StrictMono f → ∀ {c : α}, 0 < c → StrictMono fun x => f x / c
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact)
  (f : S₁ ⟶ S₂),
  (CategoryTheory.ShortComplex.ShortExact.singleTriangle.map h₁ h₂ f).hom₂ =
    (DerivedCategory.singleFunctor C 0).map f.τ₂
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.getStateUnsafe : {σ : Type} →
  [Inhabited σ] →
    (ext : Lean.EnvExtension σ) →
      Lean.Environment → optParam Lean.EnvExtension.AsyncMode ext.asyncMode → optParam Lean.Name Lean.Name.anonymous → σ
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_add_atTop_nat : ∀ (k : ℕ), Filter.Tendsto (fun a => a + k) Filter.atTop Filter.atTop
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.List.applyId_eq_self : ∀ {α : Type u} [inst : DecidableEq α] {xs ys : List α},
  ∀ x ∉ xs, Plausible.InjectiveFunction.List.applyId (xs.zip ys) x = x
-- Mathlib.Data.List.Cycle
List.nextOr_concat : ∀ {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x : α} (d : α), x ∉ xs → (xs ++ [x]).nextOr x d = d
-- Mathlib.Topology.MetricSpace.ProperSpace.Real
NNReal.instSecondCountableTopology : SecondCountableTopology NNReal
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.forM_eq_forM_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit.{w + 1}}, forM t f = forM t.toArray f
-- Std.Data.TreeSet.Basic
/-- Returns `true` if the tree set contains no mappings.  -/
Std.TreeSet.isEmpty : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → Bool
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom : ∀ {R : Type u_1} {M : Type u_8} {N : Type u_9} {O : Type u_10} [inst : CommSemiring R] [inst_1 : Monoid M]
  [inst_2 : Monoid N] [inst_3 : Monoid O] (f : N →* O) (g : M →* N) (x : MonoidAlgebra R M),
  (MonoidAlgebra.mapDomainBialgHom R f) ((MonoidAlgebra.mapDomainBialgHom R g) x) =
    (MonoidAlgebra.mapDomainBialgHom R (f.comp g)) x
-- Mathlib.Order.Filter.Cocardinal
Filter.mem_cocountable : ∀ {α : Type u} {s : Set α}, s ∈ Filter.cocountable ↔ sᶜ.Countable
-- Init.Data.List.MinMax
List.min?_eq_head? : ∀ {α : Type u} [inst : Min α] {l : List α}, List.Pairwise (fun a b => a ⊓ b = a) l → l.min? = l.head?
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft_map_app_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y)
  (H : CategoryTheory.Functor D E) (c : C),
  (((CategoryTheory.Functor.whiskeringLeft C D E).map τ).app H).app c = H.map (τ.app c)
-- Mathlib.Topology.Connected.Basic
isConnected_iff_connectedSpace : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsConnected s ↔ ConnectedSpace ↑s
-- Aesop.Util.Tactic.Ext
Aesop.ExtResult : Type
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The inclusion into the first summand of a binary biproduct.  -/
CategoryTheory.Limits.biprod.inl : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → X ⟶ X ⊞ Y
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastExtractAndExtend : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (assign : α → Bool) (aig : Std.Sat.AIG α) (w : ℕ)
  (xc : aig.RefVec w) (x : BitVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := xc.get idx hidx }⟧ = x.getLsbD idx) →
    ∀ (idx : ℕ) (hidx : idx < w * w),
      ⟦assign,
          { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend aig { w := w, x := xc, h := ⋯ }).aig,
            ref :=
              (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend aig { w := w, x := xc, h := ⋯ }).vec.get idx
                hidx }⟧ =
        (BitVec.extractAndExtend w x).getLsbD idx
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Protoset.coe_inj : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps₁ ps₂ : DiscreteTiling.Protoset G X ιₚ}, ↑ps₁ = ↑ps₂ ↔ ps₁ = ps₂
-- Mathlib.Order.Interval.Set.Image
StrictMono.image_Ioo_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  StrictMono f → f '' Set.Ioo a b ⊆ Set.Ioo (f a) (f b)
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.isCoveringMap : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_3)
  [inst_2 : AddGroup G] [inst_3 : AddAction G E], IsAddQuotientCoveringMap f G → IsCoveringMap f
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.isHermitian : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {M : Matrix n n R},
  M.PosDef → M.IsHermitian
-- Batteries.Data.List.Lemmas
List.nil_union : ∀ {α : Type u_1} [inst : BEq α] (l : List α), [] ∪ l = l
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.inv : ∀ {α : Type u_1} {M : Type u_3} [inst : DivisionMonoid M] {f : α → M},
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport f⁻¹
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_of_isZero_H : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r : ℤ) (hr : r₀ ≤ r) (pq : κ) (n : ℤ),
  n = data.deg pq →
    ∀ (i₁ i₂ : ι) (h₁ : i₁ = data.i₁ pq) (h₂ : i₂ = data.i₂ pq),
      CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))) →
        CategoryTheory.Limits.IsZero (((X.spectralSequence data).page r ⋯).X pq)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.mk.inj : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} {inst : L.Structure M} {inst_1 : L.Structure N} {toFun : M → N}
  {map_fun' :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (toFun ∘ x))
      FirstOrder.Language.Hom.map_fun'._autoParam}
  {map_rel' :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (toFun ∘ x))
      FirstOrder.Language.Hom.map_rel'._autoParam}
  {toFun_1 : M → N}
  {map_fun'_1 :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toFun_1 (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (toFun_1 ∘ x))
      FirstOrder.Language.Hom.map_fun'._autoParam}
  {map_rel'_1 :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (toFun_1 ∘ x))
      FirstOrder.Language.Hom.map_rel'._autoParam},
  { toFun := toFun, map_fun' := map_fun', map_rel' := map_rel' } =
      { toFun := toFun_1, map_fun' := map_fun'_1, map_rel' := map_rel'_1 } →
    toFun = toFun_1