mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
Summable.mul_right : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : TopologicalSpace α] [IsTopologicalSemiring α] {f : ι → α} (a : α),
  Summable f L → Summable (fun i => f i * a) L
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_one : ISize.toNatClampNeg 1 = 1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α], Finset.div = { div := Finset.image₂ fun x1 x2 => x1 / x2 }
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.of.sizeOf_spec : ∀ (α : Type u) [isCommRing : CommRing α] [isTopologicalSpace : TopologicalSpace α]
  [isTopologicalRing : IsTopologicalRing α],
  sizeOf (TopCommRingCat.of α) = 1 + sizeOf α + sizeOf isCommRing + sizeOf isTopologicalSpace + sizeOf isTopologicalRing
-- Mathlib.Tactic.Ring.Common
/-- The proof that `e` splits into the coefficient `k` and the monic monomial `e'`.  -/
Mathlib.Tactic.Ring.Common.ExtractCoeff.p : {e : Q(ℕ)} → (self : Mathlib.Tactic.Ring.Common.ExtractCoeff e) → Q(«$e» = unknown_1 * unknown_2)
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.addSuggestions : Lean.Syntax → Array Lean.Meta.Tactic.TryThis.Suggestion → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.image_vsub_product : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t : Finset β},
  Finset.image₂ (fun x1 x2 => x1 -ᵥ x2) s t = s -ᵥ t
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.toSubring_subtype_eq_subtype : ∀ (K : Type u) [inst : DivisionRing K] (S : Subfield K), S.subtype = S.subtype
-- Init.Data.UInt.Bitwise
UInt16.neg_one_xor : ∀ {a : UInt16}, -1 ^^^ a = ~~~a
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.const_one : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : One β], MeasureTheory.SimpleFunc.const α 1 = 1
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.hom_ext_iff : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} {f g : X ⟶ Y}, f = g ↔ f.hom = g.hom
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_floor_atBot : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [IsStrictOrderedRing α],
  Filter.Tendsto Int.floor Filter.atBot Filter.atBot
-- Init.Data.List.Lemmas
List.flatMap_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → List γ) (l : List α),
  List.flatMap g (List.map f l) = List.flatMap (fun a => g (f a)) l
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.forIn_map : ∀ {α : Type u₁} {n : Type u₁ → Type u_1} {β₂ γ : Type u₁} {m : Type u₁ → Type u_2} {β : Type u₁} {ps : Std.Do.PostShape}
  [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Std.Do.WPMonad n ps]
  [inst_5 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_7 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_9 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n] {it : Std.IterM m β} {f : β → β₂} {init : γ}
  {g : β₂ → γ → n (ForInStep γ)} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄ forIn it init fun out acc => g (f out) acc ⦃Q⦄ → ⦃P⦄ forIn (Std.IterM.map f it) init g ⦃Q⦄
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.mk : {V : Type u} → (V → V → Type v) → Quiver V
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.Valid.setCurr : ∀ {c : Char} {it : String.Legacy.Iterator}, it.Valid → (it.setCurr c).Valid
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getEntry!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) [inst_1 : Inhabited ((a : α) × β a)]
  (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getEntry! a x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => default
    | Std.DHashMap.Internal.AssocList.cons k v es =>
      if (k == a) = true then ⟨k, v⟩ else Std.DHashMap.Internal.AssocList.getEntry! a es
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.Candidate.mk.sizeOf_spec : ∀ (kind : Lean.Server.FileWorker.SignatureHelp.CandidateKind) (appStx : Lean.Syntax),
  sizeOf { kind := kind, appStx := appStx } = 1 + sizeOf kind + sizeOf appStx
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- Orbit-stabilizer theorem.  -/
AddAction.orbitProdStabilizerEquivAddGroup : (G : Type u) →
  {X : Type v} →
    [inst : AddGroup G] → [inst_1 : AddAction G X] → (b : X) → ↑(AddAction.orbit G b) × ↥(AddAction.stabilizer G b) ≃ G
-- Mathlib.Algebra.LinearRecurrence
LinearRecurrence.charPoly_degree_eq_order : ∀ {R : Type u_1} [inst : CommRing R] (E : LinearRecurrence R) [Nontrivial R], E.charPoly.degree = ↑E.order
-- Mathlib.Algebra.Group.Hom.Instances
instIsRightCancelMulOneHom : ∀ {M : Type uM} {N : Type uN} [inst : One M] [inst_1 : MulOneClass N] [IsRightCancelMul N],
  IsRightCancelMul (OneHom M N)
-- Mathlib.Data.Finset.NAry
/-- The other direction does not hold because of the `s`-`s` cross terms on the RHS.  -/
Finset.image₂_distrib_subset_left : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ' : Type u_6} {δ : Type u_7} {ε : Type u_9} [inst : DecidableEq β']
  [inst_1 : DecidableEq γ'] [inst_2 : DecidableEq ε] {s : Finset α} {t : Finset β} [inst_3 : DecidableEq δ]
  {γ : Type u_14} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ} {f₁ : α → β → β'} {f₂ : α → γ → γ'} {g' : β' → γ' → ε},
  (∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)) →
    Finset.image₂ f s (Finset.image₂ g t u) ⊆ Finset.image₂ g' (Finset.image₂ f₁ s t) (Finset.image₂ f₂ s u)
-- Mathlib.Algebra.Group.Units.Basic
mul_eq_one' : ∀ {α : Type u} [inst : CancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 ↔ a = 1 ∧ b = 1
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.toSet_iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} (W : ι → CategoryTheory.MorphismProperty C),
  (⨆ i, W i).toSet = ⋃ i, (W i).toSet
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_inter_setOfPred_isNonloop_eq : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.closure (X ∩ {e | M.IsNonloop e}) = M.closure X
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.mulUnop.eq_1 : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β], AddEquiv.mulUnop = AddEquiv.mulOp.symm
-- Init.SimpLemmas
or_iff_left_of_imp : ∀ {b a : Prop}, (b → a) → (a ∨ b ↔ a)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_sInf : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set (Submodule R M)), Submodule.span R ↑(sInf s) = sInf s
-- Mathlib.Algebra.DirectSum.Internal
/-- Build a `DirectSum.GAlgebra` instance for a collection of `Submodule`s.  -/
Submodule.galgebra : {ι : Type u_1} →
  {S : Type u_3} →
    {R : Type u_4} →
      [inst : AddMonoid ι] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Semiring R] →
            [inst_3 : Algebra S R] →
              (A : ι → Submodule S R) → [inst_4 : SetLike.GradedMonoid A] → DirectSum.GAlgebra S fun i => ↥(A i)
-- Mathlib.Data.List.TakeDrop
List.cons_getElem_drop_succ : ∀ {α : Type u} {l : List α} {n : ℕ} {h : n < l.length}, l[n] :: List.drop (n + 1) l = List.drop n l
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_zero : ∀ (p : Fin 0 → Type u) (τ : Type u), Function.FromTypes p τ = τ
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
ULift.nndist_up_up : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] (x y : β), nndist { down := x } { down := y } = nndist x y
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- All points lie in the circumsphere.  -/
Affine.Simplex.mem_circumsphere : ∀ {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) (i : Fin (n + 1)), s.points i ∈ s.circumsphere
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.coflat_of_preservesFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasFiniteColimits C] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesFiniteColimits F], CategoryTheory.RepresentablyCoflat F
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → (↑m).toList.isEmpty = (↑m).isEmpty
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.CofibrantObject.homMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] {X Y : C} [inst_3 : HomotopicalAlgebra.IsCofibrant X]
  [inst_4 : HomotopicalAlgebra.IsCofibrant Y]
  (f : HomotopicalAlgebra.CofibrantObject.mk X ⟶ HomotopicalAlgebra.CofibrantObject.mk Y),
  ∃ g, f = HomotopicalAlgebra.CofibrantObject.homMk g
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinitesimal.not_infinite : ∀ {x : ℝ*}, x.Infinitesimal → ¬x.Infinite
-- Mathlib.Order.Concept
Concept.strictMono_extent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, StrictMono Concept.extent
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The structural isomorphism between `𝟙_ C ⊙ₗ d` and `d`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso : {C : Type u_1} →
  {D : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
        {inst_2 : CategoryTheory.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D] →
            (d : D) →
              CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d ≅
                d
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_smul_sphere : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ), (fun x => c • x) ⁻¹' Metric.sphere x r = Metric.sphere (c⁻¹ • x) r
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological.R.add.injEq : ∀ {A : Type u} {M : Type v} (m₁ m₂ m₁_1 m₂_1 : M),
  (Module.Presentation.tautological.R.add m₁ m₂ = Module.Presentation.tautological.R.add m₁_1 m₂_1) =
    (m₁ = m₁_1 ∧ m₂ = m₂_1)
-- Mathlib.RingTheory.IsGaloisGroup.Basic
instIsGaloisGroupSubtypeMemSubringRangeAlgebraMap : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_3) [inst : Group G] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : MulSemiringAction G B] [inst_4 : Algebra A B] [IsGaloisGroup G A B],
  IsGaloisGroup G (↥(algebraMap A B).range) B
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.diam_eq_zero_iff_ediam_eq_top : ∀ {α : Type u_1} {G : SimpleGraph α} [Nontrivial α], G.diam = 0 ↔ G.ediam = ⊤
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The projection from the pullback to the second component.
 -/
CompHausLike.pullback.snd : {P : TopCat → Prop} →
  {X Y B : CompHausLike P} →
    (f : X ⟶ B) → (g : Y ⟶ B) → [inst : CompHausLike.HasExplicitPullback f g] → CompHausLike.pullback f g ⟶ Y
-- Init.Data.Float.Model.Float
Float.Model.instInhabited : Inhabited Float.Model
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.Anisotropic.eq_1 : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N),
  Q.Anisotropic = ∀ (x : M), Q x = 0 → x = 0
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.beq_self_eq_true : ∀ {w : ℕ} (a : BitVec w), (a == a) = true
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_map_of_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] {L : BooleanSubalgebra α}
  (f : BoundedLatticeHom α β) {a : α}, a ∈ L → f a ∈ BooleanSubalgebra.map f L
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_three : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  (CategoryTheory.ComposableArrows.fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 3 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂₃ f₄).obj 3)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.le_aleph_ord : ∀ (c : Cardinal.{u_1}), c ≤ Cardinal.aleph c.ord
-- Mathlib.Data.Int.ModEq
Int.mul_modulus_add_modEq_iff : ∀ {n a b c : ℤ}, b * n + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- This is important for iterating Kruskal-Katona: the shadow of an initial segment is also an
initial segment.  -/
Finset.Colex.shadow_initSeg : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} [inst_1 : Fintype α] (hs : s.Nonempty),
  (Finset.Colex.initSeg s).shadow = Finset.Colex.initSeg (s.erase (s.min' hs))
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.instHasOfPostcompPropertySchemeIsOpenImmersionOfIsStableUnderBaseChange : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange],
  P.HasOfPostcompProperty AlgebraicGeometry.IsOpenImmersion
-- Mathlib.Order.Monotone.MonovaryOrder
/-- **Alias** of the forward direction of `monovaryOn_iff_exists_monotoneOn`. -/
MonovaryOn.exists_monotoneOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn f g s → ∃ x, MonotoneOn f s ∧ MonotoneOn g s
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- Composition of morphisms between reflexive quivers.  -/
CategoryTheory.ReflPrefunctor.comp : {U : Type u_1} →
  [inst : CategoryTheory.ReflQuiver U] →
    {V : Type u_2} →
      [inst_1 : CategoryTheory.ReflQuiver V] →
        {W : Type u_3} → [inst_2 : CategoryTheory.ReflQuiver W] → U ⥤rq V → V ⥤rq W → U ⥤rq W
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a countable family of metric spaces, one may put a distance on their product `Π i, E i`.

It is highly non-canonical, though, and therefore not registered as a global instance.
The distance we use here is `edist x y = ∑' i, min (1/2)^(encode i) (edist (x i) (y i))`.  -/
PiCountable.metricSpace : {ι : Type u_2} → [Encodable ι] → {F : ι → Type u_3} → [(i : ι) → MetricSpace (F i)] → MetricSpace ((i : ι) → F i)
-- Mathlib.CategoryTheory.Limits.EpiMono
CategoryTheory.epi_iff_isIso_inr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : X ⟶ Y}
  {c : CategoryTheory.Limits.PushoutCocone f f} (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Epi f ↔ CategoryTheory.IsIso c.inr
-- Mathlib.SetTheory.Cardinal.NatCard
List.Nodup.length_le_natCard : ∀ {α : Type u_1} {l : List α}, l.Nodup → ∀ [Finite α], l.length ≤ Nat.card α
-- Mathlib.Control.Traversable.Basic
instTraversableList : Traversable List
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_div : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Div α] (s : ι → Set α) (t : Set α), (⋃ i, s i) / t = ⋃ i, s i / t
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.leadingCoeff.congr_simp : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  (D D_1 : A → B),
  D = D_1 →
    ∀ [inst_3 : Nonempty A] (f f_1 : AddMonoidAlgebra R A),
      f = f_1 → AddMonoidAlgebra.leadingCoeff D f = AddMonoidAlgebra.leadingCoeff D_1 f_1
-- Mathlib.CategoryTheory.Limits.Types.Coequalizers
CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv : ∀ {X Y : Type u} (f g : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (TypeCat.ofHom
        (Function.Coequalizer.mk ⇑(CategoryTheory.ConcreteCategory.hom f) ⇑(CategoryTheory.ConcreteCategory.hom g)))
      (CategoryTheory.Limits.Types.coequalizerIso f g).inv =
    CategoryTheory.Limits.coequalizer.π f g
-- Mathlib.Combinatorics.Schnirelmann
/-- **Alias** of `schnirelmannDensity_setOfPred_mod_eq_one`.

---

The Schnirelmann density of the set of naturals which are `1 mod m` is `m⁻¹`, for any `m ≠ 1`.

Note that if `m = 1`, this set is empty.
 -/
schnirelmannDensity_setOf_mod_eq_one : ∀ {m : ℕ}, m ≠ 1 → schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹
-- Mathlib.LinearAlgebra.Ray
/-- Two vectors are in the same ray, or they are nonzero and the first is in the same ray as the
negation of the second, if and only if they are not linearly independent.  -/
sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.IsTorsionFree R M] {x y : M},
  SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
-- Mathlib.CategoryTheory.Sites.Plus
/-- The plus construction, associating a presheaf to any presheaf.
See `plusFunctor` below for a functorial version.  -/
CategoryTheory.GrothendieckTopology.plusObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            CategoryTheory.Functor Cᵒᵖ D →
              [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] → CategoryTheory.Functor Cᵒᵖ D
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.single_pos : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : DecidableEq X] [inst_2 : Zero Y]
  [inst_3 : Preorder Y] {x : X} {y : Y}, 0 < Function.locallyFinsuppWithin.single x y ↔ 0 < y
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- `x` is additive semiconjugate to `y` by `a` if `a + x = y + a`  -/
AddSemiconjBy : {M : Type u_2} → [Add M] → M → M → M → Prop
-- Mathlib.Algebra.Group.Defs
IsAddCommutative.instAddCommMagma.eq_1 : ∀ {M : Type u_2} [inst : Add M] [inst_1 : IsAddCommutative M],
  IsAddCommutative.instAddCommMagma = { toAdd := inst, add_comm := ⋯ }
-- Init.Data.Vector.Range
Vector.zipIdx_eq_zip_range' : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n}, xs.zipIdx i = xs.zip (Vector.range' i n)
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.lTensorBot_one_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  {A : Subalgebra R S} (a : ↥A), A.lTensorBot (1 ⊗ₜ[R] a) = a
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.ext : ∀ {R : Type v} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type w}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B) [Algebra.FormallyUnramified R A],
  IsNilpotent I →
    ∀ {g₁ g₂ : A →ₐ[R] B}, (∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)) → g₁ = g₂
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
toIdeal_le_toIdeal_iff : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  {I J : HomogeneousIdeal 𝒜}, I.toIdeal ≤ J.toIdeal ↔ I ≤ J
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIci_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a x : α}, x ≤ a → Set.projIci a x = ⟨a, ⋯⟩
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id I)]
  [inst_2 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.id I)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.id I)).unit
      ((CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.id I)).whiskerLeft
        (CategoryTheory.ExponentiableMorphism.pushforwardId I).hom) =
    (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.id I)).unit
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mem_localTriv_source : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι) (p : Z.TotalSpace), p ∈ (Z.localTriv i).source ↔ p.proj ∈ (Z.localTriv i).baseSet
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.Iter.forIn_filterMapM : ∀ {α β β₂ γ : Type w} [inst : Std.Iterator α Id β] {ps : Std.Do.PostShape} {n : Type w → Type u_1}
  {o : Type w → Type u_2} [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o]
  [inst_5 : Std.Do.WPMonad o ps] [inst_6 : MonadAttach n] [WeaklyLawfulMonadAttach n] [inst_8 : MonadLiftT n o]
  [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id] [inst_11 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o]
  {it : Std.Iter β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Std.Do.Assertion ps}
  {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        match __do_lift with
          | some c => g c acc
          | none => pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.Iter.filterMapM f it) init g ⦃Q⦄
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.mk.inj : ∀ {R : Type u} {inst : Ring R} {toTopologicalSpace : TopologicalSpace R} {toIsTopologicalRing : IsTopologicalRing R}
  {toTopologicalSpace_1 : TopologicalSpace R} {toIsTopologicalRing_1 : IsTopologicalRing R},
  { toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing } =
      { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalRing := toIsTopologicalRing_1 } →
    toTopologicalSpace = toTopologicalSpace_1
-- Mathlib.Data.Sym.Sym2
Sym2.inductionOn : ∀ {α : Type u_1} {f : Sym2 α → Prop} (i : Sym2 α), (∀ (x y : α), f s(x, y)) → f i
-- Mathlib.Combinatorics.SimpleGraph.Diam
/-- In a finite graph with nontrivial vertex set, the graph is connected
if and only if the extended diameter is not `⊤`.
See `connected_of_ediam_ne_top` for one of the implications without
the finiteness assumptions  -/
SimpleGraph.connected_iff_ediam_ne_top : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α] [Finite α], G.Connected ↔ G.ediam ≠ ⊤
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instSubNegMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubNegMonoid α],
  AddOpposite.instSubNegMonoid =
    { toAddMonoid := AddOpposite.instAddMonoid, toNeg := AddOpposite.instNeg, sub := SubNegMonoid.sub',
      zsmul := fun n a => AddOpposite.op (n • AddOpposite.unop a), sub_eq_add_neg := ⋯, zsmul_zero' := ⋯,
      zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
-- Mathlib.Topology.Algebra.Module.FiniteDimension
ContinuousLinearMap.isQuotientMap_of_finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E]
  [ContinuousSMul 𝕜 E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [IsTopologicalAddGroup F]
  [inst_10 : Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space F] [FiniteDimensional 𝕜 F] (f : E →L[𝕜] F),
  (↑f).range = ⊤ → Topology.IsQuotientMap ⇑f
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_zero : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : StarAddMonoid A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : StarAddMonoid B], ⇑0 = 0