mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
/-- **Alias** of `AlgebraicGeometry.IsSchemeTheoreticallyDominant.ker_eq_bot`. -/
AlgebraicGeometry.Scheme.Hom.ker_eq_bot : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsSchemeTheoreticallyDominant f],
  AlgebraicGeometry.Scheme.Hom.ker f = ⊥
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.toIsStrictOrderedRing : ∀ {α : Type u_5} (self : ConditionallyCompleteLinearOrderedField α), IsStrictOrderedRing α
-- Lean.Attributes
Lean.AttributeApplicationTime.beforeElaboration : Lean.AttributeApplicationTime
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_left_inj : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [IsLeftCancelAdd α], x ≠ ⊥ → (x + y = x + z ↔ y = z)
-- Aesop.Tree.Data
Aesop.Goal.setLastExpandedInIteration : Aesop.Iteration → Aesop.Goal → Aesop.Goal
-- Mathlib.RepresentationTheory.Basic
Representation.free_single_single : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {α : Type u_3} (g h : G) (i : α) (r : k),
  (((Representation.free k G α) g) fun₀ | i => MonoidAlgebra.single h r) = fun₀ | i => MonoidAlgebra.single (g * h) r
-- Mathlib.CategoryTheory.ObjectProperty.Small
_private.Mathlib.CategoryTheory.ObjectProperty.Small.0.CategoryTheory.ObjectProperty.instSmallMax.match_1.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {P Q : CategoryTheory.ObjectProperty C}
  (motive : Subtype P ⊕ Subtype Q → Sort u_2) (x : Subtype P) (h_1 : (x : Subtype P) → motive (Sum.inl x))
  (h_2 : (x : Subtype Q) → motive (Sum.inr x)),
  (match Sum.inl x with
    | Sum.inl x => h_1 x
    | Sum.inr x => h_2 x) =
    h_1 x
-- Mathlib.Data.Sum.Interval
Finset.sumLift₂_eq_empty : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f : α₁ → β₁ → Finset γ₁} {g : α₂ → β₂ → Finset γ₂} {a : α₁ ⊕ α₂} {b : β₁ ⊕ β₂},
  Finset.sumLift₂ f g a b = ∅ ↔
    (∀ (a₁ : α₁) (b₁ : β₁), a = Sum.inl a₁ → b = Sum.inl b₁ → f a₁ b₁ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), a = Sum.inr a₂ → b = Sum.inr b₂ → g a₂ b₂ = ∅
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.ρ_naturality : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y), CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Aesop.RuleTac.Forward.Basic
/-- Prefix of the regular hyps added by `forward`.  -/
Aesop.forwardHypPrefix : Lean.Name
-- Lean.Elab.Do.Legacy
/-- Return true if we should generate an error message when lifting a nested action over this kind of syntax.  -/
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.nestedActionForbiddenBinder : Lean.Syntax → Bool
-- Init.Data.Fin.Bitwise
Fin.or_val : ∀ {n : ℕ} (a b : Fin n), ↑(a ||| b) = (↑a ||| ↑b) % n
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side.  -/
Orientation.norm_div_tan_oangle_add_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle (x + y) y).tan = ‖y‖
-- Mathlib.Algebra.Algebra.Operations
Submodule.map_one : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {A' : Type u_1}
  [inst_3 : Semiring A'] [inst_4 : Algebra R A'] (f : A →ₐ[R] A'), Submodule.map f.toLinearMap 1 = 1
-- Mathlib.Topology.Constructible
QuasiSeparatedSpace.of_isOpenCover : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_4} {U : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover U →
    (∀ (i : ι), IsRetrocompact ↑(U i)) → (∀ (i : ι), IsQuasiSeparated ↑(U i)) → QuasiSeparatedSpace X
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_diff!_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ((m₁.diff! m₂).isEmpty = true ↔
        ∀ (k : α), Std.DTreeMap.Internal.Impl.contains k m₁ = true → Std.DTreeMap.Internal.Impl.contains k m₂ = true)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toProd_zero : ∀ {R : Type u_3} {A : Type u_4} [inst : Zero R] [inst_1 : Zero A], Unitization.toProd 0 = 0
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- Taking the product under `h` is an additive-to-multiplicative homomorphism of finsupps,
if `h` is an additive-to-multiplicative homomorphism on the support.
This is a more general version of `Finsupp.prod_add_index'`; the latter has simpler hypotheses.  -/
Finsupp.prod_add_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : DecidableEq α] [inst_1 : AddZeroClass M] [inst_2 : CommMonoid N]
  {f g : α →₀ M} {h : α → M → N},
  (∀ a ∈ f.support ∪ g.support, h a 0 = 1) →
    (∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) → (f + g).prod h = f.prod h * g.prod h
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.ReflectsEffectiveEpiFamilies],
  F.ReflectsFiniteEffectiveEpiFamilies
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).card = OfNat.ofNat n
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci.injEq : ∀ (lo lo_1 : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound),
  (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci lo = Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci lo_1) =
    (lo = lo_1)
-- Mathlib.Analysis.Calculus.TangentCone.Basic
zero_mem_tangentConeAt_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E}, 0 ∈ tangentConeAt 𝕜 s x ↔ x ∈ closure s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂)[k]? = if k ∈ m₂ then none else m₁[k]?
-- Mathlib.RepresentationTheory.Coinvariants
/-- A `G`-invariant linear map induces a linear map out of the coinvariants of a
`G`-representation.  -/
Representation.Coinvariants.lift : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommRing k] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : Module k V] →
                [inst_4 : AddCommGroup W] →
                  [inst_5 : Module k W] →
                    (ρ : Representation k G V) → (f : V →ₗ[k] W) → (∀ (x : G), f ∘ₗ ρ x = f) → ρ.Coinvariants →ₗ[k] W
-- Mathlib.Order.Directed
Std.Total.directed : ∀ {α : Type u_1} {ι : Sort u_3} {r : α → α → Prop} [Std.Total r] (f : ι → α), Directed r f
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.image_degenerate_le : ∀ {X Y : SSet} (f : X ⟶ Y) (n : ℕ),
  ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) '' X.degenerate n ⊆ Y.degenerate n
-- Mathlib.RingTheory.Polynomial.Dickson
_private.Mathlib.RingTheory.Polynomial.Dickson.0.Polynomial.dickson.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_2 ()
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.subst_sub : ∀ {M : Type u_1} [inst : Ring M] {x₁ x₂ X₁ X₂ Y y a : M},
  x₁ = a * X₁ → x₂ = a * X₂ → X₁ - X₂ = Y → a * Y = y → x₁ - x₂ = y
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.coe_sInf : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (t : Set (AffineSubspace k P)), ↑(sInf t) = ⋂ s ∈ t, ↑s
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_one : Cardinal.ord 1 = 1
-- Lean.Server.References
/-- Groups `refs` by identifier and range s.t. references with the same identifier and range
are added to the `aliases` of the representative of the group.
Yields to separate groups for declaration and usages if `allowSimultaneousBinderUse` is set.
 -/
Lean.Server.dedupReferences : Array Lean.Server.Reference → optParam Bool false → Array Lean.Server.Reference
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.ins.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (t : RBTree.RBNode α)
  (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a)
  (h_3 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b)
  (h_4 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a)
  (h_5 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b),
  (match RBTree.RBNode.Path.root, t with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a => h_2 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b => h_3 a y parent b
    | RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a => h_4 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b => h_5 a y parent b) =
    h_1 t
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_one : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  (v : AddValuation R Γ₀), v 1 = 0
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.submoduleImage_apply_of_le : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_10}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {O : Submodule R M} (ϕ : ↥O →ₗ[R] M') (N : Submodule R M)
  (hNO : N ≤ O), ϕ.submoduleImage N = (ϕ ∘ₗ Submodule.inclusion hNO).range
-- Mathlib.Data.Ordmap.Invariants
/-- Build a tree from three nodes, with `a () b -> (a ()) b` and `a (b c) d -> ((a b) (c d))`.  -/
Ordnode.node4L : {α : Type u_1} → Ordnode α → α → Ordnode α → α → Ordnode α → Ordnode α
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.connected_induce_top_sup : ∀ {V : Type u} {G : SimpleGraph V} {H K : G.Subgraph},
  H.Preconnected →
    K.Preconnected → ∀ {u v : V}, u ∈ H.verts → v ∈ K.verts → G.Adj u v → (⊤.induce {u, v} ⊔ H ⊔ K).Connected
-- Aesop.Tree.ExtractScript
Aesop.ExtractScript.visitGoal : Aesop.Goal → Aesop.ExtractScriptM Unit
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.ext.sizeOf_spec : ∀ (declName : Lean.Name), sizeOf (Lean.Meta.Grind.Entry.ext declName) = 1 + sizeOf declName
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.map_fst_toList_eq_keys : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp},
  List.map Prod.fst (Std.DTreeMap.Const.toList t) = t.keys
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.false_imp : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, (⌜False⌝ → P) ⊣⊢ₛ ⌜True⌝
-- Mathlib.Algebra.Quaternion
Quaternion.coe_div : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] (x y : R),
  ↑(x / y) = ↑x / ↑y
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalk_hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {F : TopCat.Presheaf C X} {x : ↑X} {Y : C} {f₁ f₂ : F.stalk x ⟶ Y},
  f₁ = f₂ ↔
    ∀ (U : TopologicalSpace.Opens ↑X) (hxU : x ∈ U),
      CategoryTheory.CategoryStruct.comp (F.germ U x hxU) f₁ = CategoryTheory.CategoryStruct.comp (F.germ U x hxU) f₂
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientEquivProdOfLE_symm_apply : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (h_le : s ≤ t) (a : (α ⧸ t) × ↥t ⧸ s.addSubgroupOf t),
  (AddSubgroup.quotientEquivProdOfLE h_le).symm a = Quotient.map' (fun b => Quotient.out a.1 + ↑b) ⋯ a.2
-- Init.Data.SInt.Lemmas
Int8.not_lt_minValue : ∀ {a : Int8}, ¬a < Int8.minValue
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.pushLetRecs : Array Lean.Elab.PreDefinition →
  List Lean.Elab.Term.MutualClosure.LetRecClosure →
    Lean.Elab.DefKind → Lean.Elab.Modifiers → Lean.MetaM (Array Lean.Elab.PreDefinition)
-- Mathlib.LinearAlgebra.Orientation
Module.Basis.orientation_isEmpty : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_4} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  [inst_7 : IsEmpty ι] (b : Module.Basis ι R M), b.orientation = positiveOrientation
-- Mathlib.Algebra.Algebra.RestrictScalars
instAddCommGroupRestrictScalars : (R : Type u_1) → (S : Type u_2) → (M : Type u_3) → [I : AddCommGroup M] → AddCommGroup (RestrictScalars R S M)
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.isZero_homology_of_isLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory.Plus C) (n : ℤ) [X.IsLE n] (i : ℤ),
  n < i → CategoryTheory.Limits.IsZero ((DerivedCategory.Plus.homologyFunctor C i).obj X)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instIsTwoSidedSupp : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], (ValuativeRel.supp R).IsTwoSided
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.map_join' : ∀ {α : Type u} {β : Type v} (f : α → β) (S : Stream'.Seq (Stream'.Seq1 α)),
  Stream'.Seq.map f S.join = (Stream'.Seq.map (Stream'.Seq1.map f) S).join
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_rco_eq_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m...n).toList[i]! = 0 ↔ (n - m).toNat ≤ i ∨ m + ↑i = 0
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinite_omega : Hyperreal.omega.Infinite
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.forIn'_eq_match_step.match_1.eq_1 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.yield c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_1 c
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.ae_le_essSup : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal),
  ∀ᵐ (y : α) ∂μ, f y ≤ essSup f μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α},
      Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.erase! k t) =
        (!compare k a == Ordering.eq && Std.DTreeMap.Internal.Impl.contains a t)
-- Std.Sat.AIG.Basic
/-- Given a `cache`, valid with respect to some `decls`, we can extend the `decls` without
extending the cache and remain valid.
 -/
Std.Sat.AIG.Cache.noUpdate : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {decls : Array (Std.Sat.AIG.Decl α)} →
        {decl : Std.Sat.AIG.Decl α} → Std.Sat.AIG.Cache α decls → Std.Sat.AIG.Cache α (decls.push decl)
-- Mathlib.Algebra.Category.MonCat.Limits
/-- (Internal use only; use the limits API.)  -/
AddMonCat.HasLimits.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddMonCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] →
        CategoryTheory.Limits.IsLimit (AddMonCat.HasLimits.limitCone F)
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.minimalPrimes_eq_empty_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R), I.minimalPrimes = ∅ ↔ I = ⊤
-- Lean.EnvExtension
Lean.mkTagDeclarationExtension : autoParam Lean.Name Lean.mkTagDeclarationExtension._auto_1 →
  optParam Lean.EnvExtension.AsyncMode Lean.EnvExtension.AsyncMode.mainOnly → IO Lean.TagDeclarationExtension
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Left Kan extensions of isomorphic functors are isomorphic.  -/
CategoryTheory.Functor.leftKanExtensionUniqueOfIso : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : F ⟶ L.comp F') →
                    [F'.IsLeftKanExtension α] →
                      {G : CategoryTheory.Functor C H} →
                        (F ≅ G) →
                          (G' : CategoryTheory.Functor D H) → (β : G ⟶ L.comp G') → [G'.IsLeftKanExtension β] → F' ≅ G'
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.foldl_folder_none_eq_none : ∀ {n : ℕ} {ls : List (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))},
  List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder none ls = none
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- Given `S : Finset (Fin (n + 1))`, this is the corresponding face of `Δ[n]`,
as a subcomplex.  -/
SSet.stdSimplex.face : {n : ℕ} → Finset (Fin (n + 1)) → (SSet.stdSimplex.obj { len := n }).Subcomplex
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.length.hcongr_5 : ∀ (V V' : Type u),
  V = V' →
    ∀ (G : SimpleGraph V) (G' : SimpleGraph V'),
      G ≍ G' →
        ∀ (u : V) (u' : V'),
          u ≍ u' → ∀ (v : V) (v' : V'), v ≍ v' → ∀ (a : G.Walk u v) (a' : G'.Walk u' v'), a ≍ a' → a.length ≍ a'.length
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.of_sdiv_left : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t : Set β}, (s /ₛ t).Nonempty → s.Nonempty
-- Mathlib.Order.CompactlyGenerated.Basic
complementedLattice_iff_isAtomistic : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α],
  ComplementedLattice α ↔ IsAtomistic α
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.extendScalars_top : ∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L),
  IntermediateField.extendScalars ⋯ = ⊤
-- Init.Data.Int.DivMod.Lemmas
Int.neg_one_ediv : ∀ (b : ℤ), -1 / b = -b.sign
-- Mathlib.Algebra.BigOperators.Finprod
finprod_dmem : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {s : Set α} [inst_1 : DecidablePred fun x => x ∈ s]
  (f : (a : α) → a ∈ s → M), ∏ᶠ (a : α) (h : a ∈ s), f a h = ∏ᶠ (a : α) (_ : a ∈ s), if h' : a ∈ s then f a h' else 1
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The underlying set of a non-empty directed sSup of subfields is just a union of the subfields.
Note that this fails without the directedness assumption (the union of two subfields is
typically not a subfield)  -/
Subfield.mem_iSup_of_directed : ∀ {K : Type u} [inst : DivisionRing K] {ι : Sort u_1} [hι : Nonempty ι] {S : ι → Subfield K},
  Directed (fun x1 x2 => x1 ≤ x2) S → ∀ {x : K}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.map_id : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, Algebra.Extension.Cotangent.map (Algebra.Extension.Hom.id P) = LinearMap.id
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.rotateL_size : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α}, r.Sized → (l.rotateL x r).size = l.size + r.size + 1
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Being terminal is independent of the empty diagram, its universe, and the cone over it,
as long as the cone points are isomorphic.  -/
CategoryTheory.Limits.isLimitChangeEmptyCone : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F₁ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C} →
      {F₂ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w' + 1}) C} →
        {c₁ : CategoryTheory.Limits.Cone F₁} →
          CategoryTheory.Limits.IsLimit c₁ →
            (c₂ : CategoryTheory.Limits.Cone F₂) → (c₁.pt ≅ c₂.pt) → CategoryTheory.Limits.IsLimit c₂
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Given a graph on a set of vertices, we can make it be a `SimpleGraph V` by
adding in the remaining vertices without adding in any additional edges.
This is a wrapper around `SimpleGraph.map`.  -/
SimpleGraph.spanningCoe : {V : Type u_1} → {s : Set V} → SimpleGraph ↑s → SimpleGraph V
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  {J : CategoryTheory.GrothendieckTopology C} [inst_1 : F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C}
  {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  (hf' : CategoryTheory.Sieve.ofArrows X' f' ∈ J S) {D₁ D₂ : F.DescentData f}
  (φ :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂)
  (i : ι),
  CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom✝ w hf' φ i =
    F.presheafHomObjHomEquiv.symm
      (⋯.amalgamate (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements✝ w φ i) ⋯)
-- Mathlib.Topology.Category.UniformSpace
/-- Typecheck a function which is `UniformContinuous` as a morphism in `UniformSpaceCat`.  -/
UniformSpaceCat.ofHom : {X Y : Type u} →
  [inst : UniformSpace X] →
    [inst_1 : UniformSpace Y] →
      { f // UniformContinuous f } → ({ carrier := X, str := inst } ⟶ { carrier := Y, str := inst_1 })
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.coe_withBot : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β),
  ⇑f.withBot = WithBot.map ⇑f
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_ofNat_add' : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddCommMonoidWithOne G]
  [inst_2 : AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) [inst_4 : n.AtLeastTwo] (x : G),
  f (OfNat.ofNat n + x) = f x + OfNat.ofNat n • b
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_singleton_one : ∀ {R : Type u} [inst : NonAssocRing R], Subring.closure {1} = ⊥
-- Mathlib.Order.Atoms
GaloisCoinsertion.isCoatom_of_l_top : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α]
  [inst_3 : OrderTop β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u),
  l ⊤ = ⊤ → ∀ {a : α}, IsCoatom (l a) → IsCoatom a
-- Mathlib.Algebra.Order.Kleene
KleeneAlgebra.one_le_kstar : ∀ {α : Type u_5} [self : KleeneAlgebra α] (a : α), 1 ≤ KStar.kstar a
-- Init.Data.Vector.Lemmas
Vector.back?_isSome : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.back?.isSome = true ↔ n ≠ 0
-- Mathlib.GroupTheory.OrderOfElement
finEquivZPowers_apply : ∀ {G : Type u_1} [inst : Group G] {x : G} (hx : IsOfFinOrder x) {n : Fin (orderOf x)},
  (finEquivZPowers hx) n = ⟨x ^ ↑n, ⋯⟩