mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.symm_comp_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e →
    ∀ {x : M}, x ∈ e.source → mfderiv% ↑e.symm (↑e x) ∘SL mfderiv% ↑e x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
-- Lean.Elab.MatchAltView
Lean.Elab.Term.MatchAltView.ref : {k : Lean.SyntaxNodeKinds} → Lean.Elab.Term.MatchAltView k → Lean.Syntax
-- Lean.Expr
Lean.Expr.sort.injEq : ∀ (u u_1 : Lean.Level), (Lean.Expr.sort u = Lean.Expr.sort u_1) = (u = u_1)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.instIsScalarTowerRingTensorProductBaseChange : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  {T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T], IsScalarTower R P.Ring P.baseChange.Ring
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_pow : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {x : Submonoid A} (y : HomogeneousLocalization 𝒜 x) (n : ℕ), (y ^ n).val = y.val ^ n
-- Init.Data.String.Defs
String.instDecidableEqPos : {s : String} → DecidableEq s.Pos
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.mem_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {x : B × F}, x ∈ e.target ↔ x.1 ∈ e.baseSet
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.summable_norm_zpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E)
  [DiscreteTopology ↥L], ∀ n < -↑(Module.finrank ℤ ↥L), Summable fun z => ‖z‖ ^ n
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- An `n`-dimensional `InnerProductSpace` equipped with a decomposition as an internal direct
sum has an orthonormal basis indexed by `Fin n` and subordinate to that direct sum. This function
provides the mapping by which it is subordinate.  -/
DirectSum.IsInternal.subordinateOrthonormalBasisIndex : {ι : Type u_7} →
  {𝕜 : Type u_8} →
    [inst : RCLike 𝕜] →
      {E : Type u_9} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [Fintype ι] →
              [FiniteDimensional 𝕜 E] →
                {n : ℕ} →
                  Module.finrank 𝕜 E = n →
                    [inst_5 : DecidableEq ι] →
                      {V : ι → Submodule 𝕜 E} →
                        DirectSum.IsInternal V →
                          Fin n → (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → ι
-- Mathlib.Data.NNReal.Defs
Real.nnabs_natCast : ∀ (n : ℕ), Real.nnabs ↑n = ↑n
-- Mathlib.GroupTheory.EckmannHilton
EckmannHilton.MulOneClass.isUnital : ∀ {X : Type u} [_G : MulOneClass X], EckmannHilton.IsUnital (fun x1 x2 => x1 * x2) 1
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.instBEqSimpKind.beq : Lean.Elab.Tactic.SimpKind → Lean.Elab.Tactic.SimpKind → Bool
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` induces a `G ⧸ S`-representation on
the coinvariants of `ρ|_S`.  -/
Rep.quotientToCoinvariants : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] → Rep.{w, u, v} k G → (S : Subgroup G) → [inst_2 : S.Normal] → Rep.{w, u, v} k (G ⧸ S)
-- Mathlib.Topology.ShrinkingLemma
/-- Choice of an element of a nonempty chain of partial refinements. If `i` belongs to one of
`carrier v`, `v ∈ c`, then `find c ne i` is one of these partial refinements.  -/
ShrinkingLemma.PartialRefinement.find : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {u : ι → Set X} →
        {s : Set X} →
          {p : Set X → Prop} →
            (c : Set (ShrinkingLemma.PartialRefinement u s p)) → c.Nonempty → ι → ShrinkingLemma.PartialRefinement u s p
-- Mathlib.FieldTheory.Separable
Algebra.IsSeparable.isAlgebraic : ∀ (F : Type u_1) (K : Type u_3) [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K] [Nontrivial F]
  [Algebra.IsSeparable F K], Algebra.IsAlgebraic F K
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.interSmallerFnₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m sofar : Std.DHashMap.Internal.Raw₀ α β) (k : α),
  m.interSmallerFnₘ sofar k =
    match m.getEntry?ₘ k with
    | some kv' => sofar.insertₘ kv'.fst kv'.snd
    | none => sofar
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_subset : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s i ⊆ i
-- Mathlib.Algebra.Star.Basic
/-- `star` as a ring endomorphism, for commutative `R`. This is used to denote complex
conjugation, and is available under the notation `conj` in the scope `ComplexConjugate`.

Note that this is the preferred form (over `starRingAut`, available under the same hypotheses)
because the notation `E →ₗ⋆[R] F` for an `R`-conjugate-linear map (short for
`E →ₛₗ[starRingEnd R] F`) does not pretty-print if there is a coercion involved, as would be the
case for `(↑starRingAut : R →* R)`.  -/
starRingEnd : (R : Type u) → [inst : CommSemiring R] → [StarRing R] → R →+* R
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_apply₀ : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (f : ι → MeasureTheory.Measure α) {s : Set α},
  MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.sum f) →
    (MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s
-- Lean.Elab.Calc
Lean.Elab.Term.mkCalcTrans : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- `nndist x x` vanishes  -/
nndist_self : ∀ {α : Type u} [inst : PseudoMetricSpace α] (a : α), nndist a a = 0
-- Init.Data.SInt.Bitwise
UInt32.toInt32_xor : ∀ (a b : UInt32), (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.PropertyIsLocal.localizationAwayPreserves : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.PropertyIsLocal P → RingHom.LocalizationAwayPreserves P
-- Mathlib.Algebra.Category.ModuleCat.Algebra
/-- Type synonym for considering a module over a `k`-algebra as a `k`-module.  -/
ModuleCat.moduleOfAlgebraModule : {k : Type u} → [inst : Field k] → {A : Type w} → [inst_1 : Ring A] → [Algebra k A] → (M : ModuleCat A) → Module k ↑M
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Topology of `𝔖`-convergence, i.e uniform convergence on the elements of `𝔖`, declared as an
instance on `α →ᵤ[𝔖] β`.  -/
UniformOnFun.topologicalSpace : (α : Type u_1) → (β : Type u_2) → [UniformSpace β] → (𝔖 : Set (Set α)) → TopologicalSpace (UniformOnFun α β 𝔖)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The space of affine maps from `P1` to `P2` is an affine space over the space of affine maps
from `P1` to the vector space `V2` corresponding to `P2`.  -/
AffineMap.instAddTorsor : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [inst_2 : Module k V1] →
                [inst_3 : AddTorsor V1 P1] →
                  [inst_4 : AddCommGroup V2] →
                    [inst_5 : Module k V2] → [inst_6 : AddTorsor V2 P2] → AddTorsor (P1 →ᵃ[k] V2) (P1 →ᵃ[k] P2)
-- Init.Prelude
instTransEq_1 : {α : Sort u_1} → {β : Sort u_2} → (r : α → β → Sort u) → Trans r Eq r
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_maxKey?_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t → t.maxKey?.isSome = true
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.eq_bot_of_card_le_two : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], Nat.card α ≤ 2 → alternatingGroup α = ⊥
-- Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice
/-- Braided structure for the preorder category of a meet-semilattice with a greatest element.  -/
CategoryTheory.SemilatticeInf.braidedCategory : (C : Type u) → [inst : SemilatticeInf C] → [inst_1 : OrderTop C] → CategoryTheory.BraidedCategory C
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.sub_apply : ∀ {M : Type u_2} {G : Type u_5} [inst : AddZeroClass M] [inst_1 : AddCommGroup G] (f g : M →+ G) (x : M),
  (f - g) x = f x - g x
-- Std.Data.Iterators.Consumers.Set
/-- Traverses the given iterator and stores the emitted values in a `ExtTreeSet`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.toExtTreeSet`.
 -/
Std.Iter.Total.toExtTreeSet : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    [Std.Iterators.Finite α Id] →
      [Std.IteratorLoop α Id Id] →
        Std.Iter.Total β →
          (cmp : autoParam (β → β → Ordering) Std.Iter.Total.toExtTreeSet._auto_1) →
            [Std.TransCmp cmp] → Std.ExtTreeSet β cmp
-- Mathlib.Data.PNat.Basic
Nat.succPNat_strictMono : StrictMono Nat.succPNat
-- Mathlib.Algebra.Group.Ext
AddRightCancelMonoid.ext_iff : ∀ {M : Type u} {m₁ m₂ : AddRightCancelMonoid M}, m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpaceCore.chart_mem_atlas : ∀ {H : Type u_5} [inst : TopologicalSpace H] {M : Type u_6} (self : ChartedSpaceCore H M) (x : M),
  self.chartAt x ∈ self.atlas
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] {f : (a : α) → β a → γ a} {k : α},
  (Std.ExtDTreeMap.map f t).getKey! k = t.getKey! k
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- Vertical composition of modifications.  -/
CategoryTheory.Pseudofunctor.StrongTrans.Modification.vcomp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          {η θ ι : F ⟶ G} →
            CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ →
              CategoryTheory.Pseudofunctor.StrongTrans.Modification θ ι →
                CategoryTheory.Pseudofunctor.StrongTrans.Modification η ι
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Submodule.pow_smul_top_le : ∀ {R : Type u_1} [inst : Ring R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m n : ℕ},
  m ≤ n → I ^ n • ⊤ ≤ I ^ m • ⊤
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} [inst_1 : Inhabited (β k)],
      Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter m₂ ⋯).get! k = default
-- Mathlib.NumberTheory.SmoothNumbers
/-- `m` is `s`-factored if and only if `m` is nonzero and all prime divisors `≤ m` of `m`
are in `s`.  -/
Nat.mem_factoredNumbers_iff_forall_le : ∀ {s : Finset ℕ} {m : ℕ}, m ∈ Nat.factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, Nat.Prime p → p ∣ m → p ∈ s
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] (E : Type u'') [inst_4 : CategoryTheory.Category.{v'', u''} E]
  [inst_5 : CategoryTheory.Abelian E] [inst_6 : L.IsLocalization P.isoModSerre] [inst_7 : CategoryTheory.Preadditive D]
  [inst_8 : L.Additive] (G : D ⥤ₑ E),
  ((CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft L P E).obj G).obj = L.comp G.obj
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.mem_genEigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ∞} {x : M}, x ∈ (f.genEigenspace μ) k ↔ ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₄_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  (app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝) (app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝)
  (app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝) (app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝)
  (app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝)
  (w₀ :
    CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝)
        app₁.hom =
      CategoryTheory.CategoryStruct.comp app₀.hom
        (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝))
  (w₁ :
    CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_363✝) app₂.hom =
      CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_363✝))
  (w₂ :
    CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_364✝) app₃.hom =
      CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_299✝ _proof_364✝))
  (w₃ :
    CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_365✝) app₄.hom =
      CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_364✝ _proof_365✝)),
  (CategoryTheory.ComposableArrows.isoMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).hom =
    CategoryTheory.ComposableArrows.homMk₄ app₀.hom app₁.hom app₂.hom app₃.hom app₄.hom w₀ w₁ w₂ w₃
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a co-Heyting homomorphism preserves the top element.  -/
CoheytingHom.map_top' : ∀ {α : Type u_6} {β : Type u_7} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] (self : CoheytingHom α β),
  self.toFun ⊤ = ⊤
-- Init.Data.Dyadic.Basic
Dyadic.mul_zero : ∀ (x : Dyadic), x * 0 = 0
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.forget₂_obj : ∀ (R : Type u) [inst : Semiring R] (X : SemimoduleCat R),
  (CategoryTheory.forget₂ (SemimoduleCat R) AddCommMonCat).obj X = AddCommMonCat.of ↑X
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- If the order of a family of `PowerSeries` tends to infinity, the collection of all
possible products over `Finset` is summable.  -/
PowerSeries.WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : CommSemiring R] {ι : Type u_2} [inst_2 : LinearOrder ι]
  [LocallyFiniteOrderBot ι] {f : ι → PowerSeries R},
  Filter.Tendsto (fun i => (f i).order) Filter.atTop (nhds ⊤) → Summable fun x => ∏ i ∈ x, f i
-- Mathlib.Topology.Separation.Regular
ULift.instT3Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T3Space X], T3Space (ULift.{u_3, u_1} X)
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
/-- Möbius inversion for functions to an `AddCommGroup`.  -/
ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq : ∀ {R : Type u_1} [inst : AddCommGroup R] {f g : ℕ → R},
  (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 • g x.2 = f n
-- Mathlib.Data.Multiset.MapFold
Multiset.attach_map_val' : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → β), Multiset.map (fun i => f ↑i) s.attach = Multiset.map f s
-- Lean.Meta.AppBuilder
/-- Returns `a ≤ b`. This method assumes `a` and `b` have the same type.  -/
Lean.Meta.mkLE : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.forget_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : C ⥤ₗ D), (CategoryTheory.LeftExactFunctor.forget C D).obj F = F.obj
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.comp.match_1.eq_3 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D]
  (motive : (x x_1 x_2 : CategoryTheory.Join C D) → x.Hom x_1 → x_1.Hom x_2 → Sort u_5) (_x : C) (_y _z : D)
  (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.right _y))
  (x_1 : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z))
  (h_1 :
    (_x _y _z : C) →
      (f : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
        (g : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.left _z)) →
          motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y) (CategoryTheory.Join.left _z) f g)
  (h_2 :
    (_x _y : C) →
      (_z : D) →
        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
          (x_2 : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.right _z)) →
            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y) (CategoryTheory.Join.right _z) x x_2)
  (h_3 :
    (_x : C) →
      (_y _z : D) →
        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.right _y)) →
          (x_2 : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.right _y) (CategoryTheory.Join.right _z) x x_2)
  (h_4 :
    (_x _y _z : D) →
      (f : (CategoryTheory.Join.right _x).Hom (CategoryTheory.Join.right _y)) →
        (g : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
          motive (CategoryTheory.Join.right _x) (CategoryTheory.Join.right _y) (CategoryTheory.Join.right _z) f g),
  (match CategoryTheory.Join.left _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, x, x_1 with
    | CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.left _z, f, g => h_1 _x _y _z f g
    | CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.right _z, x, x_2 =>
      h_2 _x _y _z x x_2
    | CategoryTheory.Join.left _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, x, x_2 =>
      h_3 _x _y _z x x_2
    | CategoryTheory.Join.right _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, f, g =>
      h_4 _x _y _z f g) =
    h_3 _x _y _z x x_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionList.items : Lean.Lsp.CompletionList → Array Lean.Lsp.CompletionItem
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.Options.mk : Bool → Bool → Lean.Lsp.DeleteFile.Options
-- Mathlib.Data.Set.Prod
Set.graphOn_union : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), Set.graphOn f (s ∪ t) = Set.graphOn f s ∪ Set.graphOn f t
-- Mathlib.CategoryTheory.Subobject.Comma
CategoryTheory.CostructuredArrow.projectQuotient_factors : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} [inst_2 : CategoryTheory.Limits.HasFiniteColimits C]
  [inst_3 : CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T}
  (P : CategoryTheory.Subobject (Opposite.op A)),
  ∃ q,
    CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.projectQuotient P).arrow.unop) q = A.hom
-- Mathlib.Topology.UrysohnsLemma
_private.Mathlib.Topology.UrysohnsLemma.0.Urysohns.CU.approx.match_1.splitter : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {P : Set X → Set X → Prop} →
      (motive : ℕ → Urysohns.CU P → X → Sort u_2) →
        (x : ℕ) →
          (x_1 : Urysohns.CU P) →
            (x_2 : X) →
              ((c : Urysohns.CU P) → (x : X) → motive 0 c x) →
                ((n : ℕ) → (c : Urysohns.CU P) → (x : X) → motive n.succ c x) → motive x x_1 x_2
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isMatch_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch c pos ↔
    ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.ofMulEquivOfDom_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {k : P ≃* M}
  (H : Submonoid.map k.toMonoidHom T = S) (x : P), (f.ofMulEquivOfDom H) x = f (k x)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} [inst_2 : SizeOf B] [inst_3 : SizeOf C] (app : (a : B) → F.obj a ⟶ G.obj a)
  (naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (app a) (G.map f) ⟶ CategoryTheory.CategoryStruct.comp (F.map f) (app b))
  (naturality_naturality :
    autoParam
      (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
        CategoryTheory.CategoryStruct.comp (naturality f) (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)) (naturality g))
      CategoryTheory.Oplax.LaxTrans.naturality_naturality._autoParam)
  (naturality_id :
    autoParam
      (∀ (a : B),
        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.id a))
            (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (app a)).hom
              (CategoryTheory.Bicategory.leftUnitor (app a)).inv))
      CategoryTheory.Oplax.LaxTrans.naturality_id._autoParam)
  (naturality_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.comp f g))
            (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).inv
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (naturality f) (G.map g))
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).hom
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g))
                    (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).inv)))))
      CategoryTheory.Oplax.LaxTrans.naturality_comp._autoParam),
  sizeOf
      { app := app, naturality := naturality, naturality_naturality := naturality_naturality,
        naturality_id := naturality_id, naturality_comp := naturality_comp } =
    1