mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Ind
/-- If `P` ind-spreads and all under categories are finitely accessible, `ind P`
is stable under composition if `P` is.  -/
CategoryTheory.MorphismProperty.IsStableUnderComposition.ind_of_preIndSpreads : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [∀ (X : C), CategoryTheory.IsFinitelyAccessibleCategory (CategoryTheory.Under X)]
  [CategoryTheory.Limits.HasPushouts C] [P.IsStableUnderComposition] [P.IsStableUnderCobaseChange] [P.PreIndSpreads],
  P ≤ CategoryTheory.MorphismProperty.isFinitelyPresentable C → P.ind.IsStableUnderComposition
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.max!.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : Unit → motive none) (h_2 : (x : α) → motive (some x)),
  (match some x with
    | none => h_1 ()
    | some x => h_2 x) =
    h_2 x
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_reindex_left : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {l' : Type u_15}
  {m' : Type u_16} {n' : Type u_17} (f : α → β → γ) (el : l ≃ l') (em : m ≃ m') (M : Matrix l m α) (N : Matrix n n' β),
  Matrix.kroneckerMap f ((Matrix.reindex el em) M) N =
    (Matrix.reindex (el.prodCongr (Equiv.refl n)) (em.prodCongr (Equiv.refl n'))) (Matrix.kroneckerMap f M N)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : EquivBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)} {k : α} (hl : Std.Internal.List.DistinctKeys l)
  {h : Std.Internal.List.containsKey k (List.filter (fun p => f p.fst p.snd) l) = true},
  Std.Internal.List.getKey k (List.filter (fun p => f p.fst p.snd) l) h = Std.Internal.List.getKey k l ⋯
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.degree_C_mul_T_ite : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] (n : ℤ) (a : R),
  (LaurentPolynomial.C a * LaurentPolynomial.T n).degree = if a = 0 then ⊥ else ↑n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorArbitraryShiftTargetBlastShiftRight : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.ArbitraryShiftTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight
-- Std.Internal.Do.Order.Basic
/-- Embedding of propositions into an CompleteLattice type. `⌜p⌝` embeds `p : Prop` as `⊤` if `p` holds
and `⊥` otherwise.  -/
Lean.Order.CompleteLattice.ofProp : {l : Type u_1} → [Lean.Order.CompleteLattice l] → Prop → l
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Inhabited β] (a : α) (l : List ((_ : α) × β)),
  Std.Internal.List.getValue! a l = (Std.Internal.List.getValue? a l).get!
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], Cardinal.lift.{u, v} (OfNat.ofNat n) = OfNat.ofNat n
-- Lean.Parser.Term.Basic
/-- Instance-implicit binder, like `[C]` or `[inst : C]`.
In regular applications without `@` explicit mode, it is automatically inserted
and solved for by typeclass inference for the specified class `C`.
In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
 -/
Lean.Parser.Term.instBinder : Lean.Parser.Parser
-- Lean.Message
Lean.instInhabitedMessageLog : Inhabited Lean.MessageLog
-- Mathlib.Data.Nat.Bitwise
Nat.instXorOp.eq_1 : Nat.instXorOp = { xor := Nat.xor }
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.prec1 : ∀ {f : ℕ → ℕ} (m : ℕ), Nat.Primrec f → Nat.Primrec fun n => Nat.rec m (fun y IH => f (Nat.pair y IH)) n
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle as a ratio of sides, version subtracting
vectors.  -/
Orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).sin = ‖x‖ / ‖y - x‖
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The norm of the difference of two non-zero vectors equals the absolute value
of the difference of their norms if and only the angle between the two vectors is 0.  -/
InnerProductGeometry.norm_sub_eq_abs_sub_norm_iff_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  x ≠ 0 → y ≠ 0 → (‖x - y‖ = |‖x‖ - ‖y‖| ↔ InnerProductGeometry.angle x y = 0)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instIteratorRxoIteratorIdSigma : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.Iterator (Std.DTreeMap.Internal.RxoIterator α β) Id ((a : α) × β a)
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_C_mul : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : StrongNormalizedGCDMonoid R] (r : R) (p : Polynomial R),
  (Polynomial.C r * p).content = normalize r * p.content
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
/-- A choice of cocone for a functor `F : A ⥤ J` such that `HasCardinalLT (Arrow A) κ`
when `J` is a `κ`-filtered category, and `Arrow A` has cardinality `< κ`.  -/
CategoryTheory.IsCardinalFiltered.cocone : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {κ : Cardinal.{w}} →
      [hκ : Fact κ.IsRegular] →
        [CategoryTheory.IsCardinalFiltered J κ] →
          {A : Type v'} →
            [inst_2 : CategoryTheory.Category.{u', v'} A] →
              (F : CategoryTheory.Functor A J) →
                HasCardinalLT (CategoryTheory.Arrow A) κ → CategoryTheory.Limits.Cocone F
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comp_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂)
  (g : sq₂.Hom sq₃), (f.comp g).τ₂ = CategoryTheory.CategoryStruct.comp f.τ₂ g.τ₂
-- Mathlib.Order.WellFounded
/-- Let `r` be a relation on `α`, let `f : α → β` be a function, let `C : β → Prop`, and
let `bot : α`. This induction principle shows that `C (f bot)` holds, given that
* some `a` that is accessible by `r` satisfies `C (f a)`, and
* for each `b` such that `f b ≠ f bot` and `C (f b)` holds, there is `c`
  satisfying `r c b` and `C (f c)`.  -/
Acc.induction_bot' : ∀ {α : Sort u_4} {β : Sort u_5} {r : α → α → Prop} {a bot : α},
  Acc r a →
    ∀ {C : β → Prop} {f : α → β}, (∀ (b : α), f b ≠ f bot → C (f b) → ∃ c, r c b ∧ C (f c)) → C (f a) → C (f bot)
-- Mathlib.RingTheory.TensorProduct.Basic
AlgHom.ofLinearMap.congr_simp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f f_1 : A →ₗ[R] B) (e_f : f = f_1) (map_one : f 1 = 1)
  (map_mul : ∀ (x y : A), f (x * y) = f x * f y), AlgHom.ofLinearMap f map_one map_mul = AlgHom.ofLinearMap f_1 ⋯ ⋯
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_surjective_eq_zero_iff : ∀ {α β : Type u},
  Cardinal.mk ↑{f | Function.Surjective f} = 0 ↔ Cardinal.mk α < Cardinal.mk β ∨ Cardinal.mk α ≠ 0 ∧ Cardinal.mk β = 0
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {toPrelaxFunctorStruct : CategoryTheory.PrelaxFunctorStruct B C}
  {map₂_id :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.id f) =
          CategoryTheory.CategoryStruct.id (toPrelaxFunctorStruct.map f))
      CategoryTheory.PrelaxFunctor.map₂_id._autoParam}
  {map₂_comp :
    autoParam
      (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
        toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.comp η θ) =
          CategoryTheory.CategoryStruct.comp (toPrelaxFunctorStruct.map₂ η) (toPrelaxFunctorStruct.map₂ θ))
      CategoryTheory.PrelaxFunctor.map₂_comp._autoParam}
  {toPrelaxFunctorStruct_1 : CategoryTheory.PrelaxFunctorStruct B C}
  {map₂_id_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctorStruct_1.map₂ (CategoryTheory.CategoryStruct.id f) =
          CategoryTheory.CategoryStruct.id (toPrelaxFunctorStruct_1.map f))
      CategoryTheory.PrelaxFunctor.map₂_id._autoParam}
  {map₂_comp_1 :
    autoParam
      (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
        toPrelaxFunctorStruct_1.map₂ (CategoryTheory.CategoryStruct.comp η θ) =
          CategoryTheory.CategoryStruct.comp (toPrelaxFunctorStruct_1.map₂ η) (toPrelaxFunctorStruct_1.map₂ θ))
      CategoryTheory.PrelaxFunctor.map₂_comp._autoParam},
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp } =
      { toPrelaxFunctorStruct := toPrelaxFunctorStruct_1, map₂_id := map₂_id_1, map₂_comp := map₂_comp_1 } →
    toPrelaxFunctorStruct = toPrelaxFunctorStruct_1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.measurable_polarCoordReal_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Measurable ↑(NumberField.mixedEmbedding.polarCoordReal K).symm
-- Batteries.Data.List.Basic
/-- `mapDiagM f l` calls `f` on all elements in the upper triangular part of `l × l`.
That is, for each `e ∈ l`, it will run `f e e` and then `f e e'`
for each `e'` that appears after `e` in `l`.
```
mapDiagM f [1, 2, 3] =
  return [← f 1 1, ← f 1 2, ← f 1 3, ← f 2 2, ← f 2 3, ← f 3 3]
```
 -/
List.mapDiagM : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [Monad m] → (α → α → m β) → List α → m (List β)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The map `normalizedFactorsEquivOfQuotEquiv` preserves multiplicities.  -/
IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) (L : Ideal R)
  (hL : L ∈ UniqueFactorizationMonoid.normalizedFactors I),
  emultiplicity (↑((IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv f hI hJ) ⟨L, hL⟩)) J = emultiplicity L I
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.mem_support_restrict : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] {s : Set X} {x : X},
  x ∈ (μ.restrict s).support ↔ ∃ᶠ (u : Set X) in (nhdsWithin x s).smallSets, 0 < μ u
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnity_zero : ∀ (M : Type u_7) [inst : CommMonoid M], rootsOfUnity 0 M = ⊤
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_deterministic_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [MeasurableSingletonClass γ] {f : α × β → γ} (hf : Measurable f) {s : Set (β × γ)},
  MeasurableSet s →
    ∀ (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (x : α),
      ((κ.compProd (ProbabilityTheory.Kernel.deterministic f hf)) x) s = (κ x) {b | (b, f (x, b)) ∈ s}
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The conjugate of the golden ratio `ψ := (1 - √5)/2`.  -/
goldenRatio.termψ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.comp_nat_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {f : ℕ → M} {k : ℕ},
  (Summable fun n => f (n + k)) → Summable f
-- Mathlib.Algebra.LinearRecurrence
/-- If `u` is a solution to `E` and `init` designates its first `E.order` values,
then `u = E.mkSol init`. This proves that `E.mkSol init` is the only solution
of `E` whose first `E.order` values are given by `init`.  -/
LinearRecurrence.eq_mk_of_is_sol_of_eq_init' : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) {u : ℕ → R} {init : Fin E.order → R},
  E.IsSolution u → (∀ (n : Fin E.order), u ↑n = init n) → u = E.mkSol init
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_add : ∀ {α : Type u_1} [inst : AddZeroClass α] {a b : WithTop α}, a ≠ ⊤ → b ≠ ⊤ → (a + b).untop₀ = a.untop₀ + b.untop₀
-- Mathlib.Order.Atoms
/-- A lower-modular lattice that is coatomistic is strongly coatomic.
Not an instance to prevent loops.  -/
Lattice.isStronglyCoatomic : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : OrderTop α] [IsLowerModularLattice α] [IsCoatomistic α],
  IsStronglyCoatomic α
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ImportData.mk : IO.Ref (Array Lean.Meta.LazyDiscrTree.ImportFailure) → Lean.Meta.LazyDiscrTree.ImportData
-- Init.Data.SInt.Lemmas
Int8.toBitVec_toUInt8 : ∀ (x : Int8), x.toUInt8.toBitVec = x.toBitVec
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.GlobalPreprocessorToGlobalBranchingPreprocessor : Coe Mathlib.Tactic.Linarith.GlobalPreprocessor Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
-- Mathlib.Order.Heyting.Basic
ne_compl_self : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α} [Nontrivial α], a ≠ aᶜ
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.nthHomSeq_mul : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r s : R),
  PadicInt.nthHomSeq f_compat (r * s) ≈ PadicInt.nthHomSeq f_compat r * PadicInt.nthHomSeq f_compat s
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Return true if `declName` is automatically generated,
or otherwise unsuitable as a lemma suggestion.  -/
Lean.Meta.RefinedDiscrTree.blacklistInsertion : Lean.Environment → Lean.Name → Bool
-- Init.Prelude
/-- `a * b` computes the product of `a` and `b`. See `HMul`.  -/
Mul.mul : {α : Type u} → [self : Mul α] → α → α → α
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- The normalization functor for the free monoidal category over `C`.  -/
CategoryTheory.FreeMonoidalCategory.fullNormalize : (C : Type u) →
  CategoryTheory.Functor (CategoryTheory.FreeMonoidalCategory C)
    ((CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.functorExt_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1}
  {F G : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ι) C} (base : F.obj none ≅ G.obj none)
  (comp : (i : ι) → F.obj (some i) ≅ G.obj (some i))
  (w :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)) base.hom =
          CategoryTheory.CategoryStruct.comp (comp i).hom (G.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)))
      CategoryTheory.Limits.WidePullbackShape.functorExt._auto_1)
  (X : CategoryTheory.Limits.WidePullbackShape ι),
  (CategoryTheory.Limits.WidePullbackShape.functorExt base comp w).hom.app X =
    (match X with
      | none => base
      | some i => comp i).hom
-- Mathlib.Analysis.Real.Spectrum
QuasispectrumRestricts.lt_nnreal_iff : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A},
  QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal →
    ∀ {r : NNReal}, (∀ x ∈ quasispectrum NNReal a, x < r) ↔ ∀ x ∈ quasispectrum ℝ a, x < ↑r
-- Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
ValuativeRel.eq_trivialRel_of_compatible_one : ∀ {R Γ : Type} [inst : Ring R] [inst_1 : DecidableEq R] [inst_2 : IsDomain R]
  [inst_3 : LinearOrderedCommGroupWithZero Γ] [h : ValuativeRel R] [hv : Valuation.Compatible 1],
  h = ValuativeRel.trivialRel
-- Mathlib.Analysis.Calculus.Conformal.InnerProduct
/-- A real differentiable map `f` is conformal at point `x` if and only if its
differential `fderiv ℝ f x` at that point scales every inner product by a positive scalar.  -/
conformalAt_iff' : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {f : E → F} {x : E},
  ConformalAt f x ↔ ∃ c, 0 < c ∧ ∀ (u v : E), inner ℝ ((fderiv ℝ f x) u) ((fderiv ℝ f x) v) = c * inner ℝ u v
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_iSup_Iio_add_one : ∀ {a : Ordinal.{u_1}} {f : ↑(Set.Iio a) → Ordinal.{u_1}}, StrictMono f → (⨆ i, f i + 1).cof = a.cof
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preservesColimitIso_inv_comp_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesColimit F G]
  [inst_4 : CategoryTheory.Limits.HasColimit F] (t : CategoryTheory.Limits.Cocone F),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).inv
      (G.map (CategoryTheory.Limits.colimit.desc F t)) =
    CategoryTheory.Limits.colimit.desc (F.comp G) (G.mapCocone t)
-- Mathlib.Logic.Function.DependsOn
Function.FactorsThrough.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (g : α → γ) (f : α → β),
  Function.FactorsThrough g f = ∀ ⦃a b : α⦄, f a = f b → g a = g b
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidIso.withZeroUnits_apply : ∀ {α : Type u_6} [inst : LinearOrderedCommGroupWithZero α] [inst_1 : DecidablePred fun a => a = 0] (n : WithZero αˣ),
  OrderMonoidIso.withZeroUnits n = WithZero.recZeroCoe 0 Units.val n
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith.eq_1 : ∀ (f : Ordinal.{u} → Ordinal.{u}) (o : Ordinal.{u}),
  Ordinal.veblenWith f o =
    if o = 0 then f
    else
      Ordinal.derivFamily fun x =>
        match (motive := { x // x ∈ Set.Iio o } → Ordinal.{u} → Ordinal.{u}) x with
        | ⟨x, property⟩ => Ordinal.veblenWith f x
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- Permuting the rows and columns of a Hadamard matrix gives a Hadamard matrix.  -/
Matrix.IsHadamard.reindex : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : Semiring R] [inst_5 : StarRing R] {A : Matrix n n R} (e₁ e₂ : n ≃ m),
  A.IsHadamard → ((Matrix.reindex e₁ e₂) A).IsHadamard
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k k' : α}, (k == k') = true → m.getKey! k = m.getKey! k'
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `Continuous.sub` -/
Continuous.fun_sub : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Sub G]
  [ContinuousSub G] {f g : X → G}, Continuous f → Continuous g → Continuous fun i => f i - g i
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toWeakDualBCNN.congr_simp : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (μ μ_1 : MeasureTheory.FiniteMeasure Ω), μ = μ_1 → μ.toWeakDualBCNN = μ_1.toWeakDualBCNN
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_comap : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E)
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] (f : L →ₐ[F] E) (B : IntermediateField F L),
  (IntermediateField.comap f A).relrank B = A.relrank (IntermediateField.map f B)
-- Lean.Meta.Closure
Lean.Meta.Closure.State.visitedLevel : Lean.Meta.Closure.State → Lean.LevelMap Lean.Level
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB5StarOfSize_of_univLE : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C] [inst_2 : UnivLE.{w, w₂}]
  [inst_3 : UnivLE.{w', w₂'}] [CategoryTheory.AB5StarOfSize.{w₂, w₂', v, u} C],
  CategoryTheory.AB5StarOfSize.{w, w', v, u} C
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- Maps elements of `α` to their `n`-th successor, or none if no successor exists.
This should semantically behave like repeatedly applying `succ?`, but it might be more efficient.

`LawfulUpwardEnumerable` ensures the compatibility with `succ?`.

If no other implementation is provided in `UpwardEnumerable` instance, `succMany?` repeatedly
applies `succ?`.
 -/
Std.PRange.UpwardEnumerable.succMany? : {α : Type u} → [self : Std.PRange.UpwardEnumerable α] → ℕ → α → Option α
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.AffineCover.cover_I₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.AffineCover P X), 𝒰.cover.I₀ = 𝒰.I₀
-- Mathlib.CategoryTheory.GradedObject.Single
CategoryTheory.GradedObject.single_map_singleObjApplyIso_hom : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f j)
      (CategoryTheory.GradedObject.singleObjApplyIso j Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j X).hom f
-- Mathlib.LinearAlgebra.Lagrange
/-- Lagrange interpolation induces isomorphism between functions from `s`
and polynomials of degree less than `Fintype.card ι`.  -/
Lagrange.funEquivDegreeLT : {F : Type u_1} →
  [inst : Field F] →
    {ι : Type u_2} →
      [DecidableEq ι] → {s : Finset ι} → {v : ι → F} → Set.InjOn v ↑s → ↥(Polynomial.degreeLT F s.card) ≃ₗ[F] ↥s → F
-- Init.Data.BitVec.Bitblast
BitVec.udiv_intMin_of_msb_false : ∀ {w : ℕ} {x : BitVec w}, x.msb = false → x / BitVec.intMin w = 0#w
-- Mathlib.Analysis.Normed.Group.Bounded
Filter.HasBasis.cobounded_of_norm : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] {ι : Sort u_5} {p : ι → Prop} {s : ι → Set ℝ},
  Filter.atTop.HasBasis p s → (Bornology.cobounded E).HasBasis p fun i => norm ⁻¹' s i
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.isCasesAttrCandidate : Lean.Name → Bool → Lean.CoreM Bool
-- Mathlib.Analysis.Calculus.MeanValue
/-- If `f` has zero derivative on an open set, then `f` is locally constant on `s`.  -/
IsOpen.isOpen_inter_preimage_of_fderiv_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {s : Set E},
  IsOpen s → DifferentiableOn 𝕜 f s → Set.EqOn (fderiv 𝕜 f) 0 s → ∀ (t : Set G), IsOpen (s ∩ f ⁻¹' t)
-- Mathlib.Algebra.Group.Units.Equiv
MulEquiv.isUnit_map : ∀ {F : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : EquivLike F M N]
  [MulEquivClass F M N] (f : F) {x : M}, IsUnit (f x) ↔ IsUnit x
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.frobeniusRotationCoeff.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  {a₁ a₂ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0),
  WittVector.frobeniusRotationCoeff p ha₁ ha₂ 0 = WittVector.RecursionBase.solution p a₁ a₂
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.unop_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ≅ Y), f.unop.hom = f.hom.unop
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f) →
    ∀ {x : M} {y : N} {n : ℕ},
      f x ≡ y [SMOD I ^ n • ⊤] → ∃ x', x ≡ x' [SMOD I ^ n • ⊤] ∧ f x' ≡ y [SMOD I ^ (n + 1) • ⊤]