mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
/-- Constructor for natural transformations from a right derived functor.  -/
CategoryTheory.Functor.rightDerivedDesc : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (RF : CategoryTheory.Functor D H) →
              {F : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (α : F ⟶ L.comp RF) →
                    (W : CategoryTheory.MorphismProperty C) →
                      [inst_3 : L.IsLocalization W] →
                        [RF.IsRightDerivedFunctor α W] → (G : CategoryTheory.Functor D H) → (F ⟶ L.comp G) → (RF ⟶ G)
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.zsmul_add : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → ∀ (n : ℤ), n • (a + b) = n • a + n • b
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_comp_lTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (f : M →ₗ[R] P)
  (g : N →ₗ[R] Q), LinearMap.rTensor Q f ∘ₗ LinearMap.lTensor M g = TensorProduct.map f g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff m₂ ⋯).getKey! k = default
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.FinStronglyMeasurable.sub : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → β}
  [inst : TopologicalSpace β] [inst_1 : SubtractionMonoid β] [ContinuousSub β],
  MeasureTheory.FinStronglyMeasurable f μ →
    MeasureTheory.FinStronglyMeasurable g μ → MeasureTheory.FinStronglyMeasurable (f - g) μ
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasStrictFDerivAt.cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ} {f' g' : StrongDual ℂ E}
  {x : E},
  HasStrictFDerivAt f f' x →
    HasStrictFDerivAt g g' x →
      f x ∈ Complex.slitPlane →
        HasStrictFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.Clause.mk.injEq : ∀ (lits : Array ℤ) (expr proof : Lean.Expr) (lits_1 : Array ℤ) (expr_1 proof_1 : Lean.Expr),
  ({ lits := lits, expr := expr, proof := proof } = { lits := lits_1, expr := expr_1, proof := proof_1 }) =
    (lits = lits_1 ∧ expr = expr_1 ∧ proof = proof_1)
-- Mathlib.Algebra.Group.Hom.Defs
/-- If the codomain of an injective monoid homomorphism is torsion free,
then so is the domain.  -/
Function.Injective.isMulTorsionFree : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] [IsMulTorsionFree N] (f : M →* N),
  Function.Injective ⇑f → IsMulTorsionFree M
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_sSup : ∀ {V : Type u} {s : Set (SimpleGraph V)}, (sSup s).edgeSet = ⋃₀ (SimpleGraph.edgeSet '' s)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.reverseAux.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (l r : List α) (h_1 : (r : List α) → motive [] r)
  (h_2 : (a : α) → (l r : List α) → motive (a :: l) r),
  (match a :: l, r with
    | [], r => h_1 r
    | a :: l, r => h_2 a l r) =
    h_2 a l r
-- Mathlib.Algebra.Homology.Opposite
imageToKernel_op : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Abelian V] {X Y Z : V}
  (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0),
  imageToKernel g.op f.op ⋯ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.imageSubobjectIso g.op ≪≫ (CategoryTheory.imageOpOp g).symm).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).op
        (CategoryTheory.Limits.kernelSubobjectIso f.op ≪≫ CategoryTheory.kernelOpOp f).inv)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer reflection of colimits of shape along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.reflectsColimitsOfShape_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {F G : CategoryTheory.Functor C D} (h : F ≅ G)
  [CategoryTheory.Limits.ReflectsColimitsOfShape J F], CategoryTheory.Limits.ReflectsColimitsOfShape J G
-- Mathlib.Order.Filter.Map
Function.RightInverse.filter_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α},
  Function.RightInverse g f → Function.RightInverse (Filter.map g) (Filter.map f)
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coe_mul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [inst : Semiring A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} (f g : 𝒜 →+*ᵍ 𝒜),
  ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.toAddSubmonoid_injective : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Injective Submodule.toAddSubmonoid
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.mk'_add : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] (x y : B) (hx : IsIntegral R x)
  (hy : IsIntegral R y), IsIntegralClosure.mk' A (x + y) ⋯ = IsIntegralClosure.mk' A x hx + IsIntegralClosure.mk' A y hy
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.πTruncGE_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] [inst_4 : ∀ (i : ℤ), HomologicalComplex.HasHomology L i]
  (n : ℤ) {Z : CochainComplex C ℤ} (h : L.truncGE n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.πTruncGE n)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.truncGEMap φ n) h) =
    CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (L.πTruncGE n) h)
-- Mathlib.NumberTheory.NumberField.Ideal.Basic
/-- For `I` an integral ideal of `K`, the group morphism from the group of roots of unity of `K`
of order `n` to `(𝓞 K ⧸ I)ˣ`.
 -/
Ideal.rootsOfUnityMapQuot : {K : Type u_1} →
  [inst : Field K] →
    (I : Ideal (NumberField.RingOfIntegers K)) →
      (n : ℕ) → ↥(rootsOfUnity n (NumberField.RingOfIntegers K)) →* (NumberField.RingOfIntegers K ⧸ I)ˣ
-- Mathlib.Data.List.Sublists
List.sublists'.eq_1 : ∀ {α : Type u_1} (l : List α),
  l.sublists' = (List.foldr (fun a arr => Array.foldl (fun r l => r.push (a :: l)) arr arr) #[[]] l).toList
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.sinh : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => Real.sinh (f x)
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_fintype_card : ∀ {α : Type u_1} [inst : Fintype α], Nat.card α = Fintype.card α
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_symm_snd : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} (x : E × F), ((WithCStarModule.equiv A (E × F)).symm x).2 = x.2
-- Mathlib.Order.Heyting.Basic
fst_himp : ∀ {α : Type u_2} {β : Type u_3} [inst : HImp α] [inst_1 : HImp β] (a b : α × β), (a ⇨ b).1 = a.1 ⇨ b.1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
StarAlgHom.ofId.congr_simp : ∀ (R : Type u_7) (A : Type u_8) [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A] [inst_3 : StarMul A]
  [inst_4 : Algebra R A] [inst_5 : StarModule R A], StarAlgHom.ofId R A = StarAlgHom.ofId R A
-- Mathlib.NumberTheory.SumTwoSquares
/-- If `p` is a prime factor of `n` such that `-1` is a square modulo `n`, then `p % 4 ≠ 3`.  -/
Nat.mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one : ∀ {p n : ℕ}, p ∈ n.primeFactors → IsSquare (-1) → p % 4 ≠ 3
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.add_neg_cancel_left : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α}, IsAddUnit a → ∀ (b : α), a + (-a + b) = b
-- Mathlib.MeasureTheory.Order.Group.Lattice
AEMeasurable.oneLePart : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Group α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} {μ : MeasureTheory.Measure β} [MeasurableSup α],
  AEMeasurable f μ → AEMeasurable (fun x => (f x)⁺ᵐ) μ
-- Lean.Elab.Tactic.Ext
/-- Derives the type of the `iff` form of an ext theorem.
 -/
_private.Lean.Elab.Tactic.Ext.0.Lean.Elab.Tactic.Ext.mkExtIffType : Lean.Name → Lean.MetaM Lean.Expr
-- Init.System.IO
IO.instReprTaskState.repr : IO.TaskState → ℕ → Std.Format
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_eq_iff_eq_or_eq_neg : ∀ {θ ψ : Real.Angle}, θ.cos = ψ.cos ↔ θ = ψ ∨ θ = -ψ
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
continuousMultilinearCurryFin0_symm_apply : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (x : G'),
  (continuousMultilinearCurryFin0 𝕜 G G').symm x = ContinuousMultilinearMap.uncurry0 𝕜 G x
-- Mathlib.Condensed.Light.TopCatAdjunction
LightCondSet.instFaithfulTopCatTopCatToLightCondSet : topCatToLightCondSet.Faithful
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k}, a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.comap_comp : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {S₁ : Type u_6} {S₂ : Type u_7} [inst_2 : Ring S₁] [inst_3 : Ring S₂] (f : S₁ →+* S₂) (g : S₂ →+* R),
  AddValuation.comap (g.comp f) v = AddValuation.comap f (AddValuation.comap g v)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δ_eq_δ : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} {σ' : Type w₄} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ)
  (P' : Algebra.Generators R S σ'), Algebra.Generators.H1Cotangent.δ Q P = Algebra.Generators.H1Cotangent.δ Q P'
-- Mathlib.Order.Interval.Finset.Box
Int.card_box : ∀ {n : ℕ}, n ≠ 0 → (Finset.box n).card = 8 * n
-- Mathlib.Probability.Kernel.Disintegration.Basic
ProbabilityTheory.Kernel.instIsCondKernel_zero : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} (κCond : ProbabilityTheory.Kernel (α × β) Ω), ProbabilityTheory.Kernel.IsCondKernel 0 κCond
-- Lean.Meta.Tactic.Cases
Lean.Meta.CasesSubgoal.mk.inj : ∀ {toInductionSubgoal : Lean.Meta.InductionSubgoal} {ctorName : Option Lean.Name}
  {toInductionSubgoal_1 : Lean.Meta.InductionSubgoal} {ctorName_1 : Option Lean.Name},
  { toInductionSubgoal := toInductionSubgoal, ctorName := ctorName } =
      { toInductionSubgoal := toInductionSubgoal_1, ctorName := ctorName_1 } →
    toInductionSubgoal = toInductionSubgoal_1 ∧ ctorName = ctorName_1
-- Mathlib.Order.WellFounded
WellFoundedGT.toOrderTop.eq_1 : ∀ (α : Type u_4) [inst : LinearOrder α] [inst_1 : Nonempty α] [h : WellFoundedGT α],
  WellFoundedGT.toOrderTop α = { top := ⋯.min Set.univ ⋯, le_top := ⋯ }
-- Mathlib.Order.SymmDiff
symmDiff_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a : α), symmDiff a a = ⊥
-- Init.Data.BitVec.Basic
BitVec.instOrOp : {w : ℕ} → OrOp (BitVec w)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instSMulInt : {A : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring A] →
      [inst_1 : Monoid G] →
        {V : Type u_6} →
          {W : Type u_7} →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommGroup W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → SMul ℤ (ρ.IntertwiningMap σ)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_id : ∀ {G : Type u_1} [inst : AddGroup G], (AddMonoidHom.id G).ker = ⊥
-- Init.Grind.AC
Lean.Grind.AC.Seq.beq'_eq : ∀ (s₁ s₂ : Lean.Grind.AC.Seq), (s₁.beq' s₂ = true) = (s₁ = s₂)
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.of_mulHom_image : ∀ {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst_1 : Mul H] {A B : Finset G} {a0 b0 : G} [inst_2 : DecidableEq H]
  (f : G →ₙ* H),
  (∀ ⦃a b c d : G⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d) →
    UniqueMul (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0) → UniqueMul A B a0 b0
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_left_inj : ∀ {w : ℕ} (a b c : BitVec w), (a + c == b + c) = (a == b)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.DHashMap.Const.insertMany m l).getKeyD k' fallback = k
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_roi : ∀ {α : Type u_1} {xs : List α} {lo : ℕ}, Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = List.drop (lo + 1) xs
-- Mathlib.Control.Monad.Cont
_private.Mathlib.Control.Monad.Cont.0.ExceptT.run_bind.match_1.splitter : {ε α : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((x : α) → motive (Except.ok x)) → ((e : ε) → motive (Except.error e)) → motive x
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- The width of the cusp `∞`, i.e. the `x` such that `𝒢.periods = zmultiples x`, or 0 if no such
`x` exists.  -/
Subgroup.widthInfty : Subgroup (GL (Fin 2) ℝ) → ℝ
-- Lean.Elab.PreDefinition.WF.Preprocess
Lean.Elab.WF.mkWfParam : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {f : β k → β k}, (t.modify k f).size = t.size
-- Batteries.Data.Char.Basic
/-- Minimum surrogate code point.
(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).)
 -/
Char.minSurrogate : ℕ
-- Mathlib.Algebra.Order.Monovary
monovaryOn_iff_forall_smul_nonneg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β} {s : Set ι},
  MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i)
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_pos : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K),
  0 < Height.mulHeight x
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.isScalarTowerRight : ∀ {M : Type u_2} {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Monoid M] [inst_2 : DistribMulAction M α]
  [inst_3 : SMulCommClass M α α] [inst_4 : IsScalarTower M α α], IsScalarTower M (CentroidHom α) (CentroidHom α)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- If `AddCommMonoid` homs `g : M →+ P, l : P →+ A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`.  -/
AddSubmonoid.LocalizationMap.map_comp_map : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [inst_4 : AddCommMonoid A]
  {U : AddSubmonoid A} {R : Type u_6} [inst_5 : AddCommMonoid R] (j : U.LocalizationMap R) {l : P →+ A}
  (hl : ∀ (w : ↥T), l ↑w ∈ U), (k.map hl j).comp (f.map hy k) = f.map ⋯ j
-- Batteries.Data.Fin.Lemmas
Bool.toNat.eq_1 : ∀ (b : Bool), b.toNat = bif b then 1 else 0
-- Init.Data.BitVec.Lemmas
BitVec.and_append : ∀ {w v : ℕ} {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v}, x₁ ++ y₁ &&& x₂ ++ y₂ = (x₁ &&& x₂) ++ (y₁ &&& y₂)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorZero_hom_app_shift : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] {X : C} (n : A),
  (CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C n).obj X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C n 0).hom.app X)
      ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanDidOpenTextDocumentParams.toDidOpenTextDocumentParams : Lean.Lsp.LeanDidOpenTextDocumentParams → Lean.Lsp.DidOpenTextDocumentParams
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts a `UInt16` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofUInt16 : Float.Model.Format → UInt16 → Float.Model.UnpackedFloat
-- Mathlib.Data.QPF.Univariate.Basic
/-- constructor of a type defined by a qpf  -/
QPF.Fix.mk : {F : Type u → Type u} → [q : QPF F] → F (QPF.Fix F) → QPF.Fix F
-- Mathlib.Data.Sum.Interval
Finset.inl_mem_sumLift₂ : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f : α₁ → β₁ → Finset γ₁} {g : α₂ → β₂ → Finset γ₂} {a : α₁ ⊕ α₂} {b : β₁ ⊕ β₂} {c₁ : γ₁},
  Sum.inl c₁ ∈ Finset.sumLift₂ f g a b ↔ ∃ a₁ b₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ c₁ ∈ f a₁ b₁
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.mkNatModuleInst? : Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.Order.Interval.Set.Monotone
AntitoneOn.Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β} {s : Set α},
  AntitoneOn f s → MonotoneOn g s → MonotoneOn (fun x => Set.Ioo (f x) (g x)) s
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_compl_iff_disjoint_right : ∀ {α : Type u_1} {s t : Set α}, s ⊆ tᶜ ↔ Disjoint s t
-- Mathlib.Algebra.GroupWithZero.Defs
/-- `a / b := a * b⁻¹`  -/
GroupWithZero.div_eq_mul_inv : ∀ {G₀ : Type u} [self : GroupWithZero G₀] (a b : G₀), a / b = a * b⁻¹
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.instTrans : {n : ℕ} → Trans n.ModEq n.ModEq n.ModEq
-- Mathlib.Topology.Subpath
/-- Following the subpath of `γ` from `t₀` to `t₁`, and then that from `t₁` to `t₂`,
is in natural homotopy with following the subpath of `γ` from `t₀` to `t₂`.  -/
Path.Homotopy.subpathTransSubpath : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {a b : X} →
      (γ : Path a b) →
        (t₀ t₁ t₂ : ↑unitInterval) → ((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).Homotopy (γ.subpath t₀ t₂)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.ofSubsingleton_symm_apply_apply : ∀ (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : TopologicalSpace M₂]
  [inst_6 : TopologicalSpace M₃] [inst_7 : Subsingleton ι] (i : ι) (f : ContinuousMultilinearMap R (fun x => M₂) M₃)
  (x : M₂), ((ContinuousMultilinearMap.ofSubsingleton R M₂ M₃ i).symm f) x = f fun x_1 => x
-- Mathlib.Order.Filter.Basic
Filter.eventuallyEq_iff_all_subsets : ∀ {α : Type u} {β : Type v} {f g : α → β} {l : Filter α}, f =ᶠ[l] g ↔ ∀ (s : Set α), ∀ᶠ (x : α) in l, x ∈ s → f x = g x
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k n : ℤ), complEDS b c d k n = ↑n.sign * complEDS' b c d k n.natAbs
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : FrameHom α β) (f' : α → β)
  (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.SetTheory.Ordinal.Notation
ONote.zero : ONote
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termι'_2 : Lean.ParserDescr
-- Mathlib.Order.Bounded
Set.unbounded_le_inter_lt : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a < b}) ↔ Set.Unbounded (fun x1 x2 => x1 ≤ x2) s
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.startPos : ∀ {l m r : List Char} {s : Substring.Raw}, Substring.Raw.ValidFor l m r s → s.startPos = { byteIdx := String.utf8Len l }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c).hom.hom = α.hom.app c.pt
-- Mathlib.Topology.Constructions.SumProd
/-- If `f` and `g` are inducing maps whose ranges are separated, then `Sum.elim f g` is inducing.  -/
Topology.IsInducing.sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z},
  Topology.IsInducing f →
    Topology.IsInducing g →
      Disjoint (closure (Set.range f)) (Set.range g) →
        Disjoint (Set.range f) (closure (Set.range g)) → Topology.IsInducing (Sum.elim f g)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.isoMk_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (h : V₀.V ≅ V₁.V)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp V₀.str (F.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom V₁.str)
      CategoryTheory.Endofunctor.Coalgebra.isoMk._auto_1),
  (CategoryTheory.Endofunctor.Coalgebra.isoMk h w).hom.f = h.hom
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData),
  S.Exact ↔ CategoryTheory.CategoryStruct.comp h.left.i h.right.p = 0
-- Std.Http.Data.URI.Basic
/-- The URI scheme (e.g., "http", "https", "ftp").
 -/
Std.Http.URI.scheme : Std.Http.URI → Std.Http.URI.Scheme
-- Mathlib.Data.List.Intervals
List.Ico.filter_le : ∀ (n m l : ℕ), List.filter (fun x => decide (l ≤ x)) (List.Ico n m) = List.Ico (max n l) m
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.continuous_symm : ∀ {𝕜 : 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),
  Continuous ↑I.symm