mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.FP.Basic
FP.Float.finite.injEq : ∀ [C : FP.FloatCfg] (a : Bool) (e : ℤ) (m : ℕ) (a_1 : FP.ValidFinite e m) (a_2 : Bool) (e_1 : ℤ) (m_1 : ℕ)
  (a_3 : FP.ValidFinite e_1 m_1),
  (FP.Float.finite a e m a_1 = FP.Float.finite a_2 e_1 m_1 a_3) = (a = a_2 ∧ e = e_1 ∧ m = m_1)
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.linearIndependent_of_add_mem_range_root' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [CharZero R]
  [IsDomain R] [P.IsReduced] {i j : ι},
  P.root i + P.root j ∈ Set.range ⇑P.root → LinearIndependent R ![P.root i, P.root j]
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.coe_toOrderIso : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (f : α ≃+*o β), ⇑↑f = ⇑f
-- Init.Data.Fin.Bitwise
Fin.shiftRight_val : ∀ {n : ℕ} (a b : Fin n), ↑(a >>> b) = ↑a >>> ↑b
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.inr_biprodXIso_inv : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (K.biprodXIso L i).inv =
    CategoryTheory.Limits.biprod.inr.f i
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
fderiv_csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  DifferentiableAt ℂ f x → fderiv ℂ (fun x => Complex.sinh (f x)) x = Complex.cosh (f x) • fderiv ℂ f x
-- Mathlib.Algebra.Order.Group.PosPart
negPart_sub_posPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] (a : α), a⁻ - a⁺ = -a
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.maxDegree_induce_of_support_subset : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj] {s : Set V}
  [inst_2 : DecidablePred fun x => x ∈ s], G.support ⊆ s → (SimpleGraph.induce s G).maxDegree = G.maxDegree
-- Mathlib.Analysis.Calculus.TangentCone.Defs
UniqueDiffWithinAt.mk : ∀ {R : Type u} {E : Type v} [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : TopologicalSpace E] {s : Set E} {x : E},
  Dense ↑(Submodule.span R (tangentConeAt R s x)) → x ∈ closure s → UniqueDiffWithinAt R s x
-- Mathlib.Data.Nat.ModEq
/-- **Alias** of the reverse direction of `Nat.modEq_iff_dvd`. -/
Nat.modEq_of_dvd : ∀ {n a b : ℕ}, ↑n ∣ ↑b - ↑a → a ≡ b [MOD n]
-- Mathlib.Probability.HasLaw
ProbabilityTheory.iIndepFun.hasLaw_pi : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_3} [inst : Fintype ι]
  {𝓧 : ι → Type u_4} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {μ : (i : ι) → MeasureTheory.Measure (𝓧 i)}
  {X : (i : ι) → Ω → 𝓧 i},
  (∀ (i : ι), ProbabilityTheory.HasLaw (X i) (μ i) P) →
    ProbabilityTheory.iIndepFun X P → ProbabilityTheory.HasLaw (fun ω i => X i ω) (MeasureTheory.Measure.pi μ) P
-- Mathlib.RingTheory.Ideal.Basic
Ideal.sum_pow_mem_span_pow : ∀ {α : Type u_2} [inst : CommSemiring α] {ι : Type u_5} (s : Finset ι) (f : ι → α) (n : ℕ),
  (∑ i ∈ s, f i) ^ (s.card * n + 1) ∈ Ideal.span ((fun i => f i ^ (n + 1)) '' ↑s)
-- Mathlib.Algebra.Group.Defs
nsmulRec_succ : ∀ {M : Type u} [inst : Zero M] [inst_1 : AddSemigroup M] (n : ℕ),
  n ≠ 0 → ∀ (a : M), 0 + a = a → nsmulRec (n + 1) a = a + nsmulRec n a
-- Mathlib.RingTheory.LocalProperties.IntegrallyClosed
/-- An integral domain `R` is integral closed if `Rₘ` is integral closed
for any maximal ideal `m` of `R`.  -/
IsIntegrallyClosed.of_localization_maximal : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R],
  (∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)) →
    IsIntegrallyClosed R
-- Aesop.Stats.Basic
Aesop.Stats.trace : Aesop.Stats → Aesop.TraceOption → Lean.CoreM Unit
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.liftLinear_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β}
  (hf : ∀ (μ : MeasureTheory.Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory) {s : Set β},
  MeasurableSet s → ((MeasureTheory.Measure.liftLinear f hf) μ) s = (f μ.toOuterMeasure) s
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.toSubfield_injective : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  Function.Injective IntermediateField.toSubfield
-- Mathlib.Order.RelClasses
/-- **Alias** of `Order.Preimage.antisymm`. -/
Order.Preimage.isAntisymm : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Antisymm r] {f : β → α},
  Function.Injective f → Std.Antisymm (f ⁻¹'o r)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_le_arsinh : ∀ {x y : ℝ}, Real.arsinh x ≤ Real.arsinh y ↔ x ≤ y
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_one : ∀ {o : Type u_4} {m' : o → Type u_7} {α : Type u_12} [inst : Zero α] [inst_1 : DecidableEq o]
  [inst_2 : (i : o) → DecidableEq (m' i)] [inst_3 : One α], Matrix.blockDiag' 1 = 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_mono : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f g : R → R} {a : A},
  (∀ x ∈ spectrum R a, f x ≤ g x) →
    autoParam (ContinuousOn f (spectrum R a)) cfc_mono._auto_1 →
      autoParam (ContinuousOn g (spectrum R a)) cfc_mono._auto_3 → cfc f a ≤ cfc g a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.instFreePolynomial : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R}, Module.Free (Polynomial R) W'.CoordinateRing
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.revAll_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.toSlice.revAll pat = s.revAll pat
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.instBEqSeq.beq.match_1.eq_3 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (x x_1 : Lean.Grind.AC.Seq)
  (h_1 : (a b : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var a) (Lean.Grind.AC.Seq.var b))
  (h_2 :
    (a : Lean.Grind.AC.Var) →
      (a_1 : Lean.Grind.AC.Seq) →
        (b : Lean.Grind.AC.Var) →
          (b_1 : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons a a_1) (Lean.Grind.AC.Seq.cons b b_1))
  (h_3 : (x x_2 : Lean.Grind.AC.Seq) → motive x x_2),
  (∀ (a b : Lean.Grind.AC.Var), x = Lean.Grind.AC.Seq.var a → x_1 = Lean.Grind.AC.Seq.var b → False) →
    (∀ (a : Lean.Grind.AC.Var) (a_1 : Lean.Grind.AC.Seq) (b : Lean.Grind.AC.Var) (b_1 : Lean.Grind.AC.Seq),
        x = Lean.Grind.AC.Seq.cons a a_1 → x_1 = Lean.Grind.AC.Seq.cons b b_1 → False) →
      (match x, x_1 with
        | Lean.Grind.AC.Seq.var a, Lean.Grind.AC.Seq.var b => h_1 a b
        | Lean.Grind.AC.Seq.cons a a_1, Lean.Grind.AC.Seq.cons b b_1 => h_2 a a_1 b b_1
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Std.Data.DTreeMap.Internal.Model
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.minEntry?ₘ' : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.Logic.Function.Iterate
Function.iterate_mul : ∀ {α : Type u} (f : α → α) (m n : ℕ), f^[m * n] = f^[m] ^[n]
-- Mathlib.LinearAlgebra.Dimension.Basic
Module.rank_eq_zero_of_not_faithfulSMul : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ¬FaithfulSMul R M → Module.rank R M = 0
-- Mathlib.Tactic.Ring.Common
/-- Returns whether `x` is less than, equal to or greater than `y`. Can be any total order.  -/
Mathlib.Tactic.Ring.Common.RingCompare.compare : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      Mathlib.Tactic.Ring.Common.RingCompare BaseType → {x y : Q(«$α»)} → BaseType x → BaseType y → Ordering
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous₂.comp : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] [inst_3 : UniformSpace δ] {f : α → β → γ} {g : γ → δ},
  UniformContinuous g → UniformContinuous₂ f → UniformContinuous₂ (Function.bicompr g f)
-- Mathlib.Data.Set.Card.Arithmetic
Set.Finite.ncard_biUnion : ∀ {α : Type u_1} {ι : Type u_2} {t : Set ι},
  t.Finite →
    ∀ {s : ι → Set α},
      (∀ i ∈ t, (s i).Finite) → t.PairwiseDisjoint s → (⋃ i ∈ t, s i).ncard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard
-- Init.Data.Ord.Vector
Vector.instLawfulEqOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.LawfulEqOrd α] {n : ℕ}, Std.LawfulEqOrd (Vector α n)
-- Mathlib.Analysis.Complex.Exponential
Real.one_lt_exp_iff : ∀ {x : ℝ}, 1 < Real.exp x ↔ 0 < x
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {x y : S₁.Hom S₂}, x.τ₁ = y.τ₁ → x.τ₂ = y.τ₂ → x.τ₃ = y.τ₃ → x = y
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- For `x : R` a non zero divisor, `ord R (x ^ n) = n • ord R x`.
 -/
Ring.ord_pow : ∀ {R : Type u_1} [inst : CommRing R] {x : R}, x ∈ nonZeroDivisors R → ∀ (n : ℕ), Ring.ord R (x ^ n) = n • Ring.ord R x
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.boolKernel_apply : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (b : Bool),
  (ProbabilityTheory.Kernel.boolKernel μ ν) b = if b = true then ν else μ
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [F.HasPointwiseRightDerivedFunctor W] [L.IsLocalization W], L.HasPointwiseLeftKanExtension F
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor `F` preserves limits of `K` (written as `PreservesLimit K F`)
if `F` maps any limit cone over `K` to a limit cone.
 -/
CategoryTheory.Limits.PreservesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] → CategoryTheory.Functor J C → CategoryTheory.Functor C D → Prop
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.updateForall!Impl : Lean.Expr → Lean.BinderInfo → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Tactic.Simps.Basic
/-- An internal representation of a name to be used for a generated lemma.  -/
_private.Mathlib.Tactic.Simps.Basic.0.NameStruct : Type
-- Lean.Meta.ArgsPacker.Basic
Lean.Meta.ArgsPacker.mk.sizeOf_spec : ∀ (varNamess : Array (Array Lean.Name)), sizeOf { varNamess := varNamess } = 1 + sizeOf varNamess
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.instCategoryOver : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Over X)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.pentagon_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''}
  {τ : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''} {A'''' : Type u₁₃} {B'''' : Type u₁₄}
  {C'''' : Type u₁₅} [inst_12 : CategoryTheory.Category.{v₁₃, u₁₃} A'''']
  [inst_13 : CategoryTheory.Category.{v₁₄, u₁₄} B''''] [inst_14 : CategoryTheory.Category.{v₁₅, u₁₅} C'''']
  {F'''' : CategoryTheory.Functor A'''' B''''} {G'''' : CategoryTheory.Functor C'''' B''''}
  {σ : CategoryTheory.Limits.CatCospanTransform F''' G''' F'''' G''''}
  {Z : CategoryTheory.Limits.CatCospanTransform F G F'''' G''''} (h : ψ.comp (φ.comp (τ.comp σ)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (ψ.associator φ τ).hom σ)
      (CategoryTheory.CategoryStruct.comp (ψ.associator ⋯ σ).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ ⋯) h)) =
    CategoryTheory.CategoryStruct.comp ((ψ.comp φ).associator τ σ).hom
      (CategoryTheory.CategoryStruct.comp (ψ.associator φ ⋯).hom h)
-- Mathlib.Data.Nat.Totient
/-- Euler's product formula for the totient function.  -/
Nat.totient_mul_prod_primeFactors : ∀ (n : ℕ), n.totient * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- If a global section is nilpotent on each member of a finite open cover, then `f` is
nilpotent.  -/
AlgebraicGeometry.Scheme.isNilpotent_of_isNilpotent_cover : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) [Finite 𝒰.I₀],
  (∀ (i : 𝒰.I₀), IsNilpotent ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (𝒰.f i) U)) s)) →
    IsNilpotent s
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.instDecidableEq.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α], FreeAddGroup.instDecidableEq = ⋯.decidableEq
-- Mathlib.Algebra.Ring.Defs
Semiring.toNatCast : {α : Type u} → [self : Semiring α] → NatCast α
-- Mathlib.Lean.Meta.CongrTheorems
/-- A version of `Subsingleton` with few instances. It should fail fast.  -/
Lean.Meta.FastSubsingleton : Sort u → Prop
-- Init.Data.Nat.Lemmas
Nat.sub_lt_of_pos_le : ∀ {a b : ℕ}, 0 < a → a ≤ b → b - a < b
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousComponent_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} (n : M)
  (φ : MvPolynomial σ R) [inst_2 : SemilatticeSup M] [inst_3 : OrderBot M],
  MvPolynomial.weightedTotalDegree w φ < n → (MvPolynomial.weightedHomogeneousComponent w n) φ = 0
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_add_right : ∀ {M : Type u} [inst : Add M] [inst_1 : PseudoMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M),
  dist (a + c) (b + c) = dist a b
-- Mathlib.Data.Multiset.Basic
Multiset.choose_spec : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : Multiset α) (hp : ∃! a, a ∈ l ∧ p a),
  Multiset.choose p l hp ∈ l ∧ p (Multiset.choose p l hp)
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- A morphism in `C` lifts to a chain map between projective resolutions.  -/
CategoryTheory.ProjectiveResolution.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        (Y ⟶ Z) →
          (P : CategoryTheory.ProjectiveResolution Y) →
            (Q : CategoryTheory.ProjectiveResolution Z) → P.complex ⟶ Q.complex
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- The factorization obtained from a factorization in the opposite category.  -/
CategoryTheory.MorphismProperty.MapFactorizationData.unop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty Cᵒᵖ} →
      {X Y : Cᵒᵖ} → {f : X ⟶ Y} → W₁.MapFactorizationData W₂ f → W₂.unop.MapFactorizationData W₁.unop f.unop
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.coeAddHom_apply : ∀ {α : Type u} [inst : Add α] (a : α), WithZero.coeAddHom a = ↑a
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.union_iff : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ s₂ s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.IndepSets (s₁ ∪ s₂) s' κ μ ↔
    ProbabilityTheory.Kernel.IndepSets s₁ s' κ μ ∧ ProbabilityTheory.Kernel.IndepSets s₂ s' κ μ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
/-- Like `evalPropStep`, but specialized for `@Ne.{u} α a b`. When the values differ, calls
`mkNeProof` to build a proof of `a ≠ b`. When equal, uses `eq_false (not_not_intro rfl)`
which requires no kernel evaluation.
 -/
Lean.Meta.Simp.evalNePropStep : Lean.Expr → Bool → Lean.Meta.SimpM Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_roc_eq_none : ∀ {m n i : ℕ}, n ≤ i + m → (m<...=n).toArray[i]? = none
-- Mathlib.Topology.Separation.Basic
/-- A T₁ space, also known as a Fréchet space, is a topological space
where every singleton set is closed. Equivalently, for every pair
`x ≠ y`, there is an open set containing `x` and not `y`.  -/
T1Space : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumToIter_Xl : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (b : S₁),
  (MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.X (Sum.inl b)) = MvPolynomial.X b
-- Mathlib.GroupTheory.Goursat
/-- For `I` a subgroup of `G × H`, `I.goursatSnd` is the kernel of the projection map `I → G`,
considered as a subgroup of `H`.

This is the second subgroup appearing in Goursat's lemma. See `AddSubgroup.goursat`.  -/
AddSubgroup.goursatSnd : {G : Type u_1} → {H : Type u_2} → [inst : AddGroup G] → [inst_1 : AddGroup H] → AddSubgroup (G × H) → AddSubgroup H
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nontrivial.pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : CancelMonoid α] {s : Finset α},
  s.Nontrivial → ∀ {n : ℕ}, n ≠ 0 → (s ^ n).Nontrivial
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.le_of_zeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J K : CategoryTheory.Precoverage C},
  (∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X) → J ≤ K
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instSymmetricCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.SymmetricCategory C] → CategoryTheory.SymmetricCategory (CategoryTheory.AddMon C)
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.List.headI.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (tail : List α) → motive (a :: tail)) → motive x
-- Init.Data.SInt.Lemmas
Int16.ofInt_le_iff_le : ∀ {a b : ℤ},
  Int16.minValue.toInt ≤ a →
    a ≤ Int16.maxValue.toInt →
      Int16.minValue.toInt ≤ b → b ≤ Int16.maxValue.toInt → (Int16.ofInt a ≤ Int16.ofInt b ↔ a ≤ b)
-- Mathlib.Algebra.Ring.Parity
Odd.not_two_dvd_nat : ∀ {n : ℕ}, Odd n → ¬2 ∣ n
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_self : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E),
  IntermediateField.adjoin F ↑K = K
-- Mathlib.Tactic.Widget.SelectInsertParamsClass
/-- Locations currently selected in the goal state.  -/
SelectInsertParamsClass.selectedLocations : {α : Type} → [self : SelectInsertParamsClass α] → α → Array Lean.SubExpr.GoalsLocation
-- Init.Data.Array.Zip
Array.zipWith_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : Array α} {bs : Array β},
  Array.zipWith f as bs = Array.zipWith (fun b a => f a b) bs as
-- Mathlib.Logic.Equiv.Basic
/-- Combining permutations on `ε` that permute only inside or outside the subtype
split induced by `p : ε → Prop` constructs a permutation on `ε`.  -/
Equiv.Perm.subtypeCongr : {ε : Type u_9} → {p : ε → Prop} → [DecidablePred p] → Equiv.Perm { a // p a } → Equiv.Perm { a // ¬p a } → Equiv.Perm ε
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.normedAddCommGroup : {E : Type u_2} → [NormedAddCommGroup E] → NormedAddCommGroup (ULift.{u_5, u_2} E)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgsResult.ctx : Lean.Elab.Tactic.ElabSimpArgsResult → Lean.Meta.Simp.Context
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The functoriality of `pullbackObj f g` in both arguments: Given a map from the pullback cospans
of `f' : Y' ⟶ X'` and `g' : Z' ⟶ X'` to the pullback cospan of `f : Y ⟶ X` and `g : Z ⟶ X`
as in the diagram below
```
Y' ⟶ Y
  ↘   ↘
  X' ⟶ X
  ↗   ↗
Z' ⟶ Z
```
if the morphisms `g'` and `g` both have chosen pullbacks, then we get an induced morphism
`pullbackMap f g f' g' comm₁ comm₂` from the chosen pullback of
`f' : Y' ⟶ X'` along `g'` to the chosen pullback of `f : Y ⟶ X` along `g`.
Here `comm₁` and `comm₂` are the commutativity conditions of the squares in the diagram above.
 -/
CategoryTheory.ChosenPullbacksAlong.pullbackMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z X : C} →
      (f : Y ⟶ X) →
        (g : Z ⟶ X) →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong g] →
            {Y' Z' X' : C} →
              (f' : Y' ⟶ X') →
                (g' : Z' ⟶ X') →
                  [inst_2 : CategoryTheory.ChosenPullbacksAlong g'] →
                    (γ₁ : Y' ⟶ Y) →
                      (γ₂ : Z' ⟶ Z) →
                        (γ₃ : X' ⟶ X) →
                          autoParam (CategoryTheory.CategoryStruct.comp f' γ₃ = CategoryTheory.CategoryStruct.comp γ₁ f)
                              CategoryTheory.ChosenPullbacksAlong.pullbackMap._auto_1 →
                            autoParam
                                (CategoryTheory.CategoryStruct.comp g' γ₃ = CategoryTheory.CategoryStruct.comp γ₂ g)
                                CategoryTheory.ChosenPullbacksAlong.pullbackMap._auto_3 →
                              (CategoryTheory.ChosenPullbacksAlong.pullbackObj f' g' ⟶
                                CategoryTheory.ChosenPullbacksAlong.pullbackObj f g)
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.aevalEquiv.eq_1 : ∀ (R : Type u) (A : Type z) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Polynomial.aevalEquiv R A =
    { toFun := fun x => Polynomial.eval₂AlgHom (Algebra.ofId R A) x ⋯, invFun := fun f => f Polynomial.X, left_inv := ⋯,
      right_inv := ⋯ }
-- Init.Data.Nat.Basic
Nat.right_distrib : ∀ (n m k : ℕ), (n + m) * k = n * k + m * k
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMultispan.functorExt.match_1.splitter : {J : CategoryTheory.Limits.MultispanShape} →
  (motive : CategoryTheory.Limits.WalkingMultispan J → Sort u_3) →
    (j : CategoryTheory.Limits.WalkingMultispan J) →
      ((i : J.L) → motive (CategoryTheory.Limits.WalkingMultispan.left i)) →
        ((i : J.R) → motive (CategoryTheory.Limits.WalkingMultispan.right i)) → motive j