mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Inductive predicate stating that a list of search steps represents a valid search from a given
position in a slice.

"Searching" here means always taking the longest match at the first position where the pattern
matches.

Hence, this predicate determines the list of search steps up to grouping of rejections.
 -/
String.Slice.Pattern.Model.IsValidSearchFrom : {ρ : Type} →
  (pat : ρ) →
    [String.Slice.Pattern.Model.PatternModel pat] →
      {s : String.Slice} → s.Pos → List (String.Slice.Pattern.SearchStep s) → Prop
-- Mathlib.Order.SuccPred.Basic
/-- There is at most one way to define the predecessors in a `PartialOrder`.  -/
Order.instSubsingletonPredOrder : ∀ {α : Type u_1} [inst : PartialOrder α], Subsingleton (PredOrder α)
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.of_subsingleton : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Subsingleton M], IsHausdorff I M
-- Batteries.Data.Array.Basic
Array.scanlM.loop.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (init : β) (as : Array α)
  (start stop : ℕ) (h_stop : stop ≤ as.size) (acc : Array β),
  Array.scanlM.loop f init as start stop h_stop acc =
    if h_lt : start < stop then do
      let __do_lift ← f init as[start]
      Array.scanlM.loop f __do_lift as (start + 1) stop h_stop (acc.push init)
    else pure (acc.push init)
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
/-- The binary product of finite measures.  -/
MeasureTheory.FiniteMeasure.prod : {α : Type u_1} →
  [inst : MeasurableSpace α] →
    {β : Type u_2} →
      [inst_1 : MeasurableSpace β] →
        MeasureTheory.FiniteMeasure α → MeasureTheory.FiniteMeasure β → MeasureTheory.FiniteMeasure (α × β)
-- Mathlib.Analysis.Complex.Norm
Complex.range_normSq : Set.range ⇑Complex.normSq = Set.Ici 0
-- Mathlib.GroupTheory.Index
Subgroup.isFiniteRelIndex_top_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.IsFiniteRelIndex ⊤ ↔ H.FiniteIndex
-- Lean.Server.InfoUtils
Lean.Elab.Info.size? : Lean.Elab.Info → Option String.Pos.Raw
-- Batteries.Recycling.RBTree.Lemmas
/-- Auxiliary definition for `zoom_ins`: set the root of the tree to `v`, creating a node if necessary.
 -/
RBTree.RBNode.delRoot : {α : Type u_1} → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.Algebra.Lie.Basic
LieEquiv.self_trans_symm : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂), e.trans e.symm = LieEquiv.refl
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.zero_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.AddGrpObj G],
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero CategoryTheory.AddGrpObj.neg =
    CategoryTheory.AddMonObj.zero
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.Y_sub_Y_add_Y_sub_negY : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
    P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3 + (P 1 * Q 2 ^ 3 - W'.negY Q * P 2 ^ 3) = (P 1 - W'.negY P) * Q 2 ^ 3
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.diagonalization_symm_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] (hT : T.IsSymmetric)
  (w : PiLp 2 fun μ => ↥(Module.End.eigenspace T (↑T 1 μ))), hT.diagonalization.symm w = ∑ μ, ↑(w.ofLp μ)
-- Mathlib.Data.Fin.Tuple.Basic
/-- **Alias** of `Fin.exists_fin_succ`. -/
Fin.exists_iff_succ : ∀ {n : ℕ} {P : Fin (n + 1) → Prop}, (∃ i, P i) ↔ P 0 ∨ ∃ i, P i.succ
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRupAdd.eq_1 : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ),
  f.performRupAdd c rupHints =
    match f.insertRupUnits c.negate with
    | (f, foundContradiction) =>
      if foundContradiction = true then
        have f := f.clearRupUnits;
        (f.insert c, true)
      else
        match f.performRupCheck rupHints with
        | (f, derivedLits, derivedEmpty, encounteredError) =>
          if encounteredError = true then (f, false)
          else
            if (!derivedEmpty) = true then (f, false)
            else
              match f with
              | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
                have assignments :=
                  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments assignments derivedLits;
                have f :=
                  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                      assignments := assignments }.clearRupUnits;
                (f.insert c, true)
-- Mathlib.Util.AtLocation
Mathlib.Tactic.instInhabitedBehaviorIfUnchanged : Inhabited Mathlib.Tactic.BehaviorIfUnchanged
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.dilatransvection.eq_1 : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} (h : IsUnit (1 + f v)),
  LinearEquiv.dilatransvection h =
    { toFun := ⇑(LinearMap.transvection f v), map_add' := ⋯, map_smul' := ⋯,
      invFun := ⇑(LinearMap.transvection f (-h.unit⁻¹ • v)), left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Simple
CategoryTheory.instIsSimpleOrderSubobjectOfSimple : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} [CategoryTheory.Simple X],
  IsSimpleOrder (CategoryTheory.Subobject X)
-- Mathlib.Algebra.Group.Prod
Prod.instCancelCommMonoid : {M : Type u_3} → {N : Type u_4} → [CancelCommMonoid M] → [CancelCommMonoid N] → CancelCommMonoid (M × N)
-- Mathlib.Topology.Category.LightProfinite.Basic
instFullLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.Full
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_insertList_of_contains_eq_false_left : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.containsKey k l = false →
        Std.Internal.List.getValue? k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getValue? k toInsert
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.join_think : ∀ {α : Type u} (S : Stream'.WSeq (Stream'.WSeq α)), S.think.join = S.join.think
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.List.of_toArrayAux_eq_toArrayAux : ∀ {α : Type u_1} {as bs : List α} {cs ds : Array α},
  as.toArrayAux cs = bs.toArrayAux ds → cs.size = ds.size → as = bs ∧ cs = ds
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_union : ∀ {α : Type u_2} [inst : Div α] {s t₁ t₂ : Set α}, s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mk_set : ∀ {α : Type u}, Cardinal.mk (Set α) = 2 ^ Cardinal.mk α
-- Mathlib.RepresentationTheory.FDRep
FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G] [IsNoetherianRing R],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G))
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.opensNhds.instFunLike : {X : TopCat} → {x : ↑X} → {U V : TopologicalSpace.OpenNhds x} → FunLike (U ⟶ V) ↥↑U ↥↑V
-- Mathlib.Topology.Sheaves.EtaleSpace
TopCat.Presheaf.EtaleSpace.homeomorph.congr_simp : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X}
  [inst_4 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (U : TopologicalSpace.Opens ↑X)
  (hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (F.germ U x hx))) (x : ↑X)
  (hx : x ∈ U),
  TopCat.Presheaf.EtaleSpace.homeomorph U hF_bij x hx = TopCat.Presheaf.EtaleSpace.homeomorph U hF_bij x hx
-- Mathlib.RepresentationTheory.Equiv
Representation.ofMulActionSubsingletonEquivTrivial_apply : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : Monoid G] (H : Type w) [inst_2 : Subsingleton H]
  [inst_3 : MulOneClass H] [inst_4 : MulAction G H] (f : MonoidAlgebra k H),
  (↑(Representation.ofMulActionSubsingletonEquivTrivial k G H)).toLinearMap f = f.coeff 1
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Ico_add_intCast : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (a : α),
  ⋃ n, Set.Ico (a + ↑n) (a + ↑n + 1) = Set.univ
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod : ∀ {n : ℕ} {R : Type u_1} [inst : CommRing R] (σ : Equiv.Perm (Fin n)) {f : Fin n → Fin n → R},
  (∀ (i j : Fin n), f i j = -f j i) → ∏ j, ∏ i < j, f (σ i) (σ j) = ↑↑(Equiv.Perm.sign σ) * ∏ j, ∏ i < j, f i j
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_of_const_add : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f : α → M} (C : M), Filter.Tendsto (fun x => C + f x) l Filter.atTop → Filter.Tendsto f l Filter.atTop
-- Mathlib.Algebra.GradedMonoid
/-- Construct an element of a graded monoid.  -/
GradedMonoid.mk : {ι : Type u_1} → {A : ι → Type u_2} → (i : ι) → A i → GradedMonoid A
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.intrinsicStar_eq_comp : ∀ {E : Type u_2} {F : Type u_3} [inst : AddCommMonoid E] [inst_1 : StarAddMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : StarAddMonoid F] [inst_4 : TopologicalSpace E] [inst_5 : TopologicalSpace F] [inst_6 : ContinuousStar E]
  [inst_7 : ContinuousStar F] {R : Type u_4} [inst_8 : CommSemiring R] [inst_9 : StarRing R] [inst_10 : Module R E]
  [inst_11 : StarModule R E] [inst_12 : Module R F] [inst_13 : StarModule R F] (f : WithConv (E →L[R] F)),
  star f = WithConv.toConv (↑(starL R) ∘SL f.ofConv ∘SL ↑(starL R))
-- Mathlib.Data.Multiset.AddSub
Multiset.count_erase_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α},
  a ≠ b → ∀ (s : Multiset α), Multiset.count a (s.erase b) = Multiset.count a s
-- Mathlib.RingTheory.Kaehler.Basic
/-- The map `I/I² → B ⊗[A] Ω[A⁄R]` where `I = ker(A → B)`.  -/
KaehlerDifferential.kerCotangentToTensor : (R : Type u) →
  [inst : CommRing R] →
    (A : Type u_2) →
      (B : Type u_3) →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra A B] → (RingHom.ker (algebraMap A B)).Cotangent →ₗ[A] TensorProduct A B Ω[A⁄R]
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
ULift.instPseudoMetricSpace : {β : Type u_2} → [PseudoMetricSpace β] → PseudoMetricSpace (ULift.{u_3, u_2} β)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- A base angle of an isosceles triangle is acute, oriented vector angle form.  -/
Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, ‖x‖ = ‖y‖ → |(o.oangle x (x - y)).toReal| < Real.pi / 2
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.of_diseq : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] {a b : α} {a' b' : ℤ},
  ↑a = a' → ↑b = b' → a ≠ b → a' ≠ b'
-- Mathlib.Order.Filter.CardinalInter
Filter.EventuallyEq.cardinal_iUnion : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s t : ι → Set α},
  Cardinal.mk ι < c → (∀ (i : ι), s i =ᶠ[l] t i) → ⋃ i, s i =ᶠ[l] ⋃ i, t i
-- Mathlib.GroupTheory.Perm.Cycle.Type
/-- For every prime `p` dividing the order of a finite group `G` there exists an element of order
`p` in `G`. This is known as Cauchy's theorem.  -/
exists_prime_orderOf_dvd_card : ∀ {G : Type u_3} [inst : Group G] [inst_1 : Fintype G] (p : ℕ) [hp : Fact (Nat.Prime p)],
  p ∣ Fintype.card G → ∃ x, orderOf x = p
-- Mathlib.Analysis.SpecialFunctions.Exp
Continuous.rexp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ}, Continuous f → Continuous fun y => Real.exp (f y)
-- Lean.Meta.InferType
/-- `isArrowProp type n` is an "approximate" predicate which returns `LBool.true`
if `type` is of the form `A_1 → ... → A_n → Prop`.

Remark: `type` can be a dependent arrow.
 -/
_private.Lean.Meta.InferType.0.Lean.Meta.isArrowProp : Lean.Expr → ℕ → Lean.MetaM Lean.LBool
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.toSlashInvariantForm_natCast : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] (n : ℕ), (↑n).toSlashInvariantForm = ↑n
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {m : Type u_1 → Type u_2} {δ : Type u_1}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldrM f init t = List.foldrM (fun p acc => f p.fst p.snd acc) init t.toListModel
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `GroupExtension`s are equivalent iff there is an isomorphism making a commuting diagram.
Use `GroupExtension.Equiv.ofMonoidHom` in `Mathlib/GroupTheory/GroupExtension/Basic.lean` to
construct an equivalence without providing the inverse map.  -/
GroupExtension.Equiv : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] →
          [inst_2 : Group G] →
            GroupExtension N E G → {E' : Type u_4} → [inst_3 : Group E'] → GroupExtension N E' G → Type (max u_2 u_4)
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.pow_comp : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_7} [inst : Pow M α] (f : β → M) (a : α) (g : ι → β),
  (f ^ a) ∘ g = f ∘ g ^ a
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_mul_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal},
  Measurable f → ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.isAcc_iff : ∀ (o : Ordinal.{u_1}) (S : Set Ordinal.{u_1}), o.IsAcc S ↔ o ≠ 0 ∧ ∀ p < o, (S ∩ Set.Ioo p o).Nonempty
-- Mathlib.MeasureTheory.Function.EssSup
ae_essInf_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLinearOrder β] {f : α → β} [inst_1 : TopologicalSpace β] [FirstCountableTopology β]
  [OrderTopology β],
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) f) ae_essInf_le._auto_1 →
    ∀ᵐ (y : α) ∂μ, essInf f μ ≤ f y
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.IsoCat.refl_inverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  (CategoryTheory.IsoCat.refl C).inverse = CategoryTheory.Functor.id C
-- Mathlib.FieldTheory.Galois.Basic
isGalois_iff_isGalois_bot : ∀ {F : Type u_1} {E : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IsGalois (↥⊥) E ↔ IsGalois F E
-- Mathlib.Algebra.DirectSum.Decomposition
/-- Two linear maps from a module with a decomposition agree if they agree on every piece.

Note this cannot be `@[ext]` as `ℳ` cannot be inferred.  -/
DirectSum.decompose_lhom_ext : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (ℳ : ι → Submodule R M) [DirectSum.Decomposition ℳ] {N : Type u_5} [inst : AddCommMonoid N]
  [inst_4 : Module R N] ⦃f g : M →ₗ[R] N⦄, (∀ (i : ι), f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype) → f = g
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) [addGrp : CategoryTheory.AddGrpObj X] (X_1 : C) (addGrp_1 : CategoryTheory.AddGrpObj X_1),
  ({ X := X, addGrp := addGrp } = { X := X_1, addGrp := addGrp_1 }) = (X = X_1 ∧ addGrp ≍ addGrp_1)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The diagram of finite quotients of `P` viewed in `ProfiniteAddGrp`.  -/
ProfiniteAddGrp.diagram : (P : ProfiniteAddGrp.{u}) → CategoryTheory.Functor (OpenNormalAddSubgroup ↑P.toProfinite.toTop) ProfiniteAddGrp.{u}
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.mkHomToSingle_f : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι}
  {K : HomologicalComplex V c} {j : ι} {A : V} (φ : K.X j ⟶ A)
  (hφ : ∀ (i : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (K.d i j) φ = 0),
  (HomologicalComplex.mkHomToSingle φ hφ).f j =
    CategoryTheory.CategoryStruct.comp φ (HomologicalComplex.singleObjXSelf c j A).inv
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.openPartialHomeomorph_source : ∀ {A : Type u_1} [inst : CStarAlgebra A], Unitary.openPartialHomeomorph.source = Metric.ball 1 2
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ_assoc : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F]
  (X Y : C) {Z : E} (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (L.obj X) (L.obj Y)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F (L.obj X) (L.obj Y)) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.Localization.Lifting.iso L W G F).hom.app X)
        ((CategoryTheory.Localization.Lifting.iso L W G F).hom.app Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ G X Y)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Localization.Lifting.iso L W G F).inv.app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
          (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.OplaxMonoidal.δ L X Y)) h)))
-- Mathlib.Tactic.Polynomial.Core
/-- Attempts to infer the base `R` of an `Algebra R A` based only on `A`. e.g. returns `R` given
`Polynomial R`.  -/
Mathlib.Tactic.Polynomial.PolynomialExt.infer : Mathlib.Tactic.Polynomial.PolynomialExt → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Computability.RecursiveIn
/-- The type of partial functions recursive in a set of oracles `O` is the smallest type containing
the constant zero, the successor, left and right projections, each oracle `g ∈ O`,
and is closed under pairing, composition, primitive recursion, and μ-recursion.
 -/
Nat.RecursiveIn : Set (ℕ →. ℕ) → (ℕ →. ℕ) → Prop
-- Mathlib.LinearAlgebra.Basis.Defs
/-- An unbundled version of `repr_eq_iff`  -/
Module.Basis.repr_apply_eq : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (f : M → ι → R),
  (∀ (x y : M), f (x + y) = f x + f y) →
    (∀ (c : R) (x : M), f (c • x) = c • f x) →
      (∀ (i : ι), f (b i) = ⇑fun₀ | i => 1) → ∀ (x : M) (i : ι), (b.repr x) i = f x i
-- Mathlib.Algebra.Module.SpanRankOperations
TensorProduct.spanRank_top_le : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (N : Submodule R M), ⊤.spanRank ≤ Cardinal.lift.{u_2, u_3} N.spanRank
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.containsThenInsertIfNew k v).1 = t.contains k
-- Mathlib.Algebra.GCDMonoid.Basic
/-- GCD monoid: a cancellative `CommMonoidWithZero` with `gcd` (greatest common divisor) and
`lcm` (least common multiple) operations, determined up to a unit. The type class focuses on `gcd`
and we derive the corresponding `lcm` facts from `gcd`.
 -/
GCDMonoid : (α : Type u_2) → [CommMonoidWithZero α] → Type u_2
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.optionEquivalence_functor : ∀ {J : Type w₁} (C' : Option J → Type u₁) [inst : (i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)],
  (CategoryTheory.Pi.optionEquivalence C').functor =
    (CategoryTheory.Pi.eval C' none).prod' (CategoryTheory.Functor.pi' fun i => CategoryTheory.Pi.eval C' (some i))
-- Mathlib.Order.SuccPred.Archimedean
strictAnti_of_lt_pred : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : PredOrder α]
  [IsPredArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMin a → f a < f (Order.pred a)) → StrictAnti f
-- Mathlib.Topology.TietzeExtension
Prod.instTietzeExtension : ∀ {Y : Type v} {Z : Type w} [inst : TopologicalSpace Y] [TietzeExtension Y] [inst_2 : TopologicalSpace Z]
  [TietzeExtension Z], TietzeExtension (Y × Z)
-- Aesop.Stats.Basic
Aesop.instToJsonForwardInstantiationStats.toJson : Aesop.ForwardInstantiationStats → Lean.Json
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstr.mk.inj : ∀ {p : Lean.Grind.Linarith.Poly} {h : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof} {p_1 : Lean.Grind.Linarith.Poly}
  {h_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof}, { p := p, h := h } = { p := p_1, h := h_1 } → p = p_1 ∧ h = h_1
-- Std.Http.Data.Version
Std.Http.Version.v11.sizeOf_spec : sizeOf Std.Http.Version.v11 = 1
-- Mathlib.GroupTheory.Perm.Cycle.Basic
List.Nodup.isCycleOn_formPerm : ∀ {α : Type u_2} [inst : DecidableEq α] {l : List α}, l.Nodup → l.formPerm.IsCycleOn {a | a ∈ l}
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.coeffs_apply : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M} (h : Module.DualBases e ε) (m : M) (i : ι), (h.coeffs m) i = (ε i) m
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.mul_closedBall_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → s * Metric.closedBall 1 δ = Metric.cthickening δ s
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddCommGroup.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : IsTopologicalAddGroup G],
  SeparationQuotient.instAddCommGroup = { toAddGroup := SeparationQuotient.instAddGroup, add_comm := ⋯ }
-- Mathlib.Util.Notation3
/-- Get the accumulated array of delaborated terms for a given foldr/foldl.
Returns `#[]` if nothing has been pushed yet.  -/
Mathlib.Notation3.MatchState.getFoldArray : Mathlib.Notation3.MatchState → Lean.Name → Array Lean.Term
-- Lean.Elab.App
Lean.Elab.Term.elabProj : Lean.Elab.Term.TermElab