mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainRingHom.eq_1 : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (f : M →+ N),
  AddMonoidAlgebra.mapDomainRingHom R f =
    { toFun := AddMonoidAlgebra.mapDomain ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_le_of_le : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ}
  [IsStrictOrderedRing R], a ≤ ↑n → ⌊a⌋₊ ≤ n
-- Batteries.Lean.AttributeExtra
Lean.instInhabitedTagAttributeExtra : Inhabited Lean.TagAttributeExtra
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.End.equivAddOpposite.eq_1 : ∀ {M : Type u_2} [inst : AddMonoid M],
  AddActionHom.End.equivAddOpposite =
    { toFun := fun f => AddOpposite.op (f 0),
      invFun := fun m => { toFun := fun x => x + AddOpposite.unop m, map_vadd' := ⋯ }, left_inv := ⋯, right_inv := ⋯,
      map_add' := ⋯ }
-- Mathlib.Data.Fintype.Defs
Fintype.decidableEqEquivFintype : {α : Type u_1} → {β : Type u_2} → [DecidableEq β] → [Fintype α] → DecidableEq (α ≃ β)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.interSmallerFn_eq_interSmallerFnₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m sofar : Std.DHashMap.Internal.Raw₀ α β) (k : α),
  m.interSmallerFn sofar k = m.interSmallerFnₘ sofar k
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_natCast_zmodRepr : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), (↑x.zmodRepr).zmodRepr = x.zmodRepr
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Equiv.union_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₃).WF → (↑m₂).Equiv ↑m₃ → (↑(m₁.union m₂)).Equiv ↑(m₁.union m₃)
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_lt_self_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] {a : R},
  ↑⌊a⌋ < a ↔ a ∉ Set.range Int.cast
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_lt : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι],
  MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.minEntry!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited ((a : α) × β a)], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minEntry! = t₂.minEntry!
-- Lean.DocString.Parser
/-- Parses any inline element.
 -/
Lean.Doc.Parser.inline : Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList_eq_nil : ∀ (n : ℕ), n.primeFactorsList = [] ↔ n = 0 ∨ n = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_mapIso_mkNatIso_eq_mkIso : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J K : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)}
  (e₁ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G))
  (e₂ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G))
  (coh :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom F)
          (CategoryTheory.CategoryStruct.comp (K.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
            (CategoryTheory.CategoryStruct.comp
              (K.whiskerLeft
                (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                    (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
              (K.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv)) =
        CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
          (CategoryTheory.CategoryStruct.comp
            (J.whiskerLeft
              (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                  (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
            (CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv
              (CategoryTheory.Functor.whiskerRight e₂.hom G))))
      CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_mapIso_mkNatIso_eq_mkIso._auto_1),
  (CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X).mapIso
      (CategoryTheory.Limits.CategoricalPullback.mkNatIso e₁ e₂ coh) =
    CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso e₁ e₂ ⋯
-- Mathlib.Algebra.Notation
OneLePart.mk : {α : Type u_1} → (α → α) → OneLePart α
-- Std.Do.SPred.SVal
Std.Do.SVal.uncurry_nil : ∀ {σ : Type u} {s : σ}, Std.Do.SVal.uncurry s = fun x => s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_eq_getLast?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey? = t.keys.getLast?
-- Mathlib.Data.Seq.Defs
Stream'.Seq.ofList_get? : ∀ {α : Type u} (l : List α) (n : ℕ), (↑l).get? n = l[n]?
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.closure_image_eq : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsClosedEmbedding f → ∀ (s : Set X), closure (f '' s) = f '' closure s
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- `Additive (∀ i : ι, K i)` is equivalent to `∀ i : ι, Additive (K i)`.  -/
AddEquiv.piAdditive : {ι : Type u_1} →
  (K : ι → Type u_4) → [inst : (i : ι) → Mul (K i)] → Additive ((i : ι) → K i) ≃+ ((i : ι) → Additive (K i))
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.nontrivial_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N : AddSubgroup G}, Nontrivial (G ⧸ N) ↔ N ≠ ⊤
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.brecOn.go : {C : Type u} →
  {motive : (a a_1 : CategoryTheory.FreeMonoidalCategory C) → a.Hom a_1 → Sort u_1} →
    {a a_1 : CategoryTheory.FreeMonoidalCategory C} →
      (t : a.Hom a_1) →
        ((a a_2 : CategoryTheory.FreeMonoidalCategory C) →
            (t : a.Hom a_2) → CategoryTheory.FreeMonoidalCategory.Hom.below t → motive a a_2 t) →
          motive a a_1 t ×' CategoryTheory.FreeMonoidalCategory.Hom.below t
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- An affine equivalence, denoted `P₁ ≃ᵃ[k] P₂`, is an equivalence between affine spaces
such that both forward and inverse maps are affine.

We define it using an `Equiv` for the map and a `LinearEquiv` for the linear part in order
to allow affine equivalences with good definitional equalities.  -/
AffineEquiv : (k : Type u_1) →
  (P₁ : Type u_2) →
    (P₂ : Type u_3) →
      {V₁ : Type u_4} →
        {V₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [Module k V₁] →
                  [Module k V₂] → [AddTorsor V₁ P₁] → [AddTorsor V₂ P₂] → Type (max (max (max u_2 u_3) u_4) u_5)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.getLsbD.injEq : ∀ {w : ℕ} (expr : Std.Tactic.BVDecide.BVExpr w) (idx w_1 : ℕ) (expr_1 : Std.Tactic.BVDecide.BVExpr w_1) (idx_1 : ℕ),
  (Std.Tactic.BVDecide.BVPred.getLsbD expr idx = Std.Tactic.BVDecide.BVPred.getLsbD expr_1 idx_1) =
    (w = w_1 ∧ expr ≍ expr_1 ∧ idx = idx_1)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instFaithfulSMul_1 : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : Semiring R]
  (v : AbsoluteValue R S) [inst_3 : SMul T R] [FaithfulSMul T R], FaithfulSMul T (WithAbs v)
-- Mathlib.Data.Num.Lemmas
PosNum.commMonoid : CommMonoid PosNum
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.coforkOfCokernelCofork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.CokernelCofork (f - g)), (CategoryTheory.Preadditive.coforkOfCokernelCofork c).pt = c.pt
-- Mathlib.Analysis.Fourier.Notation
FourierModule.mk : {R : Type u_5} →
  {E : Type u_6} →
    {F : outParam (Type u_7)} →
      [inst : Add E] →
        [inst_1 : Add F] →
          [inst_2 : SMul R E] →
            [inst_3 : SMul R F] →
              (toFourierTransform : FourierTransform E F) →
                (∀ (f g : E),
                    FourierTransform.fourier (f + g) = FourierTransform.fourier f + FourierTransform.fourier g) →
                  (∀ (r : R) (f : E), FourierTransform.fourier (r • f) = r • FourierTransform.fourier f) →
                    FourierModule R E F
-- Mathlib.Geometry.Convex.Hull
Convexity.mem_convexHull_iff : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X} {x : X},
  x ∈ (Convexity.convexHull R) s ↔ ∀ (t : Set X), s ⊆ t → Convexity.IsConvexSet R t → x ∈ t
-- Mathlib.Data.Complex.Basic
Complex.normSq_add : ∀ (z w : ℂ), Complex.normSq (z + w) = Complex.normSq z + Complex.normSq w + 2 * (z * (starRingEnd ℂ) w).re
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.isoApp_hom : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y), (CategoryTheory.DifferentialObject.isoApp f).hom = f.hom.f
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Localization.mulEquivOfQuotient_monoidOf : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f : S.LocalizationMap N} (x : M), (Localization.mulEquivOfQuotient f) ((Localization.monoidOf S) x) = f x
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.smul_toEquiv : ∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [inst_3 : MeasurableConstSMul G α] (c : G), (MeasurableEquiv.smul c).toEquiv = MulAction.toPerm c
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Returns `.true` if `c` is satisfied by the current partial model,
`.undef` if `c` contains unassigned variables, and `.false` otherwise.
 -/
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.satisfied : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.GoalM Lean.LBool
-- Mathlib.Data.Num.Lemmas
PosNum.succ.eq_def : ∀ (x : PosNum),
  x.succ =
    match x with
    | PosNum.one => PosNum.one.bit0
    | n.bit1 => n.succ.bit0
    | n.bit0 => n.bit1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.instCategoryAugmented : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Category.{v, max u v} (CategoryTheory.CosimplicialObject.Augmented C)
-- Lean.Elab.InfoTree.Types
Lean.Elab.DelabTermInfo.toTermInfo : Lean.Elab.DelabTermInfo → Lean.Elab.TermInfo
-- Mathlib.Algebra.Group.Center
Set.sub_mem_addCenter : ∀ {M : Type u_1} [inst : SubtractionMonoid M] {a b : M},
  a ∈ Set.addCenter M → b ∈ Set.addCenter M → a - b ∈ Set.addCenter M
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.μIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C),
  (CategoryTheory.Functor.Monoidal.μIso F X Y).hom = CategoryTheory.Functor.LaxMonoidal.μ F X Y
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_X_of_ne_one : ∀ {R : Type u} [inst : Semiring R] {n : ℕ}, n ≠ 1 → Polynomial.X.coeff n = 0
-- Init.Data.Fin.Lemmas
Fin.ext : ∀ {n : ℕ} {a b : Fin n}, ↑a = ↑b → a = b
-- Mathlib.Order.Interval.Finset.Nat
Nat.decreasing_induction_of_not_bddAbove : ∀ {P : ℕ → Prop}, (∀ (n : ℕ), P (n + 1) → P n) → ¬BddAbove {x | P x} → ∀ (n : ℕ), P n
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g g' : M → M'} {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    (∀ y ∈ s, g' y = g y) →
      g' x = g x → (ChartedSpace.LiftPropWithinAt P g' s x ↔ ChartedSpace.LiftPropWithinAt P g s x)
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.isHomLift_cartesianLift : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {R S : 𝒮}
  (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S),
  (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsHomLift f
    (CategoryTheory.Pseudofunctor.CoGrothendieck.cartesianLift a f)
-- Lean.Data.OpenDecl
Lean.rootNamespace : Lean.Name
-- Lean.Environment
Lean.instInhabitedVisibilityMap.default : {α : Type} → [Inhabited α] → Lean.VisibilityMap✝ α
-- Init.Data.Order.PackageFactories
Std.PreorderPackage.toLT : {α : Type u} → [self : Std.PreorderPackage α] → LT α
-- Mathlib.CategoryTheory.Iso
CategoryTheory.comp_hom_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (g : Y ⟶ X) [inst_1 : CategoryTheory.IsIso g]
  {f : X ⟶ Y}, CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X ↔ f = CategoryTheory.inv g
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.diff.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m₁ m₁_1 : Std.ExtDHashMap α β),
  m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtDHashMap α β), m₂ = m₂_1 → m₁.diff m₂ = m₁_1.diff m₂_1
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.conjTranspose_kronecker : ∀ {R : Type u_1} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : CommMagma R]
  [inst_1 : StarMul R] (x : Matrix l m R) (y : Matrix n p R),
  (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y).conjTranspose =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x.conjTranspose y.conjTranspose
-- Mathlib.Analysis.SpecificLimits.Normed
tendsto_smul_comp_nat_floor_of_tendsto_mul : ∀ {R : Type u_4} {K : Type u_5} [inst : NormedRing K] [inst_1 : NormedRing R] [inst_2 : Module K R]
  [Module.IsTorsionFree K R] [NormSMulClass K R] [NormSMulClass ℤ K] [inst_6 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_8 : FloorSemiring K] [HasSolidNorm K] {g : ℕ → R} {t : R},
  Filter.Tendsto (fun n => ↑n * g n) Filter.atTop (nhds t) → Filter.Tendsto (fun x => x • g ⌊x⌋₊) Filter.atTop (nhds t)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.transfer.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (H : SimpleGraph V) (v_2 : V) (h_2 : G.Adj u v_2) (p_2 : G.Walk v_2 v)
  (h_3 : ∀ e ∈ (SimpleGraph.Walk.cons' u v_2 v h_2 p_2).edges, e ∈ H.edgeSet),
  (SimpleGraph.Walk.cons h_2 p_2).transfer H h_3 = SimpleGraph.Walk.cons ⋯ (p_2.transfer H ⋯)
-- Init.Data.SInt.Basic
instDivInt32 : Div Int32
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_b_ne_zero' : ∀ {R : Type u_1} {b c d : R} [inst : Semiring R], b ≠ 0 → { a := 0, b := b, c := c, d := d }.toPoly.natDegree = 2
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instGOneIntOfHasDetPlusMinusOneFinOfNatNatReal : (Γ : Subgroup (GL (Fin 2) ℝ)) → [Γ.HasDetPlusMinusOne] → GradedMonoid.GOne (ModularForm Γ)
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.divOf_add : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G]
  (x : AddMonoidAlgebra k G) (a b : G), x.divOf (a + b) = (x.divOf a).divOf b
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasStrictDerivAt.congr_simp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousSMul 𝕜 F] (f f_1 : 𝕜 → F),
  f = f_1 →
    ∀ (f' f'_1 : F), f' = f'_1 → ∀ (x x_1 : 𝕜), x = x_1 → HasStrictDerivAt f f' x = HasStrictDerivAt f_1 f'_1 x_1
-- Mathlib.Data.List.FinRange
List.idxOf_finRange : ∀ {k : ℕ} (i : Fin k), List.idxOf i (List.finRange k) = ↑i
-- Mathlib.Order.Filter.Map
Filter.mem_comap : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} {s : Set α}, s ∈ Filter.comap m g ↔ ∃ t ∈ g, m ⁻¹' t ⊆ s
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.tensorObj_carrier : ∀ (X Y : SFinKer), (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).carrier = (X.carrier × Y.carrier)
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.factor_eval_liftRingHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m)
  (n : ℕ) (x : R) (h : I ^ n • ⊤ ≤ I ^ n),
  (Submodule.factor h) ((AdicCompletion.eval I S n) ((AdicCompletion.liftRingHom I f ⋯) x)) = (f n) x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.IsCycle.exists_isCycle_snd_verts_eq : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v v},
  p.IsCycle → p.toSubgraph.Adj v w → ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.freeAdjunction_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat)
  (F : CategoryTheory.Functor Cᵒᵖ (Type u)),
  (PresheafOfModules.freeAdjunction R).unit.app F = PresheafOfModules.freeAdjunctionUnit R F
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  m.WF → m.getKey? k = some k' → (Std.HashMap.Raw.filterMap f m)[k]! = (m[k]?.bind fun x => f k' x).get!
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.comap_comap : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : Semiring A] [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B]
  [inst_7 : StarRing B] [inst_8 : Algebra R B] [inst_9 : StarModule R B] [inst_10 : Semiring C] [inst_11 : StarRing C]
  [inst_12 : Algebra R C] [inst_13 : StarModule R C] (S : StarSubalgebra R C) (g : B →⋆ₐ[R] C) (f : A →⋆ₐ[R] B),
  StarSubalgebra.comap f (StarSubalgebra.comap g S) = StarSubalgebra.comap (g.comp f) S
-- Mathlib.CategoryTheory.Functor.FunctorHom
/-- When `F`, `G`, and `A` are all functors `C ⥤ Type w`, then `HomObj F G A` is in
bijection with `F ⊗ A ⟶ G`.  -/
CategoryTheory.Functor.homObjEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G A : CategoryTheory.Functor C (Type w)) →
      F.HomObj G A ≃ (CategoryTheory.MonoidalCategoryStruct.tensorObj F A ⟶ G)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Assume that
1. `C` has binary products and pullbacks,
2. `D` has pullbacks, binary products and a terminal object, and
3. `F : C ⥤ D` is full and preserves binary products and pullbacks.

For an object `X` in a category `D`, the diagonal morphism `X ⟶ X × X` is relatively representable
with respect to `F` if and only if so is every morphism of the form `F.obj a ⟶ X`.
 -/
CategoryTheory.Functor.relativelyRepresentable.diag_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks D]
  [inst_4 : CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {X : D}
  [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F],
  F.relativelyRepresentable (CategoryTheory.Limits.diag X) ↔ ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.exists_basis : ∀ (K : Type u_3) (V : Type u_4) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  ∃ s, Nonempty (Module.Basis (↑s) K V)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- If `μ` has finite spanning sets in the collection of measurable sets `C`, then `μ` is σ-finite.
 -/
MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)}
  (h : μ.FiniteSpanningSetsIn C), MeasureTheory.SigmaFinite μ
-- Lean.Attributes
Lean.TagAttribute.mk.injEq : ∀ (attr : Lean.AttributeImpl) (ext : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet)
  (attr_1 : Lean.AttributeImpl) (ext_1 : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet),
  ({ attr := attr, ext := ext } = { attr := attr_1, ext := ext_1 }) = (attr = attr_1 ∧ ext = ext_1)
-- Mathlib.Data.Set.Lattice.Image
Set.biUnion_iInter_of_pairwise_disjoint : ∀ {α : Type u_1} {ι : Type u_9} {κ : Type u_10} [hκ : Nonempty κ] {f : ι → Set α},
  Pairwise (Function.onFun Disjoint f) → ∀ (s : κ → Set ι), ⋃ i ∈ ⋂ j, s j, f i = ⋂ j, ⋃ i ∈ s j, f i
-- Mathlib.Data.FunLike.Group
FunLike.subtractionMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : Neg F] [inst_5 : Sub F] [inst_6 : SMul ℤ F] [inst_7 : SubtractionMonoid β]
  [inst_8 : IsZeroApply F α β] [inst_9 : IsAddApply F α β] [inst_10 : IsNegApply F α β] [inst_11 : IsSubApply F α β]
  [inst_12 : IsSMulApply ℕ F α β] [inst_13 : IsSMulApply ℤ F α β],
  FunLike.subtractionMonoid = Function.Injective.subtractionMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Nat.MaxPowDiv
Nat.fst_maxPowDvdDiv : ∀ (p n : ℕ), (p.maxPowDvdDiv n).1 = padicValNat p n
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.torsionOrder_ne_zero : ∀ (K : Type u_1) [inst : Field K] [NumberField K], NumberField.Units.torsionOrder K ≠ 0
-- Mathlib.Order.WithBot
/-- There is a general version `top_le_iff`, but this lemma does not require a `PartialOrder`.  -/
WithTop.top_le_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithTop α}, ⊤ ≤ x ↔ x = ⊤
-- Mathlib.Topology.Compactness.Lindelof
/-- In a Lindelöf space, `Set.univ` is a Lindelöf set.  -/
LindelofSpace.isLindelof_univ : ∀ {X : Type u_2} {inst : TopologicalSpace X} [self : LindelofSpace X], IsLindelof Set.univ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_insert_le_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k fallback : α}, (cmp ((t.insert k).minD fallback) (t.minD fallback)).isLE = true
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_one : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Equiv.Perm.support 1 = ∅
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- A functor between groupoid defines a map of subgroupoids in the reverse direction
by taking preimages.
 -/
CategoryTheory.Subgroupoid.comap : {C : Type u} →
  [inst : CategoryTheory.Groupoid C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Groupoid D] →
        CategoryTheory.Functor C D → CategoryTheory.Subgroupoid D → CategoryTheory.Subgroupoid C