mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.valuation_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], PadicInt.valuation 1 = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.fromAffine_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [inst_1 : Nontrivial R] {X Y : R}
  (h : W'.toAffine.Nonsingular X Y),
  WeierstrassCurve.Jacobian.Point.fromAffine (WeierstrassCurve.Affine.Point.some X Y h) =
    { point := ⟦![X, Y, 1]⟧, nonsingular := ⋯ }
-- Mathlib.Topology.Separation.Basic
R1Space.sInf : ∀ {X : Type u_3} {T : Set (TopologicalSpace X)}, (∀ t ∈ T, R1Space X) → R1Space X
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- The proximity function is even.
 -/
ValueDistribution.proximity_even : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {a : WithTop E},
  Function.Even (ValueDistribution.proximity f a)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.nsmul : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → SMul ℕ (NormedAddGroupHom V₁ V₂)
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.mem_unitaryGroup_iff' : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  {A : Matrix n n α}, A ∈ Matrix.unitaryGroup n α ↔ star A * A = 1
-- Mathlib.RingTheory.DedekindDomain.Basic
/-- Make a Dedekind domain from a Dedekind ring given that it is a domain.

`IsDedekindRing` and `IsDedekindDomain` form a cycle in the typeclass hierarchy:
`IsDedekindRing R + IsDomain R` imply `IsDedekindDomain R`, which implies `IsDedekindRing R`.
This should be safe since the start and end point is the literal same expression,
which the tabled typeclass synthesis algorithm can deal with.
 -/
instIsDedekindDomainOfIsDomainOfIsDedekindRing : ∀ (A : Type u_2) [inst : CommRing A] [IsDomain A] [IsDedekindRing A], IsDedekindDomain A
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map : ∀ {X Y : SSet.Truncated 2}
  {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e : SSet.Truncated.Edge x₀ x₁)
  {y₀ y₁ : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e' : SSet.Truncated.Edge y₀ y₁),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.functor X Y).map
      (SSet.Truncated.HomotopyCategory.homMk (e.tensor e')) =
    (SSet.Truncated.HomotopyCategory.homMk e, SSet.Truncated.HomotopyCategory.homMk e')
-- Lean.Parser.Syntax
Lean.Parser.Command.infixl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_eq_zero : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {x : ↥S}, ↑x = 0 ↔ x = 0
-- Aesop.Script.ScriptM
Aesop.ScriptT : (Type → Type) → Type → Type
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_filterMap_le_size : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ}, (Std.TreeMap.filterMap f t).size ≤ t.size
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.ExtTreeSet.ofList l cmp).getD k fallback = fallback
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
/-- The short complex  `Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁) ⟶ Hⱼ(G, X₂)` associated to an exact sequence
of representations `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0`.  -/
groupHomology.mapShortComplex₁ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} →
        X.ShortExact → {i j : ℕ} → j + 1 = i → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.mem_blockTriangularSubsemiring : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {b : m → α} [inst : LinearOrder α] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : Semiring R] {M : Matrix m m R},
  M ∈ Matrix.blockTriangularSubsemiring R b ↔ M.BlockTriangular b
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.negFn? : Lean.Meta.Sym.Arith.Ring → Option Lean.Expr
-- Mathlib.MeasureTheory.OuterMeasure.OfAddContent
MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure : ∀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent ENNReal C)
  (s : Set α), MeasurableSet s → (MeasureTheory.inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯).IsCaratheodory s
-- Init.Data.List.Perm
_private.Init.Data.List.Perm.0.List.reverseAux.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (l r : List α) (h_1 : (r : List α) → motive [] r)
  (h_2 : (a : α) → (l r : List α) → motive (a :: l) r),
  (match a :: l, r with
    | [], r => h_1 r
    | a :: l, r => h_2 a l r) =
    h_2 a l r
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.BuiltinSimprocs.procs : Lean.Meta.Simp.BuiltinSimprocs → Std.HashMap Lean.Name (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.norm.eq_1 : ∀ {R : Type u_2} {a b : R} [inst : CommRing R],
  QuadraticAlgebra.norm =
    { toFun := fun z => z.re * z.re + b * z.re * z.im - a * z.im * z.im, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix.mk.sizeOf_spec : ∀ {n m : ℕ} (data : Array (Std.HashMap ℕ ℚ)), sizeOf { data := data } = 1 + sizeOf data
-- Mathlib.Topology.ContinuousMap.Algebra
/-- The `AddSubgroup` of continuous maps `α → β`.  -/
continuousAddSubgroup : (α : Type u_1) →
  (β : Type u_2) →
    [TopologicalSpace α] →
      [inst : TopologicalSpace β] → [inst_1 : AddGroup β] → [IsTopologicalAddGroup β] → AddSubgroup (α → β)
-- Lean.Meta.Tactic.Grind.Util
Lean.Meta.Grind.isMatchCond : Lean.Expr → Bool
-- Mathlib.Order.WithBot
WithTop.map_coe : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), WithTop.map f ↑a = ↑(f a)
-- Mathlib.Algebra.Ring.Parity
odd_two_mul_add_one : ∀ {α : Type u_2} [inst : Semiring α] (a : α), Odd (2 * a + 1)
-- Mathlib.RingTheory.Valuation.IsTrivialOn
Polynomial.valuation_aeval_monomial_eq_valuation_pow : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : CommSemiring A] {B : Type u_3}
  [inst_2 : Ring B] [inst_3 : Algebra A B] {v : Valuation B Γ} [hv : Valuation.IsTrivialOn A v] (w : B) (n : ℕ) {a : A},
  a ≠ 0 → v ((Polynomial.aeval w) ((Polynomial.monomial n) a)) = v w ^ n
-- Mathlib.NumberTheory.Padics.Measure.Topology
/-- The strong topology on `AbstractMeasure G R E` (the topology induced by the norm).  -/
AbstractMeasure.StrongTopology : {X : Type u_1} →
  {R : Type u_2} →
    {E : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : NontriviallyNormedField R] →
          [inst_2 : NormedAddCommGroup E] → [inst_3 : NormedSpace R E] → TopologicalSpace (AbstractMeasure X R E)
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type with `0` and negation is a `NegZeroClass` if `β` is a
`NegZeroClass`.  -/
FunLike.negZeroClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Zero F] →
          [inst_2 : Neg F] → [inst_3 : NegZeroClass β] → [IsZeroApply F α β] → [IsNegApply F α β] → NegZeroClass F
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.DischargeResult.notProved.sizeOf_spec : sizeOf Lean.Meta.Simp.DischargeResult.notProved = 1
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.ι_mapBifunctorAssociatorX_hom_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_8 : CategoryTheory.Limits.HasZeroMorphisms C₃] [inst_9 : CategoryTheory.Preadditive C₁₂]
  [inst_10 : CategoryTheory.Preadditive C₂₃] [inst_11 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_12 : F₁₂.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_14 : G.Additive]
  [inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [inst_16 : G₂₃.PreservesZeroMorphisms]
  [inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_18 : F.PreservesZeroMorphisms]
  [inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7}
  {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_20 : DecidableEq ι₄]
  {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃)
  (c₄ : ComplexShape ι₄) [inst_21 : TotalComplexShape c₁ c₂ c₁₂] [inst_22 : TotalComplexShape c₁₂ c₃ c₄]
  [inst_23 : TotalComplexShape c₂ c₃ c₂₃] [inst_24 : TotalComplexShape c₁ c₂₃ c₄], ⋯
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inv_aux : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] {f : CauSeq β abv},
  ¬f.LimZero → ∀ ε > 0, ∃ i, ∀ j ≥ i, abv ((↑f j)⁻¹ - (↑f i)⁻¹) < ε
-- Lean.Parser.Types
Lean.Parser.SyntaxStack.toSubarray : Lean.Parser.SyntaxStack → Subarray Lean.Syntax
-- Batteries.Data.List.Lemmas
List.ge_of_mem_findIdxs : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ}, ∀ y ∈ List.findIdxs p xs s, s ≤ y
-- Mathlib.Algebra.Order.Module.Defs
smul_neg_of_neg_of_pos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosStrictMono α β], a < 0 → 0 < b → a • b < 0
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_sq : ∀ (x : ℂ), Complex.cosh x ^ 2 = Complex.sinh x ^ 2 + 1
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
TopModuleCat.hom_cokerπ : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) (x : ↑N.toModuleCat),
  (TopModuleCat.Hom.hom (TopModuleCat.cokerπ φ)) x = (↑(TopModuleCat.Hom.hom φ)).range.mkQ x
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.δ_map_of_lt_assoc : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  (self : f.RelStruct g i),
  ∀ j < i.castSucc,
    ∀ {Z : SSet} (h : X ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) =
        CategoryTheory.CategoryStruct.comp (SSet.const x) h
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
/-- Let `G` be a complete nonarchimedean additive abelian group. Then a function
`f : α → G` is unconditionally summable if and only if it tends to zero on the filter of cofinite
sets.  -/
NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G]
  [NonarchimedeanAddGroup G] [CompleteSpace G] (f : α → G), Summable f ↔ Filter.Tendsto f Filter.cofinite (nhds 0)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- Equivalence of colorings induced by isomorphisms of graphs and equivalence of colors.  -/
SimpleGraph.coloringCongr : {V : Type u} →
  {G : SimpleGraph V} →
    {α : Type u_2} →
      {β : Type u_3} → {W : Type u_4} → {H : SimpleGraph W} → G ≃g H → α ≃ β → G.Coloring α ≃ H.Coloring β
-- Mathlib.Order.Basic
PUnit.instLinearOrder : LinearOrder PUnit.{u_5 + 1}
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.isCandidateSymbol : Lean.Name → Bool → Lean.Meta.Grind.NormalizePattern.M✝ Bool
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
/-- The regular sheaf condition on an essentially small site can be checked after precomposing with
the equivalence with a small category.
 -/
CategoryTheory.Equivalence.preregular_isSheaf_iff_of_essentiallySmall : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C] (A : Type u_3)
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] [inst_3 : CategoryTheory.EssentiallySmall.{u_4, v_1, u_1} C]
  (F : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F ↔
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology (CategoryTheory.SmallModel.{u_4, v_1, u_1} C))
      ((CategoryTheory.equivSmallModel C).inverse.op.comp F)
-- Mathlib.Algebra.Ring.BooleanRing
toBoolAlg_add : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : α), toBoolAlg (a + b) = symmDiff (toBoolAlg a) (toBoolAlg b)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolAux.detail? : {Self : Type} → Lean.Lsp.DocumentSymbolAux Self → Option String
-- Std.Sat.AIG.Basic
/-- Given a `cache`, valid with respect to some `decls`, we can extend the `decls`
and the `cache` at the same time with the same values and remain valid.
 -/
Std.Sat.AIG.Cache.WF.push_cache : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {decls : Array (Std.Sat.AIG.Decl α)}
  {cache : Std.HashMap (Std.Sat.AIG.Decl α) ℕ} {decl : Std.Sat.AIG.Decl α},
  Std.Sat.AIG.Cache.WF decls cache → Std.Sat.AIG.Cache.WF (decls.push decl) (cache.insert decl decls.size)
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.uniformContinuous_fst : ∀ {R : Type u_3} {M : Type u_4} [inst : UniformSpace R] [inst_1 : UniformSpace M], UniformContinuous TrivSqZeroExt.fst
-- Std.Data.HashMap.Raw
/-- Returns `true` if the hash map contains no mappings.

Note that if your `BEq` instance is not reflexive or your `Hashable` instance is not
lawful, then it is possible that this function returns `false` even though is not possible
to get anything out of the hash map.
 -/
Std.HashMap.Raw.isEmpty : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → Bool
-- Mathlib.Topology.Algebra.ConstMulAction
MulAction.isOpenQuotientMap_quotientMk : ∀ {Γ : Type u_4} [inst : Group Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : MulAction Γ T]
  [ContinuousConstSMul Γ T], IsOpenQuotientMap (Quotient.mk (MulAction.orbitRel Γ T))
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.filterMap : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      ((a : α) → β a → Option (γ a)) → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α γ
-- Init.Data.AC
Lean.Data.AC.evalList.eq_1 : ∀ {α : Sort u_1} (β : Sort u) [inst : Lean.Data.AC.EvalInformation α β] (ctx : α),
  Lean.Data.AC.evalList β ctx [] = Lean.Data.AC.EvalInformation.arbitrary ctx
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restriction.hasHomology : ∀ {ι : 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') [inst_2 : e.IsRelIff] (i j k : ι),
  c.prev j = i →
    c.next j = k →
      ∀ {i' j' k' : ι'},
        e.f i = i' →
          e.f j = j' →
            e.f k = k' → c'.prev j' = i' → c'.next j' = k' → ∀ [K.HasHomology j'], (K.restriction e).HasHomology j
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.getDefInfoTemp : Lean.ConstantInfo → Lean.MetaM (Option Lean.ConstantInfo)
-- Batteries.Recycling.MonadSatisfying.Basic
MonadSatisfying.instOption : MonadSatisfying Option
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.integral_eval_projectiveFamily : ∀ (I : Finset NNReal) (s : ↥I), ∫ (x : ↥I → ℝ), x s ∂ProbabilityTheory.BrownianReal.projectiveFamily I = 0
-- Mathlib.Tactic.Ring.Basic
/-- Evaluate the product of two rational number expressions.  -/
Mathlib.Tactic.Ring.RingCompute.mul : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {a b : Q(«$α»)} →
        Mathlib.Tactic.Ring.RatCoeff a →
          Mathlib.Tactic.Ring.RatCoeff b →
            Lean.MetaM (Mathlib.Tactic.Ring.Common.Result Mathlib.Tactic.Ring.RatCoeff q(«$a» * «$b»))
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.length_filter_eq_length_iff : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {f : α → β → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst p.snd) l).length = l.length ↔
      ∀ (a : α) (h : Std.Internal.List.containsKey a l = true),
        f (Std.Internal.List.getKey a l h) (Std.Internal.List.getValue a l h) = true)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.mem_cycles₂_of_mem_boundaries₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G},
  ∀ x ∈ groupHomology.boundaries₂ A, x ∈ groupHomology.cycles₂ A
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_single_le : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ} {r : R},
  ↑a ≤ ((HahnSeries.single a) r).orderTop
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.mk.sizeOf_spec : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} [inst_10 : SizeOf R] [inst_11 : SizeOf G]
  [inst_12 : SizeOf V] [inst_13 : SizeOf W] (toContinuousLinearMap : V →L[R] W)
  (isIntertwining' : ∀ (g : G), toContinuousLinearMap ∘SL π₁ g = π₂ g ∘SL toContinuousLinearMap),
  sizeOf { toContinuousLinearMap := toContinuousLinearMap, isIntertwining' := isIntertwining' } =
    1 + sizeOf toContinuousLinearMap
-- Mathlib.Data.Nat.Factorization.LCM
Nat.factorizationLCMRight_pos : ∀ (a b : ℕ), 0 < a.factorizationLCMRight b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k a : α} {v : β},
  Std.ExtDHashMap.Const.get! (m.insertIfNew k v) a =
    if (k == a) = true ∧ k ∉ m then v else Std.ExtDHashMap.Const.get! m a
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piCongrRight_symm : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} {ψ : ι → Type u_2}
  [inst_1 : (i : ι) → AddCommMonoid (φ i)] [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : (i : ι) → AddCommMonoid (ψ i)]
  [inst_4 : (i : ι) → Module R (ψ i)] (e : (i : ι) → φ i ≃ₗ[R] ψ i),
  (LinearEquiv.piCongrRight e).symm = LinearEquiv.piCongrRight fun i => (e i).symm
-- Init.Data.Option.Lemmas
Option.pfilter_eq_pbind_ite : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool},
  o.pfilter p = o.pbind fun a h => if p a h = true then some a else none
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
integrally closed and Noetherian, the integral closure `C` of `A` in `L` is
Noetherian.  -/
IsIntegralClosure.isNoetherianRing : ∀ (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] (C : Type u_4) [inst_5 : CommRing C] [inst_6 : Algebra K L] [inst_7 : Algebra A L]
  [IsScalarTower A K L] [inst_9 : Algebra C L] [IsIntegralClosure C A L] [inst_11 : Algebra A C] [IsScalarTower A C L]
  [FiniteDimensional K L] [IsDomain A] [Algebra.IsSeparable K L] [IsIntegrallyClosed A] [IsNoetherianRing A],
  IsNoetherianRing C
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.univUnitBall_target : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  OpenPartialHomeomorph.univUnitBall.target = Metric.ball 0 1
-- Aesop.Stats.Report
Aesop.StatsReport : Type
-- Mathlib.Data.FunLike.IsApply
IsOneApply.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [inst : FunLike F α β] [inst_1 : One β]
  [inst_2 : One F], (∀ (x : α), 1 x = 1) → IsOneApply F α β
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.Unit_of_divided_by_X_pow_order.eq_1 : ∀ {k : Type u_2} [inst : Field k] (f : PowerSeries k),
  f.Unit_of_divided_by_X_pow_order =
    if hf : f = 0 then 1
    else { val := f.divXPowOrder, inv := PowerSeries.Inv_divided_by_X_pow_order hf, val_inv := ⋯, inv_val := ⋯ }
-- Init.Data.UInt.Bitwise
UInt32.neg_one_and : ∀ {a : UInt32}, -1 &&& a = a
-- Init.Data.List.Find
List.findIdx_eq_length : ∀ {α : Type u_1} {p : α → Bool} {xs : List α}, List.findIdx p xs = xs.length ↔ ∀ x ∈ xs, p x = false
-- Std.Http.Data.Request
/-- The HTTP protocol version for the request (e.g. HTTP/1.1, HTTP/2.0, HTTP/3.0).

Reference: https://httpwg.org/specs/rfc9112.html#http.version
 -/
Std.Http.Request.Head.version : Std.Http.Request.Head → Std.Http.Version
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntryD_eq_getD_maxEntry? : ∀ {α : Type u} {β : Type v} [Ord α] {l : Std.DTreeMap.Internal.Impl α fun x => β} {fallback : α × β},
  Std.DTreeMap.Internal.Impl.Const.maxEntryD l fallback = (Std.DTreeMap.Internal.Impl.Const.maxEntry? l).getD fallback
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.map_add : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] {X Y : C} {f g : X ⟶ Y},
  F.map (f + g) = F.map f + F.map g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- the first component of `f : Hom x y` is a morphism `x.fst ⟶ y.fst`  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.fst : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {X : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} →
                      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y → (x.fst ⟶ y.fst)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instMono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f], CategoryTheory.Mono f
-- Init.Data.List.Nat.TakeDrop
List.drop_set_of_lt : ∀ {α : Type u_1} {a : α} {i j : ℕ} {l : List α}, i < j → List.drop j (l.set i a) = List.drop j l
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_glueDataObjι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V),
  CategoryTheory.CategoryStruct.comp (I.glueDataObjMap h) (I.glueDataObjι V) =
    CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (X.homOfLE h)