mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
/-- Returns expressions in the given expression equivalence class.  -/
Lean.Meta.Grind.Goal.getEqc : Lean.Meta.Grind.Goal → Lean.Expr → optParam Bool false → List Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Convenience reformulation of the second iterated derivative, as a map from `E` to bilinear maps
`E →ₗ[ℝ] E →ₗ[ℝ] ℝ`.
 -/
bilinearIteratedFDerivTwo : (𝕜 : 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] → (E → F) → E → E →ₗ[𝕜] E →ₗ[𝕜] F
-- Mathlib.Algebra.Algebra.Hom.Rat
RingEquiv.toRingEquiv_toRatAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (f : R ≃+* S), f.toRatAlgEquiv.toRingEquiv = f
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.skeletalFunctor_map : ∀ {X Y : SimplexCategory} (f : X ⟶ Y),
  SimplexCategory.skeletalFunctor.map f = NonemptyFinLinOrd.ofHom (SimplexCategory.Hom.toOrderHom f)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_dite_irrel : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (p : Prop) [inst_1 : Decidable p] (s : Finset ι) (f : p → ι → M)
  (g : ¬p → ι → M), (∏ x ∈ s, if h : p then f h x else g h x) = if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.WPath.child.inj : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} {a : P.A} {f : P.last.B a → P.last.W} {i : Fin2 n} {j : P.last.B a}
  {c : P.WPath (f j) i} {j_1 : P.last.B a} {c_1 : P.WPath (f j_1) i},
  MvPFunctor.WPath.child a f i j c = MvPFunctor.WPath.child a f i j_1 c_1 → j = j_1 ∧ c ≍ c_1
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.mul_inv_le_iff_mul_le_of_neg : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] (a c : R) {b : R}, b < 0 → (a * b⁻¹ ≤ c ↔ c * b ≤ a)
-- Mathlib.Algebra.Group.Even
Even.zsmul_right : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {a : α} (n : ℤ), Even a → Even (n • a)
-- Mathlib.Analysis.LocallyConvex.WeakDual
WeakBilin.locallyConvexSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : NormedSpace ℝ 𝕜] [inst_6 : Module ℝ E] [IsScalarTower ℝ 𝕜 E]
  {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜}, LocallyConvexSpace ℝ (WeakBilin B)
-- Init.Data.SInt.Lemmas
Int32.minValue_le : ∀ (a : Int32), Int32.minValue ≤ a
-- Mathlib.CategoryTheory.Preadditive.Projective.Internal
CategoryTheory.instIsStableUnderRetractsIsInternallyProjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C], CategoryTheory.isInternallyProjective.IsStableUnderRetracts
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- The Second-Derivative Test from calculus, maximum version.  -/
isLocalMax_of_deriv_deriv_neg : ∀ {f : ℝ → ℝ} {x₀ : ℝ}, deriv (deriv f) x₀ < 0 → deriv f x₀ = 0 → ContinuousAt f x₀ → IsLocalMax f x₀
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α} (T : Set α → F' →L[ℝ] F)
  (f : MeasureTheory.SimpleFunc α F'),
  ‖MeasureTheory.SimpleFunc.setToSimpleFunc T f‖ ≤ ∑ x ∈ f.range, ‖T (⇑f ⁻¹' {x})‖ * ‖x‖
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.apply_eq_iff_mem_orbit : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E],
  IsAddQuotientCoveringMap f G → ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂
-- Mathlib.Order.Concept
Concept.leftInverse_ofObjects_extent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, Function.LeftInverse (Concept.ofObjects r) Concept.extent
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instπWalkingCospanSchemeCospanOne : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f]
  [inst : AlgebraicGeometry.IsOpenImmersion g],
  AlgebraicGeometry.IsOpenImmersion
    (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.HasIntegral.integral_eq : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F},
  BoxIntegral.HasIntegral I l f vol y → BoxIntegral.integral I l f vol = y
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
/-- The inclusion `X ⟶ X ⊗ Δ[1]` which is `0` on the second factor.  -/
SSet.ι₀ : {X : SSet} → X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X (SSet.stdSimplex.obj { len := 1 })
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.eval : ∀ {R : Type u_6} [inst : CommRing R] {I : Ideal R} {x y : R},
  x ≡ y [SMOD I] → ∀ (f : Polynomial R), Polynomial.eval x f ≡ Polynomial.eval y f [SMOD I]
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.indicator_const_iff_of_ne : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Zero β] {s : Set α} {c : β},
  c ≠ 0 → (Filter.EventuallyConst (s.indicator fun x => c) l ↔ Filter.EventuallyConst s l)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      (I : C) →
        (i₀ i₁ : A ⟶ I) →
          (π : I ⟶ A) →
            autoParam (CategoryTheory.CategoryStruct.comp i₀ π = CategoryTheory.CategoryStruct.id A)
                HomotopicalAlgebra.Precylinder.i₀_π._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp i₁ π = CategoryTheory.CategoryStruct.id A)
                  HomotopicalAlgebra.Precylinder.i₁_π._autoParam →
                HomotopicalAlgebra.Precylinder A
-- Mathlib.Data.Sym.Basic
Sym.forall : ∀ {α : Type u_1} {n : ℕ} {p : Sym α n → Prop},
  (∀ (s : Sym α n), p s) ↔ ∀ (s : Multiset α) (hs : s.card = n), p (Sym.mk s hs)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K} [IsGalois k K],
  ¬NumberField.InfinitePlace.IsUnramified k w ↔ Nat.card ↥(MulAction.stabilizer Gal(K/k) w) = 2
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- A wide pushout shape for any type `J` can be written simply as `Option J`.  -/
CategoryTheory.Limits.WidePushoutShape : Type w → Type w
-- Lean.Compiler.IR.Basic
Lean.IR.instToStringJoinPointId : ToString Lean.IR.JoinPointId
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.monoidWithZeroHom_ext : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulZeroOneClass β] ⦃f g : WithZero α →*₀ β⦄,
  (↑f).comp WithZero.coeMonoidHom = (↑g).comp WithZero.coeMonoidHom → f = g
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.GrothendieckTopology.instIsStableUnderCompositionToPrecoverage : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] (J : CategoryTheory.GrothendieckTopology C),
  J.toPrecoverage.IsStableUnderComposition
-- Mathlib.ModelTheory.Basic
/-- Any type can be made uniquely into a structure over the empty language.  -/
FirstOrder.Language.emptyStructure : {M : Type w} → FirstOrder.Language.empty.Structure M
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.eval₂Hom_comp_expand : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] (p : ℕ) (f : R →+* S)
  (g : σ → S), (MvPolynomial.eval₂Hom f g).comp ↑(MvPolynomial.expand p) = MvPolynomial.eval₂Hom f (g ^ p)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearEquiv.baseChange_trans : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) {P : Type u_6} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R P] (e : M ≃ₗ[R] N)
  (f : N ≃ₗ[R] P),
  LinearEquiv.baseChange R A M P (e ≪≫ₗ f) = LinearEquiv.baseChange R A M N e ≪≫ₗ LinearEquiv.baseChange R A N P f
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.IsStrongPrelimit.eq_1 : ∀ (c : Cardinal.{u_1}), c.IsStrongPrelimit = ∀ ⦃x : Cardinal.{u_1}⦄, x < c → 2 ^ x < c
-- Lean.Server.References
/-- Module name of the module that is imported.  -/
Lean.Server.ModuleImport.module : Lean.Server.ModuleImport → Lean.Name
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [P.IsClosedUnderLimitsOfShape Jᵒᵖ], P.op.IsClosedUnderColimitsOfShape J
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instReflectsColimitsOfSizeModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w, w, w, max (max u v) (w + 1), max u (w + 1)}
    (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k))
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.restoreM_OptionT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  (x : m (Option α)) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred),
  ⦃ Std.Internal.Do.wp x (Std.Internal.Do.EPost.Cons.pushOption post epost) epost.tail ⦄ MonadControl.restoreM x ⦃ post;
    epost ⦄
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.factorThruImage_preComp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasImage g]
  [inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.Limits.image.preComp f g) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.factorThruImage g)
-- Mathlib.Order.Sublocale
Sublocale.carrier.instFrame : {X : Type u_1} → [inst : Order.Frame X] → {S : Sublocale X} → Order.Frame ↥S
-- Mathlib.Order.Types.Defs
_private.Mathlib.Order.Types.Defs.0.OrderType.isEmpty_toType_iff : ∀ {o : OrderType.{u_1}}, IsEmpty o.ToType ↔ o = 0
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimitRecOn_succ : ∀ {α : Type u_1} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α]
  (succ : (a : α) → ¬IsMax a → motive (Order.succ a)) (isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → motive a)
  [inst_2 : NoMaxOrder α] (b : α), Order.isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b ⋯
-- Mathlib.LinearAlgebra.Prod
Submodule.prod_map_snd : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (p : Submodule R M) (q : Submodule R M₂),
  Submodule.map (LinearMap.snd R M M₂) (p.prod q) = q
-- Mathlib.Order.Bounds.Basic
isLUB_empty_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsLUB ∅ a ↔ IsBot a
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocEntry.toSimprocOLeanEntry : Lean.Meta.Simp.SimprocEntry → Lean.Meta.Simp.SimprocOLeanEntry
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
/-- The additive equivalence `(ℤ ⟶ G) ≃+ G`  -/
AddCommGrpCat.uliftZMultiplesAddEquiv : (G : AddCommGrpCat) → (AddCommGrpCat.of (ULift.{u_1, 0} ℤ) ⟶ G) ≃+ ↑G
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.isClosed_of_subset_lattice : ∀ (L : PeriodPair) {s : Set ℂ}, s ⊆ ↑L.lattice → IsClosed s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_le_size_insertManyIfNewUnit : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} {ρ : Type w} [inst_2 : ForIn Id ρ α]
  [EquivBEq α] [LawfulHashable α], m.WF → ∀ {l : ρ}, m.size ≤ (m.insertManyIfNewUnit l).size
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.neg_add_cancel_left_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a : α}, a ≠ ⊤ → ∀ (b : α), -a + (a + b) = b
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K),
  (↑A.unitsModPrincipalUnitsEquivResidueFieldUnits).comp
      (QuotientGroup.mk' (A.principalUnitGroup.subgroupOf A.unitGroup)) =
    A.unitGroupToResidueFieldUnits
-- Mathlib.Analysis.Calculus.FDeriv.Star
fderivWithin_star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : StarModule 𝕜 F] [inst_8 : ContinuousStar F] {f : E → F} {x : E} {s : Set E}
  [inst_9 : TrivialStar 𝕜],
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (fun y => star (f y)) s x = ↑(starL' 𝕜) ∘SL fderivWithin 𝕜 f s x
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Comon_EquivMon_OpOp_counitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Comon.Comon_EquivMon_OpOp C).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.Comon.MonOpOpToComon C).comp (CategoryTheory.Comon.ComonToMonOpOp C)).obj x))
      ⋯
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `alter` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.constAlter : ∀ {α : Type u} [inst : Ord α] {x : Type v} {t : Std.DTreeMap.Internal.Impl α fun x_1 => x} {h : t.Balanced} {k : α}
  {f : Option x → Option x}, t.WF → (Std.DTreeMap.Internal.Impl.Const.alter k f t h).impl.WF
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The underlying `ContinuousMonoidHom`.  -/
ProfiniteGrp.Hom.hom' : {A B : ProfiniteGrp.{u}} → A.Hom B → ↑A.toProfinite.toTop →ₜ* ↑B.toProfinite.toTop
-- Mathlib.Data.Set.Card
Set.sdiff_nonempty_of_ncard_lt_ncard : ∀ {α : Type u_1} {s t : Set α},
  s.ncard < t.ncard → autoParam s.Finite Set.sdiff_nonempty_of_ncard_lt_ncard._auto_1 → (t \ s).Nonempty
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertList_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k toInsert = false →
    Std.Internal.List.getKey? k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getKey? k l
-- Mathlib.Data.List.Defs
List.map₂Left'.eq_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (x : List α) (x_1 : List β),
  List.map₂Left' f x x_1 =
    match x, x_1 with
    | [], bs => ([], bs)
    | a :: as, [] => (List.map (fun a => f a none) (a :: as), [])
    | a :: as, b :: bs =>
      have rec' := List.map₂Left' f as bs;
      (f a (some b) :: rec'.1, rec'.2)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Pi.hasProd : ∀ {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [inst : (x : α) → CommMonoid (X x)]
  [inst_1 : (x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} {f : ι → (x : α) → X x} {g : (x : α) → X x},
  HasProd f g L ↔ ∀ (x : α), HasProd (fun i => f i x) (g x) L
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.not_isRightDescent_one : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  ¬cs.IsRightDescent 1 i
-- Mathlib.Topology.Compactness.Lindelof
Set.Finite.isLindelof_sUnion : ∀ {X : Type u} [inst : TopologicalSpace X] {S : Set (Set X)}, S.Finite → (∀ s ∈ S, IsLindelof s) → IsLindelof (⋃₀ S)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.one_le_prod'' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s : Finset ι} [MulLeftMono N],
  (∀ (i : ι), 1 ≤ f i) → 1 ≤ ∏ i ∈ s, f i
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
/-- A family of functors jointly reflects monomorphisms if for every morphism `f : X ⟶ Y`
such that the image of `f` under all `F i` is an monomorphism, then `f` is an monomorphism.  -/
CategoryTheory.JointlyReflectMonomorphisms : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_4, u_1} C] →
    {I : Type u_2} →
      {D : I → Type u_3} →
        [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] →
          ((i : I) → CategoryTheory.Functor C (D i)) → Prop
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_sub_left : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {s t : Set G},
  interior s - t ⊆ interior (s - t)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
/-- For 0 < x we have x - x ^ 3 / 6 < sin x.

This inequality is tight, in that the constant 6 is best possible.  -/
Real.sin_gt_sub_cube : ∀ {x : ℝ}, 0 < x → x - x ^ 3 / 6 < Real.sin x
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).unmop = CategoryTheory.MonoidalCategoryStruct.rightUnitor X.unmop
-- Mathlib.CategoryTheory.Triangulated.Rotate
/-- Rotating triangles gives an auto-equivalence on the category of triangles in `C`.
 -/
CategoryTheory.Pretriangulated.triangleRotation : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
          CategoryTheory.Pretriangulated.Triangle C ≌ CategoryTheory.Pretriangulated.Triangle C
-- Mathlib.Data.Nat.Fib.Basic
/-- Shows that `fib` indeed satisfies the Fibonacci recurrence `Fₙ₊₂ = Fₙ + Fₙ₊₁`.  -/
Nat.fib_add_two : ∀ {n : ℕ}, Nat.fib (n + 2) = Nat.fib n + Nat.fib (n + 1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.nonempty_sup_left : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s₁ s₂ : AffineSubspace k P) [Nonempty ↥s₁], Nonempty ↥(s₁ ⊔ s₂)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.Iso.degree_eq : ∀ {V : Type u_1} {G : SimpleGraph V} {W : Type u_2} {G' : SimpleGraph W} (f : G ≃g G') (x : V)
  [inst : Fintype ↑(G.neighborSet x)] [inst_1 : Fintype ↑(G'.neighborSet (f x))], G'.degree (f x) = G.degree x
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.toPermFiber_apply_symm_apply_coe : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) (a : G) (x_1 : ↑(f ⁻¹' {x})),
  ↑((Equiv.symm ((hf.toPermFiber x) a)) x_1) = a⁻¹ • ↑x_1
-- Mathlib.Data.Finset.Card
Finset.card_le_two : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α}, {a, b}.card ≤ 2
-- Lean.Elab.DocString
/-- Finds registered expander names that `x` is a suffix of, for use in error message hints when the
name is shadowed. Returns display names suitable for `mkSuggestion`.
 -/
_private.Lean.Elab.DocString.0.Lean.Doc.findShadowedNames : {α : Type} → Lean.NameMap (Array Lean.Name) → Lean.NameMap α → Lean.Name → Lean.Elab.TermElabM (Array Lean.Name)
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.mem_cylinder : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S : Set ((i : ↥s) → α ↑i)) (f : (i : ι) → α i),
  f ∈ MeasureTheory.cylinder s S ↔ s.restrict f ∈ S
-- Lean.Parser.Term
Lean.Parser.Command.versoCommentBodyFn : Lean.Parser.ParserFn
-- Mathlib.LinearAlgebra.Prod
LinearMap.snd_eq_coprod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], LinearMap.snd R M M₂ = LinearMap.coprod 0 LinearMap.id
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instNontrivial : ∀ (K : Type u) [inst : CommRing K] [Nontrivial K], Nontrivial (RatFunc K)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF →
    t₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], (t₁ \ t₂).get! k = if t₂.contains k = true then default else t₁.get! k
-- Mathlib.Algebra.Order.Floor.Div
le_floorDiv_iff_mul_le : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : FloorDiv α α] {a b c : α},
  0 < a → (c ≤ b ⌊/⌋ a ↔ a • c ≤ b)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instDivisionAddCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α],
  Colex.instDivisionAddCommMonoid = { toSubtractionMonoid := Colex.instSubtractionMonoid, add_comm := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.counit_comul_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.ComonObj M] {Z : C} (f : M ⟶ Z) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit f) h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv h)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The domain of `f` is equivalent to its range as measurable spaces,
if `f` is a measurable embedding  -/
MeasurableEmbedding.equivRange : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → {f : α → β} → MeasurableEmbedding f → α ≃ᵐ ↑(Set.range f)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.not_mem_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → k ∉ m₁ \ m₂
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- (implementation) the right unitor for R-modules  -/
SemimoduleCat.MonoidalCategory.rightUnitor : {R : Type u} → [inst : CommSemiring R] → (M : SemimoduleCat R) → SemimoduleCat.of R (TensorProduct R (↑M) R) ≅ M
-- Init.GetElem
List.getElem_cons_succ : ∀ {α : Type u_1} (a : α) (as : List α) (i : ℕ) (h : i + 1 < (a :: as).length), (a :: as)[i + 1] = as[i]
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {f : α → β → Bool},
  m.WF → (Std.HashMap.Raw.filter f m).WF
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.instLE.eq_1 : Rat.instLE = { le := fun a b => b.blt a = false }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ \ t₂).get? k = none
-- Mathlib.Algebra.Group.Commute.Units
/-- If the product of two commuting elements is a unit, then the right multiplier is a unit.  -/
Units.rightOfMul : {M : Type u_1} → [inst : Monoid M] → (u : Mˣ) → (a b : M) → a * b = ↑u → Commute a b → Mˣ