mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Presieve.CoverByImageStructure.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {V U : D} {f : V ⟶ U} (obj : C)
  (lift : V ⟶ G.obj obj) (map : G.obj obj ⟶ U)
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp lift map = f)
      CategoryTheory.Presieve.CoverByImageStructure.fac._autoParam)
  (obj_1 : C) (lift_1 : V ⟶ G.obj obj_1) (map_1 : G.obj obj_1 ⟶ U)
  (fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp lift_1 map_1 = f)
      CategoryTheory.Presieve.CoverByImageStructure.fac._autoParam),
  ({ obj := obj, lift := lift, map := map, fac := fac } =
      { obj := obj_1, lift := lift_1, map := map_1, fac := fac_1 }) =
    (obj = obj_1 ∧ lift ≍ lift_1 ∧ map ≍ map_1)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.toList_roiIter : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β}
  {t_ord : t.Ordered} {lowerBound : α},
  (Std.DTreeMap.Internal.roiIterator t lowerBound).toList =
    List.filter (fun e => (compare e.fst lowerBound).isGT) t.toList
-- Init.Data.List.Lemmas
List.flatMap_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : α → List β} {g : β → List γ},
  List.flatMap g (List.flatMap f l) = List.flatMap (fun x => List.flatMap g (f x)) l
-- Init.Data.List.Nat.TakeDrop
List.drop_eq_drop_iff : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, List.drop i l = List.drop j l ↔ min i l.length = min j l.length
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.set_EStateM : ∀ {ε σ : Type} {s : σ}
  {Q : Std.Do.PostCond PUnit.{1} (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))},
  ⦃fun x => Q.1 () s⦄ set s ⦃Q⦄
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.center_eq_top : ∀ (R : Type u_1) [inst : NonUnitalCommSemiring R], NonUnitalSubsemiring.center R = ⊤
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- The identity adjunction is triangulated.
 -/
CategoryTheory.Adjunction.IsTriangulated.id : ∀ {C : Type u_1} [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],
  CategoryTheory.Adjunction.id.IsTriangulated
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- `X` is rational over `S` (or `S`-rational) if it is birational over `S` to some
affine space `𝔸(n; S)`. Note that we do not require `n` to be finite here.  -/
AlgebraicGeometry.Scheme.IsRationalOver : {S X : AlgebraicGeometry.Scheme} → (X ⟶ S) → Prop
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx!_eq_get!_entryAtIdx? : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {i : ℕ} [inst : Inhabited ((a : α) × β a)],
  t.entryAtIdx! i = (t.entryAtIdx? i).get!
-- Init.System.IO
instMonadExceptOfEIO : {ε : Type} → MonadExceptOf ε (EIO ε)
-- Mathlib.Order.Fin.Clamp
Fin.clamp_eq_last : ∀ (n m : ℕ), m ≤ n → Fin.clamp n m = Fin.last m
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime : ∀ {R : Type u} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M →ₗ[R] M)
  {p q : Polynomial R},
  IsCoprime p q → ((Polynomial.aeval f) p).ker ⊔ ((Polynomial.aeval f) q).ker = ((Polynomial.aeval f) (p * q)).ker
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_X : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.leadingCoeff = 1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α}
  {h_contains : (m₁.inter m₂).contains k = true}, (m₁.inter m₂).getKey k h_contains = m₁.getKey k ⋯
-- Mathlib.Algebra.Homology.Refinements
HomologicalComplex.comp_homologyπ_eq_zero_iff_up_to_refinements : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι),
  c.prev j = i →
    ∀ {A : C} (z₂ : A ⟶ K.cycles j),
      CategoryTheory.CategoryStruct.comp z₂ (K.homologyπ j) = 0 ↔
        ∃ A' π,
          ∃ (_ : CategoryTheory.Epi π),
            ∃ x₁, CategoryTheory.CategoryStruct.comp π z₂ = CategoryTheory.CategoryStruct.comp x₁ (K.toCycles i j)
-- Init.Data.SInt.Lemmas
Int16.ofIntClamp.eq_1 : ∀ (i : ℤ),
  Int16.ofIntClamp i =
    if hl : Int16.minValue.toInt ≤ i then
      if hr : i ≤ Int16.maxValue.toInt then Int16.ofIntLE i hl hr else Int16.maxValue
    else Int16.minValue
-- Init.Prelude
/-- Appends two lists. Normally used via the `++` operator.

Appending lists takes time proportional to the length of the first list: `O(|xs|)`.

Examples:
* `[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]`.
* `[] ++ [4, 5] = [4, 5]`.
* `[1, 2, 3] ++ [] = [1, 2, 3]`.
 -/
List.append : {α : Type u_1} → List α → List α → List α
-- Mathlib.Topology.Sets.OpenCover
TopologicalSpace.IsOpenCover.iUnion_inter : ∀ {ι : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {u : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover u → ∀ (s : Set X), ⋃ i, s ∩ ↑(u i) = s
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with shifting the function by a constant on the left.  -/
iteratedFDerivWithin_comp_add_left : ∀ {𝕜 : 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 : ℕ) (a x : E),
  iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
-- Mathlib.Algebra.Homology.EulerCharacteristic
ComplexShape.eulerCharSignsUpNat_χ : ∀ (n : ℕ), ComplexShape.EulerCharSigns.χ (ComplexShape.up ℕ) n = (-1) ^ n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_eq_getD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} {fallback : β a} {h : a ∈ t}, t.get a h = t.getD a fallback
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.mk : {G : Type u} →
  [inst : Group G] →
    (toFilterBasis : FilterBasis G) →
      (∀ {U : Set G}, U ∈ toFilterBasis.sets → 1 ∈ U) →
        (∀ {U : Set G}, U ∈ toFilterBasis.sets → ∃ V ∈ toFilterBasis.sets, V * V ⊆ U) →
          (∀ {U : Set G}, U ∈ toFilterBasis.sets → ∃ V ∈ toFilterBasis.sets, V ⊆ (fun x => x⁻¹) ⁻¹' U) →
            (∀ (x₀ : G) {U : Set G},
                U ∈ toFilterBasis.sets → ∃ V ∈ toFilterBasis.sets, V ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' U) →
              GroupFilterBasis G
-- Lean.Elab.App
/-- Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`,
and then execute the main loop.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.addEtaArg : Lean.Name → Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Std.Time.Date.PlainDate
/-- Subtracts a given number of days from a `PlainDate`.
 -/
Std.Time.PlainDate.subDays : Std.Time.PlainDate → Std.Time.Day.Offset → Std.Time.PlainDate
-- Mathlib.CategoryTheory.Category.Pointed
typeToPointed_obj_X : ∀ (X : Type u), (typeToPointed.obj X).X = Option X
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.neg_mem : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A : Matrix (l ⊕ l) (l ⊕ l) R}, A ∈ Matrix.symplecticGroup l R → -A ∈ Matrix.symplecticGroup l R
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Path.right.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (parent : RBTree.RBNode.Path α),
  sizeOf (RBTree.RBNode.Path.right c l v parent) = 1 + sizeOf c + sizeOf l + sizeOf v + sizeOf parent
-- Mathlib.Topology.Algebra.Monoid
AddSubsemigroup.separatelyContinuousAdd : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [SeparatelyContinuousAdd M]
  (S : AddSubsemigroup M), SeparatelyContinuousAdd ↥S
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.WithGeneratedByTopology.continuous_equiv`. -/
DeltaGeneratedSpace.continuous_counit : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y],
  Continuous ⇑Topology.WithGeneratedByTopology.equiv
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.matrix_top : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocRing R] [inst_1 : Fintype n], TwoSidedIdeal.matrix n ⊤ = ⊤
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ),
  (DerivedCategory.homologyFunctorFactorsh C n).hom.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) =
    CategoryTheory.CategoryStruct.comp
      ((DerivedCategory.homologyFunctor C n).map ((DerivedCategory.quotientCompQhIso C).hom.app K))
      (CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n).hom.app K)
        ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n).inv.app K))
-- Mathlib.Util.Export
Lean.Export.instOfStateExpr : Lean.Export.OfState Lean.Expr
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.coe_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : Mul M]
  [inst_3 : IsScalarTower R M M] (p q : SubMulAction R M), ↑(p * q) = ↑p * ↑q
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- If either the lhs or rhs is not a composition, compose it on the right with an identity.  -/
Mathlib.Tactic.Coherence.insertTrailingIds : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.has_add : ∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment) (b : Bool),
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b
      (Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment b assignment) =
    true
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedAddMonoid.add_le_add_left : ∀ {α : Type u_2} {inst : AddCommMonoid α} {inst_1 : Preorder α} [self : IsOrderedAddMonoid α] (a b : α),
  a ≤ b → ∀ (c : α), a + c ≤ b + c
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The setoid corresponding to commutative expressions modulo monoid Relations and identifications.
 -/
RingCat.Colimits.colimitSetoid : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → Setoid (RingCat.Colimits.Prequotient F)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The unit morphism of a monoid object.  -/
CategoryTheory.MonObj.«termη[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.inv.injEq : ∀ {R : Type u} (a a_1 : Rack.PreEnvelGroup R), (a.inv = a_1.inv) = (a = a_1)
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkInductiveAux₃ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 ⟶ Q.X 2)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X (n + 1)) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2)))
  (i j : ℕ) (h : i + 1 = j),
  CategoryTheory.CategoryStruct.comp (Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst
      (HomologicalComplex.xPrevIso Q h).hom =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P h).inv
      (Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_sub : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (f g : ρ.IntertwiningMap σ), Rep.ofHom (f - g) = Rep.ofHom f - Rep.ofHom g
-- Mathlib.Order.IsNormal
Order.IsNormal.dirSupClosed_range : ∀ {α : Type u_1} [inst : LinearOrder α] [WellFoundedLT α] {f : α → α}, Order.IsNormal f → DirSupClosed (Set.range f)
-- Lean.Environment
_private.Lean.Environment.0.Lean.saveModuleData.unsafe_1 : System.FilePath → Lean.Name → Lean.ModuleData → IO Lean.Compactor
-- Mathlib.Algebra.GroupWithZero.Action.Defs
SMulZeroClass.toZeroHom_apply : ∀ {M : Type u_1} (A : Type u_7) [inst : Zero A] [inst_1 : SMulZeroClass M A] (x : M) (x_1 : A),
  (SMulZeroClass.toZeroHom A x) x_1 = x • x_1
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_ric_eq_mkSlice_rcc : ∀ {α : Type u_1} {xs : Subarray α} {hi : ℕ},
  (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rcc.Sliceable.mkSlice xs 0...=hi
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instSMulCommClass : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M]
  [inst_2 : Mul M] [inst_3 : MulMemClass S M] [SMulCommClass R M M] (s : S), SMulCommClass R ↥s ↥s
-- Init.Data.String.PosRaw
String.Pos.Raw.mk_lt_mk : ∀ {i₁ i₂ : ℕ}, { byteIdx := i₁ } < { byteIdx := i₂ } ↔ i₁ < i₂
-- Init.Omega.Constraint
Lean.Omega.Constraint.add.eq_1 : ∀ (x y : Lean.Omega.Constraint),
  x.add y =
    { lowerBound := Option.bind x.lowerBound fun a => Option.map (fun b => a + b) y.lowerBound,
      upperBound := Option.bind x.upperBound fun a => Option.map (fun b => a + b) y.upperBound }
-- Init.Data.UInt.Lemmas
instAssociativeUSizeHAdd : Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.Data.Nat.Prime.Basic
Nat.eq_or_coprime_of_le_prime : ∀ {n p : ℕ}, n ≠ 0 → n ≤ p → Nat.Prime p → p = n ∨ p.Coprime n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.map_eq_empty_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ}, Std.ExtTreeMap.map f t = ∅ ↔ t = ∅
-- Mathlib.Data.Fin.Tuple.Sort
/-- If two permutations of a tuple `f` are both monotone, then they are equal.  -/
Tuple.unique_monotone : ∀ {n : ℕ} {α : Type u_1} [inst : PartialOrder α] {f : Fin n → α} {σ τ : Equiv.Perm (Fin n)},
  Monotone (f ∘ ⇑σ) → Monotone (f ∘ ⇑τ) → f ∘ ⇑σ = f ∘ ⇑τ
-- Mathlib.NumberTheory.ADEInequality
/-- A multiset `pqr` of positive natural numbers is `Admissible`
if it is equal to `A' q r`, or `D' r`, or one of `E6`, `E7`, or `E8`.  -/
ADEInequality.Admissible : Multiset ℕ+ → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_pi_sub : ∀ (x : ℂ), Complex.sin (↑Real.pi - x) = Complex.sin x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.neg_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) (X : Cᵒᵖ), (-f).app X = -f.app X
-- Init.Data.Rat.Basic
instDecidableEqRat : DecidableEq ℚ
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_inv_of_neg : ∀ {a b : ℝ}, a < 0 → b < 0 → ∫ (x : ℝ) in a..b, x⁻¹ = Real.log (b / a)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.distinct_keys_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) t.toList
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Fold a function across the structure of a tree.

```
fold z f {1, 2, 4} = f (f z 1 z) 2 (f z 4 z)
```

The exact structure of function applications depends on the tree and so
is unspecified.  -/
Ordnode.fold : {α : Type u_1} → {β : Sort u_2} → β → (β → α → β → β) → Ordnode α → β
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_of_not_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬a ≤ b → Set.uIoo a b = Set.Ioo b a
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanQueryModuleResponse.mk.inj : ∀ {queryResults queryResults_1 : Array Lean.Lsp.LeanQueriedModule},
  { queryResults := queryResults } = { queryResults := queryResults_1 } → queryResults = queryResults_1
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.ofLine : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X} {f : ℝ → X},
  ContinuousOn f unitInterval → f 0 = x → f 1 = y → f '' unitInterval ⊆ F → JoinedIn F x y
-- Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal
Submodule.orthogonalBilin_le : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring R₁] [inst_2 : CommSemiring R₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R₁ M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂]
  {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} {S T : Submodule R₁ M₁},
  S ≤ T → Submodule.orthogonalBilin B T ≤ Submodule.orthogonalBilin B S
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- Given a presheaf of modules `M`, this is the
canonical morphism `M.freeYonedaCoproduct ⟶ M`.  -/
PresheafOfModules.fromFreeYonedaCoproduct : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → (M : PresheafOfModules R) → M.freeYonedaCoproduct ⟶ M
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getKeyDₘ : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → α → α
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.adjoin_simple_eq_top_iff_of_isAlgebraic : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  IsAlgebraic F x → (F⟮x⟯ = ⊤ ↔ F[x] = ⊤)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_le_of_le : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ},
  0 ≤ ArchimedeanClass.mk x → x ≤ f r → ArchimedeanClass.stdPart x ≤ r
-- Mathlib.FieldTheory.Isaacs
Field.nonempty_algHom_of_range_minpoly_subset : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] [alg : Algebra.IsAlgebraic F E],
  Set.range (minpoly F) ⊆ Set.range (minpoly F) → Nonempty (E →ₐ[F] K)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln_sound : ∀ {k : ℕ} {c : Nat.Partrec.Code} {n x : ℕ}, x ∈ Nat.Partrec.Code.evaln k c n → x ∈ c.eval n
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesLE_one : Nat.primesLE 1 = ∅
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.norm_setToFun_le_mul_norm' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (f : ↥(MeasureTheory.Lp E 1 μ)),
  ‖MeasureTheory.setToFun μ T hT ↑↑f‖ ≤ max C 0 * ‖f‖
-- Lean.Meta.Match.Basic
Lean.Meta.Match.AltLHS.patterns : Lean.Meta.Match.AltLHS → List Lean.Meta.Match.Pattern
-- Mathlib.Combinatorics.Graph.Basic
Graph.noEdge_isLink : ∀ {α : Type u_1} (vertexSet : Set α) (β : Type u_3) (e : β) (x y : α), (Graph.noEdge vertexSet β).IsLink e x y ↔ False
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_mem_map : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] {f : P →ₐ[R] P'},
  Function.Injective ⇑f → ∀ {x : P} {I : FractionalIdeal S P}, f x ∈ FractionalIdeal.map f I ↔ x ∈ I
-- Mathlib.Data.List.Dedup
List.dedup_eq_nil : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.dedup = [] ↔ l = []
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
_private.Mathlib.AlgebraicGeometry.Morphisms.Flat.0.AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq.match_1_6.eq_2 : ∀ {ι : Type u_1} (motive : CategoryTheory.Pairwise ι → Sort u_2) (i j : ι)
  (h_1 : (i : ι) → motive (CategoryTheory.Pairwise.single i))
  (h_2 : (i j : ι) → motive (CategoryTheory.Pairwise.pair i j)),
  (match CategoryTheory.Pairwise.pair i j with
    | CategoryTheory.Pairwise.single i => h_1 i
    | CategoryTheory.Pairwise.pair i j => h_2 i j) =
    h_2 i j
-- Mathlib.Order.RelSeries
RelSeries.insertNth_toFun : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin p.length) (a : α)
  (prev_connect : (p.toFun i.castSucc, a) ∈ r) (connect_next : (a, p.toFun i.succ) ∈ r) (j : Fin (p.length + 1 + 1)),
  (p.insertNth i a prev_connect connect_next).toFun j = i.succ.castSucc.insertNth a p.toFun j
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.ideal_le_vanishingIdeal_zeroLocus : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (I : Ideal A),
  I ≤ (ProjectiveSpectrum.vanishingIdeal (ProjectiveSpectrum.zeroLocus 𝒜 ↑I)).toIdeal
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.congr.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {c : AddCon M} {d : AddCon N} (e : M ≃+ N)
  (h : c = AddCon.comap ⇑e ⋯ d), AddCon.congr e h = { toEquiv := Quotient.congr ↑e ⋯, map_add' := ⋯ }
-- Mathlib.Data.Multiset.Replicate
Multiset.replicate_add : ∀ {α : Type u_1} (m n : ℕ) (a : α), Multiset.replicate (m + n) a = Multiset.replicate m a + Multiset.replicate n a
-- Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
CategoryTheory.MorphismProperty.hasCardinalLT_ofHoms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {X Y : ι → C} (f : (i : ι) → X i ⟶ Y i)
  {κ : Cardinal.{u_3}}, HasCardinalLT ι κ → (CategoryTheory.MorphismProperty.ofHoms f).HasCardinalLT κ
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- The uniform structure induced by a valuative relation. Note that this is not made into a
global instance to avoid diamonds. If desired, one can equip a ring with a uniform space
from a valuative relation by hand. But as long as they do so, the fact that the topology is
valuative and nonarchimedean, and the addition is uniformly continuous,
can be automatically inferred.  -/
ValuativeRel.uniformSpace : (R : Type u_1) → [inst : Ring R] → [ValuativeRel R] → UniformSpace R
-- Mathlib.Topology.UniformSpace.Compact
Disjoint.exists_uniform_thickening_of_basis : ∀ {α : Type ua} {ι : Sort u_1} [inst : UniformSpace α] {p : ι → Prop} {s : ι → Set (α × α)},
  (uniformity α).HasBasis p s →
    ∀ {A B : Set α},
      IsCompact A →
        IsClosed B →
          Disjoint A B → ∃ i, p i ∧ Disjoint (⋃ x ∈ A, UniformSpace.ball x (s i)) (⋃ x ∈ B, UniformSpace.ball x (s i))
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- If two words correspond to the same element in the additive free group, then they
have a common maximal reduction. This is the proof that the function that sends an element of the
free group to its maximal reduction is well-defined.  -/
FreeAddGroup.reduce.sound : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂ → FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂