mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addHaarProduct.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (K₀ : Set G),
  MeasureTheory.Measure.haar.addHaarProduct K₀ =
    Set.univ.pi fun K => Set.Icc 0 ↑(MeasureTheory.Measure.haar.addIndex (↑K) K₀)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirectedHomBase_app : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] (i : 𝒰.I₀),
  𝒰.functorOfLocallyDirectedHomBase.app i = 𝒰.f i
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
/-- We construct the limit object of a functor `F : J ⥤ Mon C` given a limit cone `c` of
`F ⋙ forget C`.
 -/
CategoryTheory.Mon.limit : {J : Type w} →
  [inst : CategoryTheory.Category.{v_1, w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) →
            (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) →
              CategoryTheory.Limits.IsLimit c → CategoryTheory.Mon C
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_filter!_key : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] {f : α → Bool} {k : α},
  t.WF → (Std.DTreeMap.Internal.Impl.filter! (fun k x => f k) t).getKey! k = (Option.filter f (t.getKey? k)).get!
-- Lean.Meta.Tactic.Grind.Types
/-- Active theorems that we have not performed any round of ematching yet.  -/
Lean.Meta.Grind.EMatch.State.newThms : Lean.Meta.Grind.EMatch.State → Lean.PArray Lean.Meta.Grind.EMatchTheorem
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_Ici_sub_Ici : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  MeasureTheory.IntegrableOn f (Set.Ici a) μ →
    a ≤ b → ∫ (x : ℝ) in Set.Ici a, f x ∂μ - ∫ (x : ℝ) in Set.Ici b, f x ∂μ = ∫ (x : ℝ) in Set.Ico a b, f x ∂μ
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- See `multipliable_congr_cofinite` for a version allowing the functions to
disagree on a finite set.  -/
multipliable_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β}, (∀ (b : β), f b = g b) → (Multipliable f L ↔ Multipliable g L)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The set of good products.  -/
Profinite.NobelingProof.GoodProducts : {I : Type u} → Set (I → Bool) → [inst : LinearOrder I] → Set (Profinite.NobelingProof.Products I)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  t.contains a = false → t[a]? = none
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.BoundedAtFilter.smul : ∀ {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedAddCommGroup β]
  [inst_2 : Module 𝕜 β] [IsBoundedSMul 𝕜 β] {l : Filter α} {f : α → β} (c : 𝕜),
  l.BoundedAtFilter f → l.BoundedAtFilter (c • f)
-- Lean.Widget.Commands
_private.Lean.Widget.Commands.0.Lean.Widget.elabWidgetInstanceSpecAux : Lean.Ident → Lean.Term → Lean.Elab.TermElabM Lean.Expr
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_le_length_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  l.length ≤ (Std.Internal.List.insertEntryIfNew k v l).length
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translate_pow : ∀ (x : ℝ) (n : ℕ),
  CircleDeg1Lift.translate (Multiplicative.ofAdd x) ^ n = CircleDeg1Lift.translate (Multiplicative.ofAdd (↑n * x))
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y)
  (X_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (X_2 : (TopologicalSpace.Opens ↑Y)ᵒᵖ),
  ((TopCat.Presheaf.presheafEquivOfIso C H).counitIso.hom.app X_1).app X_2 = X_1.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.Order.InitialSeg
PrincipalSeg.lt_top : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) (a : α),
  s (f.toRelEmbedding a) f.top
-- Mathlib.Algebra.Group.Action.Pi
Pi.vadd'.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → VAdd (α i) (β i)],
  Pi.vadd' = { vadd := fun s x i => s i +ᵥ x i }
-- Init.Data.String.Basic
String.firstDiffPos.loop.eq_def : ∀ (a b : String) (stopPos i : String.Pos.Raw),
  String.firstDiffPos.loop a b stopPos i =
    if h : i < stopPos then
      if (String.Pos.Raw.get a i != String.Pos.Raw.get b i) = true then i
      else
        have this := ⋯;
        String.firstDiffPos.loop a b stopPos (String.Pos.Raw.next a i)
    else i
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.Context.elimInfo : Lean.Elab.Tactic.ElimApp.Context✝ → Lean.Meta.ElimInfo
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- Applying a `ContinuousAffineMap` commutes with `AffineMap.lineMap`.  -/
ContinuousAffineMap.apply_lineMap : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (f : P →ᴬ[R] Q) (p₀ p₁ : P) (c : R),
  f ((AffineMap.lineMap p₀ p₁) c) = (AffineMap.lineMap (f p₀) (f p₁)) c
-- Aesop.Frontend.Extension.Init
Aesop.DeclaredRuleSets.mk.sizeOf_spec : ∀ (ruleSets : Std.HashMap Aesop.RuleSetName (Aesop.RuleSetExtension × Lean.Name × Lean.Name))
  (defaultRuleSets : Std.HashSet Aesop.RuleSetName),
  sizeOf { ruleSets := ruleSets, defaultRuleSets := defaultRuleSets } = 1 + sizeOf ruleSets + sizeOf defaultRuleSets
-- Lean.Elab.DefView
Lean.Elab.instBEqDefKind : BEq Lean.Elab.DefKind
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The action of an object `c : C` on a map `f : d ⟶ d'` in `D`.
If we are to consider the action as a functor `Α : C ⥤ D ⥤ D`,
this is `(Α.obj c).map f`. This is denoted `c ⊴ₗ f`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight : {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} →
        {inst_2 : CategoryTheory.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D] →
            (c : C) →
              {d d' : D} →
                (d ⟶ d') →
                  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d ⟶
                    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d')
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.shrink_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (i : ↑E.presieve₀.uncurry), E.shrink.X i = (↑i).fst
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
/-- If `s` is a finite subset of `I`, then the good products span.  -/
Profinite.NobelingProof.GoodProducts.spanFin : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I) [WellFoundedLT I],
  ⊤ ≤
    Submodule.span ℤ
      (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => x ∈ s)))
-- Mathlib.Logic.Equiv.List
Encodable.encode_list_cons : ∀ {α : Type u_1} [inst : Encodable α] (a : α) (l : List α),
  Encodable.encode (a :: l) = (Nat.pair (Encodable.encode a) (Encodable.encode l)).succ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.addMonObjObj.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} [inst_4 : F.LaxMonoidal] (X : C) [inst_5 : CategoryTheory.AddMonObj X],
  CategoryTheory.Functor.addMonObjObj X =
    {
      zero :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F)
          (F.map CategoryTheory.AddMonObj.zero),
      add :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X)
          (F.map CategoryTheory.AddMonObj.add),
      zero_add := ⋯, add_zero := ⋯, add_assoc := ⋯ }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_eq_some_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  (he : t ≠ ∅), t.maxKey? = some (t.maxKey he)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k} {fallback : α},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKeyD fallback =
    t.maxKey?.elim k fun k' => if (compare k' k).isLE = true then k else k'
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuousWithinAt.congr_of_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → Set β} {s : Set α}
  {a : α}, LowerHemicontinuousWithinAt f s a → a ∈ s → f =ᶠ[nhdsWithin a s] g → LowerHemicontinuousWithinAt g s a
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.markAsTrailingParser : ℕ → Lean.Elab.Term.ToParserDescrM Unit
-- Mathlib.Algebra.Order.Hom.Basic
NonarchimedeanHomClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : Add α] [inst_1 : LinearOrder β]
  [inst_2 : FunLike F α β], (∀ (f : F) (a b : α), f (a + b) ≤ max (f a) (f b)) → NonarchimedeanHomClass F α β
-- Mathlib.Data.Countable.Defs
Uncountable.of_equiv : ∀ {β : Sort v} (α : Sort u_1) [Uncountable α] (e : α ≃ β), Uncountable β
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The underlying morphism of the inverse component of the associator isomorphism.  -/
Bimod.AssociatorBimod.inv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        [inst_3 :
            ∀ (X : C),
              CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                (CategoryTheory.MonoidalCategory.tensorLeft X)] →
          [inst_4 :
              ∀ (X : C),
                CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                  (CategoryTheory.MonoidalCategory.tensorRight X)] →
            {R S T U : CategoryTheory.Mon C} →
              (P : Bimod R S) →
                (Q : Bimod S T) →
                  (L : Bimod T U) → (P.tensorBimod (Q.tensorBimod L)).X ⟶ ((P.tensorBimod Q).tensorBimod L).X
-- Mathlib.Analysis.Normed.Lp.Finsupp
/-- The L^1 extended metric on `ι`-many copies of a metric space `X`  -/
Finsupp.instPseudoEMetricSpaceWithLpOfNNReal : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : Zero X] → {p : NNReal} → [Fact (1 ≤ p)] → [PseudoEMetricSpace X] → PseudoEMetricSpace (WithLp (↑p) (ι →₀ X))
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- **Alias** of `CovariantDerivative.finiteAffineCombination`.

---

A finite affine combination of covariant derivatives as a covariant derivative.  -/
CovariantDerivative.finite_affine_combination : {𝕜 : 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_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            {ι : Type u_7} →
                                              {s : Finset ι} →
                                                (ι → CovariantDerivative I F V) →
                                                  {f : ι → M → 𝕜} → ∑ i ∈ s, f i = 1 → CovariantDerivative I F V
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.exists_frequently_lt_of_liminf_ne_top' : ∀ {ι : Type u_4} {l : Filter ι} {x : ι → ℝ},
  Filter.liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤ → ∃ R, ∃ᶠ (n : ι) in l, R < x n
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.finsetProd : ∀ {α : Type u_1} {ι : Type u_2} {β : Type u_3} [inst : NormedField β] {l : Filter α} {s : Finset ι} {f g : ι → α → β},
  (∀ i ∈ s, Asymptotics.IsEquivalent l (f i) (g i)) →
    Asymptotics.IsEquivalent l (fun x => ∏ i ∈ s, f i x) fun x => ∏ i ∈ s, g i x
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.coe_zero : ∀ {M : Type u_1} [inst : Monoid M] {A : Type u_4} [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A], ⇑1 = id
-- Mathlib.Algebra.Order.Ring.Nat
Nat.instIsStrictOrderedRing : IsStrictOrderedRing ℕ
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_dual : ∀ {α : Type u_1} {P : α → Prop} {t : Ordnode α}, Ordnode.All P t.dual ↔ Ordnode.All P t
-- Mathlib.Data.Stream.Init
Stream'.tail_inits : ∀ {α : Type u} (s : Stream' α), s.inits.tail = Stream'.initsCore [s.head, s.tail.head] s.tail.tail
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieModule.nontrivial_of_isIrreducible : ∀ (R : Type u_1) (L : Type u_2) (M : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [LieModule.IsIrreducible R L M], Nontrivial M
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of the forward direction of `LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff`.

---

`ker f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = f ∘ₗ T`,
for idempotent `f`.  -/
LinearMap.IsIdempotentElem.conj_eq_of_ker_mem_invtSubmodule : ∀ {E : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T f : E →ₗ[R] E},
  IsIdempotentElem f → f.ker ∈ Module.End.invtSubmodule T → f ∘ₗ T ∘ₗ f = f ∘ₗ T
-- Std.Time.Duration
/-- Subtracts a `Second.Offset` from a `Duration`
 -/
Std.Time.Duration.subSeconds : Std.Time.Duration → Std.Time.Second.Offset → Std.Time.Duration
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : a ≤ b)
  (X : C) {Z : C} (h : (t.eTruncGE.obj b).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))
      (CategoryTheory.CategoryStruct.comp ((t.eTruncGEIsoGEGE a b hab).inv.app X) h) =
    h
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E / F` is a separable extension, `E` is perfect, then `F` is also perfect.  -/
perfectField_of_isSeparable_of_perfectField_top : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E]
  [PerfectField E], PerfectField F
-- Mathlib.MeasureTheory.Integral.MeanValue
/-- **First mean value theorem for set integrals (pointwise nonnegativity).**
Let `s` be a connected measurable set. If `f` is continuous on `s`, `g` is integrable on `s`,
`f * g` is integrable on `s`, and `g` is nonnegative on `s`, then
`∃ c ∈ s, (∫ x in s, f x * g x ∂μ) = f c * (∫ x in s, g x ∂μ)`  -/
exists_eq_const_mul_setIntegral_of_nonneg : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {s : Set α} {f g : α → ℝ}
  {μ : MeasureTheory.Measure α},
  IsConnected s →
    MeasurableSet s →
      ContinuousOn f s →
        MeasureTheory.IntegrableOn g s μ →
          MeasureTheory.IntegrableOn (fun x => f x * g x) s μ →
            (∀ x ∈ s, 0 ≤ g x) → ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
/-- Lift an element that maps to 0  -/
Submodule.exists_fg_of_baseChange_eq_zero : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S]
  [inst_2 : Algebra R S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid N]
  [inst_6 : Module R N] (f : M →ₗ[R] N) {t : TensorProduct R S M},
  (LinearMap.baseChange S f) t = 0 →
    ∃ A, ∃ (_ : A.FG), ∃ u, (LinearMap.baseChange (↥A) f) u = 0 ∧ (LinearMap.rTensor M A.val.toLinearMap) u = t
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preservesHomology : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [F.PreservesHomology], h.IsPreservedBy F
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.le : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {F C : PointedCone R M}, F.IsFaceOf C → F ≤ C
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The finite-quotient diagram viewed in `ProfiniteGrp`.  -/
ProfiniteGrp.ProfiniteCompletion.diagram : (G : GrpCat) → CategoryTheory.Functor (FiniteIndexNormalSubgroup ↑G) ProfiniteGrp.{u}
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.timeout : {β : Type} → Std.Http.Server.Connection.Recv✝ β
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  Q 2 ≠ 0 →
    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 → W'.dblXYZ P = ![W'.dblU P ^ 2, W'.dblU P ^ 3, 0]
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.coe_prodUnique : ∀ (X : Type u_1) (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Unique Y],
  ⇑(Homeomorph.prodUnique X Y) = Prod.fst
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop_iSup : ∀ {ι : Sort u_1} {G : Type u_2} [inst : AddGroup G] (S : ι → AddSubgroup Gᵃᵒᵖ), (iSup S).unop = ⨆ i, (S i).unop
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.apply_eq_true_of_revSkipWhile_le_bool : ∀ {p : Char → Bool} {s : String.Slice} {pos pos' : s.Pos} (h₁ : pos' < pos),
  pos.revSkipWhile p ≤ pos' → p (pos'.get ⋯) = true
-- Mathlib.Order.SymmDiff
le_bihimp_inf_left : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), bihimp a b ⊓ a ≤ b
-- Init.Data.String.Substring
/-- Checks whether the substring can be interpreted as the decimal representation of a natural number.

A substring can be interpreted as a decimal natural number if it is not empty and all the characters
in it are digits. Underscores ({lit}`_`) are allowed as digit separators for readability, but cannot appear
at the start, at the end, or consecutively.

Use `Substring.toNat?` to convert such a substring to a natural number.
 -/
Substring.Raw.isNat : Substring.Raw → Bool
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instNonUnitalNonAssocSemiring : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] → [NonUnitalNonAssocSemiring Y] → NonUnitalNonAssocSemiring (LocallyConstant X Y)
-- Mathlib.GroupTheory.DivisibleHull
/-- Backward direction of `archimedeanClassOrderIso`.  -/
_private.Mathlib.GroupTheory.DivisibleHull.0.DivisibleHull.archimedeanClassOrderHomInv : (M : Type u_2) →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] → ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass M
-- Mathlib.Algebra.GroupWithZero.Action.Defs
smul_eq_zero_of_right : ∀ {M : Type u_1} {A : Type u_7} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M) {b : A}, b = 0 → a • b = 0
-- Init.Data.Vector.Monadic
_private.Init.Data.Vector.Monadic.0.Vector.mapM.go.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] (f : α → m β) (xs : Vector α n)
  (k : ℕ) (h : k ≤ n) (acc : Vector β k),
  Vector.mapM.go✝ f xs k h acc =
    if h' : k < n then do
      let __do_lift ← f xs[k]
      Vector.mapM.go✝ f xs (k + 1) ⋯ (acc.push __do_lift)
    else pure (Vector.cast ⋯ acc)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
/-- **Alias** of the reverse direction of `Filter.principal_isMeasurablyGenerated_iff`. -/
MeasurableSet.principal_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, MeasurableSet s → (Filter.principal s).IsMeasurablyGenerated
-- Mathlib.Dynamics.Flow
Flow.map_zero : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (ϕ : Flow τ α), ϕ.toFun 0 = id
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_eq_of_isHomogeneous : ∀ {R : Type u_1} [inst : CommSemiring R] {p : Polynomial R} {n : ℕ} {q : MvPolynomial (Fin 2) R},
  q.IsHomogeneous n → (MvPolynomial.aeval ![Polynomial.X, 1]) q = p → p.homogenize n = q
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Connected.preconnected : ∀ {V : Type u} {G : SimpleGraph V}, G.Connected → G.Preconnected
-- Mathlib.LinearAlgebra.Finsupp.LSum
LinearMap.splittingOfFinsuppSurjective_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_4}
  (f : M →ₗ[R] α →₀ R) (s : Function.Surjective ⇑f), Function.Injective ⇑(f.splittingOfFinsuppSurjective s)
-- Mathlib.Order.Antisymmetrization
/-- The antisymmetrization relation `AntisymmRel r` is defined so that
`AntisymmRel r a b ↔ r a b ∧ r b a`.  -/
AntisymmRel : {α : Type u_1} → (α → α → Prop) → α → α → Prop
-- Mathlib.Computability.Partrec
Computable.fst : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Computable Prod.fst
-- Mathlib.Data.PEquiv
PEquiv.trans_bot : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β), f.trans ⊥ = ⊥
-- Mathlib.ModelTheory.Definability
/-- The 2-dimensional diagonal is definable independent from parameters.  -/
Set.Definable.diagonal : ∀ {M : Type w} (L : FirstOrder.Language) [inst : L.Structure M] (A : Set M), A.Definable₂ L (Set.diagonal M)
-- Mathlib.GroupTheory.GroupAction.Pointwise
IsUnit.preimage_smul_set : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : Monoid M] [inst_1 : MulAction M α]
  [inst_2 : MulAction M β] [inst_3 : FunLike F α β] [MulActionHomClass F M α β] (f : F) {c : M},
  IsUnit c → ∀ (t : Set β), ⇑f ⁻¹' (c • t) = c • ⇑f ⁻¹' t