mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.HoldsForLocalization.localRingHom : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P) →
      (RingHom.HoldsForLocalization fun {R S} [CommRing R] [CommRing S] => P) →
        ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {p : Ideal R} [inst_2 : p.IsPrime] {q : Ideal S}
          [inst_3 : q.IsPrime] {f : R →+* S} (h : p = Ideal.comap f q), P f → P (Localization.localRingHom p q f h)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.toRingHom_mapRingEquiv`. -/
MonoidAlgebra.toRingHom_mapRangeRingEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (e : R ≃+* S), (MonoidAlgebra.mapRingEquiv M e).toRingHom = MonoidAlgebra.mapRingHom M ↑e
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.macro : Lean.Lsp.SemanticTokenType
-- Mathlib.Order.Iterate
Monotone.iterate_comp_le_of_le : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {β : Type u_2} {g : β → β} {h : β → α},
  Monotone f → f ∘ h ≤ h ∘ g → ∀ (n : ℕ), f^[n] ∘ h ≤ h ∘ g^[n]
-- Mathlib.CategoryTheory.Category.Basic
/-- A preliminary structure on the way to defining a category,
containing the data, but none of the axioms.  -/
CategoryTheory.CategoryStruct : Type u → Type (max u (v + 1))
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.associated_isSymm : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : CommSemiring S] [inst_6 : Algebra S R]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2] (Q : QuadraticMap R M N) (x y : M),
  (((QuadraticMap.associatedHom S) Q) x) y = (((QuadraticMap.associatedHom S) Q) y) x
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.closedCell_subset_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n),
  Topology.RelCWComplex.closedCell n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
-- Mathlib.Computability.PartrecCode
/-- Given a code `c` taking a pair as input, returns a code using `n` as the first argument to `c`.
 -/
Nat.Partrec.Code.curry : Nat.Partrec.Code → ℕ → Nat.Partrec.Code
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.snd.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCocone.snd φ =
    (CochainComplex.mappingCone.snd φ).leftShift (-1) (-1) CochainComplex.mappingCocone.snd._proof_1
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsClique.top : ∀ {α : Type u_1} (s : Set α), ⊤.IsClique s
-- Init.Data.ToString.Name
/-- Converts a name to a string.

- If `escape` is `true`, then escapes name components using `«` and `»` to ensure that
  those names that can appear in source files round trip.
  Names with number components, anonymous names, and names containing `»` might not round trip.
  Furthermore, "pseudo-syntax" produced by the delaborator, such as `_`, `#0` or `?u`, is not escaped.
- The optional `isToken` function is used when `escape` is `true` to determine whether more
  escaping is necessary to avoid parser tokens.
  The insertion algorithm works so long as parser tokens do not themselves contain `«` or `»`.
 -/
Lean.Name.toStringWithToken : Lean.Name → optParam Bool true → (String → Bool) → String
-- Mathlib.Topology.Gluing
TopCat.GlueData.ofOpenSubsets_toGlueData_V : ∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α)
  (i :
    { J := J, U := fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i),
          V := fun x j => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j),
          t := fun i j => TopCat.ofHom { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }, V_id := ⋯, t_id := ⋯,
          t_inter := ⋯, cocycle := ⋯ }.J ×
      { J := J, U := fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i),
          V := fun x j => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j),
          t := fun i j => TopCat.ofHom { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }, V_id := ⋯, t_id := ⋯,
          t_inter := ⋯, cocycle := ⋯ }.J),
  (TopCat.GlueData.ofOpenSubsets U).V i =
    (TopologicalSpace.Opens.toTopCat ((TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i.1))).obj
      ((TopologicalSpace.Opens.map (U i.1).inclusion').obj (U i.2))
-- Init.Data.Nat.Basic
Nat.lt_sub_of_add_lt : ∀ {a b c : ℕ}, a + b < c → a < c - b
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.IsStrictlySupportedOutside.isZero : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : HomologicalComplex C c'} {e : c.Embedding c'},
  K.IsStrictlySupportedOutside e → ∀ (i : ι), CategoryTheory.Limits.IsZero (K.X (e.f i))
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_ne_one : ∀ {α : Type u} [inst : One α] {a : α}, ↑a ≠ 1 ↔ a ≠ 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, m.contains a = false → m.getKey! a = default
-- Mathlib.Algebra.Module.Presentation.Tensor
/-- The tensor product of systems of linear equations.  -/
Module.Relations.tensor : {A : Type u} → [inst : CommRing A] → Module.Relations A → Module.Relations A → Module.Relations A
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.diag_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Functor.diag C) X Y =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Functor.diag C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
-- Std.Data.DTreeMap.Internal.Def
/-- Flattens a tree into a list of key-value pairs. This function is defined for verification
purposes and should not be executed because it is very inefficient.
 -/
Std.DTreeMap.Internal.Impl.toListModel : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → List ((a : α) × β a)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_le_iSup_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal),
  ∫⁻ (x : α), f x ∂μ ≤ (⨆ x, f x) * μ Set.univ
-- Mathlib.Data.ENNReal.Action
ENNReal.nnreal_smul_lt_top : ∀ {x : NNReal} {y : ENNReal}, y < ⊤ → x • y < ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_inl_pushoutRightPushoutInlIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)] {Z_1 : C}
  (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp f f') g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f' (CategoryTheory.Limits.pushout.inl f g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutRightPushoutInlIso f g f').hom h)) =
    CategoryTheory.CategoryStruct.comp f'
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp f f') g) h)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.isMatcherCore : Lean.Environment → Lean.Name → Bool
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instSeminormedRing : {α : Type u} →
  [inst : TopologicalSpace α] →
    {R : Type u_1} → [inst_1 : SeminormedRing R] → SeminormedRing (BoundedContinuousFunction α R)
-- Mathlib.Topology.Instances.ENat
Continuous.enatSub : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f g : X → ℕ∞},
  Continuous f → Continuous g → (∀ (x : X), f x ≠ ⊤ ∨ g x ≠ ⊤) → Continuous fun x => f x - g x
-- Mathlib.Order.UpperLower.Basic
isLowerSet_preimage_toDual_iff : ∀ {α : Type u_1} [inst : LE α] {s : Set αᵒᵈ}, IsLowerSet (⇑OrderDual.toDual ⁻¹' s) ↔ IsUpperSet s
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
AddAction.is_zero_pretransitive : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {n : Type u_5} [IsEmpty n],
  AddAction.IsPretransitive G (n ↪ α)
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_srem : ∀ (a b : BitVec 16), Int16.ofBitVec (a.srem b) = Int16.ofBitVec a % Int16.ofBitVec b
-- Mathlib.Topology.SeparatedMap
isSeparatedMap_iff_isClosed_diagonal : ∀ {X : Type u_1} {Y : Sort u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsSeparatedMap f ↔ IsClosed (Function.pullbackDiagonal f)
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.piCongrLeft_apply : ∀ {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A₁ i)]
  [inst_2 : (i : ι) → Algebra R (A₁ i)] {ι' : Type u_8} (e : ι' ≃ ι) (x : (i : ι') → A₁ (e i)),
  (AlgEquiv.piCongrLeft R A₁ e) x = (Equiv.piCongrLeft A₁ e) x
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_eq_of_subset_left : ∀ {α : Type u_1} (t : Set α) {s₁ s₂ : Set α}, s₁ ⊆ s₂ → t.ite s₁ s₂ = s₁ ∪ s₂ \ t
-- Mathlib.Topology.Constructions
/-- A type synonym equipped with the topology whose open sets are the empty set and the sets with
finite complements.  -/
CofiniteTopology : Type u_5 → Type u_5
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_map_restrict' : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {I : Set ι},
  MeasureTheory.Measure.map I.domRestrict (MeasureTheory.Measure.infinitePi μ) =
    MeasureTheory.Measure.infinitePi fun i => μ ↑i
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.isUniformSpace : (self : CpltSepUniformSpace) → UniformSpace self.α
-- Mathlib.Order.Category.Preord
/-- The type of morphisms in `Preord R`.  -/
Preord.Hom : Preord → Preord → Type u
-- Mathlib.Topology.MetricSpace.IsometricSMul
Multiplicative.isIsometricSMul' : ∀ {M : Type u} [inst : Add M] [inst_1 : PseudoEMetricSpace M] [IsIsometricVAdd M M],
  IsIsometricSMul (Multiplicative M) (Multiplicative M)
-- Mathlib.Algebra.Field.Basic
div_add' : ∀ {K : Type u_1} [inst : DivisionSemiring K] (a b c : K), c ≠ 0 → a / c + b = (a + b * c) / c
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_mem_span_T : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.Chebyshev.U R ↑n ∈ Submodule.span ℕ ((fun m => Polynomial.Chebyshev.T R ↑m) '' Set.Icc 0 n)
-- Mathlib.Order.SupIndep
Finset.supIndep_iff_pairwiseDisjoint : ∀ {α : Type u_1} {ι : Type u_3} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  s.SupIndep f ↔ (↑s).PairwiseDisjoint f
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.DoIfView.optIdent : Lean.Elab.Term.Do.DoIfView → Lean.Syntax
-- Mathlib.CategoryTheory.Category.Pairwise
/-- Auxiliary definition for `diagram`.  -/
CategoryTheory.Pairwise.diagramObj : {ι : Type v} → {α : Type u} → (ι → α) → [SemilatticeInf α] → CategoryTheory.Pairwise ι → α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.bin.sizeOf_spec : ∀ {w : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr w) (op : Std.Tactic.BVDecide.BVBinPred)
  (rhs : Std.Tactic.BVDecide.BVExpr w),
  sizeOf (Std.Tactic.BVDecide.BVPred.bin lhs op rhs) = 1 + sizeOf w + sizeOf lhs + sizeOf op + sizeOf rhs
-- Init.Data.Array.Range
Array.range'_succ : ∀ {s n step : ℕ}, Array.range' s (n + 1) step = #[s] ++ Array.range' (s + step) n step
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace δ] {f : α → β} {g : γ → δ},
  Measurable f → Measurable g → Measurable (Prod.map f g)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.boundaryPoint_inr : ∀ {𝕜 : 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] {M' : Type u_5} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] (x : M'), I.IsBoundaryPoint x → I.IsBoundaryPoint (Sum.inr x)
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.bif_eq_bif : ∀ {w : ℕ} (d : Bool) (a b c : BitVec w), ((bif d then a else b) == bif d then a else c) = (d || b == c)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_equiv_eq_comap_symm : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G ≃+ N) (K : AddSubgroup G),
  AddSubgroup.map (↑f) K = AddSubgroup.comap (↑f.symm) K
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.Extension.isEMatchTheorem : Lean.Meta.Grind.Extension → Lean.Name → Lean.CoreM Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.I_le_monomorphisms : SSet.modelCategoryQuillen.I ≤ CategoryTheory.MorphismProperty.monomorphisms SSet
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instCommRing : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalCommRing A] →
        [inst_2 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → CommRing (Unitization R A)
-- Mathlib.Algebra.Order.Field.Basic
mul_sub_mul_div_mul_neg_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {a b c d : α},
  c ≠ 0 → d ≠ 0 → ((a * d - b * c) / (c * d) < 0 ↔ a / c < b / d)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.neighborSet_comap : ∀ {V : Type u_1} {W : Type u_2} (G' : SimpleGraph W) (f : V → W) (v : V),
  (SimpleGraph.comap f G').neighborSet v = f ⁻¹' G'.neighborSet (f v)
-- Mathlib.Algebra.Category.MonCat.Adjunctions
/-- The free-forgetful adjunction for commutative monoids.  -/
AddCommMonCat.adj : AddCommMonCat.free ⊣ CategoryTheory.forget AddCommMonCat
-- Mathlib.Topology.MetricSpace.Bounded
Metric.diam_triple : ∀ {α : Type u} {x y z : α} [inst : PseudoMetricSpace α],
  Metric.diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.of_div_right : ∀ {α : Type u_2} [inst : Div α] {s t : Set α}, (s / t).Nonempty → t.Nonempty
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
add_lt_add_iff_of_le_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α] [AddLeftMono α] [AddRightMono α] [AddLeftStrictMono α]
  [AddRightStrictMono α] {a₁ a₂ b₁ b₂ : α}, a₁ ≤ a₂ → b₁ ≤ b₂ → (a₁ + b₁ < a₂ + b₂ ↔ a₁ < a₂ ∨ b₁ < b₂)
-- Mathlib.Topology.UnitInterval
unitInterval.symm_one : unitInterval.symm 1 = 0
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticOnNhd.eval_linearMap' : ∀ {𝕜 : Type u_1} {E : Type u_2} {B : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedCommRing B] [inst_4 : NormedAlgebra 𝕜 B] {σ : Type u_5} [CompleteSpace 𝕜]
  [T2Space E] [FiniteDimensional 𝕜 E] (f : σ → E →ₗ[𝕜] B) (p : MvPolynomial σ B),
  AnalyticOnNhd 𝕜 (fun x => (MvPolynomial.eval fun x_1 => (f x_1) x) p) Set.univ
-- Init.Data.List.Lemmas
List.reverse_inj : ∀ {α : Type u_1} {xs ys : List α}, xs.reverse = ys.reverse ↔ xs = ys
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.Const.alter t k f) k' =
        if cmp k k' = Ordering.eq then f (Std.DTreeMap.Raw.Const.get? t k) else Std.DTreeMap.Raw.Const.get? t k'
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_comp_rTensor : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Submodule R S}
  (N : Submodule R S) {M' : Submodule R S} (hM : M' ≤ M),
  M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (Submodule.inclusion hM) = M'.mulMap N
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_lt_four : Real.pi < 4
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.coe_pos_real_smul : ∀ (x : { x // 0 < x }) (z : UpperHalfPlane), ↑(x • z) = ↑x • ↑z
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- Bird's equation (2), assuming equation (1) at `p` as the induction hypothesis.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.paper_eq2 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) {p : ℕ} (i : Fin n),
  BirdDet.Eq1✝ A p →
    -∑ k > i, (BirdDet.Spec.stepEntry A)^[p] A k k = (-1) ^ (p + 1) * ∑ α ∈ BirdDet.S✝ (p + 1) i, BirdDet.pminor✝ A α
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
integralClosure_le_span_dualBasis : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  {L : Type u_3} [inst_4 : Field L] [inst_5 : Algebra K L] [inst_6 : Algebra A L] [IsScalarTower A K L]
  [inst_8 : FiniteDimensional K L] [inst_9 : Algebra.IsSeparable K L] {ι : Type u_5} [inst_10 : Finite ι]
  [inst_11 : DecidableEq ι] (b : Module.Basis ι K L),
  (∀ (i : ι), IsIntegral A (b i)) →
    ∀ [IsIntegrallyClosed A],
      Subalgebra.toSubmodule (integralClosure A L) ≤
        Submodule.span A (Set.range ⇑((Algebra.traceForm K L).dualBasis ⋯ b))
-- Lean.Expr
/-- Return `true` if `e` is of the form `autoParam _ _`  -/
Lean.Expr.isAutoParam : Lean.Expr → Bool
-- Init.Data.ByteArray.Lemmas
ByteArray.data_empty : ByteArray.empty.data = #[]
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.toSubspaceUnit_apply : ∀ {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line α ι) (a : Unit → α), ↑l.toSubspaceUnit a = ↑l (a ())
-- Std.Http.Protocol.H1.Parser
/-- Shared core for request-line parsing: parses `request-target SP HTTP-version CRLF`
and returns the `RequestTarget` together with the raw major/minor version numbers.

Both `parseRequestLine` and `parseRequestLineRawVersion` call this after consuming
the method token, keeping URI validation and version parsing in one place.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseRequestLineBody : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser (Std.Http.RequestTarget × ℕ × ℕ)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.mk : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} →
              (I : Type u) →
                (s : I → M.sections) →
                  autoParam (CategoryTheory.Epi (M.freeHomEquiv.symm s))
                      SheafOfModules.GeneratingSections.epi._autoParam →
                    M.GeneratingSections
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.isUnit_algebraMap_end_of_le_basicOpen : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {U : (AlgebraicGeometry.Spec R).Opens} (f : ↑R),
  U ≤ PrimeSpectrum.basicOpen f → IsUnit ((algebraMap (↑R) (Module.End ↑R ↑(M.presheaf.obj (Opposite.op U)))) f)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.isoSum_hom_app_inr : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor (A ⊕ B) C) (b : B),
  F.isoSum.hom.app (Sum.inr b) = CategoryTheory.CategoryStruct.id (F.obj (Sum.inr b))
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.natAbs_valMinAbs_eq_natAbs_valMinAbs : ∀ {n : ℕ} {a b : ZMod n}, a.valMinAbs.natAbs = b.valMinAbs.natAbs ↔ a = b ∨ a = -b
-- Mathlib.Order.BooleanGenerators
IsCompactlyGenerated.BooleanGenerators.sSup_inter : ∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α} [IsCompactlyGenerated α],
  IsCompactlyGenerated.BooleanGenerators S → ∀ {T₁ T₂ : Set α}, T₁ ⊆ S → T₂ ⊆ S → sSup (T₁ ∩ T₂) = sSup T₁ ⊓ sSup T₂
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldr_loop : ∀ {n : ℕ} {α : Sort u_1} {i : ℕ} (f : Fin (n + 1) → α → α) (x : α) (h : i + 1 ≤ n + 1),
  Fin.foldr.loop (n + 1) f (i + 1) h x = f 0 (Fin.foldr.loop n (fun j => f j.succ) i ⋯ x)
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.toPrecoverage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.Pretopology C → CategoryTheory.Precoverage C
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.equivDirectSum_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (a : TensorAlgebra R M), TensorAlgebra.equivDirectSum a = TensorAlgebra.toDirectSum a
-- Init.Data.Stream
Std.ToStream.toStream : {collection : Type u} → {stream : outParam (Type u)} → [self : Std.ToStream collection stream] → collection → stream
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterStep.successor.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3) (it : α) (out : β)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it out with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_1 it out
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.forgetAdjStar.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C],
  CategoryTheory.Over.forgetAdjStar X =
    (CategoryTheory.coalgebraEquivOver X).symm.toAdjunction.comp (CategoryTheory.prodComonad X).adj
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.Term.listDecode.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_2} →
    (motive : List (α ⊕ (i : ℕ) × L.Functions i) → Sort u_4) →
      (x : List (α ⊕ (i : ℕ) × L.Functions i)) →
        (Unit → motive []) →
          ((a : α) → (l : List (α ⊕ (i : ℕ) × L.Functions i)) → motive (Sum.inl a :: l)) →
            ((n : ℕ) → (f : L.Functions n) → (l : List (α ⊕ (i : ℕ) × L.Functions i)) → motive (Sum.inr ⟨n, f⟩ :: l)) →
              motive x
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_graphOn : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : CommGroup β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (x : α × β) (s : Set α) (f : F),
  x • Set.graphOn (⇑f) s = Set.graphOn (fun a => x.2 / f x.1 * f a) (x.1 • s)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a (b + p) = toIocMod hp a b
-- Mathlib.Data.Multiset.Fintype
Multiset.coeEquiv_symm_apply_fst : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α) (x : ↥m.toEnumFinset), (m.coeEquiv.symm x).fst = (↑x).1