mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Find
Vector.findFinIdx?_append : ∀ {α : Type u_1} {n₁ n₂ : ℕ} {xs : Vector α n₁} {ys : Vector α n₂} {p : α → Bool},
  Vector.findFinIdx? p (xs ++ ys) =
    (Option.map (Fin.castLE ⋯) (Vector.findFinIdx? p xs)).or (Option.map (Fin.natAdd n₁) (Vector.findFinIdx? p ys))
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.inl_rel'_inl_iff : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₁ y₁ : X₁),
  CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl x₁) (Sum.inl y₁) ↔
    x₁ = y₁ ∨
      ∃ x₀ y₀,
        ∃ (_ : (CategoryTheory.ConcreteCategory.hom g) x₀ = (CategoryTheory.ConcreteCategory.hom g) y₀),
          x₁ = (CategoryTheory.ConcreteCategory.hom f) x₀ ∧ y₁ = (CategoryTheory.ConcreteCategory.hom f) y₀
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supportedEquivFinsupp_symm_apply_coe : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set α) [inst_3 : DecidablePred fun x => x ∈ s] (f : ↑s →₀ M),
  ↑((Finsupp.supportedEquivFinsupp s).symm f) = f.extendDomain
-- Init.Tactics
/-- `show_term tac` runs `tac`, then prints the generated term in the form
"exact X Y Z" or "refine X ?_ Z" (prefixed by `expose_names` if necessary)
if there are remaining subgoals.

(For some tactics, the printed term will not be human readable.)
 -/
Lean.Parser.Tactic.showTerm : Lean.ParserDescr
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuousWithinAt.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace β] {f : α → Set β} {s : Set α} {g : γ → α} {x : γ} {t : Set γ},
  LowerHemicontinuousWithinAt f s (g x) →
    ContinuousWithinAt g t x → Set.MapsTo g t s → LowerHemicontinuousWithinAt (f ∘ g) t x
-- Init.Data.List.Basic
List.isSuffixOf.eq_1 : ∀ {α : Type u} [inst : BEq α] (l₁ l₂ : List α), l₁.isSuffixOf l₂ = l₁.reverse.isPrefixOf l₂.reverse
-- Mathlib.Algebra.Algebra.Unitization
Unitization.linearEquiv_symm_apply : ∀ (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] (a : R × A), (Unitization.linearEquiv S R A).symm a = Unitization.mk a
-- Mathlib.Topology.Algebra.UniformMulAction
UniformContinuousConstVAdd.instContinuousConstVAdd : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : VAdd M X] [UniformContinuousConstVAdd M X],
  ContinuousConstVAdd M X
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.opEquiv_inverse_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.WithTerminal Cᵒᵖ),
  (CategoryTheory.WithInitial.opEquiv C).inverse.obj x =
    match x with
    | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
    | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_inverse_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  {Y X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T'} (f : Y ⟶ X),
  ((CategoryTheory.StructuredArrow.mapNatIso i).inverse.map f).left = CategoryTheory.CategoryStruct.id Y.left
-- Lean.Elab.ConfigEval.Basic
/-- Applies the configuration `cfg` to `init` using `eval.set`.
If `logExceptions` is true, then catches and logs exceptions.

The `onErr` callback is used for invalid configuration syntax.

Note: this should be run from within `runConfigElab`.
 -/
Lean.Elab.ConfigEval.EvalConfigItem.setConfig : {α : Type} →
  Lean.Elab.ConfigEval.EvalConfigItem α →
    α →
      Lean.Syntax →
        (optParam (α → Lean.Syntax → Lean.Elab.TermElabM α) fun cfg cfgItem =>
            Lean.Elab.ConfigEval.EvalConfigItem.defaultOnErr cfg cfgItem) →
          optParam Bool false → Lean.Elab.TermElabM α
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.type₁_ne_type₂ : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s t : h.ι), h.type₁ s ≠ h.type₂ t
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.liftOn_condition_of_liftOn'_condition : ∀ {K : Type u} [inst : CommRing K] {P : Sort v} {f : Polynomial K → Polynomial K → P},
  (∀ {p q a : Polynomial K}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q) →
    ∀ ⦃p q p' q' : Polynomial K⦄, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'
-- Init.Data.SInt.Lemmas
Int64.le_total : ∀ (a b : Int64), a ≤ b ∨ b ≤ a
-- Init.Data.Sum.Basic
/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
`α ⊕ β` and `γ ⊕ δ`.  -/
Sum.LiftRel : {α : Type u_1} →
  {γ : Type u_2} → {β : Type u_3} → {δ : Type u_4} → (α → γ → Prop) → (β → δ → Prop) → α ⊕ β → γ ⊕ δ → Prop
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_inv : ∀ {α : Type u_1} [inst : Inv α] (a : αᵒᵈ), OrderDual.ofDual a⁻¹ = (OrderDual.ofDual a)⁻¹
-- Init.Internal.Order.While
_private.Init.Internal.Order.While.0.repeatM.body.match_1.eq_1 : ∀ {α β : Type u_1} (motive : α ⊕ β → Sort u_2) (a : α) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (b : β) → motive (Sum.inr b)),
  (match Sum.inl a with
    | Sum.inl a => h_1 a
    | Sum.inr b => h_2 b) =
    h_1 a
-- Mathlib.Analysis.Normed.Group.Basic
nndist_zero_right : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), nndist a 0 = ‖a‖₊
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.pre_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : D) (X : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)),
  ((CategoryTheory.CostructuredArrow.pre F G S).obj X).right = X.right
-- Mathlib.Analysis.InnerProductSpace.Defs
_private.Mathlib.Analysis.InnerProductSpace.Defs.0.InnerProductSpace.Core.termNormSqF_1 : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_mono_on_ae : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f g : X → E}
  {s : Set X} [ClosedIciTopology E],
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.IntegrableOn g s μ →
      MeasurableSet s → (∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x) → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepSets_of_condIndepSets_of_le_left : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s₁ s₂ s₃ : Set (Set Ω)},
  ProbabilityTheory.CondIndepSets m' hm' s₁ s₂ μ → s₃ ⊆ s₁ → ProbabilityTheory.CondIndepSets m' hm' s₃ s₂ μ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.num : ℤ → Lean.Grind.CommRing.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.inl : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → (self : CategoryTheory.Limits.BinaryBicone P Q) → P ⟶ self.pt
-- Mathlib.LinearAlgebra.Contraction
/-- The natural right-handed pairing between a module and its dual.  -/
contractRight : (R : Type u_2) →
  (M : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → TensorProduct R M (Module.Dual R M) →ₗ[R] R
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ},
  t.getKey? k = some k' → (Std.TreeMap.map f t).getD k fallback = (Option.map (f k') t[k]?).getD fallback
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcUnits.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {p p_1 : A → Prop} (e_p : p = p_1) [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A]
  [inst_6 : Ring A] [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p]
  [inst_10 : ContinuousInv₀ R] (f f_1 : R → R) (e_f : f = f_1) (a a_1 : A) (e_a : a = a_1)
  (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (hf : ContinuousOn f (spectrum R a)) (ha : p a),
  cfcUnits f a hf' hf ha = cfcUnits f_1 a_1 ⋯ ⋯ ⋯
-- Mathlib.Tactic.FunProp.Core
/-- Synthesize instance of type `type` and
1. assign it to `x` if `x` is meta variable
2. check it is equal to `x`  -/
Mathlib.Meta.FunProp.synthesizeInstance : Mathlib.Meta.FunProp.Origin → Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- If `f` is a positive radius tending to zero, then the sets of pairs with distance less than
`f i` form a basis of the uniformity.  -/
Metric.mk_uniformity_basis_of_tendsto : ∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ} {l : Filter β} [l.NeBot],
  (∀ (i : β), p i → 0 < f i) →
    (∀ᶠ (i : β) in l, p i) → Filter.Tendsto f l (nhds 0) → (uniformity α).HasBasis p fun i => {x | dist x.1 x.2 < f i}
-- Mathlib.LinearAlgebra.Dual.BaseChange
/-- `LinearMap.baseChange` for `Module.Dual`.  -/
Module.Dual.baseChange : {R : Type u_1} →
  [inst : CommSemiring R] →
    {V : Type u_2} →
      [inst_1 : AddCommMonoid V] →
        [inst_2 : Module R V] →
          (A : Type u_4) →
            [inst_3 : CommSemiring A] →
              [inst_4 : Algebra R A] → Module.Dual R V →ₗ[R] Module.Dual A (TensorProduct R A V)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.top_ne_zero : ∀ {α : Type u} [inst : Zero α], ⊤ ≠ 0
-- Mathlib.Analysis.SpecialFunctions.Artanh
/-- `artanh` is the left inverse of `tanh`.  -/
Real.artanh_tanh : ∀ (x : ℝ), Real.artanh (Real.tanh x) = x
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sOppSide_vadd_left_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P} {v : V}, v ∈ s.direction → (s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Raised.right : ∀ {α : Type u_1} {l : Ordnode α} {x₁ x₂ : α} {r₁ r₂ : Ordnode α},
  Ordnode.Raised r₁.size r₂.size → Ordnode.Raised (l.node' x₁ r₁).size (l.node' x₂ r₂).size
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousLinearMap.uncurryLeft_apply : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G)
  (m : (i : Fin n.succ) → Ei i), f.uncurryLeft m = (f (m 0)) (Fin.tail m)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_radical : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R), PrimeSpectrum.zeroLocus ↑I.radical = PrimeSpectrum.zeroLocus ↑I
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_11 : HSub Std.Time.Millisecond.Offset Std.Time.Week.Offset Std.Time.Millisecond.Offset
-- Mathlib.Data.Quot
/-- A version of `Quotient.recOnSubsingleton` taking `{s₁ : Setoid α}` as an implicit argument
instead of an instance argument.  -/
Quotient.recOnSubsingleton' : {α : Sort u_1} →
  {s₁ : Setoid α} →
    {φ : Quotient s₁ → Sort u_5} →
      [∀ (a : α), Subsingleton (φ ⟦a⟧)] → (q : Quotient s₁) → ((a : α) → φ (Quotient.mk'' a)) → φ q
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (f : EsakiaHom α β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Order.OrderIsoNat
/-- A linear order that is well-founded in both directions is finite.  -/
Finite.of_wellFoundedLT_wellFoundedGT : ∀ (α : Type u_2) [inst : LinearOrder α] [WellFoundedLT α] [WellFoundedGT α], Finite α
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_le_coeSubmodule : ∀ {R : Type u_3} [inst : CommRing R] {M : Submonoid R} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S],
  M ≤ nonZeroDivisors R → ∀ {I J : Ideal R}, IsLocalization.coeSubmodule S I ≤ IsLocalization.coeSubmodule S J ↔ I ≤ J
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.instOrderTop : {X : TopCat} → (x : ↑X) → OrderTop (TopologicalSpace.OpenNhds x)
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
mem_perfectClosure_iff_pow_mem : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [ExpChar F q] {x : E},
  x ∈ perfectClosure F E ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry.eq_2 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l r r_1 : Std.DTreeMap.Internal.Impl α β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
      false),
  (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minEntry h =
    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntry ⋯
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.equiv_iff_toList_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ ↔ t₁.toList = t₂.toList
-- Mathlib.RingTheory.Idempotents
AlgEquiv.prodQuotientOfIsIdempotentElem_apply : ∀ (R : Type u_1) [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S] {e f : S}
  (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (hef₁ : e + f = 1) (hef₂ : e * f = 0) (a : S),
  (AlgEquiv.prodQuotientOfIsIdempotentElem R he hf hef₁ hef₂) a =
    ((Ideal.Quotient.mk (Ideal.span {e})) a, (Ideal.Quotient.mk (Ideal.span {f})) a)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The identity morphisms `𝟙 _` are exponentiable.  -/
CategoryTheory.ExponentiableMorphism.id : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : C) →
      [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id I)] →
        CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.id I)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeffs_monomial : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) {c : R}, c ≠ 0 → ((Polynomial.monomial n) c).coeffs = {c}
-- Init.Tactics
/-- `mexact` is like `exact`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (Q : SPred σs) : Q ⊢ₛ Q := by
  mstart
  mintro HQ
  mexact HQ
```
 -/
Lean.Parser.Tactic.mexactMacro : Lean.ParserDescr
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.snd : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E × F} {g : α → G}, f =O[𝕜; l] g → (fun x => (f x).2) =O[𝕜; l] g
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableInf.measurable_inf_const : ∀ {M : Type u_1} {inst : MeasurableSpace M} {inst_1 : Min M} [self : MeasurableInf M] (c : M), Measurable fun x => x ⊓ c
-- Mathlib.GroupTheory.Coset.Basic
AddMonoidHom.fiberEquivKerOfSurjective.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {H : Type u_2} [inst_1 : AddGroup H] {f : α →+ H} (hf : Function.Surjective ⇑f)
  (h : H), AddMonoidHom.fiberEquivKerOfSurjective hf h = ⋯ ▸ f.fiberEquivKer ⋯.choose
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.instSub : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        [inst : Ring k] →
          [inst_1 : AddCommGroup V1] →
            [inst_2 : Module k V1] →
              [inst_3 : AddTorsor V1 P1] → [inst_4 : AddCommGroup V2] → [inst_5 : Module k V2] → Sub (P1 →ᵃ[k] V2)
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.Section.add_neg_mem_range_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} (σ σ' : S.Section) (g : G), σ g + -σ' g ∈ S.inl.range
-- Mathlib.Data.Semiquot
Semiquot.mem_blur' : ∀ {α : Type u_1} (q : Semiquot α) {s : Set α} (h : q.s ⊆ s) {a : α}, a ∈ q.blur' h ↔ a ∈ s
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.rightHomologyData.cokernelCofork.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j : ι}
  {i' j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i')
  (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)),
  HomologicalComplex.extend.rightHomologyData.cokernelCofork K e hj' hi hi' cocone =
    CategoryTheory.Limits.CokernelCofork.ofπ
      (CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom (CategoryTheory.Limits.Cofork.π cocone)) ⋯
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.det_of_isUpperTriangular : ∀ {m : Type u_3} {R : Type v} {M : Matrix m m R} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : LinearOrder m], M.IsUpperTriangular → M.det = ∏ i, M i i
-- Aesop.Script.ScriptM
Aesop.ScriptT.run : {m : Type → Type} →
  {α : Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Aesop.ScriptT m α → m (α × Array Aesop.Script.LazyStep)
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃_of_isZero : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ : ι}
  (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₁ n₂ n₃ : ℤ),
  autoParam (CategoryTheory.Limits.IsZero ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₄)))
      CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃_of_isZero._auto_1 →
    ∀ (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃_of_isZero._auto_3)
      (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃_of_isZero._auto_5),
      CategoryTheory.IsIso
        (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)
-- Std.Sync.SharedMutex
_private.Std.Sync.SharedMutex.0.Std.SharedMutex.mk : {α : Type} → IO.Ref α → Std.BaseSharedMutex → Std.SharedMutex α
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedDep.mk : Lean.Name → Lean.TSyntax `ident → Lean.TSyntax `term → Bool → WantedDep✝
-- Mathlib.Data.Seq.Defs
/-- `Pairwise R s` means that all the elements with earlier indices are
`R`-related to all the elements with later indices.
```
Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3
```
For example if `R = (· ≠ ·)` then it asserts `s` has no duplicates,
and if `R = (· < ·)` then it asserts that `s` is (strictly) sorted.
 -/
Stream'.Seq.Pairwise : {α : Type u} → (α → α → Prop) → Stream'.Seq α → Prop
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm'_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x : E), o.areaForm' x = LinearMap.toContinuousLinearMap (o.areaForm x)
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.fun_finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'} {f' : ι → 𝔸'},
  (∀ i ∈ u, HasDerivAt (f i) (f' i) x) →
    HasDerivAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
-- Lean.Declaration
Lean.RecursorVal : Type
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Binary entropy is continuous everywhere.
This is due to definition of `Real.log` for negative numbers.  -/
Real.binEntropy_continuous : Continuous Real.binEntropy
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.natCard_inv : ∀ {G : Type u_1} [inst : InvolutiveInv G] (s : Set G), Nat.card ↑s⁻¹ = Nat.card ↑s
-- Batteries.Lean.EStateM
EStateM.run'_tryCatch : ∀ {σ ε α δ : Type u_1} [h : EStateM.Backtrackable δ σ] (body : EStateM ε σ α) (handler : ε → EStateM ε σ α) (s : σ),
  (tryCatch body handler).run' s =
    match body.run s with
    | EStateM.Result.ok x a => some x
    | EStateM.Result.error e s' => (handler e).run' (EStateM.Backtrackable.restore s' (EStateM.Backtrackable.save s))
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.congr_left : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v w : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → u =ᶠ[l] w → Asymptotics.IsEquivalent l w v
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.trace_def : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (z : QuadraticAlgebra R a b),
  QuadraticAlgebra.trace z = 2 * z.re + b * z.im
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.inv_apply : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G)
  (s : Set G), μ.inv s = μ s⁻¹
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.Affine.Point.sym2x_zero_zero : ∀ {R : Type u_1} [inst : CommRing R] {W' : WeierstrassCurve.Affine R},
  WeierstrassCurve.Affine.Point.sym2x 0 0 = ![1, 0, 0]
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- The proximity function of `f + g` at `⊤` is less than or equal to the sum of the proximity functions
of `f` and `g`, plus `log 2` (where `2` is the number of summands).
 -/
ValueDistribution.proximity_add_top_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f₁ f₂ : ℂ → E},
  Meromorphic f₁ →
    Meromorphic f₂ →
      ValueDistribution.proximity (f₁ + f₂) ⊤ ≤
        ValueDistribution.proximity f₁ ⊤ + ValueDistribution.proximity f₂ ⊤ + fun x => Real.log 2
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.orthogonalDecomposition.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], K.orthogonalDecomposition = K.orthogonalDecomposition
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.exists_forall_pow_toEnd_eq_zero : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsNilpotent L M], ∃ k, ∀ (x : L), (LieModule.toEnd R L M) x ^ k = 0
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.coe_pointwise_smul : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddGroup A] [inst_2 : DistribMulAction M A] (a : M)
  (S : AddSubgroup A), ↑(a • S) = a • ↑S
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.mem_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] {k : α},
  m₁.WF → m₂.WF → m₁.Equiv m₂ → (k ∈ m₁ ↔ k ∈ m₂)