mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The fourth cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 1)},
  j.castSucc < i →
    CategoryTheory.CategoryStruct.comp (X.δ i.succ) (X.σ j.castSucc) =
      CategoryTheory.CategoryStruct.comp (X.σ j) (X.δ i)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_insertIfNew_le_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {k : α} {v : β}, (cmp (t.insertIfNew k v).minKey! t.minKey!).isLE = true
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.DecompositionResult.failed.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.DecompositionResult.failed = 1
-- Std.Do.PostCond
/-- A postcondition expressing partial correctness.
That is, it expresses that *if* the asserted computation finishes without throwing an exception
*then* the result satisfies the given predicate `p`.
Nothing is asserted when the computation throws an exception.
 -/
Std.Do.«term_⇓?_=>_» : Lean.ParserDescr
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.drain_eq_forIn : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] {it : Std.IterM m β},
  it.drain = forIn it PUnit.unit fun x x_1 => pure (ForInStep.yield PUnit.unit)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.ofRepr.inj : ∀ {ι : Type u_1} {G : Type u_2} {inst : Group G} {repr repr_1 : G ≃* FreeGroup ι},
  { repr := repr } = { repr := repr_1 } → repr = repr_1
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.setInterior.eq_1 : ∀ {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] (I : Set k) {n : ℕ} (s : Affine.Simplex k P n),
  Affine.Simplex.setInterior I s =
    {p | ∃ w, ∑ i, w i = 1 ∧ (∀ (i : Fin (n + 1)), w i ∈ I) ∧ (Finset.affineCombination k Finset.univ s.points) w = p}
-- Init.Data.BitVec.Lemmas
BitVec.sdiv.eq_1 : ∀ {n : ℕ} (x y : BitVec n),
  x.sdiv y =
    match x.msb, y.msb with
    | false, false => x.udiv y
    | false, true => (x.udiv y.neg).neg
    | true, false => (x.neg.udiv y).neg
    | true, true => x.neg.udiv y.neg
-- Std.Http.Server.Connection
/-- A single HTTP connection.
 -/
Std.Http.Server.Connection : Type → Type
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The map of quotients by multiples of an integer induced by an additive group
homomorphism.  -/
QuotientAddGroup.homQuotientZSMulOfHom : {A B : Type u} →
  [inst : AddCommGroup A] →
    [inst_1 : AddCommGroup B] → (A →+ B) → (n : ℤ) → A ⧸ (zsmulAddGroupHom n).range →+ B ⧸ (zsmulAddGroupHom n).range
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.smul_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜},
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : β), MeasureTheory.AEStronglyMeasurable (fun x => f x • c) μ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.norm_cnstr_cert : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Bool
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.instIdentities : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.identities C).ContainsIdentities
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderivWithin.snd : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 f₂ s x →
      fderivWithin 𝕜 (fun x => (f₂ x).2) s x = ContinuousLinearMap.snd 𝕜 F G ∘SL fderivWithin 𝕜 f₂ s x
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.csin : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ}, Measurable f → Measurable fun x => Complex.sin (f x)
-- Mathlib.Data.Part
Part.induction_on : ∀ {α : Type u_1} {P : Part α → Prop} (a : Part α), P Part.none → (∀ (a : α), P (Part.some a)) → P a
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.isVertexCover_empty : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsVertexCover ∅ ↔ G = ⊥
-- Mathlib.Algebra.Group.Units.Hom
MonoidHom.isLocalHom_of_comp : ∀ {R : Type u_2} {S : Type u_3} {T : Type u_4} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Monoid T] (f : R →* S)
  (g : S →* T) [IsLocalHom (g.comp f)], IsLocalHom f
-- Mathlib.Algebra.Lie.Basic
LieRingModule.mk : {L : Type v} →
  {M : Type w} →
    [inst : LieRing L] →
      [inst_1 : AddCommGroup M] →
        [toBracket : Bracket L M] →
          (∀ (x y : L) (m : M), ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆) →
            (∀ (x : L) (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) →
              (∀ (x y : L) (m : M), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆) → LieRingModule L M
-- Mathlib.Algebra.Group.Conj
conj_pow : ∀ {α : Type u} [inst : Group α] {i : ℕ} {a b : α}, (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
-- Mathlib.Topology.Sheaves.LocallySurjective
/-- An equivalent condition for a map of presheaves to be locally surjective
is for all the induced maps on stalks to be surjective.  -/
TopCat.Presheaf.locally_surjective_iff_surjective_on_stalks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X : TopCat}
  {ℱ 𝒢 : TopCat.Presheaf C X} [inst_3 : CategoryTheory.Limits.HasColimits C]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (T : ℱ ⟶ 𝒢),
  TopCat.Presheaf.IsLocallySurjective T ↔
    ∀ (x : ↑X), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map T))
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : J) {Z : Cᵒᵖ}
  (h : Opposite.op (F.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j).op h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.op (Opposite.op j)) h
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.coe_injective : ∀ (K : Type u_1) [inst : Field K], Function.Injective fun x => (algebraMap (NumberField.RingOfIntegers K) K) ↑x
-- Mathlib.Order.Filter.Lift
Filter.map_lift_eq2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Filter γ} {m : α → β},
  Monotone g → (Filter.map m f).lift g = f.lift (g ∘ Set.image m)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.insert.go.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.lt),
  (match Ordering.eq with
    | Ordering.eq => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.lt => h_3 ()) =
    h_1 ()
-- Mathlib.Order.Filter.Pointwise
Filter.neg_pure : ∀ {α : Type u_2} [inst : Neg α] {a : α}, -pure a = pure (-a)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_natCast : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (↑n).natDegree = 0
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.greatestFib_ne_zero : ∀ {n : ℕ}, n.greatestFib ≠ 0 ↔ n ≠ 0
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.δ_comp_σ_of_gt : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  j.castSucc < i →
    CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i.succ) (SimplexCategoryGenRel.σ j.castSucc) =
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ j) (SimplexCategoryGenRel.δ i)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.div_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H] (f g : X ⟶ G) (h : G ⟶ H)
  [CategoryTheory.IsMonHom h] {Z : C} (h_1 : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f / g) (CategoryTheory.CategoryStruct.comp h h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h / CategoryTheory.CategoryStruct.comp g h)
      h_1
-- Mathlib.Util.MemoFix
_private.Mathlib.Util.MemoFix.0.memoFixImpl.fix : {α β : Type} → ((α → β) → α → β) → IO.Ref (Lean.PtrMap α β) → α → β
-- Mathlib.Data.Finsupp.Weight
Finsupp.degree_single : ∀ {σ : Type u_1} {R : Type u_4} [inst : AddCommMonoid R] (a : σ) (r : R), (Finsupp.degree fun₀ | a => r) = r
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_eq_get!_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)}, Std.Internal.List.minKey! l = (Std.Internal.List.minKey? l).get!
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_nat_iff_continuousOn_differentiableOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : ℕ},
  UniqueDiffOn 𝕜 s →
    (ContDiffOn 𝕜 (↑n) f s ↔
      (∀ m ≤ n, ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧
        ∀ m < n, DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.coindep_contract_iff : ∀ {α : Type u_1} {M : Matroid α} {X C : Set α}, (M.contract C).Coindep X ↔ M.Coindep X ∧ Disjoint X C
-- Batteries.Data.List.Lemmas
List.map_get_finRange : ∀ {α : Type u_1} (l : List α), List.map l.get (List.finRange l.length) = l
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.sieve₁_trivial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S W : C} {p : W ⟶ S},
  (CategoryTheory.PreOneHypercover.trivial S).sieve₁ p p = ⊤
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.isOpenMap_smul : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] {c : M}, IsUnit c → IsOpenMap fun x => c • x
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.mem_compl : ∀ {α : Type u_1} {s : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α] {a : α}, a ∈ sᶜ ↔ a ∉ s
-- Mathlib.Order.Interval.Set.Fin
Fin.range_rev : ∀ {n : ℕ}, Set.range Fin.rev = Set.univ
-- Mathlib.Topology.Algebra.ConstMulAction
ProperlyDiscontinuousSMul.finite_stabilizer' : ∀ (Γ : Type u_4) {T : Type u_5} [inst : TopologicalSpace T] [inst_1 : SMul Γ T] [ProperlyDiscontinuousSMul Γ T] (x : T),
  {γ | γ • x = x}.Finite
-- Mathlib.LinearAlgebra.TensorProduct.Basis
/-- If `{𝒞ᵢ}` is a basis for the module `N`, then every elements of `x ∈ M ⊗ N` can be uniquely written
as `∑ᵢ mᵢ ⊗ 𝒞ᵢ` for some `mᵢ ∈ M`.
 -/
TensorProduct.equivFinsuppOfBasisRight : {R : Type u_1} →
  {M : Type u_3} →
    {N : Type u_4} →
      {κ : Type u_6} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] → [DecidableEq κ] → Module.Basis κ R N → TensorProduct R M N ≃ₗ[R] κ →₀ M
-- Mathlib.Order.ModularLattice
inf_covBy_of_covBy_sup_of_covBy_sup_right : ∀ {α : Type u_1} [inst : Lattice α] [IsWeakLowerModularLattice α] {a b : α}, a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
mk_eq_mk_of_basis' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [InvariantBasisNumber R] {ι' : Type w} (v : Module.Basis ι R M) (v' : Module.Basis ι' R M),
  Cardinal.mk ι = Cardinal.mk ι'
-- Batteries.Data.Fin.Fold
Fin.foldr_eq_foldr_finRange : ∀ {n : ℕ} {α : Type u_1} (f : Fin n → α → α) (x : α), Fin.foldr n f x = List.foldr f x (List.finRange n)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
Pi.abs_apply : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → AddGroup (α i)] (f : (i : ι) → α i)
  [inst_1 : (i : ι) → Lattice (α i)] (i : ι), |f| i = |f i|
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → (Std.ExtDHashMap.ofList l).get? k' = some (cast ⋯ v)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsNegInvariant.neg_eq_self : ∀ {G : Type u_1} {inst : MeasurableSpace G} {inst_1 : Neg G} {μ : MeasureTheory.Measure G} [self : μ.IsNegInvariant],
  μ.neg = μ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.monMonoidal.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.AddMon.monMonoidal =
    { toMonoidalCategoryStruct := CategoryTheory.AddMon.monMonoidalStruct, tensorHom_def := ⋯, id_tensorHom_id := ⋯,
      tensorHom_comp_tensorHom := ⋯, whiskerLeft_id := ⋯, id_whiskerRight := ⋯, associator_naturality := ⋯,
      leftUnitor_naturality := ⋯, rightUnitor_naturality := ⋯, pentagon := ⋯, triangle := ⋯ }
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.coe_nnqsmul : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (q : ℚ≥0)
  (a : { x // 0 ≤ x }), ↑(q • a) = q • ↑a
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.instPseudoEMetricSpace : {ι : Type u_2} →
  {X : Type u_3} →
    {Y : ι → Type u_4} →
      {f : (i : ι) → X → Y i} →
        [Encodable ι] → [(i : ι) → PseudoEMetricSpace (Y i)] → PseudoEMetricSpace (Metric.PiNatEmbed X Y f)
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.instIsConnectedOfIsPretransitiveOfNonempty : ∀ {M : Type u_1} [inst : Monoid M] {X : Type u} [inst_1 : MulAction M X] [MulAction.IsPretransitive M X] [Nonempty X],
  CategoryTheory.IsConnected (CategoryTheory.ActionCategory M X)
-- Mathlib.Data.Fin.Fin2
Fin2.rev_last : ∀ {n : ℕ}, Fin2.last.rev = Fin2.fz
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.linear_eq_linear_isometry : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂),
  e.linear = e.linearIsometryEquiv.toLinearEquiv
-- Lean.Elab.PreDefinition.Structural.BRecOn
/-- Completes the `.brecOn` for the given function.
The `value` is the function with (only) the fixed parameters moved into the context.
 -/
Lean.Elab.Structural.mkBRecOnApp : Lean.Elab.Structural.Positions →
  ℕ →
    (ℕ → Lean.Expr) →
      Array Lean.Expr → Array Lean.Expr → Lean.Elab.Structural.RecArgInfo → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Fin.Basic
Fin.Internal.ofNat_eq_ofNat : ∀ {n : ℕ} {hn : 0 < n} {a : ℕ}, Fin.Internal.ofNat n hn a = Fin.ofNat n a
-- Mathlib.Topology.Sheaves.CommRingCat
/-- The localization of a presheaf of `CommRing`s with respect to a `SubmonoidPresheaf`.  -/
TopCat.Presheaf.SubmonoidPresheaf.localizationPresheaf : {X : TopCat} → {F : TopCat.Presheaf CommRingCat X} → F.SubmonoidPresheaf → TopCat.Presheaf CommRingCat X
-- Mathlib.Data.List.Map2
List.zipWith_nil : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : List α), List.zipWith f l [] = []
-- Mathlib.Order.Monotone.MonovaryOrder
antivaryOn_iff_exists_antitoneOn_monotoneOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f g s ↔ ∃ x, AntitoneOn f s ∧ MonotoneOn g s
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_eq_of_add_equiv_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : PadicSeq p}, f + g ≈ 0 → f.norm = g.norm
-- Mathlib.Analysis.Complex.Periodic
/-- The function `q ↦ f (invQParam h q)`, extended by a non-canonical choice of limit at 0.  -/
Function.Periodic.cuspFunction : ℝ → (ℂ → ℂ) → ℂ → ℂ
-- Mathlib.Data.ENNReal.Operations
ENNReal.biSup_add_biSup_le : ∀ {ι : Type u_3} {κ : Type u_4} {s : Set ι} {t : Set κ},
  s.Nonempty →
    t.Nonempty →
      ∀ {f : ι → ENNReal} {g : κ → ENNReal} {a : ENNReal},
        (∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a) → (⨆ i ∈ s, f i) + ⨆ j ∈ t, g j ≤ a
-- Mathlib.Algebra.Homology.Localization
instQFactorsThroughHomotopyDown : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : AddRightCancelSemigroup ι] [inst_3 : One ι] [CategoryTheory.Limits.HasBinaryBiproducts C]
  [inst_5 : CategoryTheory.CategoryWithHomology C], (ComplexShape.down ι).QFactorsThroughHomotopy C
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
/-- Relation on the tensor algebra which will yield the symmetric algebra when
quotiented out by.  -/
TensorAlgebra.SymRel : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → TensorAlgebra R M → TensorAlgebra R M → Prop
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instReprPoly.repr : Lean.Grind.Linarith.Poly → ℕ → Std.Format
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.norm_condExpL2_le_one : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0), ‖MeasureTheory.condExpL2 E 𝕜 hm‖ ≤ 1
-- Init.Data.List.Perm
List.Perm.eq_nil : ∀ {α : Type u_1} {l : List α}, l.Perm [] → l = []
-- Mathlib.Topology.DiscreteQuotient
/-- Given `f : C(X, Y)`, `DiscreteQuotient.LEComap f A B` is defined as
`A ≤ B.comap f`. Mathematically this means that `f` descends to a morphism `A → B`.  -/
DiscreteQuotient.LEComap : {X : Type u_2} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → C(X, Y) → DiscreteQuotient X → DiscreteQuotient Y → Prop
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.isLittleO_exp_comp_exp_comp : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℝ},
  ((fun x => Real.exp (f x)) =o[l] fun x => Real.exp (g x)) ↔ Filter.Tendsto (fun x => g x - f x) l Filter.atTop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given

X₁ - f₁ -> X₂ - f₂ -> X₃
|          |          |
i₁         i₂         i₃
∨          ∨          ∨
Y₁ - g₁ -> Y₂ - g₂ -> Y₃

Then the right square is a pushout if the left square and the big square are.
 -/
CategoryTheory.Limits.rightSquareIsPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ : C} →
      {f₁ : X₁ ⟶ X₂} →
        {f₂ : X₂ ⟶ X₃} →
          {i₁ : X₁ ⟶ Y₁} →
            {t₁ : CategoryTheory.Limits.PushoutCocone i₁ f₁} →
              {i₂ : X₂ ⟶ t₁.pt} →
                (t₂ : CategoryTheory.Limits.PushoutCocone i₂ f₂) →
                  (hi₂ : i₂ = t₁.inr) →
                    CategoryTheory.Limits.IsColimit t₁ →
                      CategoryTheory.Limits.IsColimit (t₁.pasteHoriz t₂ hi₂) → CategoryTheory.Limits.IsColimit t₂
-- Batteries.Data.Stream
Std.Stream.fst_takeTR_loop : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (acc : List α) (n : ℕ),
  (Std.Stream.takeTR.loop s acc n).1 = acc.reverseAux (Std.Stream.take s n).1
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.eq_1 : ∀ {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.PosSemidef = (M.IsHermitian ∧ ∀ (x : n →₀ R), 0 ≤ x.sum fun i xi => x.sum fun j xj => star xi * M i j * xj)
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.repr_self : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι),
  b.repr (b i) = EuclideanSpace.single i 1
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.instNeg : Neg Lean.Omega.LinearCombo
-- Mathlib.Data.Multiset.Sort
Multiset.pairwise_sort : ∀ {α : Type u_1} (s : Multiset α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], List.Pairwise r (s.sort r)
-- Mathlib.Algebra.Module.LocalizedModule.Away
IsLocalizedModule.Away.mk_of_addCommGroup : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] {f : M →ₗ[R] N} {r : R},
  IsUnit ((algebraMap R (Module.End R N)) r) →
    (∀ (x : N), ∃ n y, r ^ n • x = f y) → (∀ (x : M), f x = 0 → ∃ n, r ^ n • x = 0) → IsLocalizedModule.Away r f
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : InfSet α] → [inst_1 : InfSet β] → FunLike (sInfHom α β) α β
-- Lean.Server.References
/-- All references of this module.  -/
Lean.Server.Ilean.references : Lean.Server.Ilean → Lean.Lsp.ModuleRefs
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.diam_ne_zero_of_ediam_ne_top : ∀ {α : Type u_1} {G : SimpleGraph α} [Nontrivial α], G.ediam ≠ ⊤ → G.diam ≠ 0
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.image : ∀ {R : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y] {f : X → Y}
  {x : X} {s : Set X},
  Convexity.IsAffineMap R f → Convexity.IsStarConvexSet R x s → Convexity.IsStarConvexSet R (f x) (f '' s)
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.mk.inj : ∀ {levelParams : List Lean.Name} {largeElim : Bool} {params motives : Array Lean.Expr} {motiveToIdx : Lean.FVarIdMap ℕ}
  {minors : Array Lean.Expr} {recNames belowNames brecOnNames : Array Lean.Name} {levelParams_1 : List Lean.Name}
  {largeElim_1 : Bool} {params_1 motives_1 : Array Lean.Expr} {motiveToIdx_1 : Lean.FVarIdMap ℕ}
  {minors_1 : Array Lean.Expr} {recNames_1 belowNames_1 brecOnNames_1 : Array Lean.Name},
  { levelParams := levelParams, largeElim := largeElim, params := params, motives := motives,
        motiveToIdx := motiveToIdx, minors := minors, recNames := recNames, belowNames := belowNames,
        brecOnNames := brecOnNames } =
      { levelParams := levelParams_1, largeElim := largeElim_1, params := params_1, motives := motives_1,
        motiveToIdx := motiveToIdx_1, minors := minors_1, recNames := recNames_1, belowNames := belowNames_1,
        brecOnNames := brecOnNames_1 } →
    levelParams = levelParams_1 ∧
      largeElim = largeElim_1 ∧
        params = params_1 ∧
          motives = motives_1 ∧
            motiveToIdx = motiveToIdx_1 ∧
              minors = minors_1 ∧ recNames = recNames_1 ∧ belowNames = belowNames_1 ∧ brecOnNames = brecOnNames_1