mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Vector3
vectorAllP_cons : ∀ {α : Type u_1} {n : ℕ} (p : α → Prop) (x : α) (v : Vector3 α n),
  VectorAllP p (Vector3.cons x v) ↔ p x ∧ VectorAllP p v
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` preserves limits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits
of shape `J`.  -/
CategoryTheory.Limits.preservesColimitsOfShape_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)
  [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F.unop], CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageParams : Type
-- Mathlib.Algebra.Star.MonoidHom
/-- Transitivity of `StarMulEquiv`.  -/
StarMulEquiv.trans : {A : Type u_2} →
  {B : Type u_3} →
    {C : Type u_4} →
      [inst : Mul A] →
        [inst_1 : Mul B] →
          [inst_2 : Mul C] → [inst_3 : Star A] → [inst_4 : Star B] → [inst_5 : Star C] → (A ≃⋆* B) → (B ≃⋆* C) → A ≃⋆* C
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.instVAddSubtypeMem.eq_1 : ∀ {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : VAdd M' α],
  AddSubmonoid.instVAddSubtypeMem s = { vadd := fun m a => ↑m +ᵥ a }
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
/-- A deprecated alias for `ofRingCon`.  -/
TwoSidedIdeal.mk : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → RingCon R → TwoSidedIdeal R
-- Mathlib.Order.CompleteLattice.Lemmas
iSup_bool_eq : ∀ {α : Type u_1} [inst : CompleteLattice α] {f : Bool → α}, ⨆ b, f b = f true ⊔ f false
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.map_comap_eq_self_of_surjective : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] {f : K →+* L},
  Function.Surjective ⇑f → ∀ (s : Subfield L), Subfield.map f (Subfield.comap f s) = s
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMonNatTrans.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_6 : F.LaxBraided] [inst_7 : F'.LaxBraided] (f f_1 : F ⟶ F') (e_f : f = f_1)
  [inst_8 : CategoryTheory.NatTrans.IsMonoidal f],
  CategoryTheory.Functor.mapCommMonNatTrans f = CategoryTheory.Functor.mapCommMonNatTrans f_1
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂},
  (m₁ ∪ m₂).get k h' = m₂.get k ⋯
-- Lean.Meta.Tactic.Split
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.withEqs.go : {α : Type} →
  Array Lean.Expr →
    Array Lean.Expr →
      (Array Lean.Expr → Array Lean.Expr → Lean.MetaM α) → ℕ → Array Lean.Expr → Array Lean.Expr → Lean.MetaM α
-- Init.PropLemmas
or_or_distrib_left : ∀ {a b c : Prop}, a ∨ b ∨ c ↔ (a ∨ b) ∨ a ∨ c
-- Mathlib.GroupTheory.Sylow
Sylow.exists_comap_subtype_eq : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Subgroup G} (P : Sylow p ↥H), ∃ Q, Subgroup.comap H.subtype ↑Q = ↑P
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
/-- `inclusionOfMooreComplexMap X` is a split mono.  -/
AlgebraicTopology.DoldKan.splitMonoInclusionOfMooreComplexMap : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [inst_1 : CategoryTheory.Abelian A] →
      (X : CategoryTheory.SimplicialObject A) →
        CategoryTheory.SplitMono (AlgebraicTopology.inclusionOfMooreComplexMap X)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le : ∀ {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E']
  [inst_2 : InnerProductSpace 𝕜 E'] [inst_3 : CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E')
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  ∫⁻ (a : α), ↑‖↑↑↑((MeasureTheory.condExpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊
-- Lean.Server.Requests
Lean.Server.RequestHandler.mk.inj : ∀ {fileSource : Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri}
  {handle : Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse)}
  {fileSource_1 : Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri}
  {handle_1 : Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse)},
  { fileSource := fileSource, handle := handle } = { fileSource := fileSource_1, handle := handle_1 } →
    fileSource = fileSource_1 ∧ handle = handle_1
-- Mathlib.Analysis.Calculus.Deriv.CompMul
deriv_comp_mul_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (c : 𝕜) (f : 𝕜 → E) (x : 𝕜), deriv (fun x => f (c * x)) x = c • deriv f (c * x)
-- Mathlib.Computability.MyhillNerode
Language.leftQuotient_accepts_apply : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (x : List α), M.accepts.leftQuotient x = M.acceptsFrom (M.eval x)
-- Mathlib.RingTheory.Smooth.Basic
Algebra.instFormallySmoothMvPolynomial : ∀ {R : Type u} [inst : CommRing R] (σ : Type u_4), Algebra.FormallySmooth R (MvPolynomial σ R)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.toList.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → t.toList = t_1.toList
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMap.match_1.eq_1 : ∀ {β' : Type u_1} (motive : Option β' → Sort u_2) (h_1 : none = none → motive none)
  (h_2 : (out' : β') → none = some out' → motive (some out')),
  (match h' : none with
    | none => h_1 h'
    | some out' => h_2 out' h') =
    h_1 ⋯
-- Mathlib.Data.Fintype.EquivFin
instInfiniteListOfNonempty : ∀ {α : Type u_1} [Nonempty α], Infinite (List α)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mem_mk : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : AddSubsemigroup M} {x : M} (h_zero : 0 ∈ s.carrier),
  x ∈ { toAddSubsemigroup := s, zero_mem' := h_zero } ↔ x ∈ s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).contains k = true
-- Mathlib.Algebra.Exact.Basic
MonoidHom.mulExact_iff : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Group M] [inst_1 : Group N] [inst_2 : Group P] {f : M →* N}
  {g : N →* P}, Function.MulExact ⇑f ⇑g ↔ g.ker = f.range
-- Mathlib.Algebra.Order.Interval.Basic
instAddInterval : {α : Type u_2} → [inst : Preorder α] → [inst_1 : Add α] → [AddLeftMono α] → [AddRightMono α] → Add (Interval α)
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.Γ_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : (AlgebraicGeometry.SheafedSpace C)ᵒᵖ),
  AlgebraicGeometry.SheafedSpace.Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op ⊤)
-- Lean.SubExpr
Lean.SubExpr.mk : Lean.Expr → Lean.SubExpr.Pos → Lean.SubExpr
-- Mathlib.Probability.Distributions.Poisson.Basic
/-- The Poisson probability distribution with rate `r`.  -/
ProbabilityTheory.«termPo(_)» : Lean.ParserDescr
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.stdPart_of_tendsto : ∀ {x : ℝ*} {r : ℝ}, Filter.Germ.Tendsto x (nhds r) → ArchimedeanClass.stdPart x = r
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoOpPushout_hom_inr_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C}
  (h : Opposite.unop (CategoryTheory.Limits.pullback f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f.unop g.unop)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoOpPushout f g).hom.unop h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g).unop h
-- Init.Data.Slice.List.Basic
instSliceableListNatListSlice_5 : {α : Type u} → Std.Roi.Sliceable (List α) ℕ (ListSlice α)
-- Mathlib.Topology.Constructions
Pi.induced_precomp' : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {ι' : Type u_9} (φ : ι' → ι),
  TopologicalSpace.induced (fun f j => f (φ j)) Pi.topologicalSpace =
    ⨅ i', TopologicalSpace.induced (Function.eval (φ i')) (T (φ i'))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.brecOn_1.eq : ∀ {motive_1 : Lean.Lsp.DocumentSymbol → Sort u} {motive_2 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Sort u}
  {motive_3 : Option (Array Lean.Lsp.DocumentSymbol) → Sort u} {motive_4 : Array Lean.Lsp.DocumentSymbol → Sort u}
  {motive_5 : List Lean.Lsp.DocumentSymbol → Sort u} (t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol)
  (F_1 : (t : Lean.Lsp.DocumentSymbol) → t.below → motive_1 t)
  (F_2 : (t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_1 t → motive_2 t)
  (F_3 : (t : Option (Array Lean.Lsp.DocumentSymbol)) → Lean.Lsp.DocumentSymbol.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_3 t → motive_4 t)
  (F_5 : (t : List Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_4 t → motive_5 t),
  Lean.Lsp.DocumentSymbol.brecOn_1 t F_1 F_2 F_3 F_4 F_5 =
    F_2 t (Lean.Lsp.DocumentSymbol.brecOn_1.go t F_1 F_2 F_3 F_4 F_5).2
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.self_comp_inverse : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, f.IsInvertible → f ∘SL f.inverse = ContinuousLinearMap.id R M₂
-- Mathlib.Order.Interval.Set.Monotone
monotone_Iio : ∀ {α : Type u_1} [inst : Preorder α], Monotone Set.Iio
-- Mathlib.Order.Category.BddOrd
BddOrd.hom_id : ∀ {X : BddOrd}, BddOrd.Hom.hom (CategoryTheory.CategoryStruct.id X) = BoundedOrderHom.id ↑X.toPartOrd
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCycle_map_iff_of_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u},
  Function.Injective ⇑f → ((SimpleGraph.Walk.map f p).IsCycle ↔ p.IsCycle)
-- Init.Data.Int.Order
Int.mul_lt_mul_of_neg_left : ∀ {a b c : ℤ}, b < a → c < 0 → c * a < c * b
-- Mathlib.Data.Finset.Preimage
Finset.preimage_inl : ∀ {α : Type u} {β : Type v} (s : Finset (α ⊕ β)), s.preimage Sum.inl ⋯ = s.toLeft
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectivePresentation.shortExact_shortComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (ip : CategoryTheory.InjectivePresentation X), ip.shortComplex.ShortExact
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.eval.eq_def : ∀ (x : Turing.ToPartrec.Code),
  x.eval =
    match x with
    | Turing.ToPartrec.Code.zero' => fun v => pure (0 :: v)
    | Turing.ToPartrec.Code.succ => fun v => pure [v.headI.succ]
    | Turing.ToPartrec.Code.tail => fun v => pure v.tail
    | f.cons fs => fun v => do
      let n ← f.eval v
      let ns ← fs.eval v
      pure (n.headI :: ns)
    | f.comp g => fun v => g.eval v >>= f.eval
    | f.case g => fun v => Nat.rec (f.eval v.tail) (fun y x => g.eval (y :: v.tail)) v.headI
    | f.fix => PFun.fix fun v => Part.map (fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.isParabolic_neg_iff : ∀ {R : Type u_1} [inst : CommRing R] {m : Matrix (Fin 2) (Fin 2) R}, (-m).IsParabolic ↔ m.IsParabolic
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.not_mem_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α}, k ∉ ∅
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.inv_inv_add_inv : ∀ {p q r : NNReal}, p.HolderTriple q r → (p⁻¹ + q⁻¹)⁻¹ = r
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntryD.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : (a : α) × β a) →
          ((fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (r : Std.DTreeMap.Internal.Impl α β) →
                      (x : (a : α) × β a) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β k_1) →
                            (l r r_1 : Std.DTreeMap.Internal.Impl α β) →
                              (fallback : (a : α) × β a) →
                                motive
                                  (Std.DTreeMap.Internal.Impl.inner size k v
                                    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
                                  fallback) →
                motive x x_1
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.set_index_mem : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : l.HasBasis p s)
  (ht : t ∈ l), s ↑(h.index t ht) ∈ l
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.of_irreducible_expand_pow : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p : ℕ},
  p ≠ 0 → ∀ {f : Polynomial R} {n : ℕ}, Irreducible ((Polynomial.expand R (p ^ n)) f) → Irreducible f
-- Init.Data.SInt.Lemmas
Int8.add_mul : ∀ {a b c : Int8}, (a + b) * c = a * c + b * c
-- Mathlib.Topology.Category.Compactum
Compactum.le_nhds_of_str_eq : ∀ {X : Compactum} (F : Ultrafilter X.A) (x : X.A), X.str F = x → ↑F ≤ nhds x
-- Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
Measurable.apply_continuousLinearMap : ∀ {α : Type u_1} [inst : MeasurableSpace α] {𝕜 : Type u_2} [inst_1 : NontriviallyNormedField 𝕜] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [BorelSpace E] {F : Type u_4}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] {φ : α → F →L[𝕜] E},
  Measurable φ → ∀ (v : F), Measurable fun a => (φ a) v
-- Mathlib.Algebra.Order.Round
round_sub_ofNat : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α) (n : ℕ)
  [inst_4 : n.AtLeastTwo], round (x - OfNat.ofNat n) = round x - OfNat.ofNat n
-- Mathlib.LinearAlgebra.Eigenspace.Charpoly
Module.End.trace_eq_sum_roots_charpoly_of_splits : ∀ {K : Type u_3} {V : Type u_4} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : Module.Finite K V] {f : Module.End K V},
  (LinearMap.charpoly f).Splits → (LinearMap.trace K V) f = (LinearMap.charpoly f).roots.sum
-- Mathlib.Computability.Encoding
Computability.Encoding.mk.inj : ∀ {α : Type u} {Γ : Type v} {encode : α → List Γ} {decode : List Γ → Option α}
  {decode_encode : ∀ (x : α), decode (encode x) = some x} {encode_1 : α → List Γ} {decode_1 : List Γ → Option α}
  {decode_encode_1 : ∀ (x : α), decode_1 (encode_1 x) = some x},
  { encode := encode, decode := decode, decode_encode := decode_encode } =
      { encode := encode_1, decode := decode_1, decode_encode := decode_encode_1 } →
    encode = encode_1 ∧ decode = decode_1
-- Init.Control.Basic
/-- Extracts the value from a `ForInStep`, ignoring whether it is `ForInStep.done` or `ForInStep.yield`.
 -/
ForInStep.value : {α : Type u_1} → ForInStep α → α
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_finset_subset_smul_finset_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  {s t : Finset β} {a : α}, a ≠ 0 → (a • s ⊆ a • t ↔ s ⊆ t)
-- Init.Data.Vector.Basic
/-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds.  -/
Vector.eraseIdx! : {α : Type u_1} → {n : ℕ} → Vector α n → ℕ → Vector α (n - 1)
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaSigmaSubtypeEq_symm_apply : ∀ {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} {a : α} {b : β} (c : γ a b),
  (Equiv.sigmaSigmaSubtypeEq a b).symm c = ⟨⟨a, ⟨b, c⟩⟩, ⋯⟩
-- Mathlib.Analysis.Complex.Trigonometric
Real.tan_sq_div_one_add_tan_sq : ∀ {x : ℝ}, Real.cos x ≠ 0 → Real.tan x ^ 2 / (1 + Real.tan x ^ 2) = Real.sin x ^ 2
-- Mathlib.Order.Category.BoolAlg
BoolAlg.of.sizeOf_spec : ∀ (carrier : Type u_1) [str : BooleanAlgebra carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
/-- The shift functor by `n : ℤ` on `CochainComplex C ℤ` which sends a cochain
complex `K` to the complex which is `K.X (i + n)` in degree `i`, and which
multiplies the differentials by `(-1)^n`.  -/
CochainComplex.shiftFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → ℤ → CategoryTheory.Functor (CochainComplex C ℤ) (CochainComplex C ℤ)
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- **Alias** of `AlternatingMap.smulRight_eq_comp`. -/
LinearMap.smulRight_eq_comp : ∀ {R : Type u_12} {M₁ : Type u_13} {M₂ : Type u_14} {ι : Type u_15} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂),
  f.smulRight z = (LinearMap.id.smulRight z).compAlternatingMap f
-- Lean.Parser.Basic
Lean.Parser.withResultOf : Lean.Parser.Parser → (Lean.Syntax → Lean.Syntax) → Lean.Parser.Parser
-- Mathlib.NumberTheory.LucasLehmer
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.norm_num_ext.sModNatTR.go.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) → ((acc : ℕ) → motive 0 acc) → ((n acc : ℕ) → motive n.succ acc) → motive x x_1
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMul.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Mul M],
  Filter.Germ.instMul = { mul := Filter.Germ.map₂ fun x1 x2 => x1 * x2 }
-- Batteries.Data.String.Matcher
String.Matcher.mk.sizeOf_spec : ∀ (toMatcher : Array.Matcher Char) (pattern : Substring.Raw),
  sizeOf { toMatcher := toMatcher, pattern := pattern } = 1 + sizeOf toMatcher + sizeOf pattern
-- Mathlib.Order.Defs.LinearOrder
LinOrd.of.injEq : ∀ (carrier : Type u_2) [str : LinearOrder carrier] (carrier_1 : Type u_2) (str_1 : LinearOrder carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.eval.eq_7 : ∀ (f : Turing.ToPartrec.Code),
  f.fix.eval = PFun.fix fun v => Part.map (fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
vectorSpan_of_subsingleton : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, s.Subsingleton → vectorSpan k s = ⊥
-- Mathlib.Logic.Equiv.Basic
Equiv.semiconj_conj : ∀ {α₁ : Type u_11} {β₁ : Type u_12} (e : α₁ ≃ β₁) (f : α₁ → α₁), Function.Semiconj (⇑e) f (e.conj f)
-- Mathlib.Algebra.Group.WithOne.Basic
/-- Lift a semigroup homomorphism `f` to a bundled monoid homomorphism.  -/
WithOne.lift : {α : Type u} → {β : Type v} → [inst : Mul α] → [inst_1 : MulOneClass β] → (α →ₙ* β) ≃ (WithOne α →* β)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F}
  {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂},
  x₁ = x₂ →
    y₁ = W.negY x₂ y₂ → WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ + WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ = 0
-- Mathlib.Order.Ideal
Order.sequenceOfCofinals.encode_mem : ∀ {P : Type u_1} [inst : Preorder P] (p : P) {ι : Type u_2} [inst_1 : Encodable ι] (𝒟 : ι → Order.Cofinal P) (i : ι),
  Order.sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i
-- Lean.Elab.Command
Lean.Elab.Command.MacroExpandedSnapshot.mk.injEq : ∀ (toSnapshot : Lean.Language.Snapshot) (macroDecl : Lean.Name) (newStx : Lean.Syntax) (newNextMacroScope : ℕ)
  (hasTraces : Bool) (next : Array (Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot))
  (toSnapshot_1 : Lean.Language.Snapshot) (macroDecl_1 : Lean.Name) (newStx_1 : Lean.Syntax) (newNextMacroScope_1 : ℕ)
  (hasTraces_1 : Bool) (next_1 : Array (Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot)),
  ({ toSnapshot := toSnapshot, macroDecl := macroDecl, newStx := newStx, newNextMacroScope := newNextMacroScope,
        hasTraces := hasTraces, next := next } =
      { toSnapshot := toSnapshot_1, macroDecl := macroDecl_1, newStx := newStx_1,
        newNextMacroScope := newNextMacroScope_1, hasTraces := hasTraces_1, next := next_1 }) =
    (toSnapshot = toSnapshot_1 ∧
      macroDecl = macroDecl_1 ∧
        newStx = newStx_1 ∧ newNextMacroScope = newNextMacroScope_1 ∧ hasTraces = hasTraces_1 ∧ next = next_1)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.pos_real_smul_injective : ∀ (z : UpperHalfPlane), Function.Injective fun x => x • z
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to1.write.match_1.splitter : {Γ : Type u_3} →
  {Λ : Type u_2} →
    {σ : Type u_1} →
      (motive : List Bool → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ → Sort u_4) →
        (x : List Bool) →
          (x_1 : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) →
            ((q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) → motive [] q) →
              ((a : Bool) →
                  (l : List Bool) → (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) → motive (a :: l) q) →
                motive x x_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.le_iff : ∀ {X : SSet} {s t : X.S}, s ≤ t ↔ ∃ f, (CategoryTheory.ConcreteCategory.hom (X.map f.op)) t.simplex = s.simplex
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Given an algebra morphism whose carrier part is an epimorphism, we get an algebra epimorphism.
 -/
CategoryTheory.Monad.algebra_epi_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X Y : T.Algebra} (f : X ⟶ Y)
  [h : CategoryTheory.Epi f.f], CategoryTheory.Epi f
-- Std.Net.Addr
Std.Net.SocketAddressV6.instCoeSocketAddress : Coe Std.Net.SocketAddressV6 Std.Net.SocketAddress
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.DTreeMap.Raw.filter f t} (h : t.WF),
  (Std.DTreeMap.Raw.filter f t).get k h' = t.get k ⋯
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toHomeomorph_refl : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P],
  (AffineIsometryEquiv.refl 𝕜 P).toHomeomorph = Homeomorph.refl P
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_X_pow_mul : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ),
  p ≠ 0 → (Polynomial.X ^ n * p).natDegree = p.natDegree + n