mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (n : ℕ),
  (AlgebraicTopology.DoldKan.N₁Γ₀.hom.app K).f.f n =
    (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` is faithful on `R`-algebras.  -/
AlgebraicGeometry.algSpec.instFaithful : ∀ {R : CommRingCat}, (AlgebraicGeometry.algSpec R).Faithful
-- Mathlib.Lean.Thunk
Thunk.prod_get_fst : ∀ {α : Type u} {β : Type v} {a : Thunk α} {b : Thunk β}, (a.prod b).get.1 = a.get
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.instAssociativeHAdd_1 : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α], Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingFieldAux.algebra' : {K : Type v} →
  [inst : Field K] →
    {n : ℕ} → {f : Polynomial K} → Algebra (AdjoinRoot f.factor) (Polynomial.SplittingFieldAux n.succ f)
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
eq_of_linearIndepOn_id_of_span_subtype : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {s t : Set M}, LinearIndepOn R id s → t ⊆ s → s ⊆ ↑(Submodule.span R t) → s = t
-- Init.Data.Slice.Array.Lemmas
Array.start_mkSlice_rcc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  (Std.Rcc.Sliceable.mkSlice xs lo...=hi).start = min lo (min (hi + 1) xs.size)
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.State.mk : Bool → Aesop.Script.DynStructureM.State
-- Mathlib.Data.Matrix.Basis
Matrix.single_mulVec_eq : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : NonAssocSemiring α] (i j : n)
  (b : α) (w : n → α), (Matrix.single i j b).mulVec w = (b * w j) • Pi.single i 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.length_keys : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keys.length = m.size
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Pretrivialization.continuousLinearMap.isLinear : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj)
  (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) [inst_13 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : (x : B) → TopologicalSpace (E₂ x)] [inst_16 : FiberBundle F₂ E₂]
  [inst_17 : Bundle.Trivialization.IsLinear 𝕜₁ e₁] [inst_18 : Bundle.Trivialization.IsLinear 𝕜₂ e₂]
  [inst_19 : ∀ (x : B), ContinuousAdd (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)],
  Bundle.Pretrivialization.IsLinear 𝕜₂ (Bundle.Pretrivialization.continuousLinearMap σ e₁ e₂)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.bddBelow_expansion : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {S : Finset G},
  K ≤ 1 → S.Nonempty → BddBelow (Set.range fun A => Finset.expansion✝ K S ↑A)
-- Mathlib.Geometry.Manifold.Algebra.SMul
/-- If an action is Cⁿ for some `n`, it is also continuous. This has to be a theorem instead of an
instance because `ContMDiffSMul` depends on parameters `I`, `I'` and `n` that `ContinuousSMul`
doesn't.  -/
ContMDiffSMul.continuousSMul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : SMul G M] (n : WithTop ℕ∞)
  [ContMDiffSMul I I' n G M], ContinuousSMul G M
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.dvd_algebraMap_intNorm_self : ∀ (A : Type u_1) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsIntegrallyClosed A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B] [inst_7 : Module.Finite A B]
  [inst_8 : Module.IsTorsionFree A B] (x : B), x ∣ (algebraMap A B) ((Algebra.intNorm A B) x)
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- The `AffineTargetMorphismProperty` associated to `(targetAffineLocally P).diagonal`.
See `diagonal_targetAffineLocally_eq_targetAffineLocally`.
 -/
AlgebraicGeometry.AffineTargetMorphismProperty.diagonal : AlgebraicGeometry.AffineTargetMorphismProperty → AlgebraicGeometry.AffineTargetMorphismProperty
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {k : α}
  (h' : k ∈ t), t.get k h' = k
-- Mathlib.Analysis.Real.Sqrt
/-- The natural square root is at most the real square root  -/
Real.nat_sqrt_le_real_sqrt : ∀ {a : ℕ}, ↑a.sqrt ≤ √↑a
-- Std.Data.HashSet.IteratorLemmas
_private.Std.Data.HashSet.IteratorLemmas.0.Std.HashSet.iter.eq_1 : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.HashSet α),
  m.iter = Std.Iter.map (fun e => e.fst) m.inner.inner.iter
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndependent.linearCombination_ne_of_notMem_support : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R],
  LinearIndependent R v → ∀ {x : ι} (f : ι →₀ R), x ∉ f.support → (Finsupp.linearCombination R v) f ≠ v x
-- Mathlib.Algebra.Field.Subfield.Defs
/-- `SubfieldClass S K` states `S` is a type of subsets `s ⊆ K` closed under field operations.  -/
SubfieldClass : (S : Type u_1) → (K : Type u_2) → [DivisionRing K] → [SetLike S K] → Prop
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
/-- Construct the product over an indexed family of groupoids, as a fan.  -/
CategoryTheory.Grpd.piLimitFan : ⦃J : Type u⦄ → (F : J → CategoryTheory.Grpd) → CategoryTheory.Limits.Fan F
-- Mathlib.Combinatorics.Additive.Corner.Defs
isCorner_iff : ∀ {G : Type u_1} [inst : AddCommMonoid G] (A : Set (G × G)) (x₁ y₁ x₂ y₂ : G),
  IsCorner A x₁ y₁ x₂ y₂ ↔ (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Database.wikidata.sizeOf_spec : sizeOf Mathlib.CrossRef.Database.wikidata = 1
-- Std.Internal.Parsec.ByteArray
/-- Parses until a predicate is satisfied (exclusive).
 -/
Std.Internal.Parsec.ByteArray.takeUntil : (UInt8 → Bool) → Std.Internal.Parsec.ByteArray.Parser ByteSlice
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_sub_nsmul : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddGroup G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ), f (x - n • a) = f x - n • b
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.morphismProperty_eq_top : ∀ {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 : L.IsLocalization W] (P : CategoryTheory.MorphismProperty D)
  [P.RespectsIso] [P.IsMultiplicative],
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)) →
    (∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (CategoryTheory.Localization.isoOfHom L W f hf).inv) → P = ⊤
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- A continuous linear map is a star projection iff it is idempotent and normal.  -/
ContinuousLinearMap.isStarProjection_iff_isIdempotentElem_and_isStarNormal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E} [inst_3 : CompleteSpace E], IsStarProjection T ↔ IsIdempotentElem T ∧ IsStarNormal T
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.instMembershipPFun : Membership (ℕ →. ℕ) Nat.Partrec.Code
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Inhabited α] [inst_1 : Std.TransCmp cmp]
  {k : α}, k ∉ t₁ → (t₁ ∪ t₂).get! k = t₂.get! k
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
tendsto_rpow_atTop_of_base_gt_one : ∀ (b : ℝ), 1 < b → Filter.Tendsto (fun x => b ^ x) Filter.atTop Filter.atTop
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckStep.ofNat_ctorIdx : ∀ (x : DyckStep), DyckStep.ofNat x.ctorIdx = x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_erase!_le_maxKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k km kme : α} (hkme : (Std.DTreeMap.Internal.Impl.erase! k t).maxKey? = some kme),
  t.maxKey?.get ⋯ = km → (compare kme km).isLE = true
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reducePush : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Limits.Indization.LocallySmall
/-- Variant of `colimitYonedaHomIsoLimitOp`: natural transformations with domain
`colimit (F ⋙ yoneda)` are equivalent to a limit in a lower universe.  -/
CategoryTheory.colimitYonedaHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} I] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape I (Type v)] →
          [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type v)] →
            [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u v))] →
              (F : CategoryTheory.Functor I C) →
                (G : CategoryTheory.Functor Cᵒᵖ (Type v)) →
                  (CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda) ⟶ G) ≃
                    CategoryTheory.Limits.limit (F.op.comp G)
-- Init.Omega.Int
Lean.Omega.Int.add_nonneg_iff_neg_le : ∀ {a b : ℤ}, 0 ≤ a + b ↔ -b ≤ a
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_apply_prime_pow : ∀ {k p i : ℕ}, Nat.Prime p → (ArithmeticFunction.sigma k) (p ^ i) = ∑ j ∈ Finset.range (i + 1), p ^ (j * k)
-- Init.Data.List.OfFn
List.length_ofFn : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α}, (List.ofFn f).length = n
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.eq_C_coeff_zero_iff_natDegree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p = Polynomial.C (p.coeff 0) ↔ p.natDegree = 0
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.coe_of : ∀ (X : Type u) [inst : Fintype X] [inst_1 : TopologicalSpace X], ↑(FinTopCat.of X).toTop = X
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_biUnion_le_lift : ∀ {α : Type u} {ι : Type v} (A : ι → Set α) (s : Set ι),
  Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ x ∈ s, A x)) ≤
    Cardinal.lift.{u, v} (Cardinal.mk ↑s) * ⨆ x, Cardinal.lift.{v, u} (Cardinal.mk ↑(A ↑x))
-- Mathlib.Computability.ContextFreeGrammar
/-- The class of context-free languages is closed under reversal.  -/
Language.IsContextFree.reverse : ∀ {T : Type u_1} {L : Language T}, L.IsContextFree → L.reverse.IsContextFree
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C}
  [inst_1 : J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [inst_2 : 𝒰.HasPullbacks]
  (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T)
  (hf :
    ∀ (i j : 𝒰.I₀),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j))
  (i : 𝒰.I₀) {Z : C} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (𝒰.f i) (CategoryTheory.CategoryStruct.comp (𝒰.glueMorphisms f hf) h) =
    CategoryTheory.CategoryStruct.comp (f i) h
-- Mathlib.Algebra.Order.Interval.Basic
instZeroNonemptyInterval.eq_1 : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Zero α], instZeroNonemptyInterval = { zero := NonemptyInterval.pure 0 }
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- `colimitIsoFlipCompColim` is natural with respect to diagrams.  -/
CategoryTheory.Limits.colimIsoFlipCompWhiskerColim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C] →
              CategoryTheory.Limits.colim ≅
                (CategoryTheory.flipFunctor J K C).comp
                  ((CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj
                    CategoryTheory.Limits.colim)
-- Mathlib.Topology.MetricSpace.Bounded
tendsto_dist_left_cocompact_atTop : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α] (x : α),
  Filter.Tendsto (dist x) (Filter.cocompact α) Filter.atTop
-- Init.Data.Array.Lemmas
Array.findSomeM?_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {p : α → m (Option β)}
  {xs : Array α}, List.findSomeM? p xs.toList = Array.findSomeM? p xs
-- Mathlib.Geometry.Euclidean.Congruence
/-- Corresponding angles are equal for congruent triangles.  -/
EuclideanGeometry.angle_eq_of_congruent : ∀ {ι : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedAddCommGroup V₁]
  [inst_1 : NormedAddCommGroup V₂] [inst_2 : InnerProductSpace ℝ V₁] [inst_3 : InnerProductSpace ℝ V₂]
  [inst_4 : MetricSpace P₁] [inst_5 : MetricSpace P₂] [inst_6 : NormedAddTorsor V₁ P₁] [inst_7 : NormedAddTorsor V₂ P₂]
  {v₁ : ι → P₁} {v₂ : ι → P₂},
  Congruent v₁ v₂ →
    ∀ (i j k : ι), EuclideanGeometry.angle (v₁ i) (v₁ j) (v₁ k) = EuclideanGeometry.angle (v₂ i) (v₂ j) (v₂ k)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_insert_le_add_one : ∀ {α : Type u_1} (M : Matroid α) (e : α) (X : Set α), M.eRk (insert e X) ≤ M.eRk X + 1
-- Mathlib.Topology.Instances.CantorSet
le_ofDigits_cantorToTernary_sum : ∀ {x : ℝ}, x ∈ cantorSet → ∀ {n : ℕ}, x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, Real.ofDigitsTerm (cantorToTernary x) i
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftMin : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [P.IsStableUnderShift A] [Q.IsStableUnderShift A],
  (P ⊓ Q).IsStableUnderShift A
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S}
  (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.equalizer.ι f g)
          (CategoryTheory.Limits.pullback.fst s v))
        (CategoryTheory.Limits.equalizer.ι f g)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.equalizer.ι
        (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
        (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
      (CategoryTheory.Limits.pullback.fst s v)
-- Mathlib.Algebra.Field.Defs
/-- For a nonzero `a`, `a⁻¹` is a right multiplicative inverse.  -/
DivisionRing.mul_inv_cancel : ∀ {K : Type u_2} [self : DivisionRing K] (a : K), a ≠ 0 → a * a⁻¹ = 1
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Abelian.Ext.mapExactFunctor_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] (X Y : C) (n : ℕ), CategoryTheory.Abelian.Ext.mapExactFunctor F 0 = 0
-- Mathlib.Data.Vector.MapLemmas
/-- If `f` returns the same output and next state for every value of it's second argument, then
`ys : Vector` is ignored, and we can rewrite `mapAccumr₂` into `map`.
 -/
List.Vector.mapAccumr₂_unused_input_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {s : σ} {xs : List.Vector α n}
  {ys : List.Vector β n} (f : α → β → σ → σ × γ) (f' : α → σ → σ × γ),
  (∀ (a : α) (b : β) (s : σ), f a b s = f' a s) → List.Vector.mapAccumr₂ f xs ys s = List.Vector.mapAccumr f' xs s
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.ProjRestrict.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [inst : (i : I) → Decidable (J i)],
  Profinite.NobelingProof.ProjRestrict C J =
    Set.MapsTo.restrict (Profinite.NobelingProof.Proj J) C (Profinite.NobelingProof.π C J) ⋯
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.measure_preimage_emb : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb → MeasurableEmbedding f → ∀ (s : Set β), μa (f ⁻¹' s) = μb s
-- Lean.Environment
Lean.Kernel.Exception.appTypeMismatch.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (app funType argType : Lean.Expr),
  sizeOf (Lean.Kernel.Exception.appTypeMismatch env lctx app funType argType) =
    1 + sizeOf env + sizeOf lctx + sizeOf app + sizeOf funType + sizeOf argType
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {inst_1 : LinearOrder J} {inst_2 : OrderBot J}
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} {x y : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j},
  x = y ↔ x.f' = y.f'
-- Std.Http.Data.Method
Std.Http.Method.query.sizeOf_spec : sizeOf Std.Http.Method.query = 1
-- Mathlib.LinearAlgebra.Matrix.Dual
Matrix.toLin_transpose : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [inst : CommSemiring K]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂]
  [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] [inst_7 : DecidableEq ι₁] [inst_8 : DecidableEq ι₂]
  {B₁ : Module.Basis ι₁ K V₁} {B₂ : Module.Basis ι₂ K V₂} (M : Matrix ι₁ ι₂ K),
  (Matrix.toLin B₁.dualBasis B₂.dualBasis) M.transpose = Module.Dual.transpose ((Matrix.toLin B₂ B₁) M)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.mk : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {f₀ f₁ : C(X, Y)} →
          {P : C(X, Y) → Prop} →
            (toHomotopy : f₀.Homotopy f₁) →
              (∀ (t : ↑unitInterval), P { toFun := fun x => toHomotopy.toFun (t, x), continuous_toFun := ⋯ }) →
                f₀.HomotopyWith f₁ P
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.natDegree_U_neg_one : ∀ (R : Type u_1) [inst : CommRing R], (Polynomial.Chebyshev.U R (-1)).natDegree = 0
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_apply_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (a : L₂ ⟶ L₁) (X : D),
  ((CategoryTheory.conjugateEquiv adj₁ adj₂) a).app X =
    CategoryTheory.CategoryStruct.comp (adj₂.unit.app (R₁.obj X))
      (CategoryTheory.CategoryStruct.comp (R₂.map (a.app (R₁.obj X))) (R₂.map (adj₁.counit.app X)))
-- Mathlib.RingTheory.Polynomial.GaussLemma
Polynomial.IsPrimitive.isUnit_iff_isUnit_map : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {p : Polynomial R}, p.IsPrimitive → (IsUnit p ↔ IsUnit (Polynomial.map (algebraMap R K) p))
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instMaxOfSeparatelyContinuousMul : {G : Type u} →
  [inst : Group G] → [inst_1 : TopologicalSpace G] → [SeparatelyContinuousMul G] → Max (OpenNormalSubgroup G)
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- The special case that more or less by definition `QuaternionGroup 0` is isomorphic to the
infinite dihedral group.  -/
QuaternionGroup.quaternionGroupZeroEquivDihedralGroupZero : QuaternionGroup 0 ≃* DihedralGroup 0
-- Mathlib.Data.Rat.Cast.Defs
eq_ratCast : ∀ {F : Type u_1} {α : Type u_3} [inst : DivisionRing α] [inst_1 : FunLike F ℚ α] [RingHomClass F ℚ α] (f : F) (q : ℚ),
  f q = ↑q
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] (X Y : D) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.LaxMonoidal.μ e.inverse X Y))
      (CategoryTheory.CategoryStruct.comp (e.counitIso.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.counitIso.hom.app X) (e.counitIso.hom.app Y)) h)
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.Hom₂.mk.inj : ∀ {B : Type u_1} {C : Type u_2} {inst : CategoryTheory.Bicategory C} {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y} {hom hom_1 : f.hom ⟶ g.hom},
  { hom := hom } = { hom := hom_1 } → hom = hom_1
-- Mathlib.Order.Filter.Map
Filter.comap_fst_neBot_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α}, (Filter.comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.isSheaf_of_iso_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {J : CategoryTheory.GrothendieckTopology C} {P P' : CategoryTheory.Functor Cᵒᵖ A} (e : P ≅ P'),
  CategoryTheory.Presheaf.IsSheaf J P ↔ CategoryTheory.Presheaf.IsSheaf J P'
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff m₂ ⋯).get? k = none