mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Defs
Filter.mk.inj : ∀ {α : Type u_1} {sets : Set (Set α)} {univ_sets : Set.univ ∈ sets}
  {sets_of_superset : ∀ {x y : Set α}, x ∈ sets → x ⊆ y → y ∈ sets}
  {inter_sets : ∀ {x y : Set α}, x ∈ sets → y ∈ sets → x ∩ y ∈ sets} {sets_1 : Set (Set α)}
  {univ_sets_1 : Set.univ ∈ sets_1} {sets_of_superset_1 : ∀ {x y : Set α}, x ∈ sets_1 → x ⊆ y → y ∈ sets_1}
  {inter_sets_1 : ∀ {x y : Set α}, x ∈ sets_1 → y ∈ sets_1 → x ∩ y ∈ sets_1},
  { sets := sets, univ_sets := univ_sets, sets_of_superset := sets_of_superset, inter_sets := inter_sets } =
      { sets := sets_1, univ_sets := univ_sets_1, sets_of_superset := sets_of_superset_1, inter_sets := inter_sets_1 } →
    sets = sets_1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_zero_right_eq_empty : ∀ {m : ℕ}, (m...0).toArray = #[]
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.addMonoidWithOne : {α : Type u_1} →
  [inst : AddMonoidWithOne α] →
    [inst_1 : PartialOrder α] → [AddLeftMono α] → [ZeroLEOneClass α] → AddMonoidWithOne { x // 0 ≤ x }
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.ninePointCircle_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂),
  (s.map f.toAffineMap ⋯).ninePointCircle = { center := f s.ninePointCircle.center, radius := s.ninePointCircle.radius }
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.hom_ext : ∀ {X Y : SFinKer} {κ η : X ⟶ Y}, κ.hom = η.hom → κ = η
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.orElse_EStateM : ∀ {ε σ α : Type} (x : EStateM ε σ α) (h : Unit → EStateM ε σ α) (post : α → σ → Prop) (epost : ε → σ → Prop),
  ⦃ fun s => Std.Internal.Do.wp x post (fun x s' => Std.Internal.Do.wp (h ()) post epost s') s ⦄ OrElse.orElse x h ⦃
    post; epost ⦄
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The trivial subsemigroup `∅` of a magma `M`.  -/
Subsemigroup.instBot : {M : Type u_1} → [inst : Mul M] → Bot (Subsemigroup M)
-- Mathlib.RingTheory.WittVector.Basic
/-- `WittVector.ghostMap` is a ring homomorphism that maps each Witt vector
to the sequence of its ghost components.  -/
WittVector.ghostMap : {p : ℕ} → {R : Type u_1} → [inst : CommRing R] → [inst_1 : Fact (Nat.Prime p)] → WittVector p R →+* ℕ → R
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- `ContinuousLinearMap.snd` has a continuous right inverse.  -/
ContinuousLinearMap.HasRightInverse.snd : ∀ {R : Type u_1} [inst : Semiring R] {F : Type u_4} {G : Type u_6} [inst_1 : TopologicalSpace F]
  [inst_2 : AddCommMonoid F] [inst_3 : Module R F] [inst_4 : TopologicalSpace G] [inst_5 : AddCommMonoid G]
  [inst_6 : Module R G], (ContinuousLinearMap.snd R F G).HasRightInverse
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isEmpty_filterMap_eq_true : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l).isEmpty = true ↔
      ∀ (k : α) (h : Std.Internal.List.containsKey k l = true),
        f (Std.Internal.List.getKey k l h) (Std.Internal.List.getValue k l h) = none)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.forget_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} (f : X ⟶ Y), (CategoryTheory.Center.forget C).map f = f.f
-- Mathlib.Analysis.Normed.Group.Basic
coe_comp_nnnorm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], NNReal.toReal ∘ nnnorm = norm
-- Init.Data.String.Lemmas.FindPos
String.posGT.congr_simp : ∀ (s : String) (offset offset_1 : String.Pos.Raw) (e_offset : offset = offset_1) (h : offset < s.rawEndPos),
  s.posGT offset h = s.posGT offset_1 ⋯
-- Init.SimpLemmas
Bool.and_true : ∀ (b : Bool), (b && true) = b
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_sum : ∀ {R : Type u_1} {M : Type u_4} {ι : Type u_7} [inst : Semiring R] (s : Finset ι) (f : ι → M →₀ R),
  MonoidAlgebra.ofCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, MonoidAlgebra.ofCoeff (f i)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
/-- Bijection between a subgroup `H` and its opposite.  -/
Subgroup.equivOp : {G : Type u_2} → [inst : Group G] → (H : Subgroup G) → ↥H ≃ ↥H.op
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_union_toMeasurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  μ (s ∪ MeasureTheory.toMeasurable μ t) = μ (s ∪ t)
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.hom_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Lean.Data.Position
Lean.Position.instToString : ToString Lean.Position
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
measurable_derivWithin_Ici : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [CompleteSpace F]
  [inst_3 : MeasurableSpace F] [BorelSpace F], Measurable fun x => derivWithin f (Set.Ici x) x
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : C} (f : X ⟶ Y), J.yonedaEquiv (J.yoneda.map f) = f
-- Mathlib.Data.List.FinRange
Equiv.Perm.map_finRange_perm : ∀ {n : ℕ} (σ : Equiv.Perm (Fin n)), (List.map (⇑σ) (List.finRange n)).Perm (List.finRange n)
-- Mathlib.Order.MinMax
/-- An instance asserting that `max a a = a`  -/
max_idem : ∀ {α : Type u} [inst : LinearOrder α], Std.IdempotentOp max
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
/-- Given a `NonUnitalContinuousFunctionalCalculus S A q`. If we form the predicate `p` for `a : A`
characterized by: `q a` and the quasispectrum of `a` restricts to the scalar subring `R` via
`f : C(S, R)`, then we can get a restricted functional calculus
`NonUnitalContinuousFunctionalCalculus R A p`.  -/
QuasispectrumRestricts.nonUnitalClosedEmbeddingCFC : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Field S]
  [inst_6 : StarRing S] [inst_7 : MetricSpace S] [inst_8 : IsTopologicalRing S] [inst_9 : ContinuousStar S]
  [inst_10 : NonUnitalRing A] [inst_11 : StarRing A] [inst_12 : Module S A] [inst_13 : IsScalarTower S A A]
  [inst_14 : SMulCommClass S A A] [inst_15 : Algebra R S] [inst_16 : Module R A] [IsScalarTower R S A] [StarModule R S]
  [ContinuousSMul R S] [inst_20 : TopologicalSpace A] [NonUnitalClosedEmbeddingContinuousFunctionalCalculus S A q]
  [inst_22 : IsScalarTower R A A] [inst_23 : SMulCommClass R A A] [ContinuousMapZero.UniqueHom R A] [CompleteSpace R]
  (f : C(S, R)),
  IsUniformEmbedding ⇑(algebraMap R S) →
    p 0 →
      (∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f) → NonUnitalClosedEmbeddingContinuousFunctionalCalculus R A p
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.Grpd.freeForgetAdjunction_unit_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{u, u} C],
  (CategoryTheory.Grpd.freeForgetAdjunction.unit.app (CategoryTheory.Cat.of C)).toFunctor =
    CategoryTheory.FreeGroupoid.of C
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.pop : {K : Type u_1} → {Γ : K → Type u_2} → {σ : Type u_4} → {k : K} → (σ → Option (Γ k) → σ) → Turing.TM2to1.StAct K Γ σ k
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.image_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M M' : CategoryTheory.Functor C MonCat} (p : M ⟶ M')
  (S : CategoryTheory.SubmonoidFunctor M) (x : C),
  (CategoryTheory.SubmonoidFunctor.image p S).obj x = Submonoid.map (MonCat.Hom.hom (p.app x)) (S.obj x)
-- Mathlib.Order.SuccPred.Limit
/-- Recursion principle on a well-founded partial `PredOrder`, separating out the case of a
minimal element.  -/
PredOrder.colimitRecOn : {α : Type u_1} →
  (b : α) →
    {motive : α → Sort u_2} →
      [inst : PartialOrder α] →
        [inst_1 : PredOrder α] →
          [WellFoundedGT α] →
            ((a : α) → IsMax a → motive a) →
              ((a : α) → ¬IsMin a → motive a → motive (Order.pred a)) →
                ((a : α) → Order.IsPredLimit a → ((b : α) → a < b → motive b) → motive a) → motive b
-- Mathlib.GroupTheory.Perm.DomMulAct
/-- The cardinality of the type of permutations preserving a function
(without the finiteness assumption on target)  -/
DomMulAct.stabilizer_card' : ∀ {α : Type u_1} {ι : Type u_2} (f : α → ι) [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableEq ι],
  Fintype.card { g // f ∘ ⇑g = f } = ∏ i ∈ Finset.image f Finset.univ, (Fintype.card { a // f a = i }).factorial
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
    (∀ a ∈ t, l.contains a = false) → (t.insertMany l).size = t.size + l.length
-- Init.Data.Rat.Basic
Rat.normalize.reduced : ∀ {num : ℤ} {den g : ℕ}, den ≠ 0 → g = num.natAbs.gcd den → (num / ↑g).natAbs.Coprime (den / g)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.mk_eq_iff : ∀ {K : Type u_1} [inst : Field K] {φ ψ : K →+* ℂ},
  NumberField.InfinitePlace.mk φ = NumberField.InfinitePlace.mk ψ ↔ φ = ψ ∨ NumberField.ComplexEmbedding.conjugate φ = ψ
-- Mathlib.Analysis.Normed.Group.Hom
/-- The composition of continuous normed group homs.  -/
NormedAddGroupHom.comp : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    {V₃ : Type u_4} →
      [inst : SeminormedAddCommGroup V₁] →
        [inst_1 : SeminormedAddCommGroup V₂] →
          [inst_2 : SeminormedAddCommGroup V₃] →
            NormedAddGroupHom V₂ V₃ → NormedAddGroupHom V₁ V₂ → NormedAddGroupHom V₁ V₃
-- Mathlib.Order.CompleteLattice.Basic
Prod.swap_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : SupSet α] [inst_1 : SupSet β] (f : ι → α × β),
  (iSup f).swap = ⨆ i, (f i).swap
-- Mathlib.Analysis.Complex.Liouville
/-- **Liouville's theorem**: a complex differentiable bounded function is a constant.  -/
Differentiable.exists_const_forall_eq_of_bounded : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F},
  Differentiable ℂ f → Bornology.IsBounded (Set.range f) → ∃ c, ∀ (z : E), f z = c
-- Init.Data.BitVec.Bitblast
/-- The result of `umod` agrees with the result of the division recurrence.  -/
BitVec.umod_eq_divRec : ∀ {w : ℕ} {d n : BitVec w},
  0#w < d →
    have out := BitVec.divRec w { n := n, d := d } (BitVec.DivModState.init w);
    n % d = out.r
-- Init.Control.State
/-- Recovers from errors. The state is rolled back on error recovery. Typically used via the `<|>`
operator.
 -/
StateT.orElse : {σ : Type u} →
  {m : Type u → Type v} → [Alternative m] → {α : Type u} → StateT σ m α → (Unit → StateT σ m α) → StateT σ m α
-- Mathlib.Data.PSigma.Order
PSigma.Lex.noMaxOrder_of_nonempty : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)] [NoMaxOrder ι]
  [∀ (i : ι), Nonempty (α i)], NoMaxOrder (Σₗ' (i : ι), α i)
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_div_hasSum_exp : ∀ {𝔸 : Type u_1} [inst : NormedDivisionRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (x : 𝔸),
  HasSum (fun n => x ^ n / ↑n.factorial) (NormedSpace.exp x)
-- Mathlib.Algebra.Order.Monoid.Basic
/-- The order embedding sending `b` to `b + a`, for some fixed `a`.
See also `OrderIso.addRight` when working in an additive ordered group.  -/
OrderEmbedding.addRight : {α : Type u_2} → [inst : Add α] → [inst_1 : LinearOrder α] → [AddRightStrictMono α] → α → α ↪o α
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.comp_mapComp_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictPseudofunctor B C)
  (G : CategoryTheory.StrictPseudofunctor C D) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  ((F.comp G).mapComp f g).inv =
    CategoryTheory.CategoryStruct.comp (G.mapComp (F.map f) (F.map g)).inv (G.map₂ (F.mapComp f g).inv)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_fintype : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  [L.LeAtTop] [inst_3 : Fintype β] (f : β → α), ∑'[L] (b : β), f b = ∑ b, f b
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Section.exists_eq_inl_mul : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} (σ σ' : S.Section) (g : G), ∃ n, σ g = S.inl n * σ' g
-- Mathlib.Analysis.Analytic.Basic
hasFPowerSeriesWithinAt_iff_of_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} (f : E → F)
  (p : FormalMultilinearSeries 𝕜 E F) {U : Set E},
  U ∈ nhds x → (HasFPowerSeriesWithinAt f p U x ↔ HasFPowerSeriesAt f p x)
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.merge.match_1.eq_4 : ∀ {α : Type u_1} (motive : Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α → Sort u_2) (a₁ : α)
  (c₁ sibling : Batteries.PairingHeapImp.Heap α) (a₂ : α) (c₂ sibling_1 : Batteries.PairingHeapImp.Heap α)
  (h_1 : Unit → motive Batteries.PairingHeapImp.Heap.nil Batteries.PairingHeapImp.Heap.nil)
  (h_2 :
    (a₂ : α) →
      (c₂ sibling : Batteries.PairingHeapImp.Heap α) →
        motive Batteries.PairingHeapImp.Heap.nil (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling))
  (h_3 :
    (a₁ : α) →
      (c₁ sibling : Batteries.PairingHeapImp.Heap α) →
        motive (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling) Batteries.PairingHeapImp.Heap.nil)
  (h_4 :
    (a₁ : α) →
      (c₁ sibling : Batteries.PairingHeapImp.Heap α) →
        (a₂ : α) →
          (c₂ sibling_2 : Batteries.PairingHeapImp.Heap α) →
            motive (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling)
              (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling_2)),
  (match Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling, Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling_1 with
    | Batteries.PairingHeapImp.Heap.nil, Batteries.PairingHeapImp.Heap.nil => h_1 ()
    | Batteries.PairingHeapImp.Heap.nil, Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling => h_2 a₂ c₂ sibling
    | Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling, Batteries.PairingHeapImp.Heap.nil => h_3 a₁ c₁ sibling
    | Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling, Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling_2 =>
      h_4 a₁ c₁ sibling a₂ c₂ sibling_2) =
    h_4 a₁ c₁ sibling a₂ c₂ sibling_1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_map : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X₀ W₀ : C₀}
  (a : W₀ ⟶ X₀) {i : (data (F.obj X₀)).I₀} (p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)),
  CategoryTheory.CategoryStruct.comp p ((data (F.obj X₀)).f i) = F.map a →
    CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom data G₀ X₀) (G₀.obj.map a.op) =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ (F.obj X₀) i)
        (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ p)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_forall_mem_unit_iff : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.DTreeMap.Raw α (fun x => Unit) cmp}, t₁.WF → t₂.WF → (∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) → t₁.Equiv t₂
-- Lean.CoreM
/-- Cache for instantiating universe polymorphic declarations.  -/
Lean.Core.State.cache : Lean.Core.State → Lean.Core.Cache
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Complex.hasStrictDerivAt_log : ∀ {x : ℂ}, x ∈ Complex.slitPlane → HasStrictDerivAt Complex.log x⁻¹ x
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instInvolutiveNeg : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [InvolutiveNeg G] → InvolutiveNeg (l.Germ G)
-- Std.Data.DHashMap.Basic
Std.DHashMap.mk.inj : ∀ {α : Type u} {β : α → Type v} {inst : BEq α} {inst_1 : Hashable α} {inner : Std.DHashMap.Raw α β} {wf : inner.WF}
  {inner_1 : Std.DHashMap.Raw α β} {wf_1 : inner_1.WF},
  { inner := inner, wf := wf } = { inner := inner_1, wf := wf_1 } → inner = inner_1
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.addAux.match_3.eq_1 : ∀ (motive : ONote → Sort u_1) (h_1 : Unit → motive ONote.zero)
  (h_2 : (o' e' : ONote) → (n' : ℕ+) → (a' : ONote) → o' = e'.oadd n' a' → motive (e'.oadd n' a')),
  (match ONote.zero with
    | ONote.zero => h_1 ()
    | o'@h:(e'.oadd n' a') => h_2 o' e' n' a' h) =
    h_1 ()
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.mkIso'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} (e : G ≅ H) [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H]
  [inst_4 : CategoryTheory.IsAddMonHom e.hom],
  CategoryTheory.AddGrp.mkIso' e =
    (CategoryTheory.AddGrp.fullyFaithfulForget₂Mon C).preimageIso (CategoryTheory.AddMon.mkIso' e)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.coeff_mul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ},
  (x * y).coeff a = ∑ ij ∈ Finset.antidiagonal ⋯ ⋯ a, x.coeff ij.1 * y.coeff ij.2
-- Mathlib.GroupTheory.Complement
AddSubgroup.instAddActionLeftTransversal.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {F : Type u_2} [inst_1 : AddGroup F] [inst_2 : AddAction F G]
  [inst_3 : AddAction.QuotientAction F H],
  AddSubgroup.instAddActionLeftTransversal = { vadd := fun f T => ⟨f +ᵥ ↑T, ⋯⟩, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Topology.UniformSpace.OfFun
UniformSpace.hasBasis_ofFun : ∀ {X : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder M],
  (∃ x, 0 < x) →
    ∀ (d : X → X → M) (refl : ∀ (x : X), d x x = 0) (symm : ∀ (x y : X), d x y = d y x)
      (triangle : ∀ (x y z : X), d x z ≤ d x y + d y z) (half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε),
      (uniformity X).HasBasis (fun x => 0 < x) fun ε => {x | d x.1 x.2 < ε}
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_one : Rat.toNNRat 1 = 1
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
CategoryTheory.Over.sectionsCurry_sectionUncurry : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {I : C} [inst_2 : CategoryTheory.Closed I]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)]
  [inst_4 : CategoryTheory.BraidedCategory C] {X : CategoryTheory.Over I} {A : C}
  {v : A ⟶ (CategoryTheory.Over.sections I).obj X},
  CategoryTheory.Over.sectionsCurry (CategoryTheory.Over.sectionsUncurry v) = v
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.MonObj A]
  (X : C),
  (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A).obj X =
    CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj A X
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm' : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] {ι : Type u_4} {fi : Filter ι} [inst_1 : Fact (1 ≤ p)]
  (f : ι → ↥(MeasureTheory.Lp E p μ)) (f_lim : ↥(MeasureTheory.Lp E p μ)),
  Filter.Tendsto f fi (nhds f_lim) ↔ Filter.Tendsto (fun n => MeasureTheory.eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (nhds 0)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instPow : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : Monoid G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [ContMDiffMul I' n G] → Pow (ContMDiffMap I I' N G n) ℕ
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- A metric outer measure is additive on a finite set of pairwise metric separated sets.  -/
MeasureTheory.OuterMeasure.IsMetric.finset_iUnion_of_pairwise_separated : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {μ : MeasureTheory.OuterMeasure X},
  μ.IsMetric →
    ∀ {I : Finset ι} {s : ι → Set X},
      (∀ i ∈ I, ∀ j ∈ I, i ≠ j → Metric.AreSeparated (s i) (s j)) → μ (⋃ i ∈ I, s i) = ∑ i ∈ I, μ (s i)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindex.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (e : ι ≃ ι'), b.reindex e = { repr := b.repr ≪≫ₗ Finsupp.domLCongr e }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Limits.HasPushout.comp_left_left_iff_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} {X' : C} (i : X ⟶ X')
  [CategoryTheory.IsIso i],
  CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp f i) g ↔ CategoryTheory.Limits.HasPushout f g