mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.lieAlgebraComponent_apply : ∀ (R : Type u) (ι : Type v) [inst : CommRing R] (L : ι → Type w) [inst_1 : (i : ι) → LieRing (L i)]
  [inst_2 : (i : ι) → LieAlgebra R (L i)] (j : ι) (a : DirectSum ι fun i => L i),
  (DirectSum.lieAlgebraComponent R ι L j) a = (DirectSum.component R ι L j) a
-- Init.Data.Int.DivMod.Lemmas
Int.le_ediv_iff_mul_le : ∀ {a b c : ℤ}, 0 < c → (a ≤ b / c ↔ a * c ≤ b)
-- Init.Grind.FieldNormNum
_private.Init.Grind.FieldNormNum.0.Lean.Grind.Field.NormNum.nonzero_helper : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {z : ℤ} {n m : ℕ}, ↑n ≠ 0 → ↑m ≠ 0 → ↑(z.natAbs.gcd (n * m)) ≠ 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertIfNew! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α} {v : β},
      Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.insertIfNew! k v t) a =
        if compare k a = Ordering.eq ∧ k ∉ t then some v else Std.DTreeMap.Internal.Impl.Const.get? t a
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RicSliceData.range : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RicSliceData α → Std.Ric α
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.p_opcyclesToE_assoc : ∀ {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₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.p_opcyclesToE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.p_opcyclesToE._auto_3) {Z : C}
  (h : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f₁₂ f₃ n₁)
      (CategoryTheory.CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) h) =
    CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁)
      (CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.arrow : Lean.Meta.LazyDiscrTree.Key
-- Mathlib.Order.SuccPred.Limit
Order.isPredLimitRecOn_of_isMax : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : PredOrder α]
  (isMax : (a : α) → IsMax a → motive a) (pred : (a : α) → ¬IsMin a → motive (Order.pred a))
  (isPredLimit : (a : α) → Order.IsPredLimit a → motive a) (hb : IsMax b),
  Order.isPredLimitRecOn b isMax pred isPredLimit = isMax b hb
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.frobeniusAlgEquivOfAlgebraic_symm_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : Algebra.IsAlgebraic K L] (b : L),
  (FiniteField.frobeniusAlgEquivOfAlgebraic K L).symm b = Function.surjInv ⋯ b
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.pairwiseDisjoint_smul : ∀ {G : Type u_1} [inst : Group G] {S T : Set G}, Subgroup.IsComplement S T → S.PairwiseDisjoint fun x => x • T
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_right_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f g : X ⟶ Y),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
      CategoryTheory.MonoidalCategoryStruct.tensorHom g
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ↔
    f = g
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_unitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).unitIso =
    CategoryTheory.Idempotents.KaroubiKaroubi.unitIso C
-- Lean.Elab.PreDefinition.Structural.BRecOn
/-- See `toBelow`  -/
_private.Lean.Elab.PreDefinition.Structural.BRecOn.0.Lean.Elab.Structural.withBelowDict : {α : Type} →
  [Inhabited α] →
    Lean.Expr → ℕ → Lean.Elab.Structural.Positions → (Array Lean.Expr → Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Init.Data.List.Lemmas
List.forall_mem_cons : ∀ {α : Type u_1} {p : α → Prop} {a : α} {l : List α}, (∀ x ∈ a :: l, p x) ↔ p a ∧ ∀ x ∈ l, p x
-- Mathlib.Topology.Algebra.Constructions
/-- Put the same topological space structure on the opposite monoid as on the original
space.  -/
AddOpposite.instTopologicalSpaceAddOpposite : {M : Type u_1} → [TopologicalSpace M] → TopologicalSpace Mᵃᵒᵖ
-- Init.Guard
/-- Syntactic matching for `guard_expr`  -/
Lean.Parser.equalS : Lean.ParserDescr
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabUnsafe : Lean.Elab.Term.TermElab
-- Mathlib.Logic.Equiv.Option
Equiv.removeNoneAux_inv : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) (x : α), e.symm.removeNoneAux (e.removeNoneAux x) = x
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiable_const : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {c : M'}, MDiff fun x => c
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_inf : ∀ {V : Type u} {G : SimpleGraph V} {H₁ H₂ : G.Subgraph}, (H₁ ⊓ H₂).edgeSet = H₁.edgeSet ∩ H₂.edgeSet
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.dirac_bind : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → MeasureTheory.Measure β},
  Measurable f → ∀ (a : α), (MeasureTheory.Measure.dirac a).bind f = f a
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.State.mk : Std.HashMap String ℕ → Bool → Array ProofWidgets.Html → Mathlib.Tactic.ClickSuggestions.State
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_inv_assoc : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : data.HasFirstPageComputation] [inst_4 : X.HasSpectralSequence data] (pq : κ) (i₁ i₂ : ι)
  (hi₁ : i₁ = data.i₁ pq) (hi₂ : i₂ = data.i₂ pq) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_inv._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_inv._auto_3)
  {Z : C} (h : ((X.spectralSequence data).page r₀ ⋯).X pq ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').inv h =
    CategoryTheory.CategoryStruct.comp (X.EIsoH (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).inv
      (CategoryTheory.CategoryStruct.comp
        (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯).inv h)
-- Mathlib.Order.PartialSups
partialSups_eq_ciSup_Iic : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι]
  [inst_2 : ConditionallyCompleteLattice α] (f : ι → α) (i : ι), (partialSups f) i = ⨆ i_1, f ↑i_1
-- Init.Data.Rat.Lemmas
Rat.divInt_mul_divInt : ∀ (n₁ n₂ : ℤ) {d₁ d₂ : ℤ}, Rat.divInt n₁ d₁ * Rat.divInt n₂ d₂ = Rat.divInt (n₁ * n₂) (d₁ * d₂)
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality**: The geometric mean is less than or equal to the arithmetic mean.  -/
Real.geom_mean_le_arith_mean : ∀ {ι : Type u_1} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) →
    0 < ∑ i ∈ s, w i →
      (∀ i ∈ s, 0 ≤ z i) → (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹ ≤ (∑ i ∈ s, w i * z i) / ∑ i ∈ s, w i
-- Mathlib.Topology.Order.Compact
IsCompact.exists_isLeast : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIicTopology α] {s : Set α},
  IsCompact s → s.Nonempty → ∃ x, IsLeast s x
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instAddCommMonoid : {m : Type u_1} →
  {n : Type u_2} → {α : m → n → Type v} → [(i : m) → (j : n) → AddCommMonoid (α i j)] → AddCommMonoid (DMatrix m n α)
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- Given a linear map `f : N → P`, `f ⊗ M` is surjective if and only if `M ⊗ f` is surjective.  -/
LinearMap.lTensor_surj_iff_rTensor_surj : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P),
  Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑(LinearMap.rTensor M f)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_ext₂_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {f : J → C} {X Y Z : C}
  {g h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X) Y ⟶ Z},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y)
          g =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y)
          h) →
    g = h
-- Mathlib.Order.UpperLower.Principal
LowerSet.Ioi_le_Ici : ∀ {α : Type u_1} [inst : Preorder α] (a : α), LowerSet.Iio a ≤ LowerSet.Iic a
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coe_linearMapOfLE_apply : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : NormedRing 𝕜]
  [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] {p q : ENNReal} (h : p ≤ q)
  (f : ↥(lp E p)), ↑((lp.linearMapOfLE 𝕜 E h) f) = ↑f
-- Init.Meta.Defs
/-- Evaluator for `prec` DSL  -/
Lean.evalPrec : Lean.Syntax → Lean.MacroM ℕ
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.ext_hom : ∀ {G : Type u_1} [inst : Group G] [inst_1 : IsFreeGroup G] {H : Type u_2} [inst_2 : Group H] ⦃f g : G →* H⦄,
  (∀ (a : IsFreeGroup.Generators G), f (IsFreeGroup.of a) = g (IsFreeGroup.of a)) → f = g
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.mul_of_isUnit' : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x y : R)
  [IsLocalization.Away y S], IsUnit ((algebraMap R S) x) → IsLocalization.Away (x * y) S
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The identity of an object in `Φ.RightResolution X₂`.  -/
CategoryTheory.LocalizerMorphism.RightResolution.Hom.id : {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₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} → {X₂ : C₂} → (R : Φ.RightResolution X₂) → R.Hom R
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.pullback_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f] (g : CategoryTheory.Over Y),
  ((CategoryTheory.Over.pullback f).obj g).left = CategoryTheory.Limits.pullback g.hom f
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.tsupport_normed_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure],
  tsupport (f.normed μ) = Metric.closedBall c f.rOut
-- Mathlib.Data.Nat.Factorization.Root
Nat.floorRoot_zero_left : ∀ (a : ℕ), Nat.floorRoot 0 a = 0
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.Prod.toFun'.eq_1 : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  (p : Bundle.TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
  Bundle.Trivialization.Prod.toFun' e₁ e₂ p = (p.proj, (↑e₁ ⟨p.proj, p.snd.1⟩).2, (↑e₂ ⟨p.proj, p.snd.2⟩).2)
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- The `1`-cocycle attached to a degreewise split short exact sequence of cochain complexes.  -/
CochainComplex.cocycleOfDegreewiseSplit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) →
        ((n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) →
          CochainComplex.HomComplex.Cocycle S.X₃ S.X₁ 1
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.const.sizeOf_spec : ∀ (baseStructName structName constName : Lean.Name) (levels : List Lean.Level),
  sizeOf (Lean.Elab.Term.LValResolution.const baseStructName structName constName levels) =
    1 + sizeOf baseStructName + sizeOf structName + sizeOf constName + sizeOf levels
-- Mathlib.Algebra.Order.Ring.Abs
pow_eq_one_iff_of_ne_zero : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ},
  n ≠ 0 → (a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n)
-- Mathlib.Data.Matrix.Composition
Matrix.transpose_comp : ∀ {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (M : Matrix I J (Matrix K L R)),
  ((Matrix.comp I J K L R) M).transpose = (Matrix.comp J I L K R) (M.transpose.map fun x => x.transpose)
-- Mathlib.Analysis.Complex.Asymptotics
Complex.isBigO_ofReal_right : ∀ {α : Type u_1} {E : Type u_2} [inst : Norm E] {l : Filter α} {f : α → E} {g : α → ℝ},
  (f =O[l] fun x => ↑(g x)) ↔ f =O[l] g
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coeFnAddMonoidHom.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : AddMonoid R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R],
  BoundedContinuousFunction.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Tactic.CrossRefAttribute
/-- The syntax for a "kerodon" database identifier in a `@[kerodon]` attribute.  -/
Mathlib.CrossRef.stacksTagDBKerodon : Lean.ParserDescr
-- Mathlib.Analysis.ODE.Transform
isIntegralCurve_comp_mul_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {a : ℝ},
  a ≠ 0 → (IsIntegralCurve (γ ∘ fun x => x * a) (a • v ∘ fun x => x * a) ↔ IsIntegralCurve γ v)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.fst.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T),
  CategoryTheory.Comma.fst L R = { obj := fun X => X.left, map := fun {X Y} f => f.left, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- A diagram `WalkingSpan ⥤ C` is isomorphic to some `PushoutCocone.mk` after composing with
`diagramIsoSpan`.  -/
CategoryTheory.Limits.PushoutCocone.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} →
      (t : CategoryTheory.Limits.Cocone F) →
        (CategoryTheory.Limits.Cocone.precompose (CategoryTheory.Limits.diagramIsoSpan F).inv).obj t ≅
          CategoryTheory.Limits.PushoutCocone.mk (t.ι.app CategoryTheory.Limits.WalkingSpan.left)
            (t.ι.app CategoryTheory.Limits.WalkingSpan.right) ⋯
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (hom : (i : ι) → D₁.obj i ⟶ D₂.obj i)
  (comm :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
        CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (hom i₁)) (D₂.hom q f₁ f₂ ⋯ ⋯) =
          CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (hom i₂)))
      CategoryTheory.Pseudofunctor.DescentData.Hom.comm._autoParam)
  (hom_1 : (i : ι) → D₁.obj i ⟶ D₂.obj i)
  (comm_1 :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
        CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (hom_1 i₁)) (D₂.hom q f₁ f₂ ⋯ ⋯) =
          CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (hom_1 i₂)))
      CategoryTheory.Pseudofunctor.DescentData.Hom.comm._autoParam),
  ({ hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 }) = (hom = hom_1)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.instMonadMor₁MonoidalM : Mathlib.Tactic.BicategoryLike.MonadMor₁ Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- The dimension formula for `𝒮ℒ` modular forms of even weight.  -/
ModularForm.dimension_level_one : ∀ (k : ℕ),
  Even k →
    Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
      ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)
-- Mathlib.Order.Closure
/-- Construct a closure operator from an inflationary function `f` and a "closedness" predicate `p`
witnessing minimality of `f x` among closed elements greater than `x`.  -/
ClosureOperator.ofPred : {α : Type u_1} →
  [inst : PartialOrder α] →
    (f : α → α) →
      (p : α → Prop) →
        (∀ (x : α), x ≤ f x) → (∀ (x : α), p (f x)) → (∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y) → ClosureOperator α
-- Mathlib.Data.Complex.Basic
Complex.conj_neg_I : (starRingEnd ℂ) (-Complex.I) = Complex.I
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.zero_nnrpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {x : NNReal},
  0 ^ x = 0
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- A partial map from `X` to `Y` (`X.PartialMap Y`) is a morphism into `Y`
defined on a dense open subscheme of `X`.
 -/
AlgebraicGeometry.Scheme.PartialMap : AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Type u
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context.knowsLevel : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context → Bool
-- Mathlib.Data.Ordmap.Invariants
Ordnode.foldr_cons_eq_toList : ∀ {α : Type u_1} (t : Ordnode α) (r : List α), Ordnode.foldr List.cons t r = t.toList ++ r
-- Lean.Server.Requests
/-- Create a task which waits for the snapshot containing `lspPos` and executes `f` with it.
If no such snapshot exists, the request fails with an error.  -/
Lean.Server.RequestM.withWaitFindSnapAtPos : {α : Type} →
  Lean.Lsp.Position →
    (Lean.Server.Snapshots.Snapshot → Lean.Server.RequestM α) → Lean.Server.RequestM (Lean.Server.RequestTask α)
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.N_zero : ∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G), B.N 0 = B.filter
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- A version of the Freiman homomorphism condition expressed using `Finset`s, for practicality.  -/
IsMulFreimanHom.prod_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {n : ℕ},
  IsMulFreimanHom n A B f →
    ∀ {s t : Finset α} {hsA : ↑s ⊆ A} {htA : ↑t ⊆ A},
      s.card = n → t.card = n → ∏ i ∈ s, i = ∏ i ∈ t, i → ∏ i ∈ s, f i = ∏ i ∈ t, f i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.isPushout : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (self : F.PushoutObjObj f₁ f₂), CategoryTheory.IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) self.inl self.inr
-- Mathlib.Data.Prod.Lex
Prod.Lex.noMinOrder_of_left : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [NoMinOrder α], NoMinOrder (Lex (α × β))
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.toDescentDataFunctor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃))
  {X_1 Y : F.DescentData' sq sq₃} (φ : X_1 ⟶ Y) (i : ι),
  ((CategoryTheory.Pseudofunctor.DescentData'.toDescentDataFunctor F sq sq₃).map φ).hom i = φ.hom i
-- Mathlib.Algebra.Group.Invertible.Defs
/-- `invOf a` is a right inverse of `a`  -/
Invertible.mul_invOf_self : ∀ {α : Type u} {inst : Mul α} {inst_1 : One α} {a : α} [self : Invertible a], a * ⅟a = 1
-- Mathlib.Algebra.MvPolynomial.Counit
MvPolynomial.counit_X : ∀ {R : Type u_3} [inst : CommRing R] (r : R), (MvPolynomial.counit R) (MvPolynomial.X r) = r
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.MemLp.lpNorm_condExp_le_lpNorm : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : α → E} {p : ENNReal},
  1 ≤ p → MeasureTheory.MemLp f p μ → MeasureTheory.lpNorm μ[f | m] p μ ≤ MeasureTheory.lpNorm f p μ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l →
        ∀ {h : k' ∈ Std.ExtDHashMap.Const.insertMany m l}, (Std.ExtDHashMap.Const.insertMany m l).getKey k' h = k