mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyδOfTriangle.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  CochainComplex.homologyδOfTriangle T n₀ n₁ h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap T.mor₃ n₀)
      (((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso 1 n₀ n₁ ⋯).hom.app T.obj₁)
-- Mathlib.Algebra.Ring.Defs
one_sub_mul : ∀ {α : Type u} [inst : NonAssocRing α] (a b : α), (1 - a) * b = b - a * b
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.offset_eq_decreaseBy : ∀ {t₁ t₂ s : String} {p : s.Pos}, p.Splits t₁ t₂ → p.offset = s.rawEndPos.decreaseBy t₂.utf8ByteSize
-- Mathlib.Analysis.Normed.Ring.Basic
ULift.normedCommRing : {α : Type u_2} → [NormedCommRing α] → NormedCommRing (ULift.{u_5, u_2} α)
-- Std.Tactic.BVDecide.LRAT.Checker
/-- If the `check` functions succeeds on `lratProof` and `cnf` then the `cnf` is unsatisfiable.
 -/
Std.Tactic.BVDecide.LRAT.check_sound : ∀ (lratProof : Array Std.Tactic.BVDecide.LRAT.IntAction) (cnf : Std.Sat.CNF ℕ),
  Std.Tactic.BVDecide.LRAT.check lratProof cnf = true → cnf.Unsat
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
AddOpposite.nndist_op : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (x y : α), nndist (AddOpposite.op x) (AddOpposite.op y) = nndist x y
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.forM.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] (f : α → m PUnit.{u_1 + 1}) (c : RBTree.RBColor)
  (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  RBTree.RBNode.forM f (RBTree.RBNode.node c l v r) = do
    RBTree.RBNode.forM f l
    f v
    RBTree.RBNode.forM f r
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S : Solution`, we have that
`S.Y ^ 3 + (S.u₄ * S.Z) ^ 3 = S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.formula3 : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution.Y✝ S ^ 3 +
      (↑(FermatLastTheoremForThreeGen.Solution.u₄✝ S) * FermatLastTheoremForThreeGen.Solution.Z✝ S) ^ 3 =
    ↑(FermatLastTheoremForThreeGen.Solution.u₅✝ S) *
      ((hζ.toInteger - 1) ^ (FermatLastTheoremForThreeGen.Solution.multiplicity✝ S - 1) *
          FermatLastTheoremForThreeGen.Solution.X✝ S) ^
        3
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
/-- Let `P` be a factor of the `n`-th cyclotomic polynomial over `ZMod p`, where `p` does not divide
`n`. If the degree of `P` is the multiplicative order of `p` modulo `n` then `P` is
irreducible.  -/
ZMod.irreducible_of_dvd_cyclotomic_of_natDegree : ∀ {p n : ℕ} [hp : Fact (Nat.Prime p)] {P : Polynomial (ZMod p)} (hpn : ¬p ∣ n),
  P ∣ Polynomial.cyclotomic n (ZMod p) → P.natDegree = orderOf (ZMod.unitOfCoprime p ⋯) → Irreducible P
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.opNorm_le_iff : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ}, 0 ≤ C → (‖f‖ ≤ C ↔ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.hom_ext : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃}
  {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) {X₂ : C₂} {f g : X₂ ⟶ sq.pt},
  CategoryTheory.CategoryStruct.comp f sq.fst = CategoryTheory.CategoryStruct.comp g sq.fst →
    CategoryTheory.CategoryStruct.comp f sq.snd = CategoryTheory.CategoryStruct.comp g sq.snd → f = g
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPi_apply : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (p : (i : ι) → Submodule R (Ms i))
  (a : ((i : ι) → Ms i) ⧸ Submodule.pi Set.univ p) (i : ι),
  (Submodule.quotientPi p) a i = (Submodule.quotientPiLift p (fun i => (p i).mkQ) ⋯) a i
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.ext_of_adjoin_eq_top : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {s : Set A},
  Algebra.adjoin R s = ⊤ → ∀ ⦃φ₁ φ₂ : A →ₐ[R] B⦄, Set.EqOn (⇑φ₁) (⇑φ₂) s → φ₁ = φ₂
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.klFun.eq_1 : ∀ (x : ℝ), InformationTheory.klFun x = x * Real.log x + 1 - x
-- Mathlib.Data.List.Nodup
List.nodup_iff_count_le_one : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α}, l.Nodup ↔ ∀ (a : α), List.count a l ≤ 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_add_pi_div_two : ∀ (x : ℂ), Complex.sin (x + ↑Real.pi / 2) = Complex.cos x
-- Init.System.Uri
System.Uri.UriEscape.lettera : UInt8
-- Mathlib.LinearAlgebra.Complex.FiniteDimensional
/-- `ℂ` and `ℝ` are isomorphic as vector spaces over `ℚ`, or equivalently,
as additive groups.  -/
Complex.nonempty_linearEquiv_real : Nonempty (ℂ ≃ₗ[ℚ] ℝ)
-- Lean.Meta.Tactic.Grind.Split
/-- Anchor reference for a case-split candidate in generated tactic scripts.
`ordinal` is the 0-based position of the candidate among the (ready) candidates whose
anchors share the same displayed prefix. Distinct candidates may have identical anchors
(e.g., candidates that differ only in inaccessible variables), and the ordinal is used
to disambiguate them.
 -/
Lean.Meta.Grind.SplitAnchorRefInfo : Type
-- Mathlib.Order.Height
Set.chainHeight_ne_top_of_finite : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.Finite → s.chainHeight r ≠ ⊤
-- Std.Time.Internal.UnitVal
/-- A structure representing a unit of a given ratio type `α`.
 -/
Std.Time.Internal.UnitVal : ℚ → Type
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- An equivalence of the index set defines an equivalence between the spaces of continuous
multilinear maps. This is the forward map of this equivalence.  -/
ContinuousMultilinearMap.domDomCongr : {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₃] →
                      {ι' : Type u_1} →
                        ι ≃ ι' →
                          ContinuousMultilinearMap R (fun x => M₂) M₃ → ContinuousMultilinearMap R (fun x => M₂) M₃
-- Mathlib.Topology.Order.Lattice
Continuous.finset_sup : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [inst_3 : OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L},
  (∀ i ∈ s, Continuous (f i)) → Continuous (s.sup f)
-- Init.Data.List.BasicAux
List.getD_nil : ∀ {n : ℕ} {α : Type u_1} {d : α}, [].getD n d = d
-- Init.Data.Dyadic.Basic
Dyadic.ofIntWithPrec_zero : ∀ {i : ℤ}, Dyadic.ofIntWithPrec 0 i = 0
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
instDecidableEqQuaternionGroup : {n : ℕ} → DecidableEq (QuaternionGroup n)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_ι_bot : ∀ {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), t.eTruncLTι ⊥ = 0
-- Init.Data.UInt.Bitwise
UInt8.ofNat_shiftLeft : ∀ (a b : ℕ), b < 8 → UInt8.ofNat (a <<< b) = UInt8.ofNat a <<< UInt8.ofNat b
-- Mathlib.Computability.Language
Language.mem_reverse : ∀ {α : Type u_1} {l : Language α} {a : List α}, a ∈ l.reverse ↔ a.reverse ∈ l
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.C_eq_algebraMap : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommSemiring R], HahnSeries.C = algebraMap R (HahnSeries Γ R)
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Sieve.secondMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (S : CategoryTheory.Sieve X),
  CategoryTheory.Equalizer.Sieve.secondMap P S =
    CategoryTheory.Limits.Pi.lift fun fg =>
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) ⟨fg.fst, fg.snd.snd.snd⟩)
        (P.map fg.snd.snd.fst.op)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β k}, k ∉ m₁ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.Analysis.RCLike.Basic
RCLike.I_eq_zero_or_im_I_eq_one : ∀ {K : Type u_1} [inst : RCLike K], RCLike.I = 0 ∨ RCLike.im RCLike.I = 1
-- Mathlib.Algebra.Order.Archimedean.Hom
OrderRingIso.eq_refl : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (f : α ≃+*o α),
  f = OrderRingIso.refl α
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Abelian.Ext.homEquiv₀.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C},
  CategoryTheory.Abelian.Ext.homEquiv₀ = (Equiv.ofBijective CategoryTheory.Abelian.Ext.mk₀ ⋯).symm
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsFunctor_obj_X_carrier : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (n : ℕ),
  ↑(((groupHomology.chainsFunctor k G).obj A).X n) = ((Fin n → G) →₀ ↑A)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.FunctionTheorem.mk.injEq : ∀ (funPropName : Lean.Name) (thmOrigin funOrigin : Mathlib.Meta.FunProp.Origin) (mainArgs : Array ℕ)
  (appliedArgs priority : ℕ) (form : Mathlib.Meta.FunProp.TheoremForm) (funPropName_1 : Lean.Name)
  (thmOrigin_1 funOrigin_1 : Mathlib.Meta.FunProp.Origin) (mainArgs_1 : Array ℕ) (appliedArgs_1 priority_1 : ℕ)
  (form_1 : Mathlib.Meta.FunProp.TheoremForm),
  ({ funPropName := funPropName, thmOrigin := thmOrigin, funOrigin := funOrigin, mainArgs := mainArgs,
        appliedArgs := appliedArgs, priority := priority, form := form } =
      { funPropName := funPropName_1, thmOrigin := thmOrigin_1, funOrigin := funOrigin_1, mainArgs := mainArgs_1,
        appliedArgs := appliedArgs_1, priority := priority_1, form := form_1 }) =
    (funPropName = funPropName_1 ∧
      thmOrigin = thmOrigin_1 ∧
        funOrigin = funOrigin_1 ∧
          mainArgs = mainArgs_1 ∧ appliedArgs = appliedArgs_1 ∧ priority = priority_1 ∧ form = form_1)
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.String.Pos.Raw.get?.match_1.splitter : (motive : String → String.Pos.Raw → Sort u_1) →
  (x : String) → (x_1 : String.Pos.Raw) → ((s : String) → (p : String.Pos.Raw) → motive s p) → motive x x_1
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.kind.inj : ∀ {val val_1 : Lean.SyntaxNodeKind},
  Lean.Parser.ParserExtension.OLeanEntry.kind val = Lean.Parser.ParserExtension.OLeanEntry.kind val_1 → val = val_1
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cone.ofFork_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (t :
    CategoryTheory.Limits.Fork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
      (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
  (j : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.Cone.ofFork t).π.app j =
    CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
-- Mathlib.Order.Lattice
sup_left_comm : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)
-- Init.Data.List.Scan.Lemmas
List.getElem?_succ_scanl : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {i : ℕ} {f : β → α → β},
  (List.scanl f b l)[i + 1]? = (List.scanl f b l)[i]?.bind fun x => Option.map (fun y => f x y) l[i]?
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.topEquiv_apply : ∀ {M : Type u_1} [inst : Add M] (x : ↥⊤), AddSubsemigroup.topEquiv x = ↑x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_homologyMap'_of_epi_of_isIso_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData)
  [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃],
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.MemBaseSet.isHenstock : ∀ {ι : Type u_1} [inst : Fintype ι] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {c : NNReal}
  {r : (ι → ℝ) → ↑(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I},
  l.MemBaseSet I c r π → l.bHenstock = true → π.IsHenstock
-- Init.Data.Iterators.Lemmas.Combinators.ULift
Std.Iter.length_uLift : ∀ {α β : Type u} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id], it.uLift.length = it.length
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportState.moduleNameMap : Lean.ImportState → Std.HashMap Lean.Name Lean.ImportedModule✝
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_union!_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false →
          Std.DTreeMap.Internal.Impl.Const.getD (m₁.union! m₂) k fallback =
            Std.DTreeMap.Internal.Impl.Const.getD m₂ k fallback
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.addSubMapCoeff_condition : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] (x : Fin 3 → R) (i : Fin 3),
  ∑ j,
      (MvPolynomial.eval x) (MvPolynomial.C ↑W.Δ'⁻¹ * W.addSubMapCoeff (i, j)) * (MvPolynomial.eval x) (W.addSubMap j) =
    x i ^ 4
-- Mathlib.Algebra.Lie.Abelian
LieModule.mem_maxTrivSubmodule : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (m : M),
  m ∈ LieModule.maxTrivSubmodule R L M ↔ ∀ (x : L), ⁅x, m⁆ = 0
-- Mathlib.FieldTheory.Differential.Basic
/-- The logarithmic derivative of a is a′ / a.
 -/
Differential.logDeriv : {R : Type u_1} → [inst : Field R] → [Differential R] → R → R
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.updateCell.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l.size - 1) (l.size + 1) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l.size - 1) (l.size + 1)) →
          ((newL : Std.DTreeMap.Internal.Impl α β) →
              (h₁ : newL.Balanced) →
                (h₂ : l.size - 1 ≤ newL.size) →
                  (h₃ : newL.size ≤ l.size + 1) →
                    motive { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ }) →
            motive x
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
/-- The sum of two restriction maps in sheaf cohomology.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
            (S : J.MayerVietorisSquare) →
              (F : CategoryTheory.Sheaf J AddCommGrpCat) → (n : ℕ) → F.H' n S.X₄ ⟶ F.H' n S.X₂ ⊞ F.H' n S.X₃
-- Batteries.Data.Fin.Lemmas
/-- **Alias** of `Fin.isSome_findSome?_iff`. -/
Fin.findSome?_isSome_iff : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.findSome? f).isSome = true ↔ ∃ i, (f i).isSome = true
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Given a morphism property `P` which respects isomorphisms, then to show that a morphism
`f : X ⟶ Y` satisfies `P.relative` it suffices to show that:
* The morphism is representable.
* For any morphism `g : F.obj a ⟶ G`, the property `P` holds for *some* represented pullback
  of `f` by `g`.  -/
CategoryTheory.MorphismProperty.relative.of_exists : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {P : CategoryTheory.MorphismProperty C} [F.Faithful] [F.Full]
  [P.RespectsIso] {f : X ⟶ Y},
  (∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : CategoryTheory.IsPullback fst (F.map snd) f g), P snd) →
    CategoryTheory.MorphismProperty.relative F P f
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- For `f : ℕ → G`, the sum `∑' k, f (k + i)` tends to zero. This does not require a
summability assumption on `f`, as otherwise all such sums are zero.  -/
tendsto_sum_nat_add : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G]
  (f : ℕ → G), Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.smul'_mk : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {R₀ : Type u_3} [inst_3 : SMul R₀ R] [inst_4 : SMul R₀ M] [inst_5 : IsScalarTower R₀ R R]
  [inst_6 : IsScalarTower R₀ R M] (r : R₀) (m : M) (s : ↥S), r • LocalizedModule.mk m s = LocalizedModule.mk (r • m) s
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.differentiable_Λ₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E), Differentiable ℂ P.Λ₀
-- Mathlib.Order.SuccPred.Archimedean
/-- This isn't an instance due to a loop with `LinearOrder`.
 -/
IsPredArchimedean.linearOrder : {α : Type u_1} →
  [inst : PartialOrder α] →
    [inst_1 : PredOrder α] →
      [IsPredArchimedean α] → [DecidableEq α] → [DecidableLE α] → [DecidableLT α] → [IsDirectedOrder α] → LinearOrder α
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.uncurry.obj F)]
  [inst_5 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j)
        (CategoryTheory.Limits.limit.π (F.obj j) k)) =
    CategoryTheory.Limits.limit.π (CategoryTheory.Functor.uncurry.obj F) (j, k)
-- Std.Http.Data.Body.Any
/-- Returns the declared size.
 -/
Std.Http.Body.Any.getKnownSize : Std.Http.Body.Any → Std.Async.Async (Option Std.Http.Body.Length)
-- Std.Net.Addr
Std.Net.SocketAddressV4.addr : Std.Net.SocketAddressV4 → Std.Net.IPv4Addr
-- Mathlib.Order.Filter.Bases.Basic
/-- The filter associated to a filter basis.  -/
FilterBasis.filter : {α : Type u_1} → FilterBasis α → Filter α
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.IntegrableOn.biUnion_finite : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {s : Set ι},
  s.Finite →
    ∀ {t : ι → Set X},
      (∀ i ∈ s, MeasurableSet (t i)) → (∀ i ∈ s, μ.IntegrableOn f (t i)) → μ.IntegrableOn f (⋃ i ∈ s, t i)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.shortComplexH2.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.shortComplexH2 A =
    { X₁ := ModuleCat.of k (G × G × G →₀ ↑A), X₂ := ModuleCat.of k (G × G →₀ ↑A), X₃ := ModuleCat.of k (G →₀ ↑A),
      f := groupHomology.d₃₂ A, g := groupHomology.d₂₁ A, zero := ⋯ }
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.add_mul_left_left_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime (x + y * z) y ↔ IsRelPrime x y
-- Mathlib.Topology.Constructions.SumProd
instDiscreteTopologyProd : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [DiscreteTopology X]
  [DiscreteTopology Y], DiscreteTopology (X × Y)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolResult.mk : Array Lean.Lsp.DocumentSymbol → Lean.Lsp.DocumentSymbolResult
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.rid_symm_apply : ∀ (R : Type uR) (A : Type uA) {M : Type uM} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] (m : M),
  (TensorProduct.AlgebraTensorModule.rid R A M).symm m = m ⊗ₜ[R] 1
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautologicalSolution_isPresentation : ∀ (A : Type u) [inst : Ring A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M],
  (Module.Presentation.tautologicalSolution A M).IsPresentation
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.toLinearMap_symm_comp_eq : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₁ : R₃ →+* R₁} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂}
  [inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂),
  ↑e₁₂.symm ∘ₛₗ g = f ↔ g = ↑e₁₂ ∘ₛₗ f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toList_insert_perm : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : BEq α] [Std.TransOrd α]
  [Std.LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.toList.Perm
    (⟨k, v⟩ :: List.filter (fun x => decide ¬(k == x.fst) = true) t.toList)
-- Mathlib.Topology.Order
continuous_Prop : ∀ {α : Type u_1} [inst : TopologicalSpace α] {p : α → Prop}, Continuous p ↔ IsOpen {x | p x}