mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.DirectLimit.cod_partialEquivLimit : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_1}
  [inst_2 : Preorder ι] [inst_3 : Nonempty ι] [inst_4 : IsDirectedOrder ι] (S : ι →o L.PartialEquiv M N),
  (FirstOrder.Language.DirectLimit.partialEquivLimit S).cod = ⨆ x, (S x).cod
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Extend the base of a pretrivialization from a nonempty set to the whole space.  -/
Bundle.Pretrivialization.codExtend : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {s : Set B} →
            IsOpen s →
              s.Nonempty →
                {proj : Z → ↑s} → Bundle.Pretrivialization F proj → Bundle.Pretrivialization F (Subtype.val ∘ proj)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.mono : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f g x y : Equiv.Perm α},
  f.Disjoint g → x.support ⊆ f.support → y.support ⊆ g.support → x.Disjoint y
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
/-- Given some lift `φ'` of `g ≫ f`, the canonical map from the domain of `φ'` to the domain of
the Cartesian lift of `f`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.homCartesianLift : {𝒮 : 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) →
            {a' : F.CoGrothendieck} →
              (g : a'.base ⟶ R) →
                (φ' : a' ⟶ { base := S, fiber := a }) →
                  [(CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsHomLift
                        (CategoryTheory.CategoryStruct.comp g f) φ'] →
                    a' ⟶ CategoryTheory.Pseudofunctor.CoGrothendieck.domainCartesianLift a f
-- Mathlib.Data.Finsupp.Interval
Finsupp.instLocallyFiniteOrder : {ι : Type u_1} →
  {α : Type u_2} →
    [inst : PartialOrder α] →
      [inst_1 : Zero α] → [LocallyFiniteOrder α] → [DecidableEq ι] → [DecidableEq α] → LocallyFiniteOrder (ι →₀ α)
-- Mathlib.Data.List.Basic
List.foldl_hom₂ : ∀ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : List ι) (f : α → β → γ) (op₁ : α → ι → α) (op₂ : β → ι → β)
  (op₃ : γ → ι → γ) (a : α) (b : β),
  (∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i) →
    List.foldl op₃ (f a b) l = f (List.foldl op₁ a l) (List.foldl op₂ b l)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- The image of the restriction of an open set to the source is open.  -/
OpenPartialHomeomorph.isOpen_image_source_inter : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X}, IsOpen s → IsOpen (↑e '' (e.source ∩ s))
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.op_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y), h.op.r = h.i.op
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedTZifV2.default : Std.Time.TimeZone.TZif.TZifV2
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_same₁₄ : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b c : ℤ), IsEllipticNet.atomRel W a b c a = W a * W 0 * IsEllipticNet.atom W b c
-- Mathlib.Data.Finset.Max
Finset.max_mem_image_coe : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α}, s.Nonempty → s.max ∈ Finset.image WithBot.some s
-- Mathlib.Order.Atoms.Finite
exists_covby_infinite_Iic_of_infinite_Iic : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α} [IsStronglyCoatomic α],
  (Set.Iic a).Infinite → {x | x ⋖ a}.Finite → ∃ b, b ⋖ a ∧ (Set.Iic b).Infinite
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.one_notMem_inv_mul_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Group α] {s t : Finset α}, 1 ∉ t⁻¹ * s ↔ Disjoint s t
-- Mathlib.Analysis.Complex.Norm
Complex.norm_I : ‖Complex.I‖ = 1
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Equivalence.mapCommMon_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] (e : C ≌ D)
  [inst_6 : e.functor.Braided] [inst_7 : e.inverse.Braided] [inst_8 : e.IsMonoidal],
  e.mapCommMon.counitIso =
    CategoryTheory.Functor.mapCommMonCompIso.symm ≪≫
      CategoryTheory.Functor.mapCommMonNatIso e.counitIso ≪≫ CategoryTheory.Functor.mapCommMonIdIso
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.sum_le_lift_mk_mul_iSup : ∀ {ι : Type u} (f : ι → Cardinal.{max u v}), Cardinal.sum f ≤ Cardinal.lift.{v, u} (Cardinal.mk ι) * ⨆ i, f i
-- Mathlib.Condensed.Discrete.Basic
/-- The underlying object of a condensed object in `C` is the light condensed object evaluated at a
point. This can be viewed as a sort of forgetful functor from `LightCondensed C` to `C`
 -/
LightCondensed.underlying : (C : Type w) → [inst : CategoryTheory.Category.{u, w} C] → CategoryTheory.Functor (LightCondensed C) C
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.instProdT0Space : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → TopologicalSpace (β i)] [∀ (i : ι), T0Space (β i)],
  T0Space (PiLp p β)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
/-- If `p` is a prime such that `p ∣ n`, then
`expand R p (cyclotomic n R) = cyclotomic (p * n) R`.  -/
Polynomial.cyclotomic_expand_eq_cyclotomic : ∀ {p n : ℕ},
  Nat.Prime p →
    p ∣ n →
      ∀ (R : Type u_1) [inst : CommRing R],
        (Polynomial.expand R p) (Polynomial.cyclotomic n R) = Polynomial.cyclotomic (n * p) R
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.castLE.match_1.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x x_1 : ℕ) → x ≤ x_1 → L.BoundedFormula α x → Sort u_4)
  (_m _n : ℕ) (h : _m ≤ _n) (f₁ f₂ : L.BoundedFormula α _m)
  (h_1 : (_m _n : ℕ) → (_h : _m ≤ _n) → motive _m _n _h FirstOrder.Language.BoundedFormula.falsum)
  (h_2 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) → (t₁ t₂ : L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) →
        (l : ℕ) →
          (R : L.Relations l) →
            (ts : Fin l → L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (_m _n : ℕ) → (h : _m ≤ _n) → (f₁ f₂ : L.BoundedFormula α _m) → motive _m _n h (f₁.imp f₂))
  (h_5 : (_m _n : ℕ) → (h : _m ≤ _n) → (f : L.BoundedFormula α (_m + 1)) → motive _m _n h f.all),
  (match _m, _n, h, f₁.imp f₂ with
    | _m, _n, _h, FirstOrder.Language.BoundedFormula.falsum => h_1 _m _n _h
    | _m, _n, h, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 _m _n h t₁ t₂
    | _m, _n, h, FirstOrder.Language.BoundedFormula.rel R ts => h_3 _m _n h l R ts
    | _m, _n, h, f₁.imp f₂ => h_4 _m _n h f₁ f₂
    | _m, _n, h, f.all => h_5 _m _n h f) =
    h_4 _m _n h f₁ f₂
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_inter_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t₂.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.Topology.Instances.AddCircle.Real
ZMod.toAddCircle.eq_1 : ∀ {N : ℕ} [inst : NeZero N], ZMod.toAddCircle = (ZMod.lift N) ⟨AddMonoidHom.mk' (fun j => ↑(↑j / ↑N)) ⋯, ⋯⟩
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_snd_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C)
  (z : (CategoryTheory.FunctorToTypes.prod F G).obj a),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.snd.app a))
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryProductIso F G).inv.app a)) z) =
    z.2
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
/-- A morphism of schemes `f : X ⟶ Y` is universally injective if the base change `X ×[Y] Y' ⟶ Y'`
along any morphism `Y' ⟶ Y` is injective (on points).
 -/
AlgebraicGeometry.UniversallyInjective : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasurableEmbedding.stronglyMeasurable_extend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {g' : γ → β} {mα : MeasurableSpace α}
  {mγ : MeasurableSpace γ} [inst : TopologicalSpace β],
  MeasurableEmbedding g →
    MeasureTheory.StronglyMeasurable f →
      MeasureTheory.StronglyMeasurable g' → MeasureTheory.StronglyMeasurable (Function.extend g f g')
-- Mathlib.Topology.EMetricSpace.Defs
Metric.mem_eball' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, y ∈ Metric.eball x ε ↔ edist x y < ε
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k k' : α}
  {fallback : β} {f : β → β},
  Std.DTreeMap.Const.getD (Std.DTreeMap.Const.modify t k f) k' fallback =
    if cmp k k' = Ordering.eq then (Option.map f (Std.DTreeMap.Const.get? t k)).getD fallback
    else Std.DTreeMap.Const.getD t k' fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_insertManyIfNewUnit_empty_list : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {l : List α},
  (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)).isEmpty = l.isEmpty
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.completedHurwitzZetaEven_neg : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedHurwitzZetaEven (-a) s = HurwitzZeta.completedHurwitzZetaEven a s
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_sdiff_add_inter : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasurableSet t → μ (s \ t) + μ (s ∩ t) = μ s
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {a₁ a₂ b₁ b₂ c : R},
  Mathlib.Meta.NormNum.IsNat (a₁ + b₁) 0 → a₂ + b₂ = c → a₁ + a₂ + (b₁ + b₂) = c
-- Std.Data.TreeMap.Raw.Lemmas
/-- Simpler variant of `getElem!_filter` when `LawfulEqCmp` is available.  -/
Std.TreeMap.Raw.getElem!_filter' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited β] {f : α → β → Bool} {k : α},
  t.WF → (Std.TreeMap.Raw.filter f t)[k]! = (Option.filter (f k) t[k]?).get!
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGT_map_hom₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleLEGT n).map φ).hom₃ = (t.truncGT n).map φ
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.apply_eq_zero_of_not_le : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : LE α] {a b : α},
  ¬a ≤ b → ∀ (f : IncidenceAlgebra 𝕜 α), f a b = 0
-- Init.Data.Array.Lemmas
Array.getElem?_swap : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} (hi : i < xs.size) (hj : j < xs.size) {k : ℕ},
  (xs.swap i j hi hj)[k]? = if j = k then some xs[i] else if i = k then some xs[j] else xs[k]?
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv (CategoryTheory.ShortComplex.homologyMap φ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) h₂.homologyIso.inv
-- Mathlib.Algebra.RingQuot
/-- Any ring homomorphism `f : R →+* T` which respects a relation `r : R → R → Prop`
factors uniquely through a morphism `RingQuot r →+* T`.
 -/
RingQuot.lift : {R : Type u_1} →
  [inst : Semiring R] →
    {T : Type u_2} →
      [inst_1 : Semiring T] → {r : R → R → Prop} → { f // ∀ ⦃x y : R⦄, r x y → f x = f y } ≃ (RingQuot r →+* T)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.Produces.single : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)}, g.Produces v w → g.Derives v w
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.LClause.mk.inj : ∀ {lits : Array ℤ} {expr : Lean.Expr} {depth : ℕ} {lits_1 : Array ℤ} {expr_1 : Lean.Expr} {depth_1 : ℕ},
  { lits := lits, expr := expr, depth := depth } = { lits := lits_1, expr := expr_1, depth := depth_1 } →
    lits = lits_1 ∧ expr = expr_1 ∧ depth = depth_1
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- Being a subobject classifier is preserved under isomorphism.  -/
CategoryTheory.Subobject.Classifier.ofIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (𝒞 : CategoryTheory.Subobject.Classifier C) →
      {Ω₀ Ω : C} →
        (eΩ : 𝒞.Ω ≅ Ω) →
          (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) →
            ((C_1 : C) → C_1 ⟶ Ω₀) →
              (t : Ω₀ ⟶ Ω) →
                autoParam
                    (t = CategoryTheory.CategoryStruct.comp eΩ₀.inv (CategoryTheory.CategoryStruct.comp 𝒞.truth eΩ.hom))
                    CategoryTheory.Subobject.Classifier.ofIso._auto_1 →
                  CategoryTheory.Subobject.Classifier C
-- Mathlib.Algebra.Ring.Basic
isRegular_iff_eq_zero_of_mul : ∀ {R : Type u_3} [inst : NonUnitalNonAssocRing R] {r : R},
  IsRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0
-- Std.Data.ExtTreeMap.Basic
/-- Checks whether a key is present in a map and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.ExtTreeMap.containsThenInsert : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → β → Bool × Std.ExtTreeMap α β cmp
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunEquivPointed_counitIso_inv_app_toFun : ∀ (X : Pointed) (a : ((CategoryTheory.Functor.id Pointed).obj X).X),
  (partialFunEquivPointed.counitIso.inv.app X).toFun a = (Equiv.optionSubtypeNe X.point).symm a
-- Init.Data.Vector.Lemmas
Vector.findRev?.eq_1 : ∀ {n : ℕ} {α : Type} (f : α → Bool) (as : Vector α n), Vector.findRev? f as = Array.findRev? f as.toArray
-- Lean.Elab.PreDefinition.WF.Fix
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.getLCtxId : Lean.MetaM Lean.Elab.WF.LCtxId✝
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.mem_atBot : ∀ {α : Type u_3} [inst : Preorder α] (a : α), {b | b ≤ a} ∈ Filter.atBot
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.coeToFun_mul : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ χ' : MulChar R R'),
  ⇑(χ * χ') = ⇑χ * ⇑χ'
-- Mathlib.Data.Set.Subsingleton
Set.not_nontrivial_iff : ∀ {α : Type u} {s : Set α}, ¬s.Nontrivial ↔ s.Subsingleton
-- Lean.Elab.DocString
Lean.Doc.instFromDocArgWithSyntax : {α : Type} → [Lean.Doc.FromDocArg α] → Lean.Doc.FromDocArg (Lean.Doc.WithSyntax α)
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureRat.eq_1 : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ) (n : ℕ),
  wittStructureRat p Φ n =
    (MvPolynomial.bind₁ fun k =>
        (MvPolynomial.bind₁ fun i => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℚ k)) Φ)
      (xInTermsOfW p ℚ n)
-- Mathlib.Algebra.Group.Nat.Hom
MonoidHom.ext_mnat : ∀ {M : Type u_1} [inst : Monoid M] ⦃f g : Multiplicative ℕ →* M⦄,
  f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1) → f = g
-- Lean.Language.Lean.Types
/-- Initial snapshot of the Lean language processor: a "header parsed" snapshot.  -/
Lean.Language.Lean.InitialSnapshot : Type
-- Lean.Elab.Command
Lean.Elab.Command.withScope : {α : Type} →
  (Lean.Elab.Command.Scope → Lean.Elab.Command.Scope) →
    Lean.Elab.Command.CommandElabM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.mk : {α : Type u_1} →
  {β : Type u_2} →
    [inst : PseudoEMetricSpace α] →
      [inst_1 : PseudoEMetricSpace β] →
        (toFun : α → β) → (∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun x) (toFun y) = ↑r * edist x y) → α →ᵈ β
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_mem_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β} {b c : β}, b ∈ s → c ∈ t → b -ᵥ c ∈ s -ᵥ t
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- A locally path-connected compact space has finitely many path components.  -/
instFiniteZerothHomotopyOfCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] [CompactSpace X], Finite (ZerothHomotopy X)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_iff_contains : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {a : α},
  a ∈ m ↔ m.contains a = true
-- Mathlib.Order.Heyting.Regular
Heyting.IsRegular.inf : ∀ {α : Type u_1} [inst : HeytingAlgebra α] {a b : α},
  Heyting.IsRegular a → Heyting.IsRegular b → Heyting.IsRegular (a ⊓ b)
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] [inst_4 : SizeOf α] [inst_5 : SizeOf β] (toLatticeHom : LatticeHom α β)
  (map_top' : toLatticeHom.toFun ⊤ = ⊤) (map_bot' : toLatticeHom.toFun ⊥ = ⊥),
  sizeOf { toLatticeHom := toLatticeHom, map_top' := map_top', map_bot' := map_bot' } =
    1 + sizeOf toLatticeHom + sizeOf map_top' + sizeOf map_bot'
-- Mathlib.Topology.VectorBundle.Basic
/-- A trivialization for a vector bundle defines linear equivalences between the
fibers and the model space.  -/
Bundle.Trivialization.linearEquivAt : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : Semiring R] →
          [inst_1 : TopologicalSpace F] →
            [inst_2 : TopologicalSpace B] →
              [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
                [inst_4 : AddCommMonoid F] →
                  [inst_5 : Module R F] →
                    [inst_6 : (x : B) → AddCommMonoid (E x)] →
                      [inst_7 : (x : B) → Module R (E x)] →
                        (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                          [Bundle.Trivialization.IsLinear R e] → (b : B) → b ∈ e.baseSet → E b ≃ₗ[R] F
-- Mathlib.Geometry.Euclidean.Projection
/-- The distance to a point's orthogonal projection is 0 iff it lies in the subspace.  -/
EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p : P},
  dist p ↑((EuclideanGeometry.orthogonalProjection s) p) = 0 ↔ p ∈ s
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerRight_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {G H : CategoryTheory.Functor C D} (α : G ⟶ H)
  (F : CategoryTheory.Functor D E) (X : C), (CategoryTheory.Functor.whiskerRight α F).app X = F.map (α.app X)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.instIsSMulApplyReal : ∀ {R : Type u_1} {E : Type u_3} [inst : AddGroup E] [inst_1 : SMul R ℝ] [inst_2 : SMul R NNReal]
  [inst_3 : IsScalarTower R NNReal ℝ], IsSMulApply R (NonarchAddGroupSeminorm E) E ℝ
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (i j : A),
  CategoryTheory.shiftFunctorAdd' C i j (i + j) ⋯ = CategoryTheory.shiftFunctorAdd C i j
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.infoTree : Lean.Server.Snapshots.Snapshot → Lean.Elab.InfoTree
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.StrongTrans G H) {a b : B} {a' : C}
  (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) {Z : a' ⟶ H.obj b}
  (h_1 : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (θ.app a) (H.map h)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) (θ.app b)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality h).hom) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.map₂ β))) h_1)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcOptions.fromJson : Lean.Json → Except String Lean.Lsp.RpcOptions
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.hasEqualizers_of_hasWideEqualizers : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWideEqualizers C],
  CategoryTheory.Limits.HasEqualizers C
-- Mathlib.Algebra.Ring.GeomSum
op_geom_sum : ∀ {R : Type u_1} [inst : Semiring R] (x : R) (n : ℕ),
  MulOpposite.op (∑ i ∈ Finset.range n, x ^ i) = ∑ i ∈ Finset.range n, MulOpposite.op x ^ i
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.edgeSet_subset_powerset_vertexSet : ∀ {α : Type u_1} {H : Hypergraph α}, H.edgeSet ⊆ 𝒫 H.vertexSet
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.rootMultiplicity_U_real : ∀ {n k : ℕ},
  k < n → Polynomial.rootMultiplicity (Real.cos ((↑k + 1) * Real.pi / (↑n + 1))) (Polynomial.Chebyshev.U ℝ ↑n) = 1
-- Mathlib.Data.Analysis.Filter
CFilter.coe_mk : ∀ {α : Type u_1} {σ : Type u_3} [inst : PartialOrder α] (f : σ → α) (pt : σ) (inf : σ → σ → σ)
  (h₁ : ∀ (a b : σ), f (inf a b) ≤ f a) (h₂ : ∀ (a b : σ), f (inf a b) ≤ f b) (a : σ),
  { f := f, pt := pt, inf := inf, inf_le_left := h₁, inf_le_right := h₂ }.f a = f a
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangleMorphism₁_hom₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  (CategoryTheory.Triangulated.Octahedron'.triangleMorphism₁ comm h₁₂ h₂₃ h₁₃ h).hom₂ =
    CategoryTheory.CategoryStruct.id X₁