mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.monoidalCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.MonoidalCategory (ModuleCat R)
-- Mathlib.CategoryTheory.Localization.Adjunction
CategoryTheory.Adjunction.isLocalization : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) [F.Full] [F.Faithful],
  G.IsLocalization ((CategoryTheory.MorphismProperty.isomorphisms C₂).inverseImage G)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_smulLeftCLM_apply : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {g₁ g₂ : E → 𝕜},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      ∀ (f : SchwartzMap E F),
        (SchwartzMap.smulLeftCLM F g₁) ((SchwartzMap.smulLeftCLM F g₂) f) = (SchwartzMap.smulLeftCLM F (g₁ * g₂)) f
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq_disjoint' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α} {n m : ℕ},
  n < m →
    MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i m = ∅
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.compl : ∀ {α : Type u_1} {V : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq V] {A : Matrix V V α} [inst_2 : Zero α]
  [inst_3 : One α], A.IsAdjMatrix → A.compl.IsAdjMatrix
-- Mathlib.Data.Nat.Factorial.Basic
_private.Mathlib.Data.Nat.Factorial.Basic.0.Nat.ascFactorialBinary.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (k n : ℕ) → k = n + 2 → motive n.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k@h:n.succ.succ => h_3 k n h) =
    h_2 ()
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.hasStrictInitial_of_isUniversal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C],
  CategoryTheory.IsUniversalColimit
      (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.id (⊥_ C))
        (CategoryTheory.CategoryStruct.id (⊥_ C))) →
    CategoryTheory.Limits.HasStrictInitialObjects C
-- Mathlib.Analysis.Normed.Field.Ultra
IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_le_max_norm_one : ∀ {R : Type u_1} [inst : NormedDivisionRing R], (∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1) → IsUltrametricDist R
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_mono_cokernel_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C) [S.HasHomology] [inst_3 : CategoryTheory.Limits.HasCokernel S.f],
  S.Exact ↔ CategoryTheory.Mono (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_toLin : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂)
  (M : Matrix m n R), (LinearMap.toMatrix v₁ v₂) ((Matrix.toLin v₁ v₂) M) = M
-- Mathlib.RingTheory.PowerBasis
/-- Useful lemma to show `x` generates a power basis:
the powers of `x` less than the degree of `x`'s minimal polynomial are linearly independent.  -/
linearIndependent_pow : ∀ {S : Type u_2} [inst : Ring S] {K : Type u_6} [inst_1 : Field K] [inst_2 : Algebra K S] (x : S),
  LinearIndependent K fun i => x ^ ↑i
-- Mathlib.Data.Int.Cast.Defs
/-- The canonical homomorphism `ℤ → R` for negative values is just the negation of the values
of the canonical homomorphism `ℕ → R`.  -/
AddCommGroupWithOne.intCast_negSucc : ∀ {R : Type u} [self : AddCommGroupWithOne R] (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
Irreducible.maximalIdeal_pow_eq_setOfPred_le_v_coe_pow : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)
  [inst_2 : IsDiscreteValuationRing ↥v.integer] {ϖ : ↥v.integer},
  Irreducible ϖ → ∀ (n : ℕ), ↑(IsLocalRing.maximalIdeal ↥v.integer ^ n) = {y | v ↑y ≤ v ↑ϖ ^ n}
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_inv_τ₃ : ∀ {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]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_3),
  (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₃ =
    CategoryTheory.CategoryStruct.id (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Data.Finset.Insert
Finset.insert_def : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α),
  insert a s = { val := Multiset.ndinsert a s.val, nodup := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.exact_iff_surjective_abToCycles : ∀ (S : CategoryTheory.ShortComplex Ab), S.Exact ↔ Function.Surjective ⇑S.abToCycles
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.comp_mapGrp_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (A : CategoryTheory.Grp C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G))
      ((F.comp G).map CategoryTheory.MonObj.one)
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- The logarithmic derivative converts products into sums: away from a codiscrete subset of `𝕜`, the
logarithmic derivative of a finite product of integer powers of meromorphic functions is the
corresponding weighted sum of logarithmic derivatives. This is the shape of statement used in the
differentiated Poisson–Jensen formula, where the exponents are given by a divisor.
 -/
Meromorphic.logDeriv_finprod_zpow_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_3} {F : ι → 𝕜 → 𝕜'} {d : ι → ℤ},
  (Function.support d).Finite →
    (∀ (i : ι), Meromorphic (F i)) →
      (∀ (i : ι) (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤) →
        logDeriv (∏ᶠ (i : ι), F i ^ d i) =ᶠ[Filter.codiscrete 𝕜] fun z => ∑ᶠ (i : ι), d i • logDeriv (F i) z
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddMonoidWithOneOfContinuousAdd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddMonoidWithOne β] → [ContinuousAdd β] → AddMonoidWithOne C(α, β)
-- Init.Prelude
/-- `` `interpolatedStrKind `` is the node kind of an interpolated string literal like `"value = {x}"`
in `s!"value = {x}"`.
 -/
Lean.interpolatedStrKind : Lean.SyntaxNodeKind
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.eraseRecAppSyntax : Lean.Elab.PreDefinition → Lean.CoreM Lean.Elab.PreDefinition
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.toPermInj : ∀ (D : Type u_1) (Q : Type u_2) [inst : Group D] [inst_1 : Group Q] (Λ : Type u_3) [inst_2 : MulAction D Λ]
  [FaithfulSMul D Λ] [Nonempty Λ], Function.Injective ⇑(RegularWreathProduct.toPerm D Q Λ)
-- Mathlib.Lean.MessageData.ForExprs
_private.Mathlib.Lean.MessageData.ForExprs.0.Lean.MessageData.forExprsIn.go : {m : Type → Type u} →
  [Monad m] →
    [MonadLiftT BaseIO m] →
      {σ : Type} →
        (Lean.PPContext × Lean.Expr → σ → m (ForInStep σ)) →
          Lean.NamingContext → Option Lean.MessageDataContext → σ → Lean.MessageData → m (ForInStep σ)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.filter_eq_empty_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool},
  Std.ExtHashMap.filter f m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = false
-- Mathlib.Algebra.FreeAlgebra.Cardinality
FreeAlgebra.cardinalMk_eq_lift : ∀ (R : Type u) [inst : CommSemiring R] (X : Type v) [IsEmpty X],
  Cardinal.mk (FreeAlgebra R X) = Cardinal.lift.{v, u} (Cardinal.mk R)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.tactic.inj : ∀ {stx stx_1 : Lean.Syntax}, Lean.Elab.CompletionInfo.tactic stx = Lean.Elab.CompletionInfo.tactic stx_1 → stx = stx_1
-- Mathlib.AlgebraicGeometry.Sites.Affine
AlgebraicGeometry.Scheme.isOneHypercoverDense_toOver_Spec : ∀ {S : AlgebraicGeometry.Scheme} (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.IsMultiplicative]
  [AlgebraicGeometry.IsZariskiLocalAtSource P] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P],
  (CategoryTheory.MorphismProperty.CostructuredArrow.toOver P AlgebraicGeometry.Scheme.Spec S).IsOneHypercoverDense
    ((CategoryTheory.MorphismProperty.CostructuredArrow.toOver P AlgebraicGeometry.Scheme.Spec S).inducedTopology
      (AlgebraicGeometry.Scheme.smallGrothendieckTopology P S))
    (AlgebraicGeometry.Scheme.smallGrothendieckTopology P S)
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.smul_set_univ₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → a • Set.univ = Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.instHasPushoutComp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'],
  CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.split'.match_1.splitter : (motive : ONote × ℕ → Sort u_1) → (x : ONote × ℕ) → ((a' : ONote) → (m : ℕ) → motive (a', m)) → motive x
-- Mathlib.Topology.Bases
SecondCountableTopology.mk : ∀ {α : Type u} [t : TopologicalSpace α],
  (∃ b, b.Countable ∧ t = TopologicalSpace.generateFrom b) → SecondCountableTopology α
-- Init.Data.String.Bootstrap
String.Internal.capitalize : String → String
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.coeff_divMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (s : σ →₀ ℕ) (x : MvPolynomial σ R) (s' : σ →₀ ℕ),
  MvPolynomial.coeff s' (x.divMonomial s) = MvPolynomial.coeff (s + s') x
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_eq_left_iff : ∀ {a b : Cardinal.{u_1}}, a + b = a ↔ max Cardinal.aleph0 b ≤ a ∨ b = 0
-- Mathlib.Order.WellFoundedSet
/-- Stronger version of `WellFounded.prod_lex`. Instead of requiring `rβ on g` to be well-founded,
we only require it to be well-founded on fibers of `f`.  -/
WellFounded.prod_lex_of_wellFoundedOn_fiber : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {rα : α → α → Prop} {rβ : β → β → Prop} {f : γ → α} {g : γ → β},
  WellFounded (Function.onFun rα f) →
    (∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (Function.onFun rβ g)) →
      WellFounded (Function.onFun (Prod.Lex rα rβ) fun c => (f c, g c))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_alter!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [Inhabited α],
  t.WF →
    ∀ {k fallback : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).getKeyD k fallback =
        if (f (t.get? k)).isSome = true then k else fallback
-- Mathlib.Data.List.Lattice
List.cons_bagInter_of_mem : ∀ {α : Type u_1} {l₂ : List α} {a : α} [inst : DecidableEq α] (l₁ : List α),
  a ∈ l₂ → (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.IsUniversal.existsUnique : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal)
  (g : CategoryTheory.StructuredArrow S T), ∃! η, CategoryTheory.CategoryStruct.comp f.hom (T.map η) = g.hom
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.isBoundaryPoint_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M},
  I.IsBoundaryPoint x ↔ ↑(extChartAt I x) x ∈ frontier (Set.range ↑I)
-- Mathlib.Analysis.Convolution
/-- The convolution is continuous if one function is integrable and the other is bounded and
continuous.  -/
BddAbove.continuous_convolution_right_of_integrable : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddGroup G] [inst_10 : TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G]
  [FirstCountableTopology G] [SecondCountableTopologyEither G E'],
  BddAbove (Set.range fun x => ‖g x‖) →
    MeasureTheory.Integrable f μ → Continuous g → Continuous (MeasureTheory.convolution f g L μ)
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_eq_inv : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α} [MulLeftMono α], a⁻ᵐ = a⁻¹ ↔ a ≤ 1
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.continuous_apply : ∀ {R A : CommRingCat} [inst : TopologicalSpace ↑R] (x : ↑A), Continuous fun f => (CommRingCat.Hom.hom f) x
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
/-- [Stacks Tag 09HS](https://stacks.math.columbia.edu/tag/09HS) -/
card_algHom_le_finrank : ∀ (K : Type u_1) (M : Type u_2) (L : Type v) [inst : CommRing K] [inst_1 : Ring M] [inst_2 : Algebra K M]
  [Module.Free K M] [Module.Finite K M] [inst_5 : CommRing L] [IsDomain L] [inst_7 : Algebra K L],
  Nat.card (M →ₐ[K] L) ≤ Module.finrank K M
-- Mathlib.CategoryTheory.Action.Basic
CategoryTheory.Functor.mapAction_obj_ρ_apply : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} W] (F : CategoryTheory.Functor V W) (G : Type u_3) [inst_2 : Monoid G]
  (M : Action V G) (g : G), ((F.mapAction G).obj M).ρ g = F.map (M.ρ g)
-- Mathlib.Topology.Separation.DisjointCover
/-- Any open cover of a profinite space can be refined to a finite cover by pairwise disjoint
nonempty clopens.  -/
TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X]
  {U : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover U →
    ∃ n W,
      (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ i, ↑(W j) ⊆ ↑(U i)) ∧ Set.univ ⊆ ⋃ j, ↑(W j) ∧ Pairwise (Function.onFun Disjoint W)
-- Mathlib.CategoryTheory.Localization.Trifunctor
CategoryTheory.Localization.lift₃NatIso_inv : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13}
  [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} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃]
  [inst_6 : CategoryTheory.Category.{v_13, u_13} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (L₃ : CategoryTheory.Functor C₃ D₃) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) (W₃ : CategoryTheory.MorphismProperty C₃) [inst_7 : L₁.IsLocalization W₁]
  [inst_8 : L₂.IsLocalization W₂] [inst_9 : L₃.IsLocalization W₃] [inst_10 : W₁.ContainsIdentities]
  [inst_11 : W₂.ContainsIdentities] [inst_12 : W₃.ContainsIdentities]
  (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))
  (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)))
  [inst_13 : CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁']
  [inst_14 : CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'] (e : F₁ ≅ F₂),
  (CategoryTheory.Localization.lift₃NatIso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' e).inv =
    CategoryTheory.Localization.lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₁ F₂' F₁' e.inv
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_nonempty : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, (s -ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.process.checkMVar : Lean.Expr → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map_inv_mul_map : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (g : GL n R),
  (Matrix.GeneralLinearGroup.map f) g⁻¹ * (Matrix.GeneralLinearGroup.map f) g = 1
-- Lean.Compiler.Old
Lean.Compiler.isEagerLambdaLiftingName : Lean.Name → Bool
-- Mathlib.Data.Fintype.Powerset
Fintype.card_finset : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card (Finset α) = 2 ^ Fintype.card α
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.isoBiproductEmbedding_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (M : CategoryTheory.Mat_ C),
  M.isoBiproductEmbedding.hom =
    CategoryTheory.Limits.biproduct.lift fun i j x => if h : j = i then CategoryTheory.eqToHom ⋯ else 0
-- Mathlib.Topology.PartialHomeomorph.Defs
/-- See Note [custom simps projection]  -/
PartialHomeomorph.Simps.symm_apply : {X : Type u_1} →
  {Y : Type u_3} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → PartialHomeomorph X Y → Y → X
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.bot_meet : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l}, Lean.Order.meet Lean.Order.bot P = Lean.Order.bot
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.separatingRight_toBilin'_iff : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {M : Matrix ι ι R₂},
  LinearMap.SeparatingRight (Matrix.toBilin' M) ↔ M.SeparatingRight
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_eq_prod_iff_of_le : ∀ {ι : Type u_9} {M : Type u_10} [inst : CommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelMonoid M]
  {s : Finset ι} {f g : ι → M}, (∀ i ∈ s, f i ≤ g i) → (∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i)
-- Mathlib.Algebra.CharP.Two
CharTwo.neg_eq' : ∀ {R : Type u_1} [inst : Ring R] [CharP R 2], Neg.neg = id
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.map_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} D]
  [inst_3 : CategoryTheory.Preadditive D] (z : CochainComplex.HomComplex.Cochain K L n) (Φ : CategoryTheory.Functor C D)
  [inst_4 : Φ.Additive] (p q : ℤ) (hpq : p + n = q), (z.map Φ).v p q hpq = Φ.map (z.v p q hpq)
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.mk.sizeOf_spec : ∀ (name url cmd : String) (query : String → ℕ → Lean.MetaM (Array LeanSearchClient.SearchResult))
  (queryNum : Lean.CoreM ℕ),
  sizeOf { name := name, url := url, cmd := cmd, query := query, queryNum := queryNum } =
    1 + sizeOf name + sizeOf url + sizeOf cmd
-- Mathlib.Algebra.Ring.GeomSum
Commute.mul_geom_sum₂_Ico : ∀ {R : Type u_1} [inst : Ring R] {x y : R},
  Commute x y →
    ∀ {m n : ℕ}, m ≤ n → (x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.binary_fan_fst_toCone : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q), CategoryTheory.Limits.BinaryFan.fst c.toCone = c.fst
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceSubtype : {α : Type ua} → {p : α → Prop} → [t : UniformSpace α] → UniformSpace (Subtype p)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.totallyBounded_subsets_of_totallyBounded : ∀ {α : Type u_1} [inst : UniformSpace α] {t : Set α}, TotallyBounded t → TotallyBounded {K | ↑K ⊆ t}
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.inv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'}, Meromorphic f → Meromorphic f⁻¹
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_injective : ∀ {α : Type u_1} [inst : PartialOrder α], Function.Injective Set.Iic
-- Mathlib.CategoryTheory.Join.Basic
/-- The right inclusion is fully faithful.  -/
CategoryTheory.Join.inclRightFullyFaithful : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (CategoryTheory.Join.inclRight C D).FullyFaithful
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.mk.injEq : ∀ {R : Type u_2} [inst : NonUnitalNonAssocRing R] (toAddGroupSeminorm : AddGroupSeminorm R)
  (mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y)
  (toAddGroupSeminorm_1 : AddGroupSeminorm R)
  (mul_le'_1 :
    ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) ≤ toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y),
  ({ toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' } =
      { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 }) =
    (toAddGroupSeminorm = toAddGroupSeminorm_1)
-- Aesop.Frontend.RuleExpr
Lean.Parser.Category.Aesop.builder_name : Lean.Parser.Category
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.not_isFragment_empty : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {S : Finset G},
  K < 1 → S.Nonempty → ¬Finset.IsFragment✝ K S ∅
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.IsReflexivePair.common_section' : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A B : C} {f g : A ⟶ B}
  [self : CategoryTheory.IsReflexivePair f g],
  ∃ s,
    CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B ∧
      CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B
-- Mathlib.Order.Hom.Lattice
SupHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β] {f g : SupHom α β}, (∀ (a : α), f a = g a) → f = g
-- Lean.Elab.MutualDef
Lean.Elab.Term.debug.proofAsSorry : Lean.Option Bool