mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The canonical isomorphism between the chosen biproduct and the chosen coproduct.  -/
CategoryTheory.Limits.biprod.isoCoprod : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → X ⊞ Y ≅ X ⨿ Y
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ), ↑(MeasureTheory.AEEqFun.mk f hf) =ᵐ[μ] f
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_copy : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (S : LieSubmodule R L M) (s : Set M) (hs : s = ↑S),
  ↑(S.copy s hs) = s
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.tendsto_nhds_iff' : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y],
  Topology.IsOpenEmbedding f →
    ∀ {l : Filter Z} {x : X}, Filter.Tendsto (g ∘ f) (nhds x) l ↔ Filter.Tendsto g (nhds (f x)) l
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
/-- The stabilizer of the complement is the stabilizer of the set.  -/
stabilizer_compl : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] {s : Set α},
  MulAction.stabilizer G sᶜ = MulAction.stabilizer G s
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.sigmaProdDistrib_symm_apply : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] {ι : Type u_7} {X : ι → Type u_8}
  [inst_1 : (i : ι) → TopologicalSpace (X i)] (a : (i : ι) × X i × Y),
  Homeomorph.sigmaProdDistrib.symm a = (⟨a.fst, a.snd.1⟩, a.snd.2)
-- Mathlib.Algebra.Group.Basic
eq_of_neg_add_eq_zero : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, -a + b = 0 → a = b
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.leadingCoeff_mul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] (x y : HahnSeries Γ R) [NoZeroDivisors R],
  (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
-- Lean.Parser.Term
/-- `by tac` constructs a term of the expected type by running the tactic(s) `tac`.  -/
Lean.Parser.Term.byTactic : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.hasLimits_of_completeLattice : ∀ {α : Type u} [inst : CompleteLattice α], CategoryTheory.Limits.HasLimitsOfSize.{w, w', u, u} α
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.aeval_homogenize_of_eq_one : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {p : Polynomial R} {n : ℕ},
  p.natDegree ≤ n → ∀ (g : Fin 2 → A), g 1 = 1 → (MvPolynomial.aeval g) (p.homogenize n) = (Polynomial.aeval (g 0)) p
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- Helper construction for `liftToFinsetColimIso`.  -/
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) {J : Finset (CategoryTheory.Discrete α)} (j : ↥J) {Z : C}
  (h : CategoryTheory.Limits.colimit F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => F.obj ↑x) j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F) J)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.colimit.isoColimitCocone
              (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F)).inv
          h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F ↑j) h
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_smul : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : NNReal} {a : A},
  (r • a)⁺ = r • a⁺
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.IsIPC.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasProducts C]
  [inst_2 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, u_3, v_1, u_1} C],
  autoParam (∀ (ι : Type w), CategoryTheory.Limits.IsIPCOfShape.{w, w, v_1, u_1} ι C)
      CategoryTheory.Limits.IsIPC.isIPCOfShape._autoParam →
    CategoryTheory.Limits.IsIPC C
-- Init.Data.Nat.Basic
Nat.mul_sub_one : ∀ (n m : ℕ), n * (m - 1) = n * m - n
-- Lean.CoreM
/-- If the `diagnostics` option is not already set, gives a message explaining this option.
Begins with a `\n\n`, so an error message can look like `m!"some error occurred{useDiagnosticMsg}"`.
The double newline gives better visual separation from the main error message
 -/
Lean.useDiagnosticMsg : Lean.MessageData
-- Mathlib.Order.Antichain
isAntichain_preimage_subtypeVal : ∀ {α : Type u_1} {r : α → α → Prop} (s t : Set α),
  IsAntichain (fun x1 x2 => r ↑x1 ↑x2) (Subtype.val ⁻¹' t) ↔ IsAntichain r (s ∩ t)
-- Mathlib.Topology.Germ
Filter.Germ.sliceLeft_coe : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] {x : X} [inst_1 : TopologicalSpace Y] {y : Y}
  (f : X × Y → Z), (↑f).sliceLeft = ↑fun x' => f (x', y)
-- Mathlib.Topology.Connected.PathConnected
ZerothHomotopy.sound : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (p : Path x y), ZerothHomotopy.mk x = ZerothHomotopy.mk y
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- Euler's limit formula for the real Gamma function.  -/
Real.GammaSeq_tendsto_Gamma : ∀ (s : ℝ), Filter.Tendsto s.GammaSeq Filter.atTop (nhds (Real.Gamma s))
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseIdxTR.go.eq_2 : ∀ {α : Type u_1} (l : List α) (a : Array α) (head : α) (xs : List α),
  List.eraseIdxTR.go✝ l (head :: xs) 0 a = a.toListAppend xs
-- Mathlib.RepresentationTheory.Basic
Representation.instIsScalarTowerMonoidAlgebraAsModule : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V), IsScalarTower k (MonoidAlgebra k G) ρ.asModule
-- Init.Data.UInt.Lemmas
USize.neg_add : ∀ {a b : USize}, -(a + b) = -a - b
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.instIsSplitEpiChainComplexNatToNormalizedChainComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C), CategoryTheory.IsSplitEpi (X.toNormalizedChainComplex R)
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
/-- For fixed `ε > 0`, the mapping `x ↦ mulExpNegMulSq ε x` is bounded by `(√ε)⁻¹`.  -/
Real.abs_mulExpNegMulSq_le : ∀ {ε : ℝ}, 0 < ε → ∀ {x : ℝ}, |ε.mulExpNegMulSq x| ≤ (√ε)⁻¹
-- Mathlib.Order.Hom.Basic
/-- Notation for an `OrderEmbedding`.  -/
«term_↪o_» : Lean.TrailingParserDescr
-- Lean.Elab.Tactic.Omega.OmegaM
_private.Lean.Elab.Tactic.Omega.OmegaM.0.Lean.Elab.Tactic.Omega.groundNat?.op : (ℕ → ℕ → ℕ) → Lean.Expr → Lean.Expr → Option ℕ
-- Mathlib.RingTheory.HahnSeries.Summable
/-- A family of Hahn series whose formal coefficient-wise sum is a Hahn series.  For each
coefficient of the sum to be well-defined, we require that only finitely many series are nonzero at
any given coefficient.  For the formal sum to be a Hahn series, we require that the union of the
supports of the constituent series is partially well-ordered.  -/
HahnSeries.SummableFamily : (Γ : Type u_8) → (R : Type u_9) → [PartialOrder Γ] → [AddCommMonoid R] → Type u_7 → Type (max (max u_7 u_8) u_9)
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `(F ⋙ forget AddCommMonCat).sections` is `u`-small, `F` has a limit.  -/
AddCommMonCat.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections], CategoryTheory.Limits.HasLimit F
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- An `R`-algebra norm such that `f 1 = 1` extends the norm on `R`.  -/
AlgebraNorm.extends_norm' : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S]
  {f : AlgebraNorm R S}, f 1 = 1 → ∀ (a : R), f (a • 1) = ‖a‖
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.tensorObj_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C),
  CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_of_contains_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β k}, (m.insert k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.LinearAlgebra.Orientation
Module.Basis.adjustToOrientation.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  [inst_7 : Nonempty ι] (e : Module.Basis ι R M) (x : Orientation R M ι),
  e.adjustToOrientation x =
    if e.orientation = x then e else e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))
-- Lean.DocString.Parser
/-- Computes the `BlockCtxt` for parsing a docstring that starts at `startPos` in the given file map.
`endPos` is the position of the `-` in the closing delimiter. When the docstring content starts
mid-line (e.g. `/-! # Header -/`), the `docStartPosition` is set to the position after any leading
spaces so that headers on the first line are recognized. For indented docstrings, `baseColumn` is
computed as the minimum column among the opening delimiter, closing delimiter, and the least-indented
non-empty content line.
 -/
Lean.Doc.Parser.BlockCtxt.forDocString : Lean.FileMap → String.Pos.Raw → String.Pos.Raw → Lean.Doc.Parser.BlockCtxt
-- Init.Data.List.Basic
List.elem.eq_1 : ∀ {α : Type u} [inst : BEq α] (a : α), List.elem a [] = false
-- Mathlib.Topology.Order
TopologicalSpace.nhds_mkOfNhds_of_hasBasis : ∀ {α : Type u} {n : α → Filter α} {ι : α → Sort u_1} {p : (a : α) → ι a → Prop} {s : (a : α) → ι a → Set α},
  (∀ (a : α), (n a).HasBasis (p a) (s a)) →
    (∀ (a : α) (i : ι a), p a i → a ∈ s a i) →
      (∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x) → ∀ (a : α), nhds a = n a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The isomorphism `S₁.rightHomology ≅ S₂.rightHomology` induced by an isomorphism of
short complexes `S₁ ≅ S₂`.  -/
CategoryTheory.ShortComplex.rightHomologyMapIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ≅ S₂) →
          [inst_2 : S₁.HasRightHomology] → [inst_3 : S₂.HasRightHomology] → S₁.rightHomology ≅ S₂.rightHomology
-- Lean.MetavarContext
/-- Return `true` if the give metavariable is already assigned.  -/
Lean.MVarId.isAssigned : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → m Bool
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
contMDiffAt_localFrame_of_mem : ∀ {𝕜 : 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] (n : WithTop ℕ∞) {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 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [ContMDiffVectorBundle n F V I] {ι : Type u_7} {x : M} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [inst_15 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F) (i : ι),
  x ∈ e.baseSet → ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, e.localFrame b i x⟩) x
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y),
  CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U))
      (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U)) =
    Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Companion lemma to `ContinuousOn.circleAverage`: a function continuous on `Ioc r
R` and constant on `Ioo r R` is constant.
 -/
Real.ContinuousOn.eq_of_eqOn_Ioo : ∀ {f : ℝ → ℝ} {c r R : ℝ}, ContinuousOn f (Set.Ioc r R) → r < R → Set.EqOn f (fun x => c) (Set.Ioo r R) → f R = c
-- Mathlib.Analysis.Complex.ReImTopology
Complex.interior_setOfPred_im_le : ∀ (a : ℝ), interior {z | z.im ≤ a} = {z | z.im < a}
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the iterator `it` yields no values.

`O(|it|)` since the iterator may skip an unknown number of times before returning a result.
Short-circuits upon encountering the first result. Only the first element of `it` is examined.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.isEmpty`.
 -/
Std.IterM.Total.isEmpty : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → [Std.Iterators.Productive α m] → Std.IterM.Total m β → m (ULift.{w, 0} Bool)
-- Mathlib.Data.Sigma.Lex
PSigma.Lex.mono_left : ∀ {ι : Sort u_1} {α : ι → Sort u_2} {r₁ r₂ : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop},
  (∀ (a b : ι), r₁ a b → r₂ a b) → ∀ {a b : (i : ι) ×' α i}, PSigma.Lex r₁ s a b → PSigma.Lex r₂ s a b
-- Mathlib.Data.Multiset.ZeroCons
Multiset.Nodup.of_cons : ∀ {α : Type u_1} {s : Multiset α} {a : α}, (a ::ₘ s).Nodup → s.Nodup
-- Init.Data.List.Basic
List.zipWith_cons_cons : ∀ {α : Type u} {β : Type v} {γ : Type w} {a : α} {as : List α} {b : β} {bs : List β} {f : α → β → γ},
  List.zipWith f (a :: as) (b :: bs) = f a b :: List.zipWith f as bs
-- Init.Data.Range.Polymorphic.Basic
Std.Rio.lt_upper_of_mem : ∀ {α : Type u} {r : Std.Rio α} {a : α} [inst : LT α], a ∈ r → a < r.upper
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_lt_logb_of_base_lt_one : ∀ {b x y : ℝ}, 0 < b → b < 1 → 0 < x → x < y → Real.logb b y < Real.logb b x
-- Mathlib.Order.Lattice
sup_le_inf : ∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊔ b ≤ a ⊓ b ↔ a = b
-- Mathlib.Algebra.Algebra.Subalgebra.Prod
Subalgebra.mem_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {S : Subalgebra R A} {S₁ : Subalgebra R B} {x : A × B},
  x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.ext'_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {α β : F ⟶ G}, α = β ↔ α.app = β.app
-- Init.GetElem
of_getElem_eq : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} {e : elem}
  [inst : GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)]
  {h : dom c i}, c[i] = e → dom c i
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.instHasSupportOfLeAtTop : ∀ {β : Type u_2} (L : SummationFilter β) [L.LeAtTop], L.HasSupport
-- Init.Data.SInt.Bitwise
commandDeclare_bitwise_int_theorems__ : Lean.ParserDescr
-- Mathlib.Algebra.Category.CommBialgCat
_private.Mathlib.Algebra.Category.CommBialgCat.0.CommBialgCat.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] [inst_1 : SizeOf R] (carrier : Type v) [commRing : CommRing carrier]
  [bialgebra : Bialgebra R carrier],
  sizeOf { carrier := carrier, commRing := commRing, bialgebra := bialgebra } =
    1 + sizeOf carrier + sizeOf commRing + sizeOf bialgebra
-- Mathlib.Order.Interval.Set.Image
Antitone.image_Iic_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  Antitone f → f '' Set.Iic b ⊆ Set.Ici (f b)
-- Mathlib.Order.Hom.Lattice
SupHom.subtypeVal.eq_1 : ∀ {β : Type u_3} [inst : SemilatticeSup β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)),
  SupHom.subtypeVal Psup = { toFun := Subtype.val, map_sup' := ⋯ }
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.pushout_inl_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {Z X Y : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q]
  [inst_3 : CategoryTheory.Limits.HasPushout f g], Q f → (P (CategoryTheory.Limits.pushout.inl f g) ↔ P g)
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.map_injective : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂}, f.ker = ⊥ → Function.Injective (Submodule.map f)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.algebraMap_restrictHom_smul : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : CommRing C] [inst_5 : IsDomain C] [inst_6 : Algebra A B]
  [inst_7 : Algebra A C] [inst_8 : Algebra B C] [inst_9 : FaithfulSMul A B] [inst_10 : FaithfulSMul B C]
  [inst_11 : IsScalarTower A B C] [inst_12 : Finite G] [inst_13 : Finite G'] [inst_14 : MulSemiringAction G C]
  [inst_15 : IsGaloisGroup G A C] [inst_16 : MulSemiringAction G' B] [inst_17 : IsGaloisGroup G' A B] (g : G) (x : B),
  (algebraMap B C) ((IsGaloisGroup.restrictHom G G' A B C) g • x) = g • (algebraMap B C) x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.instNontrivial : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [Nontrivial R], Nontrivial W'.CoordinateRing
-- Mathlib.RingTheory.Length
Submodule.length_lt : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinian R M]
  [IsNoetherian R M] {N : Submodule R M}, N ≠ ⊤ → Module.length R ↥N < Module.length R M
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.coe_inv : ∀ {α : Type u_1} [inst : Inv α] (a : α), ↑a⁻¹ = (↑a)⁻¹
-- Mathlib.Order.JordanHolder
CompositionSeries.total : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X} {x y : X},
  x ∈ s → y ∈ s → x ≤ y ∨ y ≤ x
-- Lean.Meta.CoeAttr
Lean.Meta.instDecidableEqCoeFnType : DecidableEq Lean.Meta.CoeFnType
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.merge.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : α) (xs : List α) (y : α) (ys : List α)
  (h_1 : (ys : List α) → motive [] ys) (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (match x :: xs, y :: ys with
    | [], ys => h_1 ys
    | xs, [] => h_2 xs
    | x :: xs, y :: ys => h_3 x xs y ys) =
    h_3 x xs y ys
-- Mathlib.Topology.MetricSpace.Defs
dist_eq_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, dist x y = 0 ↔ x = y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.minKey! ∈ t
-- Init.Grind.Norm
Lean.Grind.or_swap12 : ∀ (p q r : Prop), (p ∨ q ∨ r) = (q ∨ p ∨ r)
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.findFinIdx?.eq_1 : ∀ {α : Type u} (p : α → Bool) (as : Array α), Array.findFinIdx? p as = Array.findFinIdx?.loop✝ p as 0
-- Mathlib.Data.Seq.Computation
Computation.LiftRelAux.ret_left : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a : α) (cb : Computation β),
  Computation.LiftRelAux R C (Sum.inl a) cb.destruct ↔ ∃ b ∈ cb, R a b
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `Module.Dual.re_extendRCLike_apply`. -/
LinearMap.extendTo𝕜'_apply_re : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] [inst_3 : Module 𝕜 F]
  [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) (x : F), RCLike.re (fr.extendRCLike x) = fr x
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The map that picks up the final vertex of a 2-simplex, as a morphism in the 2-truncated
simplex category.  -/
SSet.Truncated.ι2₂ : { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 } ⟶
  { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 }
-- Mathlib.Data.Nat.Log
Nat.clog.fun_cases_unfolding : ∀ (b n : ℕ) (motive : ℕ → Prop),
  (1 < b ∧ 1 < n → motive ((Nat.clog.go n b n).2 + 1)) → (¬(1 < b ∧ 1 < n) → motive 0) → motive (Nat.clog b n)
-- Mathlib.Order.OmegaCompletePartialOrder
instOmegaCompletePartialOrderForall : {α : Type u_2} →
  {β : α → Type u_6} → [(a : α) → OmegaCompletePartialOrder (β a)] → OmegaCompletePartialOrder ((a : α) → β a)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_iff_injective_finsuppLinearCombination : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v ↔ Function.Injective ⇑(Finsupp.linearCombination R v)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_alter_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.get? k = f (t.get? k)
-- Mathlib.Order.Category.PartOrd
PartOrd.id_apply : ∀ (X : PartOrd) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddRightCancelSemigroup α],
  Colex.instAddRightCancelSemigroup = { toAddSemigroup := Colex.instAddSemigroup, toIsRightCancelAdd := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- A `Matrix n n R` is algebra equivalent to a linear map `(n → R) →ₗ[R] (n → R)`.  -/
Matrix.toLinAlgEquiv' : {R : Type u_1} →
  [inst : CommSemiring R] →
    {n : Type u_5} → [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → Matrix n n R ≃ₐ[R] (n → R) →ₗ[R] n → R
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.martingalePart_smul : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] (c : ℝ) (n : ℕ),
  MeasureTheory.martingalePart (c • f) ℱ μ n =ᵐ[μ] c • MeasureTheory.martingalePart f ℱ μ n