mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_of_contains_insertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α},
  Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯) = true →
    (List.map Prod.fst l).contains k = false → Std.DTreeMap.Internal.Impl.contains k t = true
-- Init.Core
Prod.eta : ∀ {α : Type u_1} {β : Type u_2} (p : α × β), (p.1, p.2) = p
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceParams.mk.injEq : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams) (context : Lean.Lsp.ReferenceContext)
  (toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams) (context_1 : Lean.Lsp.ReferenceContext),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams, context := context } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1, context := context_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1 ∧ context = context_1)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.map_symm_apply_map_eq : ∀ {α : Type u_1} {β : Type u_2} {x : FreeAddMonoid α} (e : α ≃ β),
  (FreeAddMonoid.map ⇑e.symm) ((FreeAddMonoid.map ⇑e) x) = x
-- Std.Time.Zoned.TimeZone
/-- Creates an `Offset` from a given number of hour.
 -/
Std.Time.TimeZone.Offset.ofHours : Std.Time.Hour.Offset → Std.Time.TimeZone.Offset
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mk.injEq : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} (left : A) (right : B) (hom : L.obj left ⟶ R.obj right) (left_1 : A) (right_1 : B)
  (hom_1 : L.obj left_1 ⟶ R.obj right_1),
  ({ left := left, right := right, hom := hom } = { left := left_1, right := right_1, hom := hom_1 }) =
    (left = left_1 ∧ right = right_1 ∧ hom ≍ hom_1)
-- Mathlib.Data.Real.ConjExponents
/-- **Alias** of the reverse direction of `NNReal.holderTriple_coe_iff`. -/
NNReal.HolderTriple.coe : ∀ {p q r : NNReal}, p.HolderTriple q r → (↑p).HolderTriple ↑q ↑r
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- **Alias** of `Complex.UnitDisc.coe_circle_smul`. -/
Complex.UnitDisc.coe_smul_circle : ∀ (z : Circle) (w : Complex.UnitDisc), ↑(z • w) = ↑z * ↑w
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.toMk₁_of_le_castSucc : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  i ≤ j.castSucc → (CategoryTheory.ConcreteCategory.hom (SimplexCategory.toMk₁ i)) j = 1
-- Mathlib.GroupTheory.Congruence.Defs
/-- Additive congruence relations preserve addition.  -/
AddCon.add : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) {w x y z : M}, c w x → c y z → c (w + y) (x + z)
-- Mathlib.MeasureTheory.OuterMeasure.Defs
/-- A mixin class saying that elements `μ : F` are outer measures on `α`.

This typeclass is used to unify some API for outer measures and measures.  -/
MeasureTheory.OuterMeasureClass : (F : Type u_2) → (α : outParam (Type u_3)) → [FunLike F (Set α) ENNReal] → Prop
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_add : ∀ (a b : UInt16), (a + b).toUInt64 = (a.toUInt64 + b.toUInt64) % 65536
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.mul_comm : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x y : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (x.mul y) (y.mul x)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyRel.trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {f₀ f₁ f₂ : X ⟶ Y} [HomotopicalAlgebra.IsFibrant Y],
  HomotopicalAlgebra.RightHomotopyRel f₀ f₁ →
    HomotopicalAlgebra.RightHomotopyRel f₁ f₂ → HomotopicalAlgebra.RightHomotopyRel f₀ f₂
-- Lean.Meta.Basic
/-- Simpler variant of `withLocalDeclsD` for bringing variables into scope whose types do not depend
on each other.
 -/
Lean.Meta.withLocalDeclsDND : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      {α : Type} →
        [Inhabited α] →
          Array (Lean.Name × Lean.Expr) →
            (Array Lean.Expr → n α) → optParam Lean.LocalDeclKind Lean.LocalDeclKind.default → n α
-- Mathlib.Topology.Order.IsLUB
/-- The infimum of a bounded below, continuous function on a dense set is equal to the infimum on
the universe.  -/
Dense.ciInf : ∀ {γ : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLattice α]
  [ClosedIciTopology α] {f : γ → α} [inst_3 : TopologicalSpace γ] {S : Set γ},
  Dense S → Continuous f → BddBelow (Set.range f) → ⨅ s, f ↑s = ⨅ i, f i
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h₂.homologyIso.hom =
    CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom γ.φH
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Iic : Lean.Term → BigOperators.FinsetResult✝
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.isAddQuotientCoveringMap_exp : IsAddQuotientCoveringMap ⇑Circle.exp ↥(AddSubgroup.zmultiples (2 * Real.pi))
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.isTransitive_iff_subset_powerset : ∀ {x : ZFSet.{u}}, x.IsTransitive ↔ x ⊆ x.powerset
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The extension of `g` along `f`.  -/
CategoryTheory.Bicategory.LeftExtension.extension : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : a ⟶ b} → {g : a ⟶ c} → CategoryTheory.Bicategory.LeftExtension f g → (b ⟶ c)
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
/-- When `X` is `StrictSegal`, `X` is 2-coskeletal.  -/
SSet.StrictSegal.isCoskeletal : ∀ {X : SSet} (sx : X.StrictSegal), CategoryTheory.SimplicialObject.IsCoskeletal X 2
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_set_sInter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] (a : α) (S : Set (Set β)), a • ⋂₀ S ⊆ ⋂ s ∈ S, a • s
-- Init.Data.List.Impl
/-- Concatenates a list of lists into a single list, preserving the order of the elements.

`O(|flatten L|)`. This is a tail-recursive version of `List.flatten`, used in runtime code.

Examples:
* `[["a"], ["b", "c"]].flattenTR = ["a", "b", "c"]`
* `[["a"], [], ["b", "c"], ["d", "e", "f"]].flattenTR = ["a", "b", "c", "d", "e", "f"]`
 -/
List.flattenTR : {α : Type u_1} → List (List α) → List α
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.withPercents : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- The Euler product for the Riemann ζ function, valid for `s.re > 1`.
This version is stated in the form of convergence of finite partial products.  -/
riemannZeta_eulerProduct : ∀ {s : ℂ},
  1 < s.re → Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) Filter.atTop (nhds (riemannZeta s))
-- Mathlib.Topology.Closure
exists_isOpen_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {p : Set X → Prop}, (∃ t, IsOpen t ∧ p t) ↔ ∃ t, p (interior t)
-- Mathlib.GroupTheory.Finiteness
/-- An additive subgroup of `H` is finitely generated if it is the closure of a finite subset of
`H`.  -/
AddSubgroup.FG : {G : Type u_3} → [inst : AddGroup G] → AddSubgroup G → Prop
-- Init.Core
/-- The [axiom](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=axioms) of **propositional extensionality**. It asserts that if
propositions `a` and `b` are logically equivalent (that is, if `a` can be proved from `b` and vice
versa), then `a` and `b` are *equal*, meaning `a` can be replaced with `b` in all contexts.

The standard logical connectives provably respect propositional extensionality. However, an axiom is
needed for higher order expressions like `P a` where `P : Prop → Prop` is unknown, as well as for
equality. Propositional extensionality is intuitionistically valid.
 -/
propext : ∀ {a b : Prop}, (a ↔ b) → a = b
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_def : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t : Finset β},
  s -ᵥ t = Finset.image₂ (fun x1 x2 => x1 -ᵥ x2) s t
-- Mathlib.RingTheory.Length
Module.length_eq_zero_of_subsingleton_ring : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Subsingleton R],
  Module.length R M = 0
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.mkPreResult : Lean.Meta.Sym.UnifyM✝ Lean.Meta.Sym.MkPreResultResult✝
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.condition : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  {inst_1 : CategoryTheory.Category.{v_1, u_1} J} [self : W.IsStableUnderColimitsOfShape J]
  (X₁ X₂ : CategoryTheory.Functor J C) (c₁ : CategoryTheory.Limits.Cocone X₁) (c₂ : CategoryTheory.Limits.Cocone X₂)
  (h₁ : CategoryTheory.Limits.IsColimit c₁) (h₁ : CategoryTheory.Limits.IsColimit c₂) (f : X₁ ⟶ X₂),
  W.functorCategory J f →
    ∀ (φ : c₁.pt ⟶ c₂.pt),
      (∀ (j : J),
          CategoryTheory.CategoryStruct.comp (c₁.ι.app j) φ =
            CategoryTheory.CategoryStruct.comp (f.app j) (c₂.ι.app j)) →
        W φ
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatch_iff : ∀ {pat s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat.copy
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_mul : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (f g : CentroidHom α), ⇑(f * g) = ⇑f ∘ ⇑g
-- Lean.Server.FileWorker.ExampleHover
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.RWState.output.inj : ∀ {indent ticks indent_1 ticks_1 : ℕ},
  Lean.Server.FileWorker.Hover.RWState.output✝ indent ticks =
      Lean.Server.FileWorker.Hover.RWState.output✝ indent_1 ticks_1 →
    indent = indent_1 ∧ ticks = ticks_1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zsmul_eq_empty : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {s : Set α} {n : ℤ}, n • s = ∅ ↔ s = ∅ ∧ n ≠ 0
-- Mathlib.Data.Multiset.ZeroCons
Multiset.coe_eq_zero : ∀ {α : Type u_1} (l : List α), ↑l = 0 ↔ l = []
-- Lean.ProjFns
Lean.getProjectionFnInfo? : {m : Type → Type} → [Lean.MonadEnv m] → [Monad m] → Lean.Name → m (Option Lean.ProjectionFunctionInfo)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_comp : ∀ {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {σ₁₂ : R →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃)
  (p : Submodule R₃ M₃), Submodule.comap (g ∘ₛₗ f) p = Submodule.comap f (Submodule.comap g p)
-- Aesop.Forward.State
Aesop.RuleState.mk.injEq : ∀ (rule : Aesop.ForwardRule) (clusterStates : Array Aesop.ClusterState)
  (patSubstSources : Lean.PHashMap Aesop.Substitution (Lean.PHashSet Aesop.PatSubstSource)) (rule_1 : Aesop.ForwardRule)
  (clusterStates_1 : Array Aesop.ClusterState)
  (patSubstSources_1 : Lean.PHashMap Aesop.Substitution (Lean.PHashSet Aesop.PatSubstSource)),
  ({ rule := rule, clusterStates := clusterStates, patSubstSources := patSubstSources } =
      { rule := rule_1, clusterStates := clusterStates_1, patSubstSources := patSubstSources_1 }) =
    (rule = rule_1 ∧ clusterStates = clusterStates_1 ∧ patSubstSources = patSubstSources_1)
-- Mathlib.Topology.Closure
closure_mono : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, s ⊆ t → closure s ⊆ closure t
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.PullbackCone.snd_limit_cone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)],
  CategoryTheory.Limits.PullbackCone.snd (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g)) =
    CategoryTheory.Limits.pullback.snd f g
-- Mathlib.Topology.Category.Sequential
Sequential.instFaithfulTopCatSequentialToTop : Sequential.sequentialToTop.Faithful
-- Mathlib.Order.Interval.Finset.Defs
/-- `x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b`  -/
LocallyFiniteOrder.finset_mem_Icc : ∀ {α : Type u_1} {inst : Preorder α} [self : LocallyFiniteOrder α] (a b x : α),
  x ∈ LocallyFiniteOrder.finsetIcc a b ↔ a ≤ x ∧ x ≤ b
-- Init.Core
/-- The loop should continue with the next iteration, using the returned state.

`ForInStep.yield` is produced by `continue` and by reaching the bottom of the loop body.
 -/
ForInStep.yield : {α : Type u} → α → ForInStep α
-- Mathlib.Topology.Separation.Hausdorff
ULift.instT2Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X], T2Space (ULift.{u_3, u_1} X)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.mem_nthRootsFinset : ∀ {R : Type u_4} {k : ℕ} {ζ : R} [inst : CommRing R] [inst_1 : IsDomain R],
  IsPrimitiveRoot ζ k → 0 < k → ζ ∈ Polynomial.nthRootsFinset k 1
-- Mathlib.Order.ScottContinuity.Complete
/-- **Alias** of the reverse direction of `scottContinuous_iff_map_sSup`.

---

`f` is Scott continuous if and only if it commutes with `sSup` on directed sets  -/
ScottContinuous.of_map_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f : α → β},
  (∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → f (sSup d) = sSup (f '' d)) → ScottContinuous f
-- Mathlib.Algebra.Category.Grp.Subobject
AddCommGrpCat.wellPowered_addCommGrp : CategoryTheory.WellPowered.{u, u, u + 1} AddCommGrpCat
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Equivariant ring homomorphisms.  -/
«MulSemiringActionHomLocal≺» : Lean.TrailingParserDescr
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.propagateDiseqs.go : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.GoalM Unit
-- Init.Meta.Defs
Lean.Syntax.setHeadInfoAux : Lean.SourceInfo → Lean.Syntax → Option Lean.Syntax
-- Init.Data.UInt.Bitwise
UInt32.and_neg_one : ∀ {a : UInt32}, a &&& -1 = a
-- Init.Data.Int.LemmasAux
Int.blt'_eq_true : ∀ (a b : ℤ), (a.blt' b = true) = (a < b)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_pos_iff : ∀ {n m : ℕ}, 0 < n ||| m ↔ 0 < n ∨ 0 < m
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.lift_apply_of : ∀ {α : Type u} {β : Type v} [inst : Group β] {f : α → β} {x : α}, (FreeGroup.lift f) (FreeGroup.of x) = f x
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.toSyn_eq_zero_iff : ∀ {σ : Type u_1} (m : MonomialOrder σ) (a : σ →₀ ℕ), m.toSyn a = 0 ↔ a = 0
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.subset_span_trans : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {U V W : Set M},
  U ⊆ ↑(Submodule.span R V) → V ⊆ ↑(Submodule.span R W) → U ⊆ ↑(Submodule.span R W)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.instCoeOutAlgEquiv : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → CoeOut (A ≃A[R] B) (A ≃ₐ[R] B)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.Monic.ne_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [Nontrivial R] {f : MvPolynomial σ R},
  m.Monic f → f ≠ 0
-- Mathlib.Data.TypeVec
TypeVec.lastFun_comp : ∀ {n : ℕ} {α₀ : TypeVec.{u_1} (n + 1)} {α₁ : TypeVec.{u_2} (n + 1)} {α₂ : TypeVec.{u_3} (n + 1)} (f₀ : α₀.Arrow α₁)
  (f₁ : α₁.Arrow α₂), TypeVec.lastFun (TypeVec.comp f₁ f₀) = TypeVec.lastFun f₁ ∘ TypeVec.lastFun f₀
-- Mathlib.RingTheory.Flat.Tensor
/-- A module `M` over a ring `R` is flat iff for all finitely generated ideals `I` of `R`, the
tensor product of the inclusion `I → R` and the identity `M → M` is injective. See
`iff_rTensor_injective'` to extend to all ideals `I`.  -/
Module.Flat.iff_rTensor_injective : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.right_inv : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (self : L ≃ᴸ L'),
  self.toLHom.comp self.invLHom = FirstOrder.Language.LHom.id L'
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.homologyπ_restrictionHomologyIso_inv : ∀ {ι : 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 : ι) (hi : c.prev j = i)
  (hk : c.next j = k) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i')
  (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j'] [inst_4 : (K.restriction e).HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.homologyπ j')
      (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv =
    CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv
      ((K.restriction e).homologyπ j)
-- Aesop.Tree.TreeM
Aesop.Tree.nextGoalId : Aesop.Tree → Aesop.GoalId
-- Batteries.Linter.UnreachableTactic
/-- Enables the 'unreachable tactic' linter. This will warn on any tactics that are never executed.
For example, in `example : True := by trivial <;> done`, the tactic `done` is never executed
because `trivial` produces no subgoals; you could put `sorry` or `apply I_don't_exist`
or anything else there and no error would result.

A common source of such things is `simp <;> tac` in the case that `simp` improves and
closes a subgoal that was previously being closed by `tac`.
 -/
Batteries.Linter.UnreachableTactic.unreachableTacticLinter : Lean.Linter
-- Mathlib.FieldTheory.Finite.Basic
/-- **Fermat's Little Theorem**: for all `n : ℕ` coprime to `p`, we have
`n ^ (p - 1) ≡ 1 [MOD p]`.  -/
Nat.ModEq.pow_card_sub_one_eq_one : ∀ {p : ℕ}, Nat.Prime p → ∀ {n : ℕ}, n.Coprime p → n ^ (p - 1) ≡ 1 [MOD p]
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.symm_commAlgEquiv : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N],
  (AddMonoidAlgebra.commAlgEquiv R).symm = AddMonoidAlgebra.commAlgEquiv R
-- Mathlib.Order.Irreducible
not_supPrime : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, ¬SupPrime a ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.degree_sum_eq_of_linearIndepOn : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommRing R] {A : Type u_1} [inst_1 : CommRing A]
  [inst_2 : Algebra R A] {f : ι → Polynomial R} {v : ι → A},
  LinearIndepOn R v ↑s → (∑ i ∈ s, v i • Polynomial.map (algebraMap R A) (f i)).degree = s.sup fun i => (f i).degree
-- Mathlib.Algebra.Group.Action.Opposite
op_vadd_op_vadd : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid α] [inst_1 : AddAction αᵃᵒᵖ β] (b : β) (a₁ a₂ : α),
  AddOpposite.op a₂ +ᵥ AddOpposite.op a₁ +ᵥ b = AddOpposite.op (a₁ + a₂) +ᵥ b
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atTop : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (a : α),
  Filter.Tendsto (↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a)) Filter.atTop (nhds 1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_inter_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∩ t₂ ↔ k ∈ t₁ ∧ k ∈ t₂
-- Lean.Expr
/-- Auxiliary type for forcing `==` to be structural equality for `Expr`  -/
Lean.ExprStructEq : Type
-- Mathlib.RingTheory.Spectrum.Prime.Homeomorph
/-- If the kernel of `f : R →+* S` consists of nilpotent elements and for every `x : S`,
there exists `n > 0` such that `x ^ n` is in the range of `f`, then `Spec f` is a homeomorphism.
Note: This does not hold for semirings, because `ℕ →+* ℤ` satisfies these conditions, but
`Spec ℕ` has one more point than `Spec ℤ`.  -/
PrimeSpectrum.isHomeomorph_comap : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  (∀ (x : S), ∃ n > 0, x ^ n ∈ f.range) → RingHom.ker f ≤ nilradical R → IsHomeomorph (PrimeSpectrum.comap f)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instSub.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Sub Y],
  LocallyConstant.instSub = { sub := fun f g => { toFun := ⇑f - ⇑g, isLocallyConstant := ⋯ } }
-- Aesop.Script.StructureDynamic
_private.Aesop.Script.StructureDynamic.0.Aesop.Script.structureDynamicCore.goStructured : Lean.MVarId →
  Lean.Meta.SavedState →
    Array Lean.MVarId → Lean.MVarId → Aesop.Script.DynStructureM (Option Aesop.Script.DynStructureResult)
-- Mathlib.Algebra.Order.Ring.Idempotent
eq_of_mul_eq_add_eq_one : ∀ {R : Type u_1} [inst : NonAssocSemiring R] (a : R) {b c : R}, a * b = c * a → a + b = 1 → a + c = 1 → b = c
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_eq_bot_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.withBotDegree f = ⊥ ↔ f = 0
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The oriented angle at `p` between two points not equal to `p` is plus or minus the unoriented
angle.  -/
EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ : P},
  p₁ ≠ p →
    p₂ ≠ p →
      EuclideanGeometry.oangle p₁ p p₂ = ↑(EuclideanGeometry.angle p₁ p p₂) ∨
        EuclideanGeometry.oangle p₁ p p₂ = -↑(EuclideanGeometry.angle p₁ p p₂)
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F.unop : J ⥤ C` into a limit for `F : Jᵒᵖ ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.isLimitConeOfCoconeUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cocone F.unop} →
            CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeUnop c)
-- Lean.Meta.DiscrTree.Basic
_private.Lean.Meta.DiscrTree.Basic.0.Lean.Meta.DiscrTree.insertVal.loop.eq_def : ∀ {α : Type u_1} [inst : BEq α] (vs : Array α) (v : α) (i : ℕ),
  Lean.Meta.DiscrTree.insertVal.loop✝ vs v i =
    if h : i < vs.size then
      if (v == vs[i]) = true then vs.set i v h else Lean.Meta.DiscrTree.insertVal.loop✝ vs v (i + 1)
    else vs.push v
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.parser : Lean.Name → Lean.Name → ℕ → Lean.Parser.ParserExtension.OLeanEntry