mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.maxEntry!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxEntry! = t₂.maxEntry!
-- Mathlib.Data.Set.Constructions
/-- `inter_mem` states that any two intersections of sets in `S` is also in `S`.  -/
FiniteInter.inter_mem : ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
-- Lean.Meta.Sym.InstantiateS
/-- Internal variant of `instantiateRevBetaS` that runs in `AlphaShareBuilderM`.  -/
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.instantiateRevBetaS' : Lean.Expr → Array Lean.Expr → Lean.Meta.Sym.Internal.AlphaShareBuilderM Lean.Expr
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_sup_def : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R),
  max x y = Tropical.trop (max (Tropical.untrop x) (Tropical.untrop y))
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.map_edge : ∀ {X Y : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : SSet.Edge x₀ x₁) (f : X ⟶ Y),
  (e.map f).edge = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 1 }))) e.edge
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingField.instAlgebra : {K : Type u_2} →
  [inst : Field K] →
    (f : Polynomial K) → {R : Type u_1} → [inst_1 : CommSemiring R] → [Algebra R K] → Algebra R f.SplittingField
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.ofPermHom_mem_centralizer : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)), a.ofPermHom τ ∈ Subgroup.centralizer {g}
-- Mathlib.Data.Set.Lattice
Set.sUnion_union : ∀ {α : Type u_1} (S T : Set (Set α)), ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃₀ T
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuousWithinAt.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : Preorder β] {f : α → β} {s : Set α} {g : γ → α} {c : γ} {t : Set γ},
  UpperSemicontinuousWithinAt f s (g c) →
    ContinuousWithinAt g t c → Set.MapsTo g t s → UpperSemicontinuousWithinAt (f ∘ g) t c
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instOne.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : One β],
  ContinuousMap.instOne = { one := ContinuousMap.const α 1 }
-- Mathlib.Data.Matrix.Mul
dotProduct_single_one : ∀ {n : Type u_3} {α : Type v} [inst : Fintype n] [inst_1 : NonAssocSemiring α] [inst_2 : DecidableEq n] (v : n → α)
  (i : n), v ⬝ᵥ Pi.single i 1 = v i
-- Mathlib.Algebra.Lie.LieTheorem
/-- **Lie's theorem**: Lie modules of solvable Lie algebras over fields of characteristic 0
have a common eigenvector for the action of all elements of the Lie algebra.

See `LieModule.exists_nontrivial_weightSpace_of_isNilpotent` for the variant that
assumes that `L` is nilpotent and drops the condition that `k` is of characteristic zero.  -/
LieModule.exists_nontrivial_weightSpace_of_isSolvable : ∀ (k : Type u_1) [inst : Field k] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra k L] (V : Type u_3)
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : LieRingModule L V] [inst_6 : LieModule k L V] [CharZero k]
  [Module.Finite k V] [Nontrivial V] [LieAlgebra.IsSolvable L] [LieModule.IsTriangularizable k L V],
  ∃ χ, Nontrivial ↥(LieModule.weightSpace V ⇑χ)
-- Mathlib.RingTheory.Ideal.Maps
instIsPrincipalMapRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (I : Ideal R)
  [Submodule.IsPrincipal I], Submodule.IsPrincipal (Ideal.map f I)
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.isTopCompl_top_bot : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M], Submodule.IsTopCompl ⊤ ⊥
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
interior, and `f''` is nonnegative on the interior, then `f` is convex on `D`.  -/
convexOn_of_deriv2_nonneg : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D →
        DifferentiableOn ℝ f (interior D) →
          DifferentiableOn ℝ (deriv f) (interior D) → (∀ x ∈ interior D, 0 ≤ deriv^[2] f x) → ConvexOn ℝ D f
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fundamentalSequence.match_1.eq_6 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → ℕ → Sort u_1) (f : ℕ → ONote) (m : ℕ) (h_1 : Unit → motive (Sum.inl none) 0)
  (h_2 : (m : ℕ) → motive (Sum.inl none) m.succ) (h_3 : (a' : ONote) → motive (Sum.inl (some a')) 0)
  (h_4 : (a' : ONote) → (m : ℕ) → motive (Sum.inl (some a')) m.succ) (h_5 : (f : ℕ → ONote) → motive (Sum.inr f) 0)
  (h_6 : (f : ℕ → ONote) → (m : ℕ) → motive (Sum.inr f) m.succ),
  (match Sum.inr f, m.succ with
    | Sum.inl none, 0 => h_1 ()
    | Sum.inl none, m.succ => h_2 m
    | Sum.inl (some a'), 0 => h_3 a'
    | Sum.inl (some a'), m.succ => h_4 a' m
    | Sum.inr f, 0 => h_5 f
    | Sum.inr f, m.succ => h_6 f m) =
    h_6 f m
-- Init.Data.SInt.Lemmas
Int8.toBitVec_toInt64 : ∀ (x : Int8), x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_zero_inv_app : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (a : M) (X : C),
  (F.shiftIso 0 a a ⋯).inv.app X = (F.shift a).map ((CategoryTheory.shiftFunctorZero C M).inv.app X)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Pullback a presieve along a fixed map, by taking the pullback in the
category.
This is not the same as the underlying presieve of `Sieve.pullback`, but there is a relation between
them in `pullbackArrows_comm`.
 -/
CategoryTheory.Presieve.pullbackArrows : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (f : Y ⟶ X) → (R : CategoryTheory.Presieve X) → [R.HasPullbacks f] → CategoryTheory.Presieve Y
-- Mathlib.GroupTheory.OrderOfElement
orderOf_inv : ∀ {G : Type u_1} [inst : Group G] (x : G), orderOf x⁻¹ = orderOf x
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.stepAux_move : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (d : Turing.Dir)
  (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) (v : σ) (T : Turing.Tape Bool),
  Turing.TM1.stepAux (Turing.TM1to1.move n d q) v T = Turing.TM1.stepAux q v ((Turing.Tape.move d)^[n] T)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_const : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} (c : ℝ)
  [MeasureTheory.IsProbabilityMeasure μ], ProbabilityTheory.mgf (fun x => c) μ t = Real.exp (t * c)
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_rcc : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.toList (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = List.drop lo (List.take (hi + 1) xs)
-- Mathlib.Logic.Basic
and_iff_not_or_not : ∀ {a b : Prop}, a ∧ b ↔ ¬(¬a ∨ ¬b)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.c : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} → {hζ : IsPrimitiveRoot ζ 3} → FermatLastTheoremForThreeGen.Solution'✝ hζ → NumberField.RingOfIntegers K
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_roc_eq_add : ∀ {m n : ℤ} {i : ℕ}, i < (n - m).toNat → (m<...=n).toList[i]! = m + 1 + ↑i
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- A maximal clique in a graph `G` is a clique that cannot be extended by adding more vertices.  -/
SimpleGraph.isMaximalClique_iff : ∀ {α : Type u_3} {G : SimpleGraph α} {s : Set α},
  Maximal G.IsClique s ↔ G.IsClique s ∧ ∀ (t : Set α), G.IsClique t → s ⊆ t → t ⊆ s
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.isBasis_basicOpen : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], TopologicalSpace.Opens.IsBasis (Set.range (AlgebraicGeometry.Proj.basicOpen 𝒜))
-- Init.Data.UInt.Lemmas
UInt64.ofFin_toFin : ∀ (n : UInt64), UInt64.ofFin n.toFin = n
-- Mathlib.Topology.Category.CompHausLike.SigmaComparison
CompHausLike.isIsoSigmaComparison : ∀ {P : TopCat → Prop} [inst : CompHausLike.HasExplicitFiniteCoproducts P]
  (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts X]
  {α : Type u} [inst_2 : Finite α] (σ : α → Type u) [inst_3 : (a : α) → TopologicalSpace (σ a)]
  [inst_4 : ∀ (a : α), CompactSpace (σ a)] [inst_5 : ∀ (a : α), T2Space (σ a)]
  [inst_6 : ∀ (a : α), CompHausLike.HasProp P (σ a)], CategoryTheory.IsIso (CompHausLike.sigmaComparison X σ)
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.ExceptT.bindCont.match_1.eq_2 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃_obj_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : C)
  {x x_1 : C} (φ : x ⟶ x_1),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃ C).obj X₁).obj X₂).map φ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ x).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂ φ))
        (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ x_1).inv)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber_le_coveringNumber : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (A : Set X),
  Metric.externalCoveringNumber ε A ≤ Metric.coveringNumber ε A
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.comp_mapCommGrp_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] {E : Type u₃}
  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] [inst_7 : CategoryTheory.CartesianMonoidalCategory E]
  [inst_8 : CategoryTheory.BraidedCategory E] {F : CategoryTheory.Functor C D} [inst_9 : F.Braided]
  {G : CategoryTheory.Functor D E} [inst_10 : G.Braided] (A : CategoryTheory.CommGrp C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G))
      ((F.comp G).map CategoryTheory.MonObj.one)
-- Mathlib.Order.Interval.Finset.Basic
Finset.right_notMem_Ico : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], b ∉ Finset.Ico a b
-- Mathlib.Data.Fintype.Powerset
Finset.powerset_eq_univ : ∀ {α : Type u_1} [inst : Fintype α] {s : Finset α}, s.powerset = Finset.univ ↔ s = Finset.univ
-- Mathlib.Computability.TuringMachine.Computable
Turing.inhabitedTM2OutputsInTime : Inhabited
  (Turing.TM2OutputsInTime (Turing.idComputer Bool) (List.map (Equiv.cast ⋯).invFun [false])
    (some (List.map (Equiv.cast ⋯).invFun [false])) (Polynomial.eval 1 1))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKeyD_modify_eq_maxKeyD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {fallback : α},
  (Std.ExtDTreeMap.Const.modify t k f).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↥(groupCohomology.cocycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.iCocycles A 1))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₁ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.i
          (groupCohomology.cochainsIso₁ A).inv))
      x
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.CostructuredArrow.createsColimitsOfSize : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {T : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} T] →
        {G : CategoryTheory.Functor A T} →
          {X : T} →
            [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G] →
              CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₁, max u₁ v₃, u₁}
                (CategoryTheory.CostructuredArrow.proj G X)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` of an `AddGroup` inherits an inverse.  -/
AddSubgroup.neg : {G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → Neg ↥H
-- Init.Data.Option.Lemmas
Option.choice_eq_some : ∀ {α : Type u_1} [Subsingleton α] (a : α), Option.choice α = some a
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ιOrZero.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {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_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : 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_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
  HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j =
    HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j
-- Mathlib.Data.Vector.Basic
_private.Mathlib.Data.Vector.Basic.0.List.Vector.traverseAux : {F : Type u → Type u} → [Applicative F] → {α β : Type u} → (α → F β) → (x : List α) → F (List.Vector β x.length)
-- Mathlib.GroupTheory.Descent
/-- If `G` is a commutative group and `n : ℕ`, `h : G → ℝ` satisfy
* `G / G ^ 2` is finite,
* `0 ≤ h x` for all `x : G`,
* there is `C : ℝ` such that for all `x y : G`, `|h (x * y) + h(x / y) - 2 * (h x + h y)| ≤ C`,
* for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,

then `G` is finitely generated.
 -/
CommGroup.fg_of_descent' : ∀ {G : Type u_1} [inst : CommGroup G] {h : G → ℝ} {C : ℝ},
  (powMonoidHom 2).range.FiniteIndex →
    (∀ (x : G), 0 ≤ h x) → (∀ (x y : G), |h (x * y) + h (x / y) - 2 * (h x + h y)| ≤ C) → ∀ [Northcott h], Group.FG G
-- Mathlib.Logic.Equiv.Defs
Equiv.mk.sizeOf_spec : ∀ {α : Sort u_1} {β : Sort u_2} [inst : SizeOf α] [inst_1 : SizeOf β] (toFun : α → β) (invFun : β → α)
  (left_inv : autoParam (Function.LeftInverse invFun toFun) Equiv.left_inv._autoParam)
  (right_inv : autoParam (Function.RightInverse invFun toFun) Equiv.right_inv._autoParam),
  sizeOf { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } = 1
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `L / K` be a normal field extension. For any two elements `x` and `y` in `L`, `y` is a
conjugate root of `x` if and only if `x` and `y` falls in the same orbit of the action of Galois
group.
 -/
isConjRoot_iff_orbitRel : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Normal K L] {x y : L},
  IsConjRoot K x y ↔ (MulAction.orbitRel Gal(L/K) L) x y
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.Spanning.contract : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Spanning X → ∀ (C : Set α), (M.contract C).Spanning (X \ C)
-- Mathlib.Order.ZornAtoms
/-- **Zorn's lemma**: A partial order is atomic if every nonempty chain `c`, `⊥ ∉ c`, has a lower
bound not equal to `⊥`.  -/
IsAtomic.of_isChain_bounded : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α],
  (∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊥ ∉ c → ∃ x, x ≠ ⊥ ∧ x ∈ lowerBounds c) → IsAtomic α
-- Mathlib.NumberTheory.NumberField.Basic
/-- Any extension between ring of integers is integral.  -/
NumberField.RingOfIntegers.extension_algebra_isIntegral : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  Algebra.IsIntegral (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
aestronglyMeasurable_deriv_with_param : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {α : Type u_4} [inst_3 : TopologicalSpace α] [inst_4 : MeasurableSpace α]
  [OpensMeasurableSpace α] [CompleteSpace F] [LocallyCompactSpace 𝕜] [inst_8 : MeasurableSpace 𝕜]
  [OpensMeasurableSpace 𝕜] [SecondCountableTopologyEither α F] {f : α → 𝕜 → F},
  Continuous (Function.uncurry f) →
    ∀ (μ : MeasureTheory.Measure (α × 𝕜)), MeasureTheory.AEStronglyMeasurable (fun p => deriv (f p.1) p.2) μ
-- LeanSearchClient.Syntax
/-- Search from within Lean, depending on the option `leansearchclient.backend` (currently only leansearch).
Queries should be a string that ends with a `.` or `?`. This works as a command, as a term
and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

```lean
#search "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #search "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #search "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

In tactic mode, if the query string is not supplied, then [LeanStateSearch](https://premise-search.com) is queried based on the goal state.
```
  -/
LeanSearchClient.search_tactic : Lean.ParserDescr
-- Mathlib.Algebra.Star.CentroidHom
CentroidHom.instStarRingSubtypeMemSubsemiringCenter : {α : Type u_1} → [inst : NonUnitalNonAssocSemiring α] → [StarRing α] → StarRing ↥(Subsemiring.center (CentroidHom α))
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.inv_hom_id_tensor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.inv g)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W) g)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W) h)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.wf : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular], WellFounded P.AncestralRel
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
CategoryTheory.Limits.HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit : ∀ {J : Type w} {inst : LinearOrder J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  [self : CategoryTheory.Limits.HasIterationOfShape J C] (j : J),
  Order.IsSuccLimit j → CategoryTheory.Limits.HasColimitsOfShape (↑(Set.Iio j)) C
-- Mathlib.Data.PNat.Xgcd
/-- `a = ap + 1`  -/
PNat.XgcdType.a : PNat.XgcdType → ℕ+
-- Mathlib.Analysis.CStarAlgebra.Classes
instNonUnitalCommCStarAlgebraProd : {A : Type u_1} →
  {B : Type u_2} → [NonUnitalCommCStarAlgebra A] → [NonUnitalCommCStarAlgebra B] → NonUnitalCommCStarAlgebra (A × B)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.isQuasicoherent : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.QuasicoherentData), M.IsQuasicoherent
-- Lean.Meta.Tactic.Simp.LoopProtection
/-- Main entry point to the loop protection mechanism: Checks if the given theorem is looping in the
current simp set, and logs a warning if it does.

Assumes that `withRef` is set appropriately for the warning.

With `force := off`, only runs when `linter.loopingSimpArgs` is enabled and presents it as a
linter. With `force := on` (typically after `simp` threw an exception) it prints plain warnings.
 -/
Lean.Meta.Simp.checkLoops : Bool → Lean.Meta.Simp.Context → Lean.Meta.Simp.Methods → Lean.Meta.SimpTheorem → Lean.MetaM Unit
-- Lean.Meta.Basic
/-- Returns true if `mvarId.isReadOnly` returns true or if `mvarId` is a synthetic opaque metavariable.

Recall `isDefEq` will not assign a value to `mvarId` if `mvarId.isReadOnlyOrSyntheticOpaque`.
 -/
Lean.MVarId.isReadOnlyOrSyntheticOpaque : Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Algebra.Lie.Basic
LieEquiv.symm_trans : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieRing L₂] [inst_3 : LieRing L₃] [inst_4 : LieAlgebra R L₁] [inst_5 : LieAlgebra R L₂]
  [inst_6 : LieAlgebra R L₃] (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃), (e₁.trans e₂).symm = e₂.symm.trans e₁.symm
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateAnchors.mk.injEq : ∀ (candidates : Array Lean.Meta.Grind.SplitCandidateWithAnchor) (numDigits : ℕ)
  (candidates_1 : Array Lean.Meta.Grind.SplitCandidateWithAnchor) (numDigits_1 : ℕ),
  ({ candidates := candidates, numDigits := numDigits } = { candidates := candidates_1, numDigits := numDigits_1 }) =
    (candidates = candidates_1 ∧ numDigits = numDigits_1)
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.token.inj : ∀ {val val_1 : Lean.Parser.Token},
  Lean.Parser.ParserExtension.Entry.token val = Lean.Parser.ParserExtension.Entry.token val_1 → val = val_1
-- Lean.DocString.Parser
Lean.Doc.Parser.UnorderedListType.dash.sizeOf_spec : sizeOf Lean.Doc.Parser.UnorderedListType.dash = 1
-- Mathlib.Algebra.Order.Archimedean.Defs
exists_nsmul_lt : ∀ {R : Type u_1} [inst : AddCommGroup R] [inst_1 : LinearOrder R] [IsOrderedAddMonoid R] [Archimedean R] {a : R},
  a < 0 → ∀ (b : R), ∃ n, n • a < b
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.rightInvSeq_drop : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ),
  cs.rightInvSeq (List.drop j ω) = List.drop j (cs.rightInvSeq ω)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.Compatible.of_le : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H ≤ G → H.Compatible G