mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.mem_adjoin_simple_iff : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E} (x : E),
  x ∈ F⟮α⟯ ↔ ∃ r s, x = (Polynomial.aeval α) r / (Polynomial.aeval α) s
-- Mathlib.Data.Seq.Parallel
Computation.parallel_promises : ∀ {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α}, (∀ s ∈ S, s.Promises a) → (Computation.parallel S).Promises a
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.congr_fun : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  {f g : E ≃ₛₗᵢ[σ₁₂] E₂}, f = g → ∀ (x : E), f x = g x
-- Aesop.Builder.Forward
_private.Aesop.Builder.Forward.0.Aesop.RuleBuilder.getImmediatePremises.errPrefix : Lean.MessageData
-- Mathlib.Topology.EMetricSpace.BoundedVariation
LocallyBoundedVariationOn.ofDual : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s → LocallyBoundedVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.exists_variableChange_isCharTwoNF : ∀ {F : Type u_2} [inst : Field F] [CharP F 2] (W : WeierstrassCurve F), ∃ C, (C • W).IsCharTwoNF
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_star : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], (star a).im = -a.im
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.involute_involute : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (a : CliffordAlgebra Q), CliffordAlgebra.involute (CliffordAlgebra.involute a) = a
-- Std.Sat.AIG.Basic
/-- Denotation of an `AIG` at a specific `Entrypoint` with the `Entrypoint` being constructed on the fly.
 -/
Std.Sat.AIG.«term⟦_,_,_⟧» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.Saturate.hcongr_5 : ∀ (C C' : Type u_1),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v_1, u_1} C) (inst' : CategoryTheory.Category.{v_1, u_1} C'),
      inst ≍ inst' →
        ∀ (K : CategoryTheory.Coverage C) (K' : CategoryTheory.Coverage C'),
          K ≍ K' →
            ∀ (X : C) (X' : C'),
              X ≍ X' →
                ∀ (a : CategoryTheory.Sieve X) (a' : CategoryTheory.Sieve X'),
                  a ≍ a' → K.Saturate X a ≍ K'.Saturate X' a'
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.forgetToTop_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Scheme.forgetToTop.map f =
    (AlgebraicGeometry.SheafedSpace.forget CommRingCat).map
      (CategoryTheory.InducedCategory.homMk (AlgebraicGeometry.Scheme.Hom.toLRSHom f).toHom)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.isRegularEpi_iff_effectiveEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B)
  [CategoryTheory.Limits.HasPullback f f], CategoryTheory.IsRegularEpi f ↔ CategoryTheory.EffectiveEpi f
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.snd : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E × F} {g : α → G}, f =o[𝕜; l] g → (fun x => (f x).2) =o[𝕜; l] g
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.iter : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Zipper α β → Std.Iter ((a : α) × β a)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castSuccEmb_Ico : ∀ {n : ℕ} (i j : Fin n), Finset.map Fin.castSuccEmb (Finset.Ico i j) = Finset.Ico i.castSucc j.castSucc
-- Mathlib.GroupTheory.OrderOfElement
AddSubgroup.addOrderOf_coe : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} (a : ↥H), addOrderOf ↑a = addOrderOf a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter_eq_sub_one : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  k ∈ t →
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isNone = true →
      (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.size = t.size - 1
-- Mathlib.Algebra.Homology.Bifunctor
/-- The condition that `((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂` has
a total complex.  -/
HomologicalComplex.HasMapBifunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            {I₁ : Type u_4} →
              {I₂ : Type u_5} →
                {J : Type u_6} →
                  {c₁ : ComplexShape I₁} →
                    {c₂ : ComplexShape I₂} →
                      [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                        [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                          [inst_5 : CategoryTheory.Preadditive D] →
                            HomologicalComplex C₁ c₁ →
                              HomologicalComplex C₂ c₂ →
                                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                  [F.PreservesZeroMorphisms] →
                                    [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                      (c : ComplexShape J) → [TotalComplexShape c₁ c₂ c] → Prop
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getEntryDₘ_eq_getEntryD : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {fallback : (a : α) × β a},
      m.getEntryDₘ a fallback = Std.Internal.List.getEntryD a fallback (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.dual_contract_delete : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α), ((M.contract X).delete Y)✶ = (M✶.delete X).contract Y
-- Mathlib.RingTheory.ClassGroup.Basic
FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] {S : Type u_3} {L : Type u_4} [inst_5 : CommRing S]
  [inst_6 : IsDomain S] [inst_7 : Field L] [inst_8 : Algebra S L] [inst_9 : IsFractionRing S L] (f : R ≃+* S),
  Subgroup.map (Units.mapEquiv ↑(FractionalIdeal.ringEquivOfRingEquiv K L f)).toMonoidHom (toPrincipalIdeal R K).range =
    (toPrincipalIdeal S L).range
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.diam_Icc_le_of_distortion_le : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι) (i : ι) {c : NNReal},
  I.distortion ≤ c → Metric.diam (BoxIntegral.Box.Icc I) ≤ ↑c * (I.upper i - I.lower i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.differentiableWithinAt_arccos_Iic : ∀ {x : ℝ}, DifferentiableWithinAt ℝ Real.arccos (Set.Iic x) x ↔ x ≠ 1
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
HasCompactSupport.hasDerivAt_convolution_right : ∀ {𝕜 : Type u𝕜} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] {f₀ : 𝕜 → E} {g₀ : 𝕜 → E'}
  (L : E →L[𝕜] E' →L[𝕜] F) {μ : MeasureTheory.Measure 𝕜} [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ],
  MeasureTheory.LocallyIntegrable f₀ μ →
    HasCompactSupport g₀ →
      ContDiff 𝕜 1 g₀ →
        ∀ (x₀ : 𝕜), HasDerivAt (MeasureTheory.convolution f₀ g₀ L μ) (MeasureTheory.convolution f₀ (deriv g₀) L μ x₀) x₀
-- Mathlib.Data.Matrix.Basic
/-- `piEquiv` as a `RingEquiv`.  -/
Matrix.piRingEquiv : {n : Type u_3} →
  {ι : Type u_14} →
    {β : ι → Type u_15} →
      [inst : (i : ι) → AddCommMonoid (β i)] →
        [inst_1 : (i : ι) → Mul (β i)] →
          [inst_2 : Fintype n] → Matrix n n ((i : ι) → β i) ≃+* ((i : ι) → Matrix n n (β i))
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The morphism to the top object in `MonoOver X`.  -/
CategoryTheory.MonoOver.leTop : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → (f : CategoryTheory.MonoOver X) → f ⟶ ⊤
-- Init.PropLemmas
forall_prop_of_false : ∀ {p : Prop} {q : p → Prop}, ¬p → ((∀ (h' : p), q h') ↔ True)
-- Mathlib.Order.Sublattice
Sublattice.mk.sizeOf_spec : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : SizeOf α] (carrier : Set α) (supClosed' : SupClosed carrier)
  (infClosed' : InfClosed carrier),
  sizeOf { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' } = 1
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.dynEntourage_zero : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X}, Dynamics.dynEntourage T U 0 = Set.univ
-- Mathlib.Algebra.Category.Grp.Zero
CommGrpCat.subsingleton_of_isZero : ∀ {G : CommGrpCat}, CategoryTheory.Limits.IsZero G → Subsingleton ↑G
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit : {C : Type u} → CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.piIsoPi.eq_1 : ∀ {ι : Type v} (α : ι → TopCat),
  TopCat.piIsoPi α =
    (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor α)).conePointUniqueUpToIso
      (TopCat.piFanIsLimit α)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.projectiveSeminorm_apply : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun i => E i),
  PiTensorProduct.projectiveSeminorm x = ⨅ p, PiTensorProduct.projectiveSeminormAux ↑p
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun_precomp_of_bijective : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ι → Type u_8} {mβ : (i : ι) → MeasurableSpace (β i)}
  {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α}
  {f : (x : ι) → Ω → β x} {ι' : Type u_9} {g : ι' → ι},
  Function.Bijective g →
    (ProbabilityTheory.Kernel.iIndepFun (fun i => f (g i)) κ μ ↔ ProbabilityTheory.Kernel.iIndepFun f κ μ)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.directedAffineCover_trans : ∀ {X : AlgebraicGeometry.Scheme} {U V : ↑X.affineOpens} (hUV : U ≤ V),
  AlgebraicGeometry.Scheme.Cover.trans X.directedAffineCover (CategoryTheory.homOfLE hUV) = X.homOfLE hUV
-- Init.Data.List.Attach
List.attach.eq_1 : ∀ {α : Type u_1} (l : List α), l.attach = l.attachWith (Membership.mem l) ⋯
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommGroupOfMonoidHomClass.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → CommGroup (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)],
  DirectLimit.instCommGroupOfMonoidHomClass = { toGroup := DirectLimit.instGroup, mul_comm := ⋯ }
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
/-- Given two families of morphisms `f : X i ⟶ S` and `f' : X' j ⟶ S`,
two objects `D₁ D₂ : F.DescentData f`, a morphism `φ` between the images in
`F.DescentData f'` of `D₁` and `D₂` by a functor `pullFunctor`. When `F`
is a prestack and `f'` a covering family, this is the morphism `D₁.obj i ⟶ D₂.obj i`
that is deduced from `φ` by gluing.  -/
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {J : CategoryTheory.GrothendieckTopology C} →
        [F.IsPrestack J] →
          {ι : Type t} →
            {S : C} →
              {X : ι → C} →
                {f : (i : ι) → X i ⟶ S} →
                  {ι' : Type t'} →
                    {X' : ι' → C} →
                      {f' : (j : ι') → X' j ⟶ S} →
                        {α : ι' → ι} →
                          {p' : (j : ι') → X' j ⟶ X (α j)} →
                            (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j) →
                              CategoryTheory.Sieve.ofArrows X' f' ∈ J S →
                                {D₁ D₂ : F.DescentData f} →
                                  ((CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
                                      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂) →
                                    (i : ι) → D₁.obj i ⟶ D₂.obj i
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_toList_iff_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α],
  m.WF → ∀ {k : α} {v : β}, (k, v) ∈ Std.DHashMap.Raw.Const.toList m ↔ Std.DHashMap.Raw.Const.get? m k = some v
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkGateCached.go.match_1.eq_3 : ∀ (motive : Option Bool → Option Bool → Sort u_1) (x : Option Bool) (h_1 : (x : Option Bool) → motive (some false) x)
  (h_2 : (x : Option Bool) → motive x (some false)) (h_3 : (x : Option Bool) → motive (some true) x)
  (h_4 : (x : Option Bool) → motive x (some true)) (h_5 : (x x_1 : Option Bool) → motive x x_1),
  (x = some false → False) →
    (match some true, x with
      | some false, x => h_1 x
      | x, some false => h_2 x
      | some true, x => h_3 x
      | x, some true => h_4 x
      | x, x_2 => h_5 x x_2) =
      h_3 x
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
CategoryTheory.instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim : ∀ {A : Type u_1} {C : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} J]
  [inst_3 : CategoryTheory.FinitaryExtensive C] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J A]
  [CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim],
  CategoryTheory.Limits.PreservesColimitsOfShape J
    (CategoryTheory.sheafToPresheaf (CategoryTheory.extensiveTopology C) A)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `getElem`  on `BitVec`.  -/
BitVec.reduceGetElem : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {h e f : L}
  {m : M} {μ : R} {t : IsSl2Triple h e f},
  t.HasPrimitiveVectorWith m μ →
    ∀ [IsDomain R] [CharZero R] [IsNoetherian R M] [Module.IsTorsionFree R M] {n : ℕ},
      μ = ↑n → ((LieModule.toEnd R L M) f ^ (n + 1)) m = 0
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_snd_prod : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α}, Asymptotics.IsBigOWith 1 l g' fun x => (f' x, g' x)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- `∘ₗ` is notation for composition of two linear (not semilinear!) maps into a linear map.
This is useful when Lean is struggling to infer the `RingHomCompTriple` instance.  -/
LinearMap.compNotation : Lean.TrailingParserDescr
-- Mathlib.Topology.Category.Profinite.Basic
Profinite.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget Profinite)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {k a fallback : α} {v : β k},
      (m.insertIfNew k v).getKeyD a fallback =
        if (k == a) = true ∧ m.contains k = false then k else m.getKeyD a fallback
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.coe_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)], ⇑0 = 0
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.instFaithfulGradedObjectProdToGradedObjectFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂},
  (HomologicalComplex₂.toGradedObjectFunctor C c₁ c₂).Faithful
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.mk.inj : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  {toPresentation : Algebra.Presentation R S ι σ} {map : σ → ι} {map_inj : Function.Injective map}
  {toPresentation_1 : Algebra.Presentation R S ι σ} {map_1 : σ → ι} {map_inj_1 : Function.Injective map_1},
  { toPresentation := toPresentation, map := map, map_inj := map_inj } =
      { toPresentation := toPresentation_1, map := map_1, map_inj := map_inj_1 } →
    toPresentation = toPresentation_1 ∧ map = map_1
-- Aesop.Index.Basic
Aesop.IndexingMode.or.inj : ∀ {imodes imodes_1 : Array Aesop.IndexingMode},
  Aesop.IndexingMode.or imodes = Aesop.IndexingMode.or imodes_1 → imodes = imodes_1
-- Mathlib.RingTheory.Support
Module.nonempty_support_of_nontrivial : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M],
  (Module.support R M).Nonempty
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The finset `1 : Finset α` is defined as `{1}` in scope `Pointwise`.  -/
Finset.one : {α : Type u_2} → [One α] → One (Finset α)
-- Mathlib.CategoryTheory.SingleObj
MonoidHom.id_toFunctor : ∀ (M : Type u) [inst : Monoid M], (MonoidHom.id M).toFunctor = CategoryTheory.Functor.id (CategoryTheory.SingleObj M)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.symmₗ_linearMapAt : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet →
    ∀ (y : E b), (Bundle.Pretrivialization.symmₗ R e b) ((Bundle.Pretrivialization.linearMapAt R e b) y) = y
-- Mathlib.Order.Partition.Finpartition
Finpartition.extend.congr_simp : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α]
  {a b b_1 : α} (e_b : b = b_1) {c : α} (P P_1 : Finpartition a),
  P = P_1 → ∀ (hb : b ≠ ⊥) (hab : Disjoint a b) (hc : a ⊔ b = c), P.extend hb hab hc = P_1.extend ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- If `F` is full, and naturally isomorphic to some `F'`, then `F'` is also full.  -/
CategoryTheory.Functor.Full.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} [F.Full] (α : F ≅ F'), F'.Full
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∈ t₂) → (t₁ ∩ t₂).size = t₁.size
-- Mathlib.Data.Multiset.Sort
Multiset.sort_cons : ∀ {α : Type u_1} (a : α) (s : Multiset α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], (∀ b ∈ s, r a b) → (a ::ₘ s).sort r = a :: s.sort r
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.unop : C ⥤ D` creates colimits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfSizeOfUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
          [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop] →
            CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Combinatorics.Matroid.Circuit
/-- A generalization of the strong circuit elimination axiom `Matroid.IsCircuit.strong_elimination`
to an infinite collection of circuits.

It states that, given a circuit `C₀`, an arbitrary collection `C : ι → Set α` of circuits,
an element `x i` of `C₀ ∩ C i` for each `i`, and an element `z ∈ C₀` outside all the `C i`,
the union of `C₀` and the `C i` contains a circuit containing `z` but none of the `x i`.

This is one of the axioms when defining infinite matroids via circuits.

TODO : A similar statement will hold even when all mentions of `z` are removed.  -/
Matroid.IsCircuit.strong_multi_elimination : ∀ {α : Type u_1} {M : Matroid α} {ι : Type u_2} {C₀ : Set α},
  M.IsCircuit C₀ →
    ∀ (x : ι → α) (C : ι → Set α) (z : α),
      (∀ (i : ι), M.IsCircuit (C i)) →
        (∀ (i : ι), x i ∈ C₀) →
          (∀ (i : ι), x i ∈ C i) →
            (∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i') →
              z ∈ C₀ → (∀ (i : ι), z ∉ C i) → ∃ C' ⊆ (C₀ ∪ ⋃ i, C i) \ Set.range x, M.IsCircuit C' ∧ z ∈ C'
-- Mathlib.Data.Finset.Option
Finset.card_eraseNone_of_not_mem : ∀ {α : Type u_1} {s : Finset (Option α)}, none ∉ s → (Finset.eraseNone s).card = s.card
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.add_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] (X Y Z : C)
  (f g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f + g) h =
    CategoryTheory.CategoryStruct.comp f h + CategoryTheory.CategoryStruct.comp g h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany!_cons : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {l : List (α × β)} {k : α}
  {v : β},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t ((k, v) :: l)) =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! (Std.DTreeMap.Internal.Impl.insert! k v t) l)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_le_natDegree : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {q : Polynomial S},
  p.degree ≤ q.degree → p.natDegree ≤ q.natDegree
-- Mathlib.Data.Finset.Prod
Finset.coe_product : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β), ↑(s ×ˢ t) = ↑s ×ˢ ↑t
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.aemeasurable : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : MeasurableSpace β]
  [inst_1 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] {f : α → β},
  MeasureTheory.AEStronglyMeasurable f μ → AEMeasurable f μ