mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.skip?_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy) {pos : s.Pos},
  pos.skip? pat = Option.map (fun x => x.cast ⋯) ((pos.cast hst).skip? pat)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instAdd : (R : Type u_1) → (X : Type u_2) → [inst : CommSemiring R] → Add (FreeAlgebra R X)
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.stdSimplex.subcomplex_hasDimensionLT_of_neq_top : ∀ {n : ℕ} (A : (SSet.stdSimplex.obj { len := n }).Subcomplex), A ≠ ⊤ → A.toSSet.HasDimensionLT n
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1IsoOfIsTrivial.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  groupCohomology.H1IsoOfIsTrivial A =
    (HomologicalComplex.isoHomologyπ (groupCohomology.inhomogeneousCochains A) 0 1
          groupCohomology.H1IsoOfIsTrivial._proof_2 ⋯).symm ≪≫
      groupCohomology.isoCocycles₁ A ≪≫ groupCohomology.cocycles₁IsoOfIsTrivial A
-- Mathlib.Algebra.Category.Grp.Zero
CommGrpCat.isZero_of_subsingleton : ∀ (G : CommGrpCat) [Subsingleton ↑G], CategoryTheory.Limits.IsZero G
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : CompactSpace G] [inst_3 : ContinuousAdd G]
  (H : OpenNormalAddSubgroup G),
  H.toFiniteIndexNormalAddSubgroup = FiniteIndexNormalAddSubgroup.ofAddSubgroup ↑H.toOpenAddSubgroup
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- The additive submonoid generated by an element is
an additive group if that element has finite order.  -/
AddSubmonoid.addGroupMultiples : {M : Type u_1} → [inst : AddMonoid M] → {x : M} → {n : ℕ} → 0 < n → n • x = 0 → AddGroup ↥(AddSubmonoid.multiples x)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.instFunLike.eq_1 : ∀ (M : Type u_4) [inst : AddZero M],
  AddMonoid.End.instFunLike M = { coe := AddMonoid.End.instFunLike._aux_1 M, coe_injective := ⋯ }
-- Lean.Elab.Tactic.RCases
/-- Convert a list of patterns to an alternation pattern, but mapping `[p]` to `p` instead of
a unary alternation `|p`.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.alts' : Lean.Syntax → List Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Elab.Tactic.RCases.RCasesPatt
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticWith.mk.inj : ∀ {α : Type} {range : Lean.Lsp.Range} {fullRange? : Option Lean.Lsp.Range}
  {severity? : Option Lean.Lsp.DiagnosticSeverity} {isSilent? : Option Bool} {code? : Option Lean.Lsp.DiagnosticCode}
  {source? : Option String} {message : α} {tags? : Option (Array Lean.Lsp.DiagnosticTag)}
  {leanTags? : Option (Array Lean.Lsp.LeanDiagnosticTag)}
  {relatedInformation? : Option (Array Lean.Lsp.DiagnosticRelatedInformation)} {data? : Option Lean.Json}
  {range_1 : Lean.Lsp.Range} {fullRange?_1 : Option Lean.Lsp.Range} {severity?_1 : Option Lean.Lsp.DiagnosticSeverity}
  {isSilent?_1 : Option Bool} {code?_1 : Option Lean.Lsp.DiagnosticCode} {source?_1 : Option String} {message_1 : α}
  {tags?_1 : Option (Array Lean.Lsp.DiagnosticTag)} {leanTags?_1 : Option (Array Lean.Lsp.LeanDiagnosticTag)}
  {relatedInformation?_1 : Option (Array Lean.Lsp.DiagnosticRelatedInformation)} {data?_1 : Option Lean.Json},
  { range := range, fullRange? := fullRange?, severity? := severity?, isSilent? := isSilent?, code? := code?,
        source? := source?, message := message, tags? := tags?, leanTags? := leanTags?,
        relatedInformation? := relatedInformation?, data? := data? } =
      { range := range_1, fullRange? := fullRange?_1, severity? := severity?_1, isSilent? := isSilent?_1,
        code? := code?_1, source? := source?_1, message := message_1, tags? := tags?_1, leanTags? := leanTags?_1,
        relatedInformation? := relatedInformation?_1, data? := data?_1 } →
    range = range_1 ∧
      fullRange? = fullRange?_1 ∧
        severity? = severity?_1 ∧
          isSilent? = isSilent?_1 ∧
            code? = code?_1 ∧
              source? = source?_1 ∧
                message = message_1 ∧
                  tags? = tags?_1 ∧
                    leanTags? = leanTags?_1 ∧ relatedInformation? = relatedInformation?_1 ∧ data? = data?_1
-- Mathlib.Data.ZMod.Basic
ZMod.ringEquivCongr_intCast : ∀ {a b : ℕ} (h : a = b) (z : ℤ), (ZMod.ringEquivCongr h) ↑z = ↑z
-- Mathlib.Order.ModularLattice
covBy_sup_of_inf_covBy_right : ∀ {α : Type u_1} [inst : Lattice α] [IsUpperModularLattice α] {a b : α}, a ⊓ b ⋖ b → a ⋖ a ⊔ b
-- Std.Data.ExtDHashMap.Lemmas
_private.Std.Data.ExtDHashMap.Lemmas.0.Std.ExtDHashMap.lift.eq_1 : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {γ : Sort w} (f : Std.DHashMap α β → γ)
  (h : ∀ (a b : Std.DHashMap α β), a.Equiv b → f a = f b) (m : Std.ExtDHashMap α β),
  Std.ExtDHashMap.lift f h m = Quotient.lift f h m.inner
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.antidiagonal.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  (hs : s.IsPWO) (ht : t.IsPWO) (a : α), Finset.antidiagonal hs ht a = ⋯.toFinset
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.toIdeal_homogeneousCore_le : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  (I : Ideal A), (Ideal.homogeneousCore 𝒜 I).toIdeal ≤ I
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
/-- Every left pre-Lie ring is a right pre-Lie ring with the opposite multiplication  -/
LeftPreLieRing.instRightPreLieRingMulOpposite : {L : Type u_2} → [LeftPreLieRing L] → RightPreLieRing Lᵐᵒᵖ
-- Mathlib.Data.Nat.Bitwise
Nat.two_pow_and : ∀ (n i : ℕ), 2 ^ i &&& n = 2 ^ i * (n.testBit i).toNat
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_eq_zero : ∀ {R : Type u} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₂] [inst_2 : Algebra R S₂]
  (f : σ → S₂) (φ : MvPolynomial σ R),
  (∀ (d : σ →₀ ℕ), MvPolynomial.coeff d φ ≠ 0 → ∃ i ∈ d.support, f i = 0) → (MvPolynomial.aeval f) φ = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → {aig : Std.Sat.AIG α} → aig.RefVec w → ℕ → (curr : ℕ) → curr ≤ w → aig.RefVec curr → aig.RefVec w
-- Mathlib.Data.Nat.Factors
/-- For coprime `a` and `b`, the prime factors of `a * b` are the union of those of `a` and `b`  -/
Nat.perm_primeFactorsList_mul_of_coprime : ∀ {a b : ℕ}, a.Coprime b → (a * b).primeFactorsList.Perm (a.primeFactorsList ++ b.primeFactorsList)
-- Mathlib.CategoryTheory.Adjunction.Quadruple
/-- Adjunction `G ⊣ R` of the adjoint quadruple `L ⊣ F ⊣ G ⊣ R`.  -/
CategoryTheory.Adjunction.Quadruple.adj₃ : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {F : CategoryTheory.Functor D C} →
            {G : CategoryTheory.Functor C D} →
              {R : CategoryTheory.Functor D C} → CategoryTheory.Adjunction.Quadruple L F G R → (G ⊣ R)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdSndIsoProd_inv_fst_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X]
  [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f] {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.prod.snd f)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h)) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
AddEquiv.toContinuousAddEquiv_apply : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Add G] [inst_3 : Add H]
  (e : G ≃+ H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (a : G), (e.toContinuousAddEquiv he) a = e a
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
fn_min_mul_fn_max : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : CommSemigroup β] (f : α → β) (a b : α),
  f (min a b) * f (max a b) = f a * f b
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_div : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Div β] (f g : MeasureTheory.SimpleFunc α β),
  ⇑(f / g) = ⇑f / ⇑g
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_pow_mul_of_not_dvd : ∀ {m : ℕ} (k : ℕ) {p : ℕ}, Nat.Prime p → ¬p ∣ m → p ^ k * m / p ^ (p ^ k * m).factorization p = m
-- Aesop.Forward.State
Aesop.RuleState.mk.sizeOf_spec : ∀ (rule : Aesop.ForwardRule) (clusterStates : Array Aesop.ClusterState)
  (patSubstSources : Lean.PHashMap Aesop.Substitution (Lean.PHashSet Aesop.PatSubstSource)),
  sizeOf { rule := rule, clusterStates := clusterStates, patSubstSources := patSubstSources } =
    1 + sizeOf rule + sizeOf clusterStates + sizeOf patSubstSources
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.MakesOverArrow.of_yoneda_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  {η : CategoryTheory.yoneda.obj Y ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {f : X ⟶ Y},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s →
    CategoryTheory.OverPresheafAux.MakesOverArrow η s f
-- Mathlib.CategoryTheory.GradedObject.Braiding
CategoryTheory.GradedObject.Monoidal.symmetry : ∀ {I : Type u_1} [inst : AddCommMonoid I] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X Y : CategoryTheory.GradedObject I C)
  [inst_3 : CategoryTheory.SymmetricCategory C] [inst_4 : X.HasTensor Y] [inst_5 : Y.HasTensor X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding X Y).hom
      (CategoryTheory.GradedObject.Monoidal.braiding Y X).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.GradedObject.Monoidal.tensorObj X Y)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
/-- Assume that `colim : (J ⥤ C) ⥤ C` preserves monomorphisms, and
`φ : X₁ ⟶ X₂` is a monomorphism in `J ⥤ C`, then if `f : c₁.pt ⟶ c₂.pt` is a morphism
between the points of colimit cocones for `X₁` and `X₂` in such a way that `f`
identifies to `colim.map φ`, then `f` is a monomorphism.  -/
CategoryTheory.Limits.colim.map_mono' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.colim.PreservesMonomorphisms]
  {X₁ X₂ : CategoryTheory.Functor J C} (φ : X₁ ⟶ X₂) [CategoryTheory.Mono φ] {c₁ : CategoryTheory.Limits.Cocone X₁}
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) {c₂ : CategoryTheory.Limits.Cocone X₂}
  (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt),
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f = CategoryTheory.CategoryStruct.comp (φ.app j) (c₂.ι.app j)) →
    CategoryTheory.Mono f
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withBot_id : ∀ {α : Type u_1} [inst : Lattice α], (LatticeHom.id α).withBot = LatticeHom.id (WithBot α)
-- Init.Data.Nat.Lemmas
Nat.one_mod_two_pow_eq_one : ∀ {n : ℕ}, 1 % 2 ^ n = 1 ↔ 0 < n
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_eq_zero_of_ae_zero' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε],
  q ≠ 0 → μ ≠ 0 → ∀ {f : α → ε}, f =ᵐ[μ] 0 → MeasureTheory.eLpNorm' f q μ = 0
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.congr_of_forall : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P → ∀ {s : Set H} {x : H} {f g : H → H'}, (∀ y ∈ s, f y = g y) → f x = g x → P f s x → P g s x
-- Mathlib.Data.Finset.SDiff
Finset.subset_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u
-- Init.Data.List.Impl
/-- Returns the longest initial segment of `xs` for which `p` returns true.

`O(|xs|)`. This is a tail-recursive version of `List.take`, used at runtime.

Examples:
* `[7, 6, 4, 8].takeWhileTR (· > 5) = [7, 6]`
* `[7, 6, 6, 5].takeWhileTR (· > 5) = [7, 6, 6]`
* `[7, 6, 6, 8].takeWhileTR (· > 5) = [7, 6, 6, 8]`
 -/
List.takeWhileTR : {α : Type u_1} → (α → Bool) → List α → List α
-- Mathlib.Topology.Algebra.Localization
instIsTopologicalRingLocalization : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] {M : Submonoid R}, IsTopologicalRing (Localization M)
-- Init.Data.Option.Lemmas
Option.isNone_guard : ∀ {α : Type u_1} {p : α → Bool} {a : α}, (Option.guard p a).isNone = !p a
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trTape'.eq_1 : ∀ {Γ : Type u_1} {n : ℕ} {enc : Γ → List.Vector Bool n} [inst : Inhabited Γ]
  (enc0 : enc default = List.Vector.replicate n false) (L R : Turing.ListBlank Γ),
  Turing.TM1to1.trTape' enc0 L R =
    Turing.Tape.mk' (L.flatMap (fun x => (enc x).toList.reverse) ⋯) (R.flatMap (fun x => (enc x).toList) ⋯)
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_subset_sdiff_iff_subset : ∀ {α : Type u_1} {s t r : Set α}, s ⊆ r → t ⊆ r → (r \ s ⊆ r \ t ↔ t ⊆ s)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.interface : Lean.Lsp.CompletionItemKind
-- Std.Http.Data.Headers
Std.Http.Headers.mk : Std.Internal.IndexMultiMap Std.Http.Header.Name Std.Http.Header.Value → Std.Http.Headers
-- Mathlib.Data.FunLike.IsApply
/-- `IsMulApplyEqComp F α α` states for all `x : α`, `(f * g) x = f (g x)`.  -/
IsMulApplyEqComp : (F : Type u_1) → (α : outParam (Type u_2)) → [FunLike F α α] → [Mul F] → Prop
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.absolutelyContinuous_posterior_iff : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧],
  (∀ᵐ (b : 𝓧) ∂μ.bind ⇑κ, ((ProbabilityTheory.posterior κ μ) b).AbsolutelyContinuous μ) ↔
    ∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCallsParams.mk.inj : ∀ {item item_1 : Lean.Lsp.CallHierarchyItem}, { item := item } = { item := item_1 } → item = item_1
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_eq_fallback : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, a ∉ m → m.getKeyD a fallback = fallback
-- Mathlib.Order.Hom.Order
OrderHom.sInf_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : CompleteLattice β] (s : Set (α →o β)) (x : α),
  (sInf s) x = ⨅ f ∈ s, f x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.subst : Lean.Grind.Linarith.Var →
  Lean.Meta.Grind.Arith.Linear.EqCnstr →
    Lean.Meta.Grind.Arith.Linear.EqCnstr → Lean.Meta.Grind.Arith.Linear.EqCnstrProof
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.instHasInitialLeftLiftOfHasLeftKanLift : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [CategoryTheory.Bicategory.HasLeftKanLift f g],
  CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftLift f g)
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.covariance_eval : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P → ∀ (s t : NNReal), ProbabilityTheory.covariance (B s) (B t) P = ↑(min s t)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.type : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Lean.Expr
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.over_eq_inverseImage : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] (W : CategoryTheory.MorphismProperty T) (X : T),
  W.over = W.inverseImage (CategoryTheory.Over.forget X)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.seq_zero : ∀ {α β : Type u} (f : FreeAbelianGroup (α → β)), f <*> 0 = 0
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.recursive : Lean.Meta.RecursorInfo → Bool
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If G preserves coequalizers and coproducts, it preserves all colimits.  -/
CategoryTheory.Limits.preservesColimits_of_preservesCoequalizers_and_coproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Limits.HasCoproducts C] (G : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G]
  [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) G],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w, v, v₂, u, u₂} G
-- Std.Internal.Do.ExceptPost
/-- The head component of the bottom `EPost.Cons` is the bottom element. Propositional (not
definitional), because `⊥` of a complete lattice is `csup ∅`, not a constructor application.  -/
Std.Internal.Do.EPost.Cons.head_bot : ∀ {eh : Type u} {et : Type v} [inst : Lean.Order.CompleteLattice eh] [inst_1 : Lean.Order.CompleteLattice et],
  Lean.Order.bot.head = Lean.Order.bot
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
  Std.DTreeMap.Internal.Impl.containsThenInsert k v t hl =
    (Std.DTreeMap.Internal.Impl.containsThenInsert.size t == (Std.DTreeMap.Internal.Impl.insert k v t hl).impl.size,
      Std.DTreeMap.Internal.Impl.insert k v t hl)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- A face of a cone is an extreme subset of the cone.  -/
PointedCone.IsFaceOf.isExtreme : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M}, F.IsFaceOf C → IsExtreme R ↑C ↑F
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_add_emod : ∀ (m n k : ℤ), (m % n + k) % n = (m + k) % n
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
/-- The bilinear form of a finite root pairing taking values in a linearly-ordered ring, as a
root-positive form.  -/
RootPairing.posRootForm : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (P : RootPairing ι R M N) →
                    (S : Type u_5) →
                      [inst_5 : CommRing S] →
                        [inst_6 : LinearOrder S] →
                          [IsStrictOrderedRing S] →
                            [inst_8 : Algebra S R] →
                              [FaithfulSMul S R] →
                                [inst_10 : P.IsValuedIn S] → [Fintype ι] → RootPairing.RootPositiveForm S P
-- Init.Data.Int.DivMod.Lemmas
Int.one_emod : ∀ {b : ℤ}, 1 % b = if b.natAbs = 1 then 0 else 1
-- Mathlib.Order.SuccPred.InitialSeg
InitialSeg.isSuccLimit_apply_iff : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ≤i β),
  Order.IsSuccLimit (f a) ↔ Order.IsSuccLimit a
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.rs : Lean.Elab.Command.AddAndFinalizeContext✝ → Array Lean.Elab.Command.ElabHeaderResult
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_nonempty_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] {s : Finset α}, s⁻¹.Nonempty ↔ s.Nonempty
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.completeSpace_iff : ∀ {α : Type u_1} [inst : UniformSpace α], CompleteSpace (TopologicalSpace.Compacts α) ↔ CompleteSpace α
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- A variant of `id_toShHom'` that works with `𝟙 X` instead of `id X`.  -/
AlgebraicGeometry.LocallyRingedSpace.id_toShHom' : ∀ (X : AlgebraicGeometry.LocallyRingedSpace),
  AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id X.toSheafedSpace
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.map'_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] {f : α →* β}, Monotone ⇑f → Monotone ⇑(WithZero.map' f)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (n d : aig.RefVec w)
  (wn wr : ℕ) (q r : aig.RefVec w),
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r).aig.decls.size
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Rat.cast_det : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {F : Type u_3} [inst_2 : Field F] [CharZero F]
  (M : Matrix n n ℚ), ↑M.det = (M.map fun x => ↑x).det
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} {f_1 g : D₁ ⟶ D₂}, f_1 = g ↔ ∀ (i : ι), f_1.hom i = g.hom i
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.pentagon : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (W X Y Z : CategoryTheory.Dial C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
        (CategoryTheory.CategoryStruct.id Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W)
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitudeFoot_eq_point_rev : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : Affine.Simplex ℝ P 1) (i : Fin 2), s.altitudeFoot i = s.points i.rev