mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toListModel_alterₘ : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {t : Std.DTreeMap.Internal.Impl α fun x => β} {a : α} {f : Option β → Option β} (htb : t.Balanced),
  t.Ordered →
    (Std.DTreeMap.Internal.Impl.Const.alterₘ a f t htb).toListModel.Perm
      (Std.Internal.List.Const.alterKey a f t.toListModel)
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.equivAddSubgroupOrbitsQuotientAddGroup.eq_1 : ∀ {G : Type u} {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (x : X)
  [inst_2 : AddAction.IsPretransitive G X] [inst_3 : IsCancelVAdd G X] (H : AddSubgroup G),
  AddAction.equivAddSubgroupOrbitsQuotientAddGroup x H =
    { toFun := fun q => Quotient.liftOn' q (fun y => ↑⋯.choose) ⋯,
      invFun := fun q => Quotient.liftOn' q (fun g => ⟦-g +ᵥ x⟧) ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The `cons` composes an atomic 1-morphism at the end of a normalized 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.NormalizedHom.cons : Mathlib.Tactic.BicategoryLike.Mor₁ →
  Mathlib.Tactic.BicategoryLike.NormalizedHom →
    Mathlib.Tactic.BicategoryLike.Atom₁ → Mathlib.Tactic.BicategoryLike.NormalizedHom
-- Mathlib.Data.Finset.Prod
Finset.offDiag_union : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α],
  Disjoint s t → (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mono_map_0_of_mono : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) [CategoryTheory.Mono f],
  CategoryTheory.Mono (groupCohomology.map (MonoidHom.id G) f 0)
-- Mathlib.Order.Filter.SmallSets
Filter.Frequently.smallSets_of_forall_mem_basis : ∀ {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop},
  (∀ (i : ι), p i → P (s i)) → l.HasBasis p s → ∃ᶠ (t : Set α) in l.smallSets, P t
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.prodMk : ∀ {Ω : Type u_1} {ι : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : ι → Type u_5}
  [inst : (i : ι) → NormedAddCommGroup (E i)] [inst_1 : (i : ι) → NormedSpace ℝ (E i)]
  [inst_2 : (i : ι) → MeasurableSpace (E i)] [∀ (i : ι), BorelSpace (E i)] {X : (i : ι) → Ω → E i}
  [∀ (i : ι), SecondCountableTopology (E i)] [Finite ι],
  ProbabilityTheory.HasGaussianLaw (fun ω x => X x ω) P →
    ∀ (i j : ι), ProbabilityTheory.HasGaussianLaw (fun ω => (X i ω, X j ω)) P
-- Lean.Elab.Tactic.Conv.Pattern
/-- Is this pattern no longer interested in accepting matches?  -/
Lean.Elab.Tactic.Conv.PatternMatchState.isDone : Lean.Elab.Tactic.Conv.PatternMatchState → Bool
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.IterM.step_intermediateDropWhileWithPostcondition.match_3.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.Analysis.Normed.Operator.Extend
LinearMap.extendOfNorm_unique : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : NormedDivisionRing 𝕜]
  [inst_1 : NormedDivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : AddCommGroup E] [inst_3 : SeminormedAddCommGroup Eₗ]
  [inst_4 : NormedAddCommGroup F] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ F] [inst_7 : IsBoundedSMul 𝕜₂ F]
  [inst_8 : Module 𝕜 Eₗ] [inst_9 : IsBoundedSMul 𝕜 Eₗ] [inst_10 : CompleteSpace F] {f : E →ₛₗ[σ₁₂] F} {e : E →ₗ[𝕜] Eₗ},
  DenseRange ⇑e → ∀ (C : ℝ), (∀ (x : E), ‖f x‖ ≤ C * ‖e x‖) → ∀ (g : Eₗ →SL[σ₁₂] F), ↑g ∘ₛₗ e = f → f.extendOfNorm e = g
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (n : ℕ) (X : CategoryTheory.ComposableArrows Cᵒᵖ n)
  (X_1 : Fin (n + 1)),
  ((CategoryTheory.ComposableArrows.opEquivalence C n).counitIso.inv.app X).app X_1 =
    X.map
      (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).unitInv.app
          (Opposite.op X_1)).unop
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.coverEntropyEntourage_image_le : ∀ {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ (F : Set X) (V : SetRel Y Y),
      Dynamics.coverEntropyEntourage T (φ '' F) V ≤ Dynamics.coverEntropyEntourage S F (Prod.map φ φ ⁻¹' V)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.ppGoal : Lean.MVarId → Lean.Elab.TermElabM Std.Format
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_eq_zero_of_isTrivial : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsTrivial L M], LieModule.traceForm R L M = 0
-- Mathlib.AlgebraicGeometry.Gluing
/-- (Implementation) the transition maps in the glue data associated with an open cover.  -/
AlgebraicGeometry.Scheme.Cover.gluedCoverT' : {X : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (x y z : 𝒰.I₀) →
      CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
          (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
        CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z))
          (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))
-- Mathlib.Topology.Sheaves.CommRingCat
/-- A homomorphism of topological rings can be postcomposed with functions from a source space `X`;
this is a ring homomorphism (with respect to the pointwise ring operations on functions).  -/
TopCat.continuousFunctions.map : (X : TopCatᵒᵖ) → {R S : TopCommRingCat} → (R ⟶ S) → (TopCat.continuousFunctions X R ⟶ TopCat.continuousFunctions X S)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_apply₀' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → (μ.restrict s) t = μ (t ∩ s)
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.add : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f g : (i : α) → E i},
  Memℓp f p → Memℓp g p → Memℓp (f + g) p
-- Mathlib.Tactic.NormNum.Abs
Mathlib.Meta.NormNum.isNNRat_abs_neg : ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {num den : ℕ},
  Mathlib.Meta.NormNum.IsRat a (Int.negOfNat num) den → Mathlib.Meta.NormNum.IsNNRat |a| num den
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
DifferentiableWithinAt.arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x → DifferentiableWithinAt ℝ (fun x => Real.arctan (f x)) s x
-- Mathlib.Topology.Algebra.UniformConvergence
instPowUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Pow β M], instPowUniformFun = { pow := instPowUniformFun._aux_1 }
-- Mathlib.Logic.Equiv.Array
/-- If `α` is countable, then so is `Array α`.  -/
Array.countable : ∀ {α : Type u_1} [Countable α], Countable (Array α)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.uniformContinuous_restrictScalars : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [ContinuousSMul 𝕜 E] {F : Type u_3} [inst_5 : AddCommGroup F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F] [inst_8 : Module 𝕜 F] (𝕜' : Type u_4)
  [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : Module 𝕜' E]
  [inst_12 : IsScalarTower 𝕜' 𝕜 E] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F],
  UniformContinuous (ContinuousLinearMap.restrictScalars 𝕜')
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₁.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.CooperSplit},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₁ c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₁ c_1 →
    c = c_1
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c),
  CategoryTheory.CategoryStruct.comp (t.natTransTruncGEOfLE a b hab) (t.natTransTruncGEOfLE b c hbc) =
    t.natTransTruncGEOfLE a c ⋯
-- Mathlib.Order.PropInstances
Pi.isCompl_iff : ∀ {ι : Type u_1} {α' : ι → Type u_3} [inst : (i : ι) → PartialOrder (α' i)] [inst_1 : (i : ι) → BoundedOrder (α' i)]
  {f g : (i : ι) → α' i}, IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Submodule.toLinearMap_liftQL : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Ring R] [inst_1 : Ring R₂] {σ : R →+* R₂} {M : Type u_3} {M₂ : Type u_4}
  [inst_2 : TopologicalSpace M] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : TopologicalSpace M₂]
  [inst_6 : AddCommGroup M₂] [inst_7 : Module R₂ M₂] (S : Submodule R M) (f : M →SL[σ] M₂) (h : S ≤ (↑f).ker),
  ↑(S.liftQL f h) = S.liftQ (↑f) h
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.triangle_obj₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  (CochainComplex.mappingCocone.triangle φ).obj₃ = L
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.oppositeShiftFunctorAdd_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) (a b : A),
  (CategoryTheory.shiftFunctorAdd (CategoryTheory.OppositeShift C A) a b).inv.app X =
    ((CategoryTheory.shiftFunctorAdd C a b).hom.app (Opposite.unop X)).op
-- Mathlib.RingTheory.DiscreteValuationRing.TFAE
IsLocalRing.ResidueField.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R], IsLocalRing.ResidueField R = IsLocalRing.ResidueField R
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis'.contract_isBasis_of_indep : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α},
  M.IsBasis' I X → M.Indep (I ∪ J) → (M.contract J).IsBasis' (I \ J) (X \ J)
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Left scalar multiplication of a unit and a continuous linear equivalence,
as a continuous linear equivalence.  -/
ContinuousLinearEquiv.instSMulUnitsId : {S : Type u_1} →
  {R : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : Module R V] →
                [inst_4 : TopologicalSpace V] →
                  [inst_5 : Module S V] →
                    [ContinuousConstSMul S V] →
                      [inst_7 : AddCommMonoid W] →
                        [inst_8 : Module R W] →
                          [inst_9 : TopologicalSpace W] →
                            [inst_10 : Module S W] →
                              [ContinuousConstSMul S W] →
                                [SMulCommClass R S W] →
                                  [inst_13 : SMul S R] →
                                    [IsScalarTower S R V] → [IsScalarTower S R W] → SMul Sˣ (V ≃L[R] W)
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The (exact) sequence `0 ⟶ E^n(f₁, f₂, f₃) ⟶ Z^n(f₁, f₂ ≫ f₃) ⟶ H^n(f₃)`.  -/
CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i₀ i₁ i₂ i₃ : ι} →
              (i₀ ⟶ i₁) →
                (f₂ : i₁ ⟶ i₂) →
                  (f₃ : i₂ ⟶ i₃) →
                    (f₂₃ : i₁ ⟶ i₃) →
                      CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃ →
                        (n₀ n₁ n₂ : ℤ) →
                          autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_1 →
                            autoParam (n₁ + 1 = n₂)
                                CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_3 →
                              CategoryTheory.ShortComplex C
-- Mathlib.CategoryTheory.Action.Basic
Action.instIsIsoHomHom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f : M ≅ N), CategoryTheory.IsIso f.hom.hom
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `e` is a case-split that does not need to be performed anymore.  -/
Lean.Meta.Grind.isResolvedCaseSplit : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_clm_comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {x : 𝕜}
  {G : Type u_2} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {c : 𝕜 → F →L[𝕜] G} {d : 𝕜 → E →L[𝕜] F},
  DifferentiableAt 𝕜 c x →
    DifferentiableAt 𝕜 d x → deriv (fun y => c y ∘SL d y) x = deriv c x ∘SL d x + c x ∘SL deriv d x
-- Init.Data.Nat.Basic
Nat.lt_iff_le_and_ne : ∀ {m n : ℕ}, m < n ↔ m ≤ n ∧ m ≠ n
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- If two nonzero squares are negatives of each other in `ZMod p`, then `p % 4 ≠ 3`.  -/
ZMod.mod_four_ne_three_of_sq_eq_neg_sq' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {x y : ZMod p}, y ≠ 0 → x ^ 2 = -y ^ 2 → p % 4 ≠ 3
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.toList_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp}, t.toArray.toList = t.toList
-- Std.Time.Date.Unit.Day
/-- Convert `Nanosecond.Offset` into `Day.Offset`.
 -/
Std.Time.Day.Offset.ofNanoseconds : Std.Time.Nanosecond.Offset → Std.Time.Day.Offset
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cocones.CorepresentableBy X) {Y : C} (f : X ⟶ Y),
  CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom h f = { pt := Y, ι := h.homEquiv f }
-- Mathlib.Algebra.Order.Floor.Defs
/-- A version of `Int.cast_mono` for floor rings, whose addition is not necessarily monotone.  -/
FloorRing.intCast_mono : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [FloorRing α], Monotone Int.cast
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.cosZeta_neg : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.cosZeta (-a) s = HurwitzZeta.cosZeta a s
-- Mathlib.SetTheory.Cardinal.Ordinal
Cardinal.mk_biUnion_le_of_le : ∀ {β : Type u_1} {o : Ordinal.{u_1}} {c : Cardinal.{u_1}},
  o.card ≤ c →
    Cardinal.aleph0 ≤ c →
      ∀ (A : Ordinal.{u_1} → Set β), (∀ j < o, Cardinal.mk ↑(A j) ≤ c) → Cardinal.mk ↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instMulActionCircle : MulAction Circle Complex.UnitDisc
-- Mathlib.CategoryTheory.Sites.Finite
CategoryTheory.Pretopology.ofArrows_mem_finite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {ι : Type u_1} [Finite ι] (Y : ι → C) (f : (i : ι) → Y i ⟶ X),
  CategoryTheory.Presieve.ofArrows Y f ∈ (CategoryTheory.Pretopology.finite C).coverings X
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.nil_rotate : ∀ {V : Type u} {G : SimpleGraph V} {v u : V} [inst : DecidableEq V] {c : G.Walk v v} (h : u ∈ c.support),
  (c.rotate u h).Nil ↔ c.Nil
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_union_list : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : BEq α] [Std.LawfulBEqOrd α] [Std.TransOrd α]
  {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.WF) (h₂ : t₂.WF),
  (t₁.union t₂ ⋯ ⋯).toListModel.Perm (Std.Internal.List.insertList t₁.toListModel t₂.toListModel)
-- Mathlib.Algebra.Lie.Solvable
LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (k : ℕ), LieIdeal.map I.incl (LieAlgebra.derivedSeries R (↥I) k) = LieAlgebra.derivedSeriesOfIdeal R L k I
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The proposition that two submodules are orthogonal, denoted as `U ⟂ V`.  -/
Submodule.IsOrtho : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → Submodule 𝕜 E → Submodule 𝕜 E → Prop
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_one : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.scaleRoots 1 = p
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_of_le : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} {m : ι}, m ≤ n → MeasureTheory.hittingBtwn u s n m ω = m
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.eta_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T),
  f.eta.hom.left = CategoryTheory.CategoryStruct.id f.left
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag2n_coe : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] {i j : ι} (hij : i ≠ j)
  (a : F) (ha : a ≠ 0),
  ↑(Matrix.SpecialLinearGroup.diag2n hij a ha) = Matrix.diagonal fun k => if k = i then a else if k = j then a⁻¹ else 1
-- Mathlib.Analysis.InnerProductSpace.Calculus
fderiv_norm_sq_apply : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F),
  fderiv ℝ (fun x => ‖x‖ ^ 2) x = 2 • (innerSL ℝ) x
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.mk : (X : Type u) → X × X → Bipointed
-- Mathlib.Order.CompleteLattice.Basic
sup_biSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α},
  (∃ i, p i) → a ⊔ ⨆ i, ⨆ (h : p i), f i h = ⨆ i, ⨆ (h : p i), a ⊔ f i h
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.le₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y), W₂ f → r.deg X ≤ r.deg Y
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time_min : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι]
  (hτ : MeasureTheory.IsStoppingTime f τ) (hπ : MeasureTheory.IsStoppingTime f π), MeasurableSet {ω | τ ω = π ω}
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
mem_affineSpan_pair_iff_exists_lineMap_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p p₁ p₂ : P}, p ∈ line[k, p₁, p₂] ↔ ∃ r, (AffineMap.lineMap p₁ p₂) r = p
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- A monoidal category with binary coproducts is left distributive
if the left tensor product functor preserves binary coproducts.  -/
CategoryTheory.IsMonoidalLeftDistrib : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.MonoidalCategory C] → [CategoryTheory.Limits.HasBinaryCoproducts C] → Prop
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.eq_mul_inv_iff_mul_eq : ∀ {α : Type u} [inst : DivisionMonoid α] {a b c : α}, IsUnit c → (a = b * c⁻¹ ↔ a * c = b)
-- Mathlib.Topology.Compactification.StoneCech
eq_if_preStoneCechUnit_eq : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [T2Space β] [CompactSpace β]
  {g : α → β}, Continuous g → ∀ {a b : α}, preStoneCechUnit a = preStoneCechUnit b → g a = g b
-- Mathlib.Algebra.Field.Defs
Semifield.toCommGroupWithZero : {K : Type u_2} → [self : Semifield K] → CommGroupWithZero K
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.«grind_filter(_)» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRightIso_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X W : C),
  CategoryTheory.MonoidalCategory.whiskerRightIso (CategoryTheory.Iso.refl X) W =
    CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj X W)
-- Init.Data.Nat.Simproc
Nat.Simproc.bneTrueOfEqFalse : ∀ {a b : ℕ}, (a = b) = False → (a != b) = true
-- Mathlib.Computability.Primrec.Basic
/-- To show a function `f : α → ℕ` is primitive recursive, it is enough to show that the function
is bounded by a primitive recursive function and that its graph is primitive recursive  -/
Primrec.of_graph : ∀ {α : Type u_1} [inst : Primcodable α] {f : α → ℕ},
  Primrec.PrimrecBounded f → (PrimrecRel fun a b => f a = b) → Primrec f
-- Mathlib.Algebra.GroupWithZero.Action.Basic
DistribMulAction.toAddEquiv_symm_apply : ∀ {G : Type u_1} (A : Type u_3) [inst : Group G] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction G A] (x : G) (a : A),
  (DistribMulAction.toAddEquiv A x).symm a = x⁻¹ • a
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplexEquivIcc_symm_apply_coe : ∀ (𝕜 : Type u_1) [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : IsOrderedRing 𝕜] (x : ↑(Set.Icc 0 1)),
  ↑((stdSimplexEquivIcc 𝕜).symm x) = ![1 - ↑x, ↑x]
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_eq_none_iff : ∀ {w n : ℕ} {l : BitVec w}, l[n]? = none ↔ w ≤ n
-- Mathlib.Data.ENat.Basic
ENat.WithBot.add_ofNat_cancel : ∀ {a b : WithBot ℕ∞} {c : ℕ} [inst : c.AtLeastTwo], a + OfNat.ofNat c = b + OfNat.ofNat c ↔ a = b
-- Mathlib.Order.Lattice.Congruence
_private.Mathlib.Order.Lattice.Congruence.0.LatticeCon.closed_interval : ∀ {α : Type u_2} [inst : Lattice α] {r : α → α → Prop},
  (∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)) →
    (∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)) →
      ∀ (a b c d : α), a ≤ b → b ≤ d → a ≤ c → c ≤ d → r a d → r b c
-- Mathlib.Algebra.Category.Grp.Ulift
GrpCat.uliftFunctorFullyFaithful.eq_1 : GrpCat.uliftFunctorFullyFaithful =
  {
    preimage := fun {X Y} f =>
      GrpCat.ofHom (MulEquiv.ulift.toMonoidHom.comp ((GrpCat.Hom.hom f).comp MulEquiv.ulift.symm.toMonoidHom)),
    map_preimage := @GrpCat.uliftFunctorFullyFaithful._proof_1,
    preimage_map := @GrpCat.uliftFunctorFullyFaithful._proof_2 }