mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSheafFor_arrows_iff_pullbacks : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C}
  {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B)
  [inst_1 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks],
  CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔
    ∀ (x : (i : I) → P.obj (Opposite.op (X i))),
      CategoryTheory.Presieve.Arrows.PullbackCompatible P π x →
        ∃! t, ∀ (i : I), (CategoryTheory.ConcreteCategory.hom (P.map (π i).op)) t = x i
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.op_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.RightFraction X Y), φ.op.s = φ.s.op
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The left homology map data associated to the identity morphism of a short complex.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.id : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.LeftHomologyData) →
          CategoryTheory.ShortComplex.LeftHomologyMapData (CategoryTheory.CategoryStruct.id S) h h
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.nu_pos_of_prime : ∀ (self : BoundingSieve) (p : ℕ), Nat.Prime p → p ∣ self.prodPrimes → 0 < self.nu p
-- Mathlib.Order.Heyting.Basic
le_sup_sdiff_sup_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ≤ b ⊔ (a \ c ⊔ c \ b)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F₁ F₂ F₃ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) [inst_4 : F₁.LaxMonoidal] [inst_5 : F₂.LaxMonoidal]
  [inst_6 : F₃.LaxMonoidal] (τ' : F₂ ⟶ F₃) [CategoryTheory.NatTrans.IsMonoidal τ]
  [CategoryTheory.NatTrans.IsMonoidal τ'], CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.CategoryStruct.comp τ τ')
-- Std.Async.System
Std.Async.System.instReprSystemUser : Repr Std.Async.System.SystemUser
-- Init.Control.Lawful.Instances
ExceptT.seqLeft_eq : ∀ {α β ε : Type u} {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β),
  x <* y = Function.const β <$> x <*> y
-- Lean.Parser.Basic
Lean.Parser.strLitFn : Lean.Parser.ParserFn
-- Mathlib.Data.Nat.Prime.Defs
/-- Returns the smallest prime factor of `n ≠ 1`.  -/
Nat.minFac : ℕ → ℕ
-- Mathlib.Data.Finsupp.Sigma
Function.Embedding.sigmaMk.eq_1 : ∀ {α : Type u_1} {β : α → Type u_3} (a : α), Function.Embedding.sigmaMk a = { toFun := Sigma.mk a, inj' := ⋯ }
-- Init.Data.Vector.Zip
/-- Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`.  -/
Vector.getElem?_zipWith' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {as : Vector α n} {bs : Vector β n} {f : α → β → γ} {i : ℕ},
  (Vector.zipWith f as bs)[i]? = (Option.map f as[i]?).bind fun g => Option.map g bs[i]?
-- Mathlib.Logic.Equiv.Set
Equiv.Set.insert_apply_left : ∀ {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] {a : α} (H : a ∉ s),
  (Equiv.Set.insert H) ⟨a, ⋯⟩ = Sum.inr PUnit.unit
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `Units.mul_inv_le_iff`. -/
Units.le_mul_of_mul_inv_le : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a b : M} (u : Mˣ), a * ↑u⁻¹ ≤ b → a ≤ b * ↑u
-- Lean.DocString.Types
Lean.Doc.Inline.concat.inj : ∀ {i : Type u} {content content_1 : Array (Lean.Doc.Inline i)},
  Lean.Doc.Inline.concat content = Lean.Doc.Inline.concat content_1 → content = content_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.lt_sin_mul : ∀ {x : ℝ}, 0 < x → x < 1 → x < Real.sin (Real.pi / 2 * x)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey! k = default
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
AddGrpCat.binaryProductLimitCone_cone_pt : ∀ (G H : AddGrpCat), (G.binaryProductLimitCone H).cone.pt = AddGrpCat.of (↑G × ↑H)
-- Mathlib.Computability.RegularExpressions
RegularExpression.one_def : ∀ {α : Type u_1}, RegularExpression.epsilon = 1
-- Init.Data.List.Nat.InsertIdx
List.insertIdx_length_self : ∀ {α : Type u} {l : List α} {x : α}, l.insertIdx l.length x = l ++ [x]
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel_map_comp_cokernelComparison_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] {X' Y' : C} [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)] (g : X' ⟶ Y') [inst_7 : CategoryTheory.Limits.HasCokernel g]
  [inst_8 : CategoryTheory.Limits.HasCokernel (G.map g)] (p : X ⟶ X') (q : Y ⟶ Y')
  (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g) {Z : D}
  (h : G.obj (CategoryTheory.Limits.cokernel g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison g G) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison f G)
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.map f g p q hpq)) h)
-- Mathlib.Data.Nat.PrimeFin
Nat.mem_primeFactors_of_ne_zero : ∀ {n p : ℕ}, n ≠ 0 → (p ∈ n.primeFactors ↔ Nat.Prime p ∧ p ∣ n)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List α},
      List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
        (∀ a ∈ t, l.contains a = false) → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).size = t.size + l.length
-- Mathlib.Data.Nat.Cast.Order.Field
Nat.cast_inv_le_one : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (n : ℕ), (↑n)⁻¹ ≤ 1
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.mapMulHom_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Mul α] [inst_1 : Mul β] [inst_2 : Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ),
  WithOne.mapMulHom (g.comp f) = (WithOne.mapMulHom g).comp (WithOne.mapMulHom f)
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.rootMultiplicity_X_sub_C : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] [inst_2 : DecidableEq R] {x y : R},
  Polynomial.rootMultiplicity x (Polynomial.X - Polynomial.C y) = if x = y then 1 else 0
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.aleph0_ne_zero : Cardinal.aleph0 ≠ 0
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.eraseₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  m.eraseₘ a = if m.containsₘ a = true then m.eraseₘaux a else m
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux2.match_1.eq_2 : ∀ (motive : ONote × ℕ → Sort u_1) (b : ONote) (k : ℕ) (h_1 : (b : ONote) → motive (b, 0))
  (h_2 : (b : ONote) → (k : ℕ) → motive (b, k.succ)),
  (match (b, k.succ) with
    | (b, 0) => h_1 b
    | (b, k.succ) => h_2 b k) =
    h_2 b k
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_fst_add_inr_snd_eq : ∀ {R : Type u} {M : Type v} [inst : AddZeroClass R] [inst_1 : AddZeroClass M] (x : TrivSqZeroExt R M),
  TrivSqZeroExt.inl x.fst + TrivSqZeroExt.inr x.snd = x
-- Mathlib.Algebra.Group.Shrink
Shrink.instMonoid.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Monoid α], Shrink.instMonoid = (equivShrink α).symm.monoid
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- If `x` and `y` are unit vectors, then `-1 ≤ ⟪x, y⟫ ≤ 1`.  -/
real_inner_mem_Icc_of_norm_eq_one : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  ‖x‖ = 1 → ‖y‖ = 1 → inner ℝ x y ∈ Set.Icc (-1) 1
-- Batteries.Data.Array.Basic
Array.scanlM.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (init : β) (as : Array α)
  (start stop : ℕ) (h_stop : stop ≤ as.size) (acc : Array β),
  Array.scanlM.loop f init as start stop h_stop acc =
    if h_lt : start < stop then do
      let __do_lift ← f init as[start]
      Array.scanlM.loop f __do_lift as (start + 1) stop h_stop (acc.push init)
    else pure (acc.push init)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
groupHomology.δ₁_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (z : ↥(groupHomology.cycles₂ X.X₃)) (y : G × G →₀ ↑X.X₂),
  (Finsupp.mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z →
    ∀ (x : G →₀ ↑X.X₁)
      (hx :
        (Finsupp.mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x =
          (CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ X.X₂)) y),
      (CategoryTheory.ConcreteCategory.hom (groupHomology.δ hX 2 1 ⋯))
          ((CategoryTheory.ConcreteCategory.hom (groupHomology.H2π X.X₃)) z) =
        (CategoryTheory.ConcreteCategory.hom (groupHomology.H1π X.X₁)) ⟨x, ⋯⟩
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.MorphismProperty.transfiniteCompositions_pushouts_coproducts_le_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u}
      (CategoryTheory.MorphismProperty.coproducts.{w, v, u} W).pushouts ≤
    W.rlp.llp
-- Mathlib.Algebra.Group.Basic
add_zero_sub : ∀ {G : Type u_3} [inst : SubNegMonoid G] (x y : G), x + (0 - y) = x - y
-- Mathlib.Data.Setoid.Partition
Setoid.Partitions.ext_iff : ∀ {α : Type u_1} (p q : Setoid.Partitions α), p = q ↔ p.toSet = q.toSet
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelIsIsoComp_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : CategoryTheory.IsIso f] [inst_3 : CategoryTheory.Limits.HasKernel g],
  (CategoryTheory.Limits.kernelIsIsoComp f g).inv =
    CategoryTheory.Limits.kernel.lift (CategoryTheory.CategoryStruct.comp f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.inv f)) ⋯
-- Mathlib.Analysis.Complex.Circle
Circle.instMetricSpace : MetricSpace Circle
-- Lean.Meta.Basic
/-- Given `type` of the form `forall xs, A`, execute `k xs A`.
This combinator will declare local declarations, create free variables for them,
execute `k` with updated local context, and make sure the cache is restored after executing `k`.

If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
 -/
Lean.Meta.forallTelescope : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] → {α : Type} → Lean.Expr → (Array Lean.Expr → Lean.Expr → n α) → optParam Bool false → n α
-- Std.Do.WP.Sound
/-- Soundness of `wp`: a `wp`-provable postcondition is `Internal.Ensures`-witnessed.  -/
Std.Do.WPSound : (m : Type u → Type v) → (ps : outParam Std.Do.PostShape) → [Monad m] → [Std.Do.WP m ps] → Prop
-- Mathlib.Algebra.Star.StarAlgHom
/-- `Function.eval` as a `NonUnitalStarAlgHom`.  -/
Pi.evalNonUnitalStarAlgHom : {ι : Type u_1} →
  (R : Type u_2) →
    (A : ι → Type u_3) →
      (j : ι) →
        [inst : Monoid R] →
          [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] →
            [inst_2 : (i : ι) → DistribMulAction R (A i)] →
              [inst_3 : (i : ι) → Star (A i)] → ((i : ι) → A i) →⋆ₙₐ[R] A j
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOnFilter.add : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformlyOnFilter f g l l' →
    TendstoUniformlyOnFilter f' g' l l' → TendstoUniformlyOnFilter (f + f') (g + g') l l'
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- **Alias** of `AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding`. -/
AlgebraicGeometry.Scheme.Hom.isClosedEmbedding : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsClosedImmersion f],
  Topology.IsClosedEmbedding ⇑f
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.TopEdgeLabeling.labelGraph_toTopEdgeLabeling : ∀ {V : Type u_1} [inst : DecidableEq V] (C : SimpleGraph.TopEdgeLabeling V (Fin 2)),
  (SimpleGraph.EdgeLabeling.labelGraph C 1).toTopEdgeLabeling = C
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_add : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] [inst_2 : OrderTopology R]
  [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R] [inst_6 : SecondCountableTopology R]
  [inst_7 : DenselyOrdered R] (f g : StieltjesFunction R), (f + g).measure = f.measure + g.measure
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_add : ∀ {α : Type u} [inst : AddMonoid α] (a b : AddUnits α), ↑(a + b) = ↑a + ↑b
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.mk.inj : ∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {base : 𝒮}
  {fiber : ↑(F.obj { as := Opposite.op base })} {base_1 : 𝒮} {fiber_1 : ↑(F.obj { as := Opposite.op base_1 })},
  { base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 } → base = base_1 ∧ fiber ≍ fiber_1
-- Mathlib.Order.Category.LinOrd
LinOrd.inv_hom_apply : ∀ {X Y : LinOrd} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Init.Data.Fin.Lemmas
Fin.intCast : {n : ℕ} → [NeZero n] → ℤ → Fin n
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.det_matrixToStdBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.mixedEmbedding.matrixToStdBasis K).det = (2⁻¹ * Complex.I) ^ NumberField.InfinitePlace.nrComplexPlaces K
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.getKeyD a fallback = (t.getKey? a).getD fallback
-- Mathlib.Tactic.IntervalCases
/-- A "typeclass" (not actually a class) of methods for the type-specific handling of
`interval_cases`. To add support for a new type, you have to implement this interface and add
a dispatch case for it in `intervalCases`.  -/
Mathlib.Tactic.IntervalCases.Methods : Type
-- Mathlib.Data.List.Chain
List.IsChain.iff_mem_mem_tail : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α},
  List.IsChain R l ↔ List.IsChain (fun x y => x ∈ l ∧ y ∈ l.tail ∧ R x y) l
-- Init.Data.List.Find
List.find?_eq_some_iff_append : ∀ {α : Type u_1} {b : α} {p : α → Bool} {xs : List α},
  List.find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ a ∈ as, (!p a) = true
-- Lean.Meta.Tactic.Grind.Types
/-- Folds using `f` and `init` over the equivalence class containing `e`  -/
Lean.Meta.Grind.foldEqc : {α : Type} → Lean.Expr → α → (Lean.Meta.Grind.ENode → α → Lean.Meta.Grind.GoalM α) → Lean.Meta.Grind.GoalM α
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] {ι : Type u_1} [Finite ι]
  {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsVanKampenColimit c
-- Batteries.Tactic.Lint.Frontend
/-- Verbosity for the linter output.  -/
Batteries.Tactic.Lint.LintVerbosity : Type
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.lifts_iff_coeff_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} (p : Polynomial S),
  p ∈ Polynomial.lifts f ↔ ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.neg_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {x : L}, x ∈ S → -x ∈ S
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insert_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {a : α} {b : β a}, (Std.DTreeMap.Internal.Impl.insert a b t ⋯).impl.getKey! a = a
-- Lean.CoreM
Lean.Core.instMonadOptionsCoreM : Lean.MonadOptions Lean.CoreM
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit.eq_def : ∀ {n : ℕ}
  (x :
    Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) ×
      Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Bool)
  (x_1 : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit x x_1 =
    match x with
    | (units, assignments, foundContradiction) =>
      match x_1 with
      | (l, b) =>
        have curAssignment := assignments[↑l]!;
        if Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b curAssignment = true then
          (units, assignments, foundContradiction)
        else
          have units := units.push (l, b);
          have assignments := assignments.modify (↑l) (Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment b);
          have foundContradiction :=
            foundContradiction || curAssignment != Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned;
          (units, assignments, foundContradiction)
-- Mathlib.FieldTheory.Galois.Abelian
IsAbelianGalois.mk : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [toIsGalois : IsGalois K L]
  [toIsMulCommutative : IsMulCommutative Gal(L/K)], IsAbelianGalois K L
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- If `K : J ⥤ C` is a diagram with `C` thin, a cone for `K` is limiting
if and only if the cone point is the product of the components.  -/
CategoryTheory.Limits.isLimitEquivFanOfIsThin : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [Quiver.IsThin C] →
      {J : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
          {K : CategoryTheory.Functor J C} →
            (c : CategoryTheory.Limits.Cone K) →
              CategoryTheory.Limits.IsLimit c ≃
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk c.pt c.π.app)
-- Mathlib.Analysis.InnerProductSpace.l2Space
_private.Mathlib.Analysis.InnerProductSpace.l2Space.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_1 : HAdd Std.Time.Nanosecond.Offset Std.Time.Second.Offset Std.Time.Nanosecond.Offset
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.instContinuousEval : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜] [Finite ι]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : TopologicalSpace F] [inst_5 : AddCommGroup F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜 F],
  ContinuousEval (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) F
-- Mathlib.CategoryTheory.Opposites
/-- Compatibility of `Functor.unop` with respect to functor composition.  -/
CategoryTheory.Functor.unopComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
            (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
              (G : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ) → (F.comp G).unop ≅ F.unop.comp G.unop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryGT!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α}, t₁.Equiv t₂ → t₁.getEntryGT! k = t₂.getEntryGT! k
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.homMk.congr_simp : ∀ {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]
  {F G : CategoryTheory.LaxBraidedFunctor C D} (f f_1 : F.toFunctor ⟶ G.toFunctor) (e_f : f = f_1)
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal f],
  CategoryTheory.LaxBraidedFunctor.homMk f = CategoryTheory.LaxBraidedFunctor.homMk f_1
-- Mathlib.Algebra.Algebra.Tower
IsScalarTower.algebraMap_eq : ∀ (R : Type u) (S : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A],
  algebraMap R A = (algebraMap S A).comp (algebraMap R S)
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The short complex consisting of the composition of
two morphisms `X.δ`, given three composable morphisms `f₁`, `f₂`
and `f₃` in `ι`, and three consecutive integers.  -/
CategoryTheory.Abelian.SpectralObject.shortComplex : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k l : ι} →
              (i ⟶ j) →
                (j ⟶ k) →
                  (k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_1 →
                        autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_3 →
                          CategoryTheory.ShortComplex C
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
DifferentiableOn.clog : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E},
  DifferentiableOn ℂ f s → (∀ x ∈ s, f x ∈ Complex.slitPlane) → DifferentiableOn ℂ (fun t => Complex.log (f t)) s
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.HasCountableColimits.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  (∀ (J : Type) [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J],
      CategoryTheory.Limits.HasColimitsOfShape J C) →
    CategoryTheory.Limits.HasCountableColimits C
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.ofMulEquivOfLocalizations_eq : ∀ {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) {k : N ≃* P},
  (f.ofMulEquivOfLocalizations k).toMonoidHom = k.toMonoidHom.comp f.toMonoidHom
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblZ_ne_zero_of_Y_ne : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q → P 2 ≠ 0 → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3 → W'.dblZ P ≠ 0