mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.μ_inv_natural_left_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) {Z : CategoryTheory.LocalizedMonoidal L W ε}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X₂)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X₁ Y).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map f)
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y))
        h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X₂ Y).inv h)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.addGroup : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → AddGroup (CauSeq β abv)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryLeft_norm : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G), ‖f.curryLeft‖ = ‖f‖
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  (X_1 : CategoryTheory.Sheaf (J.over Z) A) (X_2 : (CategoryTheory.Over X)ᵒᵖ),
  ((J.overMapPullbackComp A f g).hom.app X_1).hom.app X_2 =
    X_1.obj.map ((CategoryTheory.Over.mapComp f g).hom.app (Opposite.unop X_2)).op
-- Mathlib.Logic.Basic
/-- This function has the same type as `Exists.recOn`, and can be used to case on an equality,
but `Exists.recOn` can only eliminate into Prop, while this version eliminates into any universe
using the axiom of choice.  -/
Exists.classicalRecOn : {α : Sort u_1} → {p : α → Prop} → (∃ a, p a) → {C : Sort u_2} → ((a : α) → p a → C) → C
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- A morphism from the "infimum" of two objects in `MonoOver A` to the first object.  -/
CategoryTheory.MonoOver.infLELeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {A : C} → (f g : CategoryTheory.MonoOver A) → (CategoryTheory.MonoOver.inf.obj f).obj g ⟶ f
-- Init.Data.SInt.Lemmas
Int64.toInt_minValue_lt_zero : Int64.minValue.toInt < 0
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.π₀.rec : ∀ {X : SSet} {motive : X.π₀ → Prop},
  (∀ (x : X.obj (Opposite.op { len := 0 })), motive (SSet.π₀.mk x)) → ∀ (x : X.π₀), motive x
-- Mathlib.Data.PNat.Prime
PNat.prime_three : PNat.Prime 3
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.instProdUniformSpace : (p : ENNReal) → (α : Type u_2) → (β : Type u_3) → [UniformSpace α] → [UniformSpace β] → UniformSpace (WithLp p (α × β))
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.IsAffineMap.const : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] [inst_4 : Convexity.ConvexSpace R N] (x : N),
  Convexity.IsAffineMap R fun x_1 => x
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instHasZeroObject : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G], CategoryTheory.Limits.HasZeroObject (Rep.{w, u, v} k G)
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkCongrDefaultProof.loop : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Init.Data.Vector.Lemmas
Vector.mem_flatten : ∀ {α : Type u_1} {n m : ℕ} {a : α} {xss : Vector (Vector α n) m}, a ∈ xss.flatten ↔ ∃ xs ∈ xss, a ∈ xs
-- Plausible.Testable
/-- `Testable p` uses random examples to try to disprove `p`.  -/
Plausible.Testable : Prop → Type
-- Init.Data.BitVec.Bitblast
BitVec.sshiftRightRec_zero_eq : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y 0 = x.sshiftRight' (y &&& BitVec.twoPow w₂ 0)
-- Mathlib.GroupTheory.Commutator.Basic
addConj_eq_addCommutatorElement_add : ∀ {G : Type u_1} [inst : AddGroup G] {g₁ g₂ : G}, (AddAut.addConj g₁) g₂ = ⁅g₁, g₂⁆ + g₂
-- Mathlib.GroupTheory.QuotientGroup.Basic
MonoidHom.domRestrictHomKerEquiv_apply_coe : ∀ {G : Type u} [inst : Group G] (A : Type u_1) [inst_1 : CommGroup A] (H : Subgroup G) [inst_2 : H.Normal]
  (f : ↥(MonoidHom.domRestrictHom H A).ker) (g : G), ((MonoidHom.domRestrictHomKerEquiv A H) f) ↑g = ↑f g
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.Set.univ_apply : ∀ (X : Type u_7) [inst : TopologicalSpace X], ⇑(Homeomorph.Set.univ X) = Subtype.val
-- Init.Data.BitVec.Bitblast
BitVec.uppcRec.eq_def : ∀ {w : ℕ} (x : BitVec w) (s : ℕ) (hs : s < w),
  x.uppcRec s hs =
    match s, hs with
    | 0, hs => x.msb
    | i.succ, hs => x[w - 1 - i] || x.uppcRec i ⋯
-- Mathlib.Analysis.Seminorm
Seminorm.instIsZeroApplyReal : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E],
  IsZeroApply (Seminorm 𝕜 E) E ℝ
-- Init.Data.Order.LemmasExtra
Std.IsLinearOrder.of_ord : ∀ {α : Type u} [inst : LE α] [inst_1 : Ord α] [Std.LawfulOrderOrd α] [Std.TransOrd α] [Std.LawfulEqOrd α],
  Std.IsLinearOrder α
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.mk : {α : Type u} →
  [toDist : Dist α] →
    (∀ (x : α), dist x x = 0) →
      (∀ (x y : α), dist x y = dist y x) →
        (∀ (x y z : α), dist x z ≤ dist x y + dist y z) →
          (edist : α → α → ENNReal) →
            autoParam (∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)) PseudoMetricSpace.edist_dist._autoParam →
              (toUniformSpace : UniformSpace α) →
                autoParam (uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε})
                    PseudoMetricSpace.uniformity_dist._autoParam →
                  (toBornology : Bornology α) →
                    autoParam ((Bornology.cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C})
                        PseudoMetricSpace.cobounded_sets._autoParam →
                      PseudoMetricSpace α
-- Lean.Elab.Tactic.Omega.Core
/-- Run Fourier-Motzkin elimination on one variable.
 -/
Lean.Elab.Tactic.Omega.Problem.fourierMotzkin : Lean.Elab.Tactic.Omega.Problem → Lean.MetaM Lean.Elab.Tactic.Omega.Problem
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.instInhabitedFeature.default : Aesop.Frontend.Feature
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∪ t₂).get? k = t₂.get? k
-- Init.Data.List.Lemmas
List.getElem?_set : ∀ {α : Type u_1} {l : List α} {i j : ℕ} {a : α},
  (l.set i a)[j]? = if i = j then if i < l.length then some a else none else l[j]?
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.orbit.pairwiseDisjoint : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X],
  (Set.range fun x => MulAction.orbit G x).PairwiseDisjoint id
-- Std.Async.System
Std.Async.System.instInhabitedGroupId : Inhabited Std.Async.System.GroupId
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles : ∀ {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₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₃₄ : i₂ ⟶ i₄),
  CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄ →
    ∀ (f₄₅ : i₃ ⟶ i₅) (h₄₅ : CategoryTheory.CategoryStruct.comp f₄ f₅ = f₄₅) (n₀ n₁ n₂ n₃ : ℤ)
      (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles._auto_1)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles._auto_3)
      (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles._auto_5),
      CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
          (CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₂)) =
        CategoryTheory.CategoryStruct.comp (X.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂)
          (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f₄ f₅ f₄₅ h₄₅ n₁) (X.δ f₂₃ f₄₅ n₁ n₂ hn₂))
-- Mathlib.LinearAlgebra.TensorProduct.Prod
TensorProduct.prodLeft_symm_tmul : ∀ (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃]
  [inst_5 : Algebra R S] [inst_6 : Module R M₁] [inst_7 : Module S M₁] [inst_8 : IsScalarTower R S M₁]
  [inst_9 : Module R M₂] [inst_10 : Module R M₃] [inst_11 : Module S M₂] [inst_12 : IsScalarTower R S M₂] (m₁ : M₁)
  (m₂ : M₂) (m₃ : M₃), (TensorProduct.prodLeft R S M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃) = (m₁, m₂) ⊗ₜ[R] m₃
-- Init.Core
/-- Transfer a decidability proof across an equivalence of propositions.  -/
decidable_of_decidable_of_iff : {p q : Prop} → [Decidable p] → (p ↔ q) → Decidable q
-- Lean.Elab.Command
Lean.Elab.Command.Context.mk.injEq : ∀ (fileName : String) (fileMap : Lean.FileMap) (currRecDepth : ℕ) (cmdPos : String.Pos.Raw)
  (macroStack : Lean.Elab.MacroStack) (quotContext? : Option Lean.Name) (currMacroScope : Lean.MacroScope)
  (ref : Lean.Syntax) (snap? : Option (Lean.Language.SnapshotBundle Lean.Language.DynamicSnapshot))
  (cancelTk? : Option IO.CancelToken) (suppressElabErrors : Bool) (fileName_1 : String) (fileMap_1 : Lean.FileMap)
  (currRecDepth_1 : ℕ) (cmdPos_1 : String.Pos.Raw) (macroStack_1 : Lean.Elab.MacroStack)
  (quotContext?_1 : Option Lean.Name) (currMacroScope_1 : Lean.MacroScope) (ref_1 : Lean.Syntax)
  (snap?_1 : Option (Lean.Language.SnapshotBundle Lean.Language.DynamicSnapshot)) (cancelTk?_1 : Option IO.CancelToken)
  (suppressElabErrors_1 : Bool),
  ({ fileName := fileName, fileMap := fileMap, currRecDepth := currRecDepth, cmdPos := cmdPos, macroStack := macroStack,
        quotContext? := quotContext?, currMacroScope := currMacroScope, ref := ref, snap? := snap?,
        cancelTk? := cancelTk?, suppressElabErrors := suppressElabErrors } =
      { fileName := fileName_1, fileMap := fileMap_1, currRecDepth := currRecDepth_1, cmdPos := cmdPos_1,
        macroStack := macroStack_1, quotContext? := quotContext?_1, currMacroScope := currMacroScope_1, ref := ref_1,
        snap? := snap?_1, cancelTk? := cancelTk?_1, suppressElabErrors := suppressElabErrors_1 }) =
    (fileName = fileName_1 ∧
      fileMap = fileMap_1 ∧
        currRecDepth = currRecDepth_1 ∧
          cmdPos = cmdPos_1 ∧
            macroStack = macroStack_1 ∧
              quotContext? = quotContext?_1 ∧
                currMacroScope = currMacroScope_1 ∧
                  ref = ref_1 ∧ snap? = snap?_1 ∧ cancelTk? = cancelTk?_1 ∧ suppressElabErrors = suppressElabErrors_1)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.sOppSide_point_excenter_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ {i : Fin (n + 1)},
      (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SOppSide (s.points i) (s.excenter signs) ↔
        s.excenterWeights signs i < 0
-- Mathlib.Analysis.CStarAlgebra.Fuglede
/-- **Fuglede–Putnam–Rosenblum**: If `a` is a normal element in a C⋆-algebra `A` which
commutes with `x`, then `star a` commutes with `x`.  -/
IsStarNormal.commute_star_left : ∀ {A : Type u_2} [inst : NonUnitalCStarAlgebra A] {a x : A}, IsStarNormal a → Commute a x → Commute (star a) x
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ici_succ : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n), ∏ i ≥ a.succ, f i = ∏ i ≥ a, f i.succ
-- Init.Grind.Lemmas
Lean.Grind.Bool.not_eq_of_eq_true : ∀ {a : Bool}, a = true → (!a) = false
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.add_kronecker : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : Distrib α]
  (A₁ A₂ : Matrix l m α) (B : Matrix n p α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (A₁ + A₂) B =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A₁ B + Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A₂ B
-- Aesop.Rule
Aesop.instInhabitedNormSimpRule.default : Aesop.NormSimpRule
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsPosSemidef.isNonneg : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : LE R]
  {B : LinearMap.BilinForm R M}, B.IsPosSemidef → B.IsNonneg
-- Aesop.Script.Tactic
Aesop.Script.UTactic : Type
-- Init.Data.Vector.Erase
Vector.mem_of_mem_eraseIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {h : i < n} {a : α}, a ∈ xs.eraseIdx i h → a ∈ xs
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- If `X ⟶ Spec A` is a morphism of schemes, then `Spec` of `A ⧸ specTargetImage f`
is the scheme-theoretic image of `f`. For this quotient as an object of `CommRingCat` see
`specTargetImage` below.  -/
AlgebraicGeometry.specTargetImageIdeal : {X : AlgebraicGeometry.Scheme} → {A : CommRingCat} → (X ⟶ AlgebraicGeometry.Spec A) → Ideal ↑A
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.priority.sizeOf_spec : ∀ (p : Aesop.Frontend.Priority), sizeOf (Aesop.Frontend.Feature.priority p) = 1 + sizeOf p
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂Hom_zero' : ∀ {R : Type u} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₂] (f : R →+* S₂),
  (MvPolynomial.eval₂Hom f fun x => 0) = f.comp MvPolynomial.constantCoeff
-- Mathlib.LinearAlgebra.Basis.Flag
/-- The subspace spanned by the first `k` vectors of the basis `b`.  -/
Module.Basis.flag : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {n : ℕ} → Module.Basis (Fin n) R M → Fin (n + 1) → Submodule R M
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roc.toList_iter : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roc α}, r.iter.toList = r.toList
-- Mathlib.Analysis.Meromorphic.Order
MeromorphicOn.eventually_analyticAt_or_mem_compl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜},
  MeromorphicOn f U → x ∈ U → ∀ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.mk.sizeOf_spec : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {L : CategoryTheory.Functor C D}
  {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : SizeOf C] [inst_4 : SizeOf D] [inst_5 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W x)] [inst_6 : SizeOf E]
  (inverts : W.IsInvertedBy L) (lift : (F : CategoryTheory.Functor C E) → W.IsInvertedBy F → CategoryTheory.Functor D E)
  (fac : ∀ (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F), L.comp (lift F hF) = F)
  (uniq : ∀ (F₁ F₂ : CategoryTheory.Functor D E), L.comp F₁ = L.comp F₂ → F₁ = F₂),
  sizeOf { inverts := inverts, lift := lift, fac := fac, uniq := uniq } = 1
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When `S₁.f` and `S₂.f` are zero and we have chosen limit kernel forks `c₁` and `c₂`
for `S₁.g` and `S₂.g` respectively, the action on right homology of a morphism `φ : S₁ ⟶ S₂` of
short complexes is given by the unique morphism `f : c₁.pt ⟶ c₂.pt` such that
`c₁.ι ≫ φ.τ₂ = f ≫ c₂.ι`.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork : {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₂) →
          (hf₁ : S₁.f = 0) →
            (c₁ : CategoryTheory.Limits.KernelFork S₁.g) →
              (hc₁ : CategoryTheory.Limits.IsLimit c₁) →
                (hf₂ : S₂.f = 0) →
                  (c₂ : CategoryTheory.Limits.KernelFork S₂.g) →
                    (hc₂ : CategoryTheory.Limits.IsLimit c₂) →
                      (f : c₁.pt ⟶ c₂.pt) →
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ =
                            CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂) →
                          CategoryTheory.ShortComplex.RightHomologyMapData φ
                            (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁)
                            (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂)
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The line derivative in direction `m` of the Fourier transform is given by the Fourier transform
of the multiplication with `-(2 * π * Complex.I) • (inner ℝ · m)`.  -/
TemperedDistribution.lineDerivOp_fourier_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] (f : TemperedDistribution E F) (m : E),
  LineDeriv.lineDerivOp m (FourierTransform.fourier f) =
    FourierTransform.fourier
      (-(2 * ↑Real.pi * Complex.I) • (TemperedDistribution.smulLeftCLM F fun x => ↑(inner ℝ x m)) f)
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.mkSEvalContext : Lean.MetaM Lean.Meta.Simp.Context
-- Batteries.Data.List.Basic
/-- `Chain' R l` means that `R` holds between adjacent elements of `l`.
```
Chain' R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d
```  -/
List.Chain' : {α : Type u_1} → (α → α → Prop) → List α → Prop
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.update_eq_sub_add_single : ∀ {I : Type u} {f : I → Type v} (i : I) [inst : DecidableEq I] [inst_1 : (i : I) → AddGroup (f i)] (g : (i : I) → f i)
  (x : f i), Function.update g i x = g - Pi.single i (g i) + Pi.single i x
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.Context.mk : Lean.Server.DocumentMeta →
  Lean.Lsp.Position →
    Option ℕ →
      Option (Lean.TSyntax `tactic) →
        ProofWidgets.RefreshToken →
          ProofWidgets.RefreshToken →
            ProofWidgets.RefreshToken →
              Lean.MVarId → Option Lean.FVarId → Lean.SubExpr.Pos → Mathlib.Tactic.ClickSuggestions.Context
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.quotientCompQhIso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} (f : K ⟶ L),
  CategoryTheory.CategoryStruct.comp (DerivedCategory.Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f))
      ((DerivedCategory.quotientCompQhIso C).hom.app L) =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.quotientCompQhIso C).hom.app K) (DerivedCategory.Q.map f)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H1Iso_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.π A 1)
      (CategoryTheory.CategoryStruct.comp (groupHomology.H1Iso A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.π h)
-- Mathlib.Algebra.Group.Units.Equiv
Units.mulLeft_symm : ∀ {M : Type u_3} [inst : Monoid M] (u : Mˣ), Equiv.symm u.mulLeft = u⁻¹.mulLeft
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegrable_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  [inst_5 : NormedSpace ℝ E],
  CurveIntegrable ω (Path.segment a b) ↔
    IntervalIntegrable (fun t => (ω ((AffineMap.lineMap a b) t)) (b - a)) MeasureTheory.volume 0 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sqrtTwoAddSeries_lt_two : ∀ (n : ℕ), Real.sqrtTwoAddSeries 0 n < 2
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_δ : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : Cᴹᵒᵖᴹᵒᵖ),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).functor X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.unmop.unmop Y.unmop.unmop)
-- Mathlib.Data.Set.Prod
Set.piMap_image_univ_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} (f : (i : ι) → α i → β i) (t : (i : ι) → Set (α i)),
  Pi.map f '' Set.univ.pi t = Set.univ.pi fun i => f i '' t i
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.nsmul : {α : Type u} → [inst : Lean.Grind.Semiring α] → ℕ → Lean.Grind.Ring.OfSemiring.Q α → Lean.Grind.Ring.OfSemiring.Q α
-- Init.Data.UInt.Basic
instShiftLeftUInt32 : ShiftLeft UInt32
-- Mathlib.Topology.Homotopy.TopCat.Basic
TopCat.Homotopy.h_comp : ∀ {X Y Z : TopCat} {f₀ f₁ : X ⟶ Y} {g₀ g₁ : Y ⟶ Z} (G : TopCat.Homotopy g₀ g₁) (F : TopCat.Homotopy f₀ f₁),
  (G.comp F).h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X
        (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id TopCat.I)
          (CategoryTheory.CategoryStruct.id TopCat.I)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X TopCat.I TopCat.I).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight F.h TopCat.I) G.h))
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- The topology induced by a valuative relation. Note that this is not made into a global instance
to avoid diamonds. If desired, one can equip a ring with a topological space from a valuative
relation by hand. But as long as they do so, the fact that the topology is valuative and
nonarchemidean can be automatically inferred.  -/
ValuativeRel.topologicalSpace : (R : Type u_1) → [inst : Ring R] → [ValuativeRel R] → TopologicalSpace R
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.divLeft_apply : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G]
  [inst_3 : IsIsometricSMul Gᵐᵒᵖ G] (c b : G), (IsometryEquiv.divLeft c) b = c / b