mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgEquiv.toCoalgIso_trans : ∀ {R : Type u} [inst : CommRing R] {X Y Z : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module R Y] [inst_5 : AddCommGroup Z] [inst_6 : Module R Z]
  [inst_7 : Coalgebra R X] [inst_8 : Coalgebra R Y] [inst_9 : Coalgebra R Z] (e : X ≃ₗc[R] Y) (f : Y ≃ₗc[R] Z),
  (e.trans f).toCoalgIso = e.toCoalgIso ≪≫ f.toCoalgIso
-- Init.Data.List.Sublist
List.suffix_nil : ∀ {α : Type u_1} {l : List α}, l <:+ [] ↔ l = []
-- Mathlib.GroupTheory.Subgroup.Center
AddGroup.addCommGroupOfCenterEqTop.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (h : AddSubgroup.center G = ⊤),
  AddGroup.addCommGroupOfCenterEqTop h = { toAddGroup := inst, add_comm := ⋯ }
-- Mathlib.Data.Set.Function
Set.InjOn.mem_of_mem_image : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : α → β} {x : α},
  Set.InjOn f s → s₁ ⊆ s → x ∈ s → f x ∈ f '' s₁ → x ∈ s₁
-- Lean.Meta.Tactic.Grind.Types
/-- Term `e` may be an inductive predicate, `match`-expression, `if`-expression, implication, etc.
 -/
Lean.Meta.Grind.SplitInfo.default : Lean.Expr → Lean.Meta.Grind.SplitSource → Lean.Meta.Grind.SplitInfo
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
_private.Mathlib.Algebra.Homology.Embedding.AreComplementary.0.ComplexShape.Embedding.AreComplementary.fromSum.match_1.eq_1 : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} (motive : ι₁ ⊕ ι₂ → Sort u_3) (i₁ : ι₁) (h_1 : (i₁ : ι₁) → motive (Sum.inl i₁))
  (h_2 : (i₂ : ι₂) → motive (Sum.inr i₂)),
  (match Sum.inl i₁ with
    | Sum.inl i₁ => h_1 i₁
    | Sum.inr i₂ => h_2 i₂) =
    h_1 i₁
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Cache decision variables used when splitting on disequalities.
This is necessary because the same disequality may be in different conflicts.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.diseqSplits : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PHashMap Int.Internal.Linear.Poly Lean.FVarId
-- Mathlib.Algebra.Group.Submonoid.Basic
AddMonoidHom.ofClosureMEqTopLeft.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] {s : Set M} (f : M → N)
  (hs : AddSubmonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ x ∈ s, ∀ (y : M), f (x + y) = f x + f y),
  AddMonoidHom.ofClosureMEqTopLeft f hs h1 hmul = { toFun := f, map_zero' := h1, map_add' := ⋯ }
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.comp_equiv : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {P : Type u_2} [inst_9 : AddCommMonoid P] [inst_10 : Module R P]
  (e : M ≃ₗ[R] P) (f : P →ₗ[R] N), IsBaseChange S f → IsBaseChange S (f ∘ₗ ↑e)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C},
  CategoryTheory.Limits.IsZero Y → ∀ (e : X ≅ Y), CategoryTheory.Limits.IsZero X
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_sub : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f g : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b →
    IntervalIntegrable g μ a b → ∫ (x : ℝ) in a..b, f x - g x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in a..b, g x ∂μ
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.instSigmaFiniteRestrictSigmaFiniteSetWRT : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  MeasureTheory.SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT ν))
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.lanPresheafIso_hom : ∀ {S : LightProfinite} {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)}
  (hF : CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))),
  (LightCondensed.lanPresheafIso hF).hom =
    CategoryTheory.Limits.colimit.desc
      ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op (Opposite.op S)).comp
        (FintypeCat.toLightProfinite.op.comp F))
      (LightProfinite.Extend.cocone F S)
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
/-- The multicofork in the category associated to the complete lattice `T`
associated to `d : MulticoequalizerDiagram x u v` with `x : T`.
(In the case `T := Set X`, this multicofork becomes colimit after the application
of the obvious functor `Set X ⥤ Type _`.)  -/
CompleteLattice.MulticoequalizerDiagram.multicofork : {T : Type u} →
  [inst : CompleteLattice T] →
    {ι : Type u_1} →
      {x : T} →
        {u : ι → T} →
          {v : ι → ι → T} →
            (d : CompleteLattice.MulticoequalizerDiagram x u v) → CategoryTheory.Limits.Multicofork d.multispanIndex
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_eq : ∀ (a b : UInt64), a.toUInt16 = b.toUInt16 ↔ a % 65536 = b % 65536
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_natCast_mul_add : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIocDiv hp a (↑m * p + b) = ↑m + toIocDiv hp a b
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.isCardinalFilteredGenerator_hasCardinalLTWithTerminal : ∀ (κ : Cardinal.{u}) [inst : Fact κ.IsRegular],
  (CategoryTheory.CardinalDirectedPoset.hasCardinalLTWithTerminal κ).IsCardinalFilteredGenerator κ
-- Mathlib.RingTheory.MvPowerSeries.Trunc
/-- The truncation of a multivariate formal power series at a total degree `n`
when the index `σ` is finite.  -/
MvPowerSeries.truncTotal : {σ : Type u_1} → [Finite σ] → {R : Type u_4} → [inst : CommSemiring R] → ℕ → MvPowerSeries σ R →ₗ[R] MvPolynomial σ R
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.Uniformizer.mk : {Γ : Type u_1} →
  [inst : LinearOrderedCommGroupWithZero Γ] →
    {A : Type u_2} →
      [inst_1 : Ring A] →
        {v : Valuation A Γ} → [hv : v.IsRankOneDiscrete] → (val : ↥v.integer) → v.IsUniformizer ↑val → v.Uniformizer
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a : α} {fallback : β},
      (t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback
-- Mathlib.Analysis.Matrix.Normed
Matrix.norm_le_iff : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] {r : ℝ}, 0 ≤ r → ∀ {A : Matrix m n α}, ‖A‖ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖ ≤ r
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffineLift_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hP : W.NonsingularLift ⟦P⟧),
  { point := ⟦P⟧, nonsingular := hP }.toAffineLift = WeierstrassCurve.Projective.Point.toAffine W P
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Pseudofunctor.mapAdjunction_unit : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {a b : B}
  {f : a ⟶ b} {g : b ⟶ a} (F : CategoryTheory.Pseudofunctor B C) (adj : CategoryTheory.Bicategory.Adjunction f g),
  (F.mapAdjunction adj).unit =
    CategoryTheory.CategoryStruct.comp (F.mapId a).inv
      (CategoryTheory.CategoryStruct.comp (F.map₂ adj.unit) (F.mapComp f g).hom)
-- Mathlib.GroupTheory.Focal
Subgroup.commutator_le_focalSubgroup : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⁅H, H⁆ ≤ H.focalSubgroup
-- Mathlib.Topology.Homeomorph.Quotient
/-- A homeomorphism `e : X ≃ₜ Y` generates an equivalence between the quotient space of `X`
by a relation `rX` and the quotient space of `Y` by the image of this relation under `e`.  -/
Homeomorph.Quot.congrLeft : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {r : X → X → Prop} → (e : X ≃ₜ Y) → Quot r ≃ₜ Quot fun y₁ y₂ => r (e.symm y₁) (e.symm y₂)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_nsmul : ∀ {α : Type u} [inst : AddMonoid α] (a : α) (n : ℕ), ↑(n • a) = n • ↑a
-- Mathlib.Logic.Small.Set
small_image2 : ∀ {α : Type u1} {β : Type u2} {γ : Type u3} (f : α → β → γ) (s : Set α) (t : Set β) [Small.{u, u1} ↑s]
  [Small.{u, u2} ↑t], Small.{u, u3} ↑(Set.image2 f s t)
-- Mathlib.Data.Num.Basic
Num.decidableLE : DecidableLE Num
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance is always nonnegative  -/
Metric.infDist_nonneg : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, 0 ≤ Metric.infDist x s
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.lift₂_def : ∀ {ι : Type u_1} [inst : Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6}
  (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)]
  [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7}
  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)]
  [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] [inst_5 : IsDirectedOrder ι] {C : Sort u_9}
  (ih : (i : ι) → F₁ i → F₂ i → C)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)) (i : ι)
  (x : F₁ i) (y : F₂ i), DirectLimit.lift₂ f₁ f₂ ih compat ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = ih i x y
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.monotone_rpow_of_nonneg : ∀ {z : ℝ}, 0 ≤ z → Monotone fun x => x ^ z
-- Mathlib.Probability.Independence.ZeroOne
/-- **Kolmogorov's 0-1 law**, conditional version: any event in the tail σ-algebra of a
conditionally independent sequence of sub-σ-algebras has conditional probability 0 or 1.  -/
ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atBot : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] [inst_3 : StandardBorelSpace Ω] (hm : m ≤ m0)
  [inst_4 : MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iCondIndep m hm s μ →
      ∀ {t : Set Ω},
        MeasurableSet t → ∀ᵐ (ω : Ω) ∂μ, μ[t.indicator fun ω => 1 | m] ω = 0 ∨ μ[t.indicator fun ω => 1 | m] ω = 1
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- The left whiskering in the bicategory `Adj B`.  -/
CategoryTheory.Bicategory.Adj.Bicategory.whiskerLeft : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : CategoryTheory.Bicategory.Adj B} →
      (α : a ⟶ b) →
        {β β' : b ⟶ c} → (β ⟶ β') → (CategoryTheory.CategoryStruct.comp α β ⟶ CategoryTheory.CategoryStruct.comp α β')
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.sub_const : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : SubtractionCommMonoid α] [inst_1 : Neg β],
  Function.Antiperiodic f c → ∀ (a : α), Function.Antiperiodic (fun x => f (x - a)) c
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_sdiff_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iic b \ Set.Ioc a b = Set.Iic (min a b)
-- Batteries.Data.List.Lemmas
List.swap_eq : ∀ {α : Type u_1} {i j : ℕ} {xs : List α},
  xs.swap i j = if h : i < xs.length ∧ j < xs.length then (xs.set i xs[j]).set j xs[i] else xs
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_middle.sizeOf_spec : ∀ (lhs : Bool) (s₁ s₂ : Lean.Grind.AC.Seq) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (c₂ : Lean.Meta.Grind.AC.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.AC.DiseqCnstrProof.simp_middle lhs s₁ s₂ c₁ c₂) =
    1 + sizeOf lhs + sizeOf s₁ + sizeOf s₂ + sizeOf c₁ + sizeOf c₂
-- Mathlib.Algebra.Category.Grp.Adjunctions
/-- The forgetful-units adjunction between `GrpCat` and `MonCat`.  -/
GrpCat.forget₂MonAdj : CategoryTheory.forget₂ GrpCat MonCat ⊣ MonCat.units
-- Mathlib.Analysis.Calculus.FDeriv.Congr
HasFDerivWithinAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → HasFDerivWithinAt f₁ f' s x
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.singularValues_pos_iff_ne_zero : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) (i : ℕ), 0 < T.singularValues i ↔ T.singularValues i ≠ 0
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)),
  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj F U c).pt = c.pt
-- Mathlib.Data.Prod.Lex
CovBy.eq_1 : ∀ {α : Type u_2} [inst : LT α] (a b : α), (a ⋖ b) = (a < b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b)
-- Mathlib.Logic.Function.Defs
Function.diag_comp : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.diag ∘ f = Function.prod f f
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_succ_Ioc : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.succ (Finset.Ioc i j) = Finset.Ioc i.succ j.succ
-- Mathlib.Data.Int.Cast.Lemmas
zmultiplesAddHom_apply : ∀ (β : Type u_4) [inst : AddCommGroup β] (x : β) (n : ℤ), ((zmultiplesAddHom β) x) n = n • x
-- Mathlib.Data.TypeVec
/-- predicate on the product of two type vectors to constrain only their last object  -/
TypeVec.RelLast' : {n : ℕ} →
  (α : TypeVec.{u_1} n) →
    {β : Type u_1} → (β → β → Prop) → ((α ::: β).prod (α ::: β)).Arrow (TypeVec.repeat (n + 1) Prop)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.instInhabited : {n : ℕ} → Inhabited (OrderedFinpartition n)
-- Mathlib.RingTheory.Smooth.NoetherianDescent
/-- Let `A` be an `R`-algebra. If `B` is a smooth `A`-algebra, there exists an
`R`-subalgebra of finite type `A₀` of `A` and a smooth `A₀`-algebra `B₀` such that
`B ≃ₐ A ⊗[A₀] B₀`.
See `Algebra.Smooth.exists_finiteType` for a version in terms of `Function.Injective`.
 -/
Algebra.Smooth.exists_subalgebra_fg : ∀ (R : Type u_1) [inst : CommRing R] (A : Type u) (B : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] [Algebra.Smooth A B],
  ∃ A₀ B₀ x x_1, A₀.FG ∧ Algebra.Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] TensorProduct (↥A₀) A B₀)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Adjunction.mapAddMon.eq_1 : ∀ {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]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.LaxMonoidal] [inst_6 : a.IsMonoidal],
  a.mapAddMon =
    {
      unit :=
        CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapAddMonIdIso.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapAddMonNatTrans a.unit)
            CategoryTheory.Functor.mapAddMonCompIso.hom),
      counit :=
        CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapAddMonCompIso.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapAddMonNatTrans a.counit)
            CategoryTheory.Functor.mapAddMonIdIso.hom),
      left_triangle_components := ⋯, right_triangle_components := ⋯ }
-- Mathlib.Topology.Order.OrderClosed
disjoint_nhds_atBot_iff : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {a : α},
  Disjoint (nhds a) Filter.atBot ↔ ¬IsBot a
-- Std.Async.Basic
Std.Async.MaybeTask.ofTask.inj : ∀ {α : Type} {a a_1 : Task α}, Std.Async.MaybeTask.ofTask a = Std.Async.MaybeTask.ofTask a_1 → a = a_1
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Submodule.linearEquiv_det_reflection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : FiniteDimensional 𝕜 ↥K],
  LinearEquiv.det K.reflection.toLinearEquiv = (-1) ^ Module.finrank 𝕜 ↥Kᗮ
-- Mathlib.Topology.Sets.Closeds
/-- The complement of an open set as a closed set.  -/
TopologicalSpace.Opens.compl : {α : Type u_2} → [inst : TopologicalSpace α] → TopologicalSpace.Opens α → TopologicalSpace.Closeds α
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.filter.go.eq_1 : ∀ {α : Type u} {β : α → Type v} (f : (a : α) → β a → Bool) (acc : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.filter.go✝ f acc Std.DHashMap.Internal.AssocList.nil = acc
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pushforward_singleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Presieve.pushforward g (CategoryTheory.Presieve.singleton f) =
    CategoryTheory.Presieve.singleton (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Group.Subgroup.Basic
div_mem_comm_iff : ∀ {G : Type u_1} [inst : Group G] {S : Type u_6} {H : S} [inst_1 : SetLike S G] [SubgroupClass S G] {a b : G},
  a / b ∈ H ↔ b / a ∈ H
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.reindex_toPresentation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ),
  (P.reindex e f).toPresentation = P.reindex e f
-- Mathlib.Data.Set.Restrict
Set.domRestrict_extend_compl_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (g' : β → γ),
  (Set.range f)ᶜ.domRestrict (Function.extend f g g') = g' ∘ Subtype.val
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.AsSmall.down.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.AsSmall.down = { obj := fun X => X.down, map := fun {X Y} f => f.down, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.CategoryTheory.Enriched.Basic
/-- We verify that an enriched functor between `Type v` enriched categories
is just the same thing as an honest functor.
 -/
CategoryTheory.enrichedFunctorTypeEquivFunctor : {C : Type u₁} →
  [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] →
    {D : Type u₂} →
      [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] →
        CategoryTheory.EnrichedFunctor (Type v) C D ≃ CategoryTheory.Functor C D
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropPrefix?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.LawfulForwardPattern pat]
  {s : String.Slice}, s.dropPrefix? pat = none ↔ s.startsWith pat = false
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The name length of the used lemma.  -/
Mathlib.Tactic.ClickSuggestions.RwKey.nameLength : Mathlib.Tactic.ClickSuggestions.RwKey → ℕ
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_xor : ∀ (a b : ISize) (h : System.Platform.numBits = 32), (a ^^^ b).toBitVec32 h = a.toBitVec32 h ^^^ b.toBitVec32 h
-- Mathlib.Algebra.Algebra.Unitization
/-- The identity map between `Unitization R A` and `R × A` as a `LinearEquiv`.  -/
Unitization.linearEquiv : (S : Type u_2) →
  (R : Type u_3) →
    (A : Type u_4) →
      [inst : Semiring S] →
        [inst_1 : AddCommMonoid R] →
          [inst_2 : AddCommMonoid A] → [inst_3 : Module S R] → [inst_4 : Module S A] → Unitization R A ≃ₗ[S] R × A
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.addRight_symm : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd Gᵃᵒᵖ G] (x : G),
  (IsometryEquiv.addRight x).symm = IsometryEquiv.addRight (-x)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsMulRightInvariantForallVolumeOfMeasurableMulOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {G : ι → Type u_4} [inst_1 : (i : ι) → Group (G i)]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableMul (G i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [∀ (i : ι), MeasureTheory.volume.IsMulRightInvariant],
  MeasureTheory.volume.IsMulRightInvariant
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.lift_f_fst_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cocycle K F 1) (β : CochainComplex.HomComplex.Cochain K G 0)
  (eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0) (p q : ℤ)
  (hpq : p + 1 = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.lift φ α β eq).f p)
      ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) =
    (↑α).v p q hpq
-- Mathlib.LinearAlgebra.Basis.Defs
/-- `repr` is the linear equivalence sending a vector `x` to its coordinates:
the `c`s such that `x = ∑ i, c i`.  -/
Module.Basis.repr : {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_6} →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Module.Basis ι R M → M ≃ₗ[R] ι →₀ R
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.snd_decompLinearIsometryEquiv : ∀ (𝕜 : Type u_1) (R : Type u_2) (V : Type u_3) (W : Type u_4) [inst : SeminormedAddCommGroup V]
  [inst_1 : SeminormedAddCommGroup W] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : Ring R] [inst_6 : Module R W] [inst_7 : ContinuousConstSMul R W]
  [inst_8 : SMulCommClass 𝕜 R W] (f : V →ᴬ[𝕜] W),
  ((ContinuousAffineMap.decompLinearIsometryEquiv 𝕜 R V W) f).2 = f.contLinear
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measure_ne_zero_iff_nonempty_of_isAddLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular],
  μ ≠ 0 → ∀ {s : Set G}, IsOpen s → (μ s ≠ 0 ↔ s.Nonempty)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.RevMatchesAt.exists_isLongestRevMatchAt : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt pat pos →
    ∃ startPos, String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos pos
-- Mathlib.CategoryTheory.Galois.Examples
/-- If `X` is a connected `G`-set and `x` is an element of `X`, `X` is isomorphic
to the quotient of `G` by the stabilizer of `x` as `G`-sets.  -/
CategoryTheory.FintypeCat.isoQuotientStabilizerOfIsConnected : {G : Type u} →
  [inst : Group G] →
    (X : Action FintypeCat G) →
      [CategoryTheory.PreGaloisCategory.IsConnected X] →
        (x : X.V.obj) →
          [inst_2 : Fintype (G ⧸ MulAction.stabilizer G x)] →
            X ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `mvfderiv_add` -/
mvfderiv_fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {g g' : M → F} {x : M},
  MDiffAt g x → MDiffAt g' x → (d% fun i => g i + g' i) x = d% g x + d% g' x