mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_alter_eq_add_one : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option β → Option β}, m.WF → k ∉ m → (f m[k]?).isSome = true → (m.alter k f).size = m.size + 1
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_inv_fac_app_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesLeftKanExtension F L] [inst_5 : L.HasLeftKanExtension F] (a : A)
  {Z : D} (h : G.obj ((L.leftKanExtension F).obj (L.obj a)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit (F.comp G)).app a)
      (CategoryTheory.CategoryStruct.comp ((G.leftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) h) =
    CategoryTheory.CategoryStruct.comp (G.map ((L.leftKanExtensionUnit F).app a)) h
-- Mathlib.Order.Bounds.Image
BddAbove.bddBelow_image2_of_bddBelow : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → BddAbove s → BddBelow t → BddBelow (Set.image2 f s t)
-- Mathlib.Combinatorics.Colex
Finset.geomSum_injective : ∀ {n : ℕ}, 2 ≤ n → Function.Injective fun s => ∑ i ∈ s, n ^ i
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minEntryD.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) (size : ℕ)
  (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β)
  (fallback : (a : α) × β a) (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : (a : α) × β a) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1,
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
      fallback => h_3 size k v l size_2 k_2 v_2 l_1 r h r_2 fallback) =
    h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 fallback
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.mkLine_ax : ∀ {P : Type u_1} {L : Type u_2} {inst : Membership P L} [self : Configuration.ProjectivePlane P L] {p₁ p₂ : P}
  (h : p₁ ≠ p₂), p₁ ∈ Configuration.ProjectivePlane.mkLine h ∧ p₂ ∈ Configuration.ProjectivePlane.mkLine h
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.Hom.hom_r_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S₁ S₂ : CategoryTheory.Span Wₗ Wᵣ c c'} (self : S₁.Hom S₂) {Z : C} (h : c' ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp S₂.r h) =
    CategoryTheory.CategoryStruct.comp S₁.r h
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.arrowCongr_apply : ∀ {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_12} {R₂' : Type u_13} {M₁ : Type u_17} {M₂ : Type u_18}
  {M₁' : Type u_20} {M₂' : Type u_21} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : CommSemiring R₁']
  [inst_3 : CommSemiring R₂'] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid M₁']
  [inst_7 : AddCommMonoid M₂'] [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] [inst_10 : Module R₁' M₁']
  [inst_11 : Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'}
  {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [inst_12 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_13 : RingHomInvPair σ₂₁ σ₁₂] [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂']
  [inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂)
  (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : M₁ →ₛₗ[σ₁₁'] M₁') (x : M₂), ((e₁.arrowCongr e₂) f) x = e₂ (f (e₁.symm x))
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_a_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a ≠ 0 → P.toPoly.natDegree = 3
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- Interpret a homotopy `H : C(I × X, Y)` as a map `C(ULift I × X, Y)`  -/
ContinuousMap.Homotopy.uliftMap : {X Y : TopCat} → {f g : C(↑X, ↑Y)} → f.Homotopy g → C(↑(TopCat.of (ULift.{u, 0} ↑unitInterval × ↑X)), ↑Y)
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.u_inf : ∀ {β : Type u} {α : Type v} {b₁ b₂ : β} [inst : SemilatticeInf β] [inst_1 : SemilatticeInf α] {u : β → α} {l : α → β},
  GaloisConnection l u → u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.opMap_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂), (CategoryTheory.ShortComplex.opMap φ).τ₁ = φ.τ₃.op
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.notValue.inj : ∀ {bvarIdx : ℕ} {strict : Bool} {bvarIdx_1 : ℕ} {strict_1 : Bool},
  Lean.Meta.Grind.EMatchTheoremConstraint.notValue bvarIdx strict =
      Lean.Meta.Grind.EMatchTheoremConstraint.notValue bvarIdx_1 strict_1 →
    bvarIdx = bvarIdx_1 ∧ strict = strict_1
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isFlat_iff : ∀ {α : Type u_2} (M : Matroid α) (F : Set α),
  M.IsFlat F ↔ (∀ ⦃I X : Set α⦄, M.IsBasis I F → M.IsBasis I X → X ⊆ F) ∧ F ⊆ M.E
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.GammaIntegral.eq_1 : ∀ (s : ℂ), s.GammaIntegral = ∫ (x : ℝ) in Set.Ioi 0, ↑(Real.exp (-x)) * ↑x ^ (s - 1)
-- Mathlib.Algebra.Group.Hom.Basic
invMonoidHom_comp_invMonoidHom : ∀ {α : Type u_1} [inst : DivisionCommMonoid α], invMonoidHom.comp invMonoidHom = MonoidHom.id α
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zero : ∀ {F : Type u_1} [inst : Field F] {v w : AbsoluteValue F ℝ},
  v.IsEquiv w → ∀ {U : Set (WithAbs v)}, U ∈ nhds 0 → ⇑(WithAbs.congr v w (RingEquiv.refl F)) '' U ∈ nhds 0
-- Mathlib.Data.Set.Basic
Set.Nonempty.some_mem : ∀ {α : Type u} {s : Set α} (h : s.Nonempty), h.some ∈ s
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- `AddActionHom` maps `fixedPoints` to `fixedPoints`.  -/
AddActionHom.map_mem_fixedPoints : ∀ {G : Type u_1} {A : Type u_2} {B : Type u_3} [inst : AddMonoid G] [inst_1 : AddAction G A] [inst_2 : AddAction G B]
  (f : A →ₑ[id] B) {H : AddSubmonoid G} {a : A}, a ∈ AddAction.fixedPoints (↥H) A → f a ∈ AddAction.fixedPoints (↥H) B
-- Mathlib.GroupTheory.OrderOfElement
/-- A nonempty idempotent subset of a finite cancellative monoid is a submonoid  -/
submonoidOfIdempotent : {M : Type u_6} → [inst : LeftCancelMonoid M] → [Finite M] → (S : Set M) → S.Nonempty → S * S = S → Submonoid M
-- Mathlib.GroupTheory.Abelianization.Defs
abelianizationCongr_of : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (e : G ≃* H) (x : G),
  e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x)
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasure.instFunLikeSetENNReal : {α : Type u_1} → FunLike (MeasureTheory.OuterMeasure α) (Set α) ENNReal
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negAddY_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.negAddY P Q = (P 0 * Q 2) ^ 3 * W'.negY Q
-- Lean.Data.Json.Basic
Lean.JsonNumber.instOfNat : {n : ℕ} → OfNat Lean.JsonNumber n
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `iteratedFDeriv_add` -/
fun_iteratedFDeriv_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {i : ℕ}
  {f g : E → F},
  ContDiff 𝕜 (↑i) f →
    ContDiff 𝕜 (↑i) g →
      (iteratedFDeriv 𝕜 i fun i => f i + g i) = fun i_1 => iteratedFDeriv 𝕜 i f i_1 + iteratedFDeriv 𝕜 i g i_1
-- Init.Data.Vector.Lemmas
Vector.getElem_append : ∀ {α : Type u_1} {n m i : ℕ} {xs : Vector α n} {ys : Vector α m} (hi : i < n + m),
  (xs ++ ys)[i] = if h : i < n then xs[i] else ys[i - n]
-- Mathlib.Analysis.Convex.Intrinsic
/-- **Alias** of the forward direction of `intrinsicClosure_nonempty`. -/
Set.Nonempty.ofIntrinsicClosure : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P}, (intrinsicClosure 𝕜 s).Nonempty → s.Nonempty
-- Init.Data.SInt.Lemmas
Int8.toBitVec_toInt16 : ∀ (x : Int8), x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.nonsing_inv_apply : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  (h : IsUnit A.det), A⁻¹ = ↑h.unit⁻¹ • A.adjugate
-- Init.Data.List.Lemmas
List.eq_nil_or_concat : ∀ {α : Type u_1} (l : List α), l = [] ∨ ∃ l' b, l = l'.concat b
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_le_measure_union_left : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α}, μ s ≤ μ (s ∪ t)
-- Init.Data.BitVec.Lemmas
BitVec.not_xor_right : ∀ {w : ℕ} {x y : BitVec w}, ~~~(x ^^^ y) = x ^^^ ~~~y
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
/-- The category `Cᵒᵖ` is equipped with the shift such that the shift by `n` on `Cᵒᵖ`
corresponds to the shift by `-n` on `C`.  -/
CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.HasShift C ℤ] → CategoryTheory.HasShift Cᵒᵖ ℤ
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.vaddInvariantMeasure_iterateAddAct : ∀ {α : Type w} {f : α → α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  Measurable f → (MeasureTheory.VAddInvariantMeasure (IterateAddAct f) α μ ↔ MeasureTheory.MeasurePreserving f μ μ)
-- Qq.Match
Qq.Impl.PatternVar.name : Qq.Impl.PatternVar → Lean.Name
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The ring isomorphism between the ring `R` and the global sections `Γ(X, 𝒪ₓ)`.  -/
AlgebraicGeometry.StructureSheaf.globalSectionsIso : (R : Type u) →
  [inst : CommRing R] → CommRingCat.of R ≅ (AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op ⊤)
-- Init.Data.List.Impl
List.filterMapTR.go.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) (a : Array β) (a_1 : α) (as : List α),
  List.filterMapTR.go f (a_1 :: as) a =
    match f a_1 with
    | none => List.filterMapTR.go f as a
    | some b => List.filterMapTR.go f as (a.push b)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.filter.pi.match_1.splitter : {n : ℕ} →
  {G : SimpleGraph (Fin n)} →
    [inst : DecidableRel G.Adj] →
      {r t t' : ℕ} →
        (K : G.CompleteEquipartiteSubgraph r t') →
          (motive : ↥(SimpleGraph.ErdosStone.filter✝ K t) → Sort u_1) →
            (x : ↥(SimpleGraph.ErdosStone.filter✝ K t)) →
              ((val : Fin n) → (h : val ∈ SimpleGraph.ErdosStone.filter✝ K t) → motive ⟨val, h⟩) → motive x
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- A **left-uniform additive group** is a topological additive group endowed with the associated
left uniform structure: the uniformity filter `𝓤 G` is the inverse image of `𝓝 0` by the map
`(x, y) ↦ (-x) + y`.

In other words, we declare that two points `x` and `y` are infinitely close
precisely when `(-x) + y` is infinitely close to `0`.  -/
IsLeftUniformAddGroup : (G : Type u_7) → [UniformSpace G] → [AddGroup G] → Prop
-- Mathlib.Topology.Separation.CompletelyRegular
/-- A space is completely regular if points can be separated from closed sets via
continuous functions to the unit interval.  -/
CompletelyRegularSpace : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the reverse direction of `isExtrFilter_dual_iff`. -/
IsExtrFilter.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsExtrFilter f l a → IsExtrFilter (⇑OrderDual.toDual ∘ f) l a
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.smul_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} {R : Type u_2} [inst_2 : Semiring R]
  [inst_3 : CategoryTheory.Linear R V] (h : Homotopy f g) (a : R) (i j : ι), (h.smul a).hom i j = a • h.hom i j
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.tendsto_re : ∀ {l : Filter ℂ}, Complex.IsExpCmpFilter l → Filter.Tendsto Complex.re l Filter.atTop
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
IterateMulAct.instDiscreteMeasurableSpace : ∀ {α : Type u_1} {f : α → α}, DiscreteMeasurableSpace (IterateMulAct f)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
LinearEquiv.coe_toAffineEquiv : ∀ {k : Type u_1} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂]
  [inst_3 : Module k V₁] [inst_4 : Module k V₂] (e : V₁ ≃ₗ[k] V₂), ⇑e.toAffineEquiv = ⇑e
-- Mathlib.Topology.ContinuousOn
/-- If a function is continuous on two closed sets, it is also continuous on their union.  -/
ContinuousOn.union_of_isClosed : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s t : Set α} {f : α → β},
  ContinuousOn f s → ContinuousOn f t → IsClosed s → IsClosed t → ContinuousOn f (s ∪ t)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ'_zero : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ' 0 = 0
-- Lean.Parser.Extension
Lean.Parser.addParser : Lean.Parser.ParserCategories →
  Lean.Name → Lean.Name → Bool → Lean.Parser.Parser → ℕ → Except String Lean.Parser.ParserCategories
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.Lifting₂.liftingLift₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                      {W₁ : CategoryTheory.MorphismProperty C₁} →
                        {W₂ : CategoryTheory.MorphismProperty C₂} →
                          (hF : W₁.IsInvertedBy₂ W₂ F) →
                            (L₁ : CategoryTheory.Functor C₁ D₁) →
                              (L₂ : CategoryTheory.Functor C₂ D₂) →
                                [inst_5 : L₁.IsLocalization W₁] →
                                  [inst_6 : L₂.IsLocalization W₂] →
                                    [inst_7 : W₁.ContainsIdentities] →
                                      [inst_8 : W₂.ContainsIdentities] →
                                        (X₁ : C₁) →
                                          CategoryTheory.Localization.Lifting L₂ W₂ (F.obj X₁)
                                            ((CategoryTheory.Localization.lift₂ F hF L₁ L₂).obj (L₁.obj X₁))
-- Mathlib.LinearAlgebra.JordanChevalley
Module.End.exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {f : Module.End K V}
  {P : Polynomial K} {k : ℕ},
  P.Separable → minpoly K f ∣ P ^ k → ∃ n ∈ K[f], ∃ s ∈ K[f], IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
-- Lean.Elab.Declaration
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.splitMutualPreamble.loop : Array Lean.Syntax → ℕ → Option (Array Lean.Syntax × Array Lean.Syntax)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_const : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (g : β → γ) (b : β),
  MeasureTheory.SimpleFunc.map g (MeasureTheory.SimpleFunc.const α b) = MeasureTheory.SimpleFunc.const α (g b)
-- Mathlib.Algebra.Squarefree.Basic
irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [WfDvdMonoid R] (r : R),
  (∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
-- Mathlib.Analysis.Normed.Operator.Extend
LinearMap.extendOfNorm_eq : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : NormedDivisionRing 𝕜]
  [inst_1 : NormedDivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : AddCommGroup E] [inst_3 : SeminormedAddCommGroup Eₗ]
  [inst_4 : NormedAddCommGroup F] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ F] [inst_7 : IsBoundedSMul 𝕜₂ F]
  [inst_8 : Module 𝕜 Eₗ] [inst_9 : IsBoundedSMul 𝕜 Eₗ] [inst_10 : CompleteSpace F] {f : E →ₛₗ[σ₁₂] F} {e : E →ₗ[𝕜] Eₗ},
  DenseRange ⇑e → (∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖) → ∀ (x : E), (f.extendOfNorm e) (e x) = f x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.RankFunction.mk.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] (rank rank_1 : h.ι → α)
  (e_rank : rank = rank_1) (lt : ∀ {x y : h.ι}, h.AncestralRel x y → rank x < rank y),
  { rank := rank, lt := lt } = { rank := rank_1, lt := ⋯ }
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_eq_iff_eq_sq_sinh : ∀ {z w : UpperHalfPlane} {r : ℝ}, 0 ≤ r → (dist z w = r ↔ dist ↑z ↑w ^ 2 / (4 * z.im * w.im) = Real.sinh (r / 2) ^ 2)
-- Mathlib.Algebra.Order.Ring.GeomSum
geom_sum_pos_and_lt_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R},
  x < 0 → 0 < x + 1 → 1 < n → 0 < ∑ i ∈ Finset.range n, x ^ i ∧ ∑ i ∈ Finset.range n, x ^ i < 1
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Given a closed set `s`, a point belongs to `s` iff its infimum edistance to this set vanishes  -/
Metric.mem_iff_infEDist_zero_of_closed : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, IsClosed s → (x ∈ s ↔ Metric.infEDist x s = 0)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda₀_mapId_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda₀ x).mapId a).inv.toNatTrans.app X = (CategoryTheory.Bicategory.leftUnitor X).inv
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.simple_mul_simple_self : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  cs.simple i * cs.simple i = 1
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_orbit_of_mem_orbit : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] {a₁ a₂ : α} (m : M),
  a₂ ∈ AddAction.orbit M a₁ → m +ᵥ a₂ ∈ AddAction.orbit M a₁
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
_private.Mathlib.Algebra.Order.Monoid.Unbundled.WithTop.0.WithTop.addMonoid.match_1.eq_3 : ∀ {α : Type u_1} (motive : WithTop α → ℕ → Sort u_2) (_n : ℕ) (h_1 : (a : α) → (n : ℕ) → motive (some a) n)
  (h_2 : Unit → motive none 0) (h_3 : (_n : ℕ) → motive none _n.succ),
  (match none, _n.succ with
    | some a, n => h_1 a n
    | none, 0 => h_2 ()
    | none, _n.succ => h_3 _n) =
    h_3 _n
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_closure : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M} {x : M},
  x ∈ (FirstOrder.Language.Substructure.closure L).toFun s ↔ ∀ (S : L.Substructure M), s ⊆ ↑S → x ∈ S
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.extend_ℐ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A) (η : A ⟶ B) [inst_1 : CategoryTheory.IsIso η],
  (P.extend η).ℐ = P.ℐ
-- Lean.Util.MonadBacktrack
/-- Execute `x?`, but backtrack state if result is `none` or an exception was thrown.
If an exception is thrown, `none` is returned.
That is, this function is similar to `commitWhenSome?`, but swallows the exception and returns `none`.
 -/
Lean.commitWhenSomeNoEx? : {m : Type → Type} →
  {s : Type} →
    {ε : Type u_1} →
      {α : Type} → [Monad m] → [Lean.MonadBacktrack s m] → [MonadExcept ε m] → m (Option α) → m (Option α)
-- Mathlib.SetTheory.Lists
Lists'.atom : {α : Type u} → α → Lists' α false
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.Bool.bif_eq_not_bif' : ∀ (d a b c : Bool), ((bif d then a else c) == !bif d then b else c) = (d && a == !b)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
orthonormal_sUnion_of_directed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {s : Set (Set E)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) s → (∀ a ∈ s, Orthonormal 𝕜 fun x => ↑x) → Orthonormal 𝕜 fun x => ↑x
-- Lean.Parser.Extension
Lean.Parser.addParserCategory : Lean.Environment → Lean.Name → Lean.Name → Lean.Parser.LeadingIdentBehavior → Except String Lean.Environment
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.biproduct_ι_comp_leftDistributor_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (X : C) (f : J → C) (j : J)
  {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) h
-- Mathlib.Data.NNReal.Basic
NNReal.le_iInf_mul_iInf : ∀ {ι : Sort u_3} [Nonempty ι] {a : NNReal} {g h : ι → NNReal}, (∀ (i j : ι), a ≤ g i * h j) → a ≤ iInf g * iInf h
-- Lean.Meta.Match.Match
Lean.Meta.Match.withMkMatcherInput : {α : Type} → Lean.Name → Bool → (Lean.Meta.Match.MkMatcherInput → Lean.MetaM α) → Lean.MetaM α