mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Lemmas
List.mem_dite_nil_left : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {l : ¬p → List α},
  (x ∈ if h : p then [] else l h) ↔ ∃ (h : ¬p), x ∈ l h
-- Lean.MetavarContext
Lean.MetavarContext.setMVarKind : Lean.MetavarContext → Lean.MVarId → Lean.MetavarKind → Lean.MetavarContext
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyLE?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getKeyLE? k = t₂.getKeyLE? k
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.mk.inj : ∀ {ι : Type u_1} {X : Type u_2} {inst : TopologicalSpace X} {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  {toFun : ι → Set X} {carrier : Set ι} {isOpen : ∀ (i : ι), IsOpen (toFun i)} {subset_iUnion : s ⊆ ⋃ i, toFun i}
  {closure_subset : ∀ {i : ι}, i ∈ carrier → closure (toFun i) ⊆ u i}
  {pred_of_mem : ∀ {i : ι}, i ∈ carrier → p (toFun i)} {apply_eq : ∀ {i : ι}, i ∉ carrier → toFun i = u i}
  {toFun_1 : ι → Set X} {carrier_1 : Set ι} {isOpen_1 : ∀ (i : ι), IsOpen (toFun_1 i)}
  {subset_iUnion_1 : s ⊆ ⋃ i, toFun_1 i} {closure_subset_1 : ∀ {i : ι}, i ∈ carrier_1 → closure (toFun_1 i) ⊆ u i}
  {pred_of_mem_1 : ∀ {i : ι}, i ∈ carrier_1 → p (toFun_1 i)} {apply_eq_1 : ∀ {i : ι}, i ∉ carrier_1 → toFun_1 i = u i},
  { toFun := toFun, carrier := carrier, isOpen := isOpen, subset_iUnion := subset_iUnion,
        closure_subset := closure_subset, pred_of_mem := pred_of_mem, apply_eq := apply_eq } =
      { toFun := toFun_1, carrier := carrier_1, isOpen := isOpen_1, subset_iUnion := subset_iUnion_1,
        closure_subset := closure_subset_1, pred_of_mem := pred_of_mem_1, apply_eq := apply_eq_1 } →
    toFun = toFun_1 ∧ carrier = carrier_1
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_succ_equiv_apply : ∀ {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u) (a : Function.FromTypes p τ),
  (Function.fromTypes_succ_equiv p τ) a = a
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.instHasPluralDefaultsMessageData : Lean.HasPluralDefaults✝ Lean.MessageData
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the horizontal composition `η ◫ θ` with `η : f₁ ⟶ g₁` and `θ : f₂ ⟶ g₂`.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp : Lean.Expr →
  Option Mathlib.Tactic.BicategoryLike.IsoLift →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.NormedSpaceInfo.mk.sizeOf_spec : ∀ (normedSpace baseField : Lean.Expr),
  sizeOf { normedSpace := normedSpace, baseField := baseField } = 1 + sizeOf normedSpace + sizeOf baseField
-- Mathlib.Topology.Algebra.Monoid
addMonoidHomOfMemClosureRangeCoe.eq_1 : ∀ {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : AddZeroClass M₁]
  [inst_3 : AddZeroClass M₂] [inst_4 : ContinuousAdd M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂]
  [inst_6 : AddMonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun f x => f x)),
  addMonoidHomOfMemClosureRangeCoe f hf = { toFun := f, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.ne_one : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, σ.IsThreeCycle → σ ≠ 1
-- Mathlib.Algebra.Module.Submodule.EqLocus
LinearMap.eqLocus_same : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂), f.eqLocus f = ⊤
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.congr_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap.Raw α β cmp},
  t₁.Equiv t₂ → (t₃.Equiv t₁ ↔ t₃.Equiv t₂)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.Sign.noConfusionType : Sort v✝ → Tactic.ComputeAsymptotics.UnitMonomial.Sign → Tactic.ComputeAsymptotics.UnitMonomial.Sign → Sort v✝
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.State.mk.injEq : ∀ (cur : Array Bool) (added : Array ℕ) (numCalls : ℕ) (found : Bool) (cur_1 : Array Bool) (added_1 : Array ℕ)
  (numCalls_1 : ℕ) (found_1 : Bool),
  ({ cur := cur, added := added, numCalls := numCalls, found := found } =
      { cur := cur_1, added := added_1, numCalls := numCalls_1, found := found_1 }) =
    (cur = cur_1 ∧ added = added_1 ∧ numCalls = numCalls_1 ∧ found = found_1)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Faithful.comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.Faithful] [G.Faithful], (F.comp G).Faithful
-- Mathlib.Order.Lattice
exists_and_iff_of_monotone : ∀ {α : Type u} [inst : SemilatticeSup α] {P Q : α → Prop},
  Monotone P → Monotone Q → (((∃ x, P x) ∧ ∃ x, Q x) ↔ ∃ x, P x ∧ Q x)
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tmul_tensorMap_apply : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : AddCommGroup M₄]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] [inst_9 : Invertible 2]
  {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄}
  (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) (x : TensorProduct R M₁ M₃),
  (Q₂.tmul Q₄) ((TensorProduct.map f.toLinearMap g.toLinearMap) x) = (Q₁.tmul Q₃) x
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Turn an element of a type `F` satisfying `DistribMulActionHomClass F M X Y` into an actual
`DistribMulActionHom`. This is declared as the default coercion from `F` to
`DistribMulActionHom M X Y`.  -/
DistribMulActionSemiHomClass.toDistribMulActionHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_4} →
            [inst_2 : AddMonoid A] →
              [inst_3 : DistribMulAction M A] →
                {B : Type u_5} →
                  [inst_4 : AddMonoid B] →
                    [inst_5 : DistribMulAction N B] →
                      {F : Type u_10} →
                        [inst_6 : FunLike F A B] → [DistribMulActionSemiHomClass F (⇑φ) A B] → F → A →ₑ+[φ] B
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj_homEquiv : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {F G : CategoryTheory.Functor Cᵒᵖ (Type v)} {X Y : C} (h₁ : F.RepresentableBy X) (h₂ : G.RepresentableBy Y) {I : C},
  (CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj h₁ h₂).homEquiv =
    CategoryTheory.CartesianMonoidalCategory.homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)
-- Aesop.Builder.Basic
Aesop.RuleBuilderInput.phaseName : Aesop.RuleBuilderInput → Aesop.PhaseName
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a fallback : α}, ∅.getKeyD a fallback = fallback
-- Mathlib.RingTheory.AdicCompletion.Topology
/-- `IsPrecomplete I R` is equivalent to being complete in the adic topology.  -/
IsAdic.isPrecomplete_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : UniformSpace R] [IsUniformAddGroup R] {I : Ideal R},
  IsAdic I → (IsPrecomplete I R ↔ CompleteSpace R)
-- Mathlib.Logic.IsEmpty.Defs
/-- Non-dependent version of `IsEmpty.elim`. Helpful if the elaborator cannot elaborate `h.elim a`
correctly.  -/
IsEmpty.elim' : {α : Sort u} → {β : Sort v} → IsEmpty α → α → β
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBySet_ideal_span_singleton_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  Submodule.torsionBySet R M ↑(Ideal.span {a}) = Submodule.torsionBy R M a
-- Mathlib.Data.TypeVec
TypeVec.diag_sub_val : ∀ {n : ℕ} {α : TypeVec.{u} n}, TypeVec.comp (TypeVec.subtypeVal α.repeatEq) TypeVec.diagSub = TypeVec.prod.diag
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfc_realPart : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : StarModule ℂ A] [inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMap.UniqueHom ℂ A]
  (f : ℂ → ℂ) (a : A),
  autoParam (ContinuousOn f (spectrum ℂ ↑(realPart a))) cfc_realPart._auto_1 →
    autoParam (IsStarNormal a) cfc_realPart._auto_3 → cfc f ↑(realPart a) = cfc (fun x => f ↑x.re) a
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.List.Sublist.filter_mono : ∀ {α : Type u} {l : List α} {P Q : α → Bool},
  (∀ (a : α), P a = true → Q a = true) → (List.filter P l).Sublist (List.filter Q l)
-- Mathlib.Data.Nat.Bits
Nat.shiftRight_eq : ∀ (m n : ℕ), m.shiftRight n = m >>> n
-- Mathlib.Topology.ContinuousMap.Polynomial
Polynomial.toContinuousMap_apply : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] (p : Polynomial R)
  (x : R), p.toContinuousMap x = Polynomial.eval x p
-- Mathlib.Analysis.Distribution.TestFunction
TestFunctionClass.tsupport_map_subset : ∀ {B : Type u_6} {E : outParam (Type u_7)} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E}
  {Ω : outParam (TopologicalSpace.Opens E)} {F : outParam (Type u_8)} {inst_2 : NormedAddCommGroup F}
  {inst_3 : NormedSpace ℝ F} {n : outParam ℕ∞} [self : TestFunctionClass B Ω F n] (f : B), tsupport ⇑f ⊆ ↑Ω
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.ofCompId_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  (t :
    CategoryTheory.Bicategory.LeftExtension f
      (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c))),
  t.ofCompId.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).inv t.unit
-- Mathlib.Analysis.Calculus.ContDiff.Defs
AnalyticOnNhd.contDiff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞}, AnalyticOnNhd 𝕜 f Set.univ → ContDiff 𝕜 n f
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.valuation_lt_one_iff : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : ↥A), a ∈ IsLocalRing.maximalIdeal ↥A ↔ A.valuation ↑a < 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_le_size_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {l : List (α × β)},
  t.size ≤ (t.insertMany l).size
-- Lean.Meta.Reduce
Lean.Meta.reduceAll : Lean.Expr → Lean.MetaM Lean.Expr
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.run_bind.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (x : α) → (s : σ) → motive (EStateM.Result.ok x s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.error e s with
    | EStateM.Result.ok x s => h_1 x s
    | EStateM.Result.error e s => h_2 e s) =
    h_2 e s
-- Mathlib.Order.Antichain
IsAntichain.of_monotoneOn_strictAntiOn : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {f : α → β} {s : Set α},
  MonotoneOn f s → StrictAntiOn f s → IsAntichain (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- Given a `p : R[X]` and a root `x : S`,
then `p.leadingCoeff • x : S` is integral over `R`.  -/
isIntegral_leadingCoeff_smul : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (p : Polynomial R) (x : S)
  [inst_2 : Algebra R S], (Polynomial.aeval x) p = 0 → IsIntegral R (p.leadingCoeff • x)
-- Mathlib.Logic.Nontrivial.Defs
false_of_nontrivial_of_subsingleton : ∀ (α : Type u_3) [Nontrivial α] [Subsingleton α], False
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.isLocallyFraction_comapFun : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u} [inst_3 : CommRing S]
  {N : Type u} [inst_4 : AddCommGroup N] [inst_5 : Module S N] {σ : R →+* S} (f : M →ₛₗ[σ] N)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier)
  (s : (x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations M ↑x),
  (AlgebraicGeometry.StructureSheaf.isLocallyFraction R M).pred s →
    (AlgebraicGeometry.StructureSheaf.isLocallyFraction S N).pred
      (AlgebraicGeometry.StructureSheaf.comapFun f U V hUV s)
-- Init.Data.SInt.Basic
/-- Bitwise complement, also known as bitwise negation, for word-sized signed integers. Usually accessed
via the `~~~` prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
Integers use the two's complement representation, so `ISize.complement a = -(a + 1)`.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.complement : ISize → ISize
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftRight_le_of_nonpos : ∀ {n : ℤ} {s : ℕ}, n ≤ 0 → n >>> s ≤ 0
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse],
  (CategoryTheory.Equivalence.sheafCongr J K e A).unitIso = CategoryTheory.Equivalence.sheafCongr.unitIso J K e A
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.indicator_of_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : Zero R] {U : Set X} (f : LocallyConstant X R)
  {a : X} (hU : IsClopen U), a ∈ U → (f.indicator hU) a = f a
-- Mathlib.Algebra.Order.Group.Lattice
sup_add : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddRightMono α] (a b c : α), a ⊔ b + c = (a + c) ⊔ (b + c)
-- Lean.CoreM
Lean.Core.instAddMessageContextCoreM : Lean.AddMessageContext Lean.CoreM
-- Mathlib.Condensed.Light.Sequence
/-- This object is used to show that a certain map `T ⟶ X` descends
to a map `S ⊗ N∪{∞} → X`. Because epimorphisms in `LightProfinite`
are effective, it does so if the two maps `pullback π π → T → S ⊗ N∪{∞}`
are equal. This can be checked by precomposing with an epimorphism,
which is given by this morphism.  -/
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.cover : {S T : LightProfinite} →
  (π : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj S LightProfinite.NatUnionInfty) →
    CompHausLike.of (fun X => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
        (↑T.toTop ⊕
          ↑(CompHausLike.pullback
                (CategoryTheory.CategoryStruct.comp
                  (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
                    (CategoryTheory.CategoryStruct.comp π
                      (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))
                  π)
                (CategoryTheory.CategoryStruct.comp
                  (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
                    (CategoryTheory.CategoryStruct.comp π
                      (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))
                  π)).toTop) ⟶
      CompHausLike.pullback π π
-- Mathlib.RingTheory.RingHom.Smooth
/-- Smoothness is a local property of ring homomorphisms.  -/
RingHom.Smooth.propertyIsLocal : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => RingHom.Smooth
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Collects all semantic tokens from the given `Elab.InfoTree`.  -/
Lean.Server.FileWorker.collectInfoBasedSemanticTokens : Lean.Elab.InfoTree → Array Lean.Server.FileWorker.LeanSemanticToken
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
  {μ : G ⟶ A} (ε : F ⟶ G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η)
  (x : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ),
  (CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ ε hε).app x =
    TypeCat.ofHom fun u => CategoryTheory.OverPresheafAux.OverArrows.map₁ u ε hε
-- Mathlib.SetTheory.Ordinal.Notation
ONote.add.eq_def : ∀ (x x_1 : ONote),
  x.add x_1 =
    match x, x_1 with
    | ONote.zero, o => o
    | e.oadd n a, o => e.addAux n (a.add o)
-- Mathlib.Order.WithBot
WithBot.unbotD_coe : ∀ {α : Type u_5} (d x : α), WithBot.unbotD d ↑x = x
-- Mathlib.Algebra.Order.Star.Basic
one_lt_star_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {x : R},
  1 < star x ↔ 1 < x
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_eq_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M),
  Finsupp.filter p f = ∑ i ∈ f.support with p i, fun₀ | i => f i
-- Mathlib.Analysis.Normed.Operator.Prod
ContinuousLinearMap.opNorm_prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : SeminormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F) (g : E →L[𝕜] G),
  ‖f.prod g‖ = ‖(f, g)‖
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.decidableElim.injEq : ∀ (classical : Bool) (p₁ x : Lean.Name) (p₂ p₃ : Mathlib.Tactic.ITauto.Proof) (classical_1 : Bool)
  (p₁_1 x_1 : Lean.Name) (p₂_1 p₃_1 : Mathlib.Tactic.ITauto.Proof),
  (Mathlib.Tactic.ITauto.Proof.decidableElim classical p₁ x p₂ p₃ =
      Mathlib.Tactic.ITauto.Proof.decidableElim classical_1 p₁_1 x_1 p₂_1 p₃_1) =
    (classical = classical_1 ∧ p₁ = p₁_1 ∧ x = x_1 ∧ p₂ = p₂_1 ∧ p₃ = p₃_1)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomology_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {A : C} (f₁ f₂ : S.leftHomology ⟶ A),
  f₁ = f₂ ↔
    CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₁ = CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₂
-- Mathlib.Order.Filter.NAry
Filter.map₂_bot_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α}, Filter.map₂ m f ⊥ = ⊥
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.trans_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {e f g : u ⟶ v} (h : CategoryTheory.Arrow.LeftHomotopy e f)
  (k : CategoryTheory.Arrow.LeftHomotopy f g), (h.trans k).hom = h.hom + k.hom
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.mk.congr_simp : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴}
  (toNatTrans toNatTrans_1 : CategoryTheory.NatTrans F.toFunctor G.toFunctor) (e_toNatTrans : toNatTrans = toNatTrans_1)
  (isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (toNatTrans.app a)),
  { toNatTrans := toNatTrans, isHomLift' := isHomLift' } = { toNatTrans := toNatTrans_1, isHomLift' := ⋯ }
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `L` have coprime degree over `F`, then they are linearly disjoint.  -/
IntermediateField.LinearDisjoint.of_finrank_coprime : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  (Module.finrank F ↥A).Coprime (Module.finrank F L) → A.LinearDisjoint L
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
min_le_add_of_nonneg_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddZeroClass α] [AddLeftMono α] {a b : α}, 0 ≤ b → min a b ≤ a + b
-- Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
/-- If `GenContFract.of v` terminates, then there is `n : ℕ` such that the `n`th convergent is
exactly `v`.
 -/
GenContFract.of_correctness_of_terminates : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] {v : K} [inst_2 : FloorRing K],
  (GenContFract.of v).Terminates → ∃ n, v = (GenContFract.of v).convs n
-- Mathlib.Data.Ordmap.Ordnode
/-- Auxiliary definition for `ofAscList`.  -/
Ordnode.ofAscListAux₂ : {α : Type u_1} → List α → Ordnode α → ℕ → Ordnode α
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Opens.partialIsoOfDense.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (hU : Dense ↑U), U.partialIsoOfDense hU = U.partialIsoOfDense hU
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_div_distrib : ∀ {ι : Type u_1} {G : Type u_5} {s : Finset ι} [inst : DivisionCommMonoid G] (f g : ι → G),
  ∏ x ∈ s, f x / g x = (∏ x ∈ s, f x) / ∏ x ∈ s, g x
-- Init.Grind.Ring.Basic
/-- Left distributivity of multiplication over addition.  -/
Lean.Grind.Semiring.left_distrib : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a b c : α), a * (b + c) = a * b + a * c
-- Lean.Meta.Tactic.IndependentOf
/-- Check if a goal is "independent" of a list of other goals.
We say a goal is independent of other goals if assigning a value to it
can not change the assignability of the other goals.

Examples:
* `?m_1 : Type` is not independent of `?m_2 : ?m_1`,
  because we could assign `true : Bool` to `?m_2`,
  but if we first assign `Nat` to `?m_1` then that is no longer possible.
* `?m_1 : Nat` is not independent of `?m_2 : Fin ?m_1`,
  because we could assign `37 : Fin 42` to `?m_2`,
  but if we first assign `2` to `?m_1` then that is no longer possible.
* `?m_1 : ?m_2` is not independent of `?m_2 : Type`, because we could assign `Bool` to ?m_2`,
  but if we first assign `0 : Nat` to `?m_1` then that is no longer possible.
* Given `P : Prop` and `f : P → Type`, `?m_1 : P` is independent of `?m_2 : f ?m_1`
  by proof irrelevance.
* Similarly given `f : Fin 0 → Type`, `?m_1 : Fin 0` is independent of `?m_2 : f ?m_1`,
  because `Fin 0` is a subsingleton.
* Finally `?m_1 : Nat` is independent of `?m_2 : α`,
  as long as `?m_1` does not appear in `Meta.getMVars α`
  (note that `Meta.getMVars` follows delayed assignments).

This function only calculates a conservative approximation of this condition.
That is, it may return `false` when it should return `true`.
(In particular it returns false whenever the type of `g` contains a metavariable,
regardless of whether this is related to the metavariables in `L`.)
 -/
Lean.MVarId.isIndependentOf : List Lean.MVarId → Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Probability.Distributions.Beta
ProbabilityTheory.betaMeasure.eq_1 : ∀ (α β : ℝ), ProbabilityTheory.betaMeasure α β = MeasureTheory.volume.withDensity (ProbabilityTheory.betaPDF α β)