mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.HoCat.resolution.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  HomotopicalAlgebra.FibrantObject.HoCat.resolution =
    {
      obj := fun X =>
        HomotopicalAlgebra.FibrantObject.toHoCat.obj
          (HomotopicalAlgebra.FibrantObject.mk (HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj X)),
      map := fun {X Y} f =>
        HomotopicalAlgebra.FibrantObject.toHoCat.map
          (HomotopicalAlgebra.FibrantObject.homMk (HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap f)),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.map_extend_symm_nhdsWithin_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {y : M},
  y ∈ f.source → Filter.map (↑(f.extend I).symm) (nhdsWithin (↑(f.extend I) y) (Set.range ↑I)) = nhds y
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- An isomorphism of multilinear maps given an isomorphism between their domains.

This is `MultilinearMap.compLinearMap` as a linear equivalence,
and the multilinear version of `LinearEquiv.congrLeft`.  -/
LinearEquiv.multilinearMapCongrLeft : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₁' : ι → Type v₁'} →
        {M₂ : Type v₂} →
          [inst : CommSemiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : (i : ι) → Module R (M₁ i)] →
                  [inst_4 : Module R M₂] →
                    [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] →
                      [inst_6 : (i : ι) → Module R (M₁' i)] →
                        ((i : ι) → M₁ i ≃ₗ[R] M₁' i) → MultilinearMap R M₁' M₂ ≃ₗ[R] MultilinearMap R M₁ M₂
-- Lean.Meta.Tactic.Grind.CheckResult
/-- Propagated equations back to the core.  -/
Lean.Meta.Grind.CheckResult.propagated : Lean.Meta.Grind.CheckResult
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.instSigmaFiniteRestrictInterSet_1 : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}
  [MeasureTheory.SigmaFinite (μ.restrict t)], MeasureTheory.SigmaFinite (μ.restrict (s ∩ t))
-- Mathlib.Combinatorics.HalesJewett
/-- The **Hales-Jewett theorem**. This version has a restriction on universe levels which is
necessary for the proof. See `exists_mono_in_high_dimension` for a fully universe-polymorphic
version.  -/
_private.Mathlib.Combinatorics.HalesJewett.0.Combinatorics.Line.exists_mono_in_high_dimension' : ∀ (α : Type u) [Finite α] (κ : Type (max v u)) [Finite κ],
  ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, Combinatorics.Line.IsMono C l
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {fallback : β} (h : t.WF),
  Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.filter f t) k fallback =
    ((Std.DTreeMap.Raw.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.not_nil_of_isCycle_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {h : G.Adj v u},
  (SimpleGraph.Walk.cons h p).IsCycle → ¬p.Nil
-- Mathlib.Order.Bounds.Basic
isGreatest_pair : ∀ {γ : Type u_3} [inst : LinearOrder γ] {a b : γ}, IsGreatest {a, b} (max a b)
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `Sigma.locallyPathConnectedSpace`.

---

Disjoint unions of locally path-connected spaces are locally path-connected.  -/
Sigma.locPathConnectedSpace : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), LocallyPathConnectedSpace (X i)], LocallyPathConnectedSpace ((i : ι) × X i)
-- Mathlib.Algebra.Order.Ring.Abs
_private.Mathlib.Algebra.Order.Ring.Abs.0.abs_geomSum_le : ∀ {α : Type u_1} [inst : CommRing α] [inst_1 : LinearOrder α] (a b : α) (n : ℕ) [IsOrderedRing α],
  |geomSum✝ a b n| ≤ (↑n + 1) * max |a| |b| ^ n
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β}, (m.insertIfNew k v).contains a = (k == a || m.contains a)
-- Mathlib.Tactic.Simps.Basic
/-- Turn `ParsedProjectionData` into `ProjectionData`.  -/
Simps.ParsedProjectionData.toProjectionData : Simps.ParsedProjectionData → Simps.ProjectionData
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Divisors are invariant under translation, special case where the set is a sphere.  -/
MeromorphicOn.divisor_sphere_comp_sub_const_eq_divisor_sphere : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c : 𝕜} {R : ℝ} {f : 𝕜 → E},
  (MeromorphicOn.divisor (f ∘ fun x => x - c) (Metric.sphere c R)) (z + c) =
    (MeromorphicOn.divisor f (Metric.sphere 0 R)) z
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.ExtDTreeMap.minKeyD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → α
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.induced : ∀ {β : Type u_1} {α : Type u_2} [s : TopologicalSpace β] (f : α → β) {T : Set (Set β)},
  TopologicalSpace.IsTopologicalBasis T → TopologicalSpace.IsTopologicalBasis (Set.preimage f '' T)
-- Std.Http.Protocol.H1
/-- Whether the chunk data is partial for the current frame/body slice
(more bytes are still required to complete it).
 -/
Std.Http.Protocol.H1.PulledChunk.incomplete : Std.Http.Protocol.H1.PulledChunk → Bool
-- Mathlib.Order.Filter.Ring
Filter.EventuallyLE.mul_le_mul' : ∀ {α : Type u} {β : Type v} [inst : Mul β] [inst_1 : Preorder β] [MulLeftMono β] [MulRightMono β] {l : Filter α}
  {f₁ f₂ g₁ g₂ : α → β}, f₁ ≤ᶠ[l] f₂ → g₁ ≤ᶠ[l] g₂ → f₁ * g₁ ≤ᶠ[l] f₂ * g₂
-- Init.Data.String.Lemmas.Iterate
String.Model.map_get_revPositionsFrom_endPos : ∀ {s : String}, List.map (fun p => (↑p).get ⋯) (String.Model.revPositionsFrom s.endPos) = s.toList.reverse
-- Mathlib.Data.FunLike.IsApply
IsMulApplyEqComp.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} [inst : FunLike F α α] [inst_1 : Mul F],
  (∀ (f g : F) (x : α), (f * g) x = f (g x)) → IsMulApplyEqComp F α
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.toUnitHom_inj : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ ψ : DirichletCharacter R n),
  MulChar.toUnitHom χ = MulChar.toUnitHom ψ ↔ χ = ψ
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewRawFact.proof : Lean.Meta.Grind.NewRawFact → Lean.Expr
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
Summable.const_div : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α}, Summable (fun x => 1 / f x) L → ∀ (b : α), Summable (fun i => b / f i) L
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_not_contains_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = false →
      Std.Internal.List.getKey? k (List.filter (fun p => !l₂.contains p.fst) l₁) = Std.Internal.List.getKey? k l₁
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {G : Type u_3} [inst_5 : SMul G β]
  [inst_6 : IsScalarTower G β β] (a : G) (f : CauSeq β abv), ↑(a • f) = a • ↑f
-- Init.Data.Nat.Lcm
Nat.lcm_comm : ∀ (m n : ℕ), m.lcm n = n.lcm m
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.cellFrontier_subset_skeleton`. -/
Topology.CWComplex.cellFrontier_subset_skeleton : ∀ {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 + 1)),
  Topology.RelCWComplex.cellFrontier (n + 1) j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
-- Mathlib.Data.Matrix.Basic
/-- Extracting entries from a matrix as an additive monoid homomorphism. Note this cannot be upgraded to
a ring homomorphism, as it does not respect multiplication.
 -/
Matrix.entryAddMonoidHom : {m : Type u_2} → {n : Type u_3} → (α : Type u_11) → [inst : AddZeroClass α] → m → n → Matrix m n α →+ α
-- Mathlib.Algebra.GroupWithZero.Range
/-- The map sending a pair of nonzero `r s : A` to the element `(v r)⁻¹ * (v s)`
of `ValueGroup₀ v`.  -/
MonoidWithZeroHom.valueGroup.mk : {A : Type u_1} →
  {B : Type u_2} →
    [inst : MonoidWithZero A] →
      [inst_1 : CommGroupWithZero B] → (f : A →*₀ B) → (r s : A) → f r ≠ 0 → f s ≠ 0 → ↥f.valueGroup
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.isNontrivial_iff_ne_trivial : ∀ {R : Type u_5} [inst : Semiring R] {S : Type u_6} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  [inst_3 : IsOrderedRing S] [inst_4 : DecidablePred fun x => x = 0] [inst_5 : NoZeroDivisors R] [inst_6 : Nontrivial S]
  (v : AbsoluteValue R S), v.IsNontrivial ↔ v ≠ AbsoluteValue.trivial
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.projectiveSeminorm_add_le : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (x y : PiTensorProduct 𝕜 fun i => E i),
  ‖x + y‖ ≤ ‖x‖ + ‖y‖
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.instCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.Category.{v, max (v + 1) u} (CommAlgCat R)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_map : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] {X_1 Y : 𝒰.I₀} (hij : X_1 ⟶ Y),
  𝒰.functorOfLocallyDirected.map hij = 𝒰.trans hij
-- Init.Data.Iterators.Consumers.Loop
Std.instForInPartialOfMonadOfIteratorLoopId : (α β : Type w) →
  (n : Type x → Type x') →
    [Monad n] → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id n] → ForIn n (Std.Iter.Partial β) β
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOp_zero : CategoryTheory.Limits.walkingParallelPairOp.obj CategoryTheory.Limits.WalkingParallelPair.zero =
  Opposite.op CategoryTheory.Limits.WalkingParallelPair.one
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The naturality for the right whiskering.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality.mkNaturalityWhiskerRight : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality m] →
    Mathlib.Tactic.BicategoryLike.NormalizedHom →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.NormalizedHom →
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.Mor₁ →
              Mathlib.Tactic.BicategoryLike.Mor₁ →
                Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                  Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                    Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                      Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → m Lean.Expr
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.of_tail : ∀ {hd : ℝ} {tl : Tactic.ComputeAsymptotics.UnitMonomial},
  hd = 0 → tl.FirstNonzeroIsNeg → Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg (hd :: tl)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A variant of `incl_lift` with `Z` a terminal object.  -/
CategoryTheory.WithTerminal.inclLiftToTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (hZ : CategoryTheory.Limits.IsTerminal Z) →
              CategoryTheory.WithTerminal.incl.comp (CategoryTheory.WithTerminal.liftToTerminal F hZ) ≅ F
-- Init.Data.Dyadic.Basic
Dyadic.precision.eq_1 : Dyadic.zero.precision = none
-- Mathlib.Data.Finsupp.Basic
/-- **Alias** of `Finsupp.mapDomain_finsetSum`. -/
Finsupp.mapDomain_finset_sum : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β} {s : Finset ι}
  {v : ι → α →₀ M}, Finsupp.mapDomain f (∑ i ∈ s, v i) = ∑ i ∈ s, Finsupp.mapDomain f (v i)
-- Init.Data.Vector.Lemmas
Vector.mem_reverse : ∀ {α : Type u_1} {n : ℕ} {x : α} {as : Vector α n}, x ∈ as.reverse ↔ x ∈ as
-- Mathlib.CategoryTheory.Sites.Coverage
/-- Associate a coverage to any Grothendieck topology.
If `J` is a Grothendieck topology, and `K` is the associated coverage, then a presieve
`S` is a covering presieve for `K` if and only if the sieve that it generates is a
covering sieve for `J`.
 -/
CategoryTheory.GrothendieckTopology.toCoverage : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.GrothendieckTopology C → CategoryTheory.Coverage C
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.spanningCoe_induce_top : ∀ {V : Type u} {G : SimpleGraph V} (s : Set V), (⊤.induce s).spanningCoe = (SimpleGraph.induce s G).spanningCoe
-- Mathlib.Algebra.Category.ModuleCat.Kernels
ModuleCat.kernelIsoKer_hom_ker_subtype_apply : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↑(CategoryTheory.Limits.kernel f)),
  ↑((CategoryTheory.ConcreteCategory.hom (ModuleCat.kernelIsoKer f).hom) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f)) x
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_eq_top_of_infinite : ∀ {α : Type u_1} [Infinite α], ENat.card α = ⊤
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.isOpenEmbedding_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.varsToConstants.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} (a : α),
  (FirstOrder.Language.var (Sum.inr a)).varsToConstants = FirstOrder.Language.var a
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftsToLimit.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cone (K.comp F)} →
                  {t : CategoryTheory.Limits.IsLimit c} →
                    (toLiftableCone : CategoryTheory.LiftableCone K F c) →
                      CategoryTheory.Limits.IsLimit toLiftableCone.liftedCone → CategoryTheory.LiftsToLimit K F c t
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The natural isomorphism `t.triangleLEGT a ≅ t.triangleLEGE a b h`
when `a + 1 = b`.  -/
CategoryTheory.Triangulated.TStructure.triangleLEGTIsoTriangleLEGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                (a b : ℤ) → (h : a + 1 = b) → t.triangleLEGT a ≅ t.triangleLEGE a b h
-- Mathlib.NumberTheory.FLT.Three
/-- To prove Fermat's Last Theorem for `n = 3`, it is enough to show that for all `a`, `b`, `c`
in `ℤ` such that `c ≠ 0`, `¬ 3 ∣ a`, `¬ 3 ∣ b`, `a` and `b` are coprime and `3 ∣ c`, we have
`a ^ 3 + b ^ 3 ≠ c ^ 3`.
 -/
_private.Mathlib.NumberTheory.FLT.Three.0.fermatLastTheoremThree_of_three_dvd_only_c : (∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3) → FermatLastTheoremFor 3
-- Mathlib.Topology.Subpath
/-- Reversing `γ.subpath t₀ t₁` results in `γ.subpath t₁ t₀`.  -/
Path.symm_subpath : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ↑unitInterval),
  (γ.subpath t₀ t₁).symm = γ.subpath t₁ t₀
-- Mathlib.Data.Finmap
Finmap.notMem_empty : ∀ {α : Type u} {β : α → Type v} {a : α}, a ∉ ∅
-- Init.Data.Nat.Lemmas
Nat.mod_two_pow_self : ∀ {n : ℕ}, n % 2 ^ n = n
-- Mathlib.Data.Finset.Lattice.Basic
Finset.ite_subset_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s s' : Finset α) (P : Prop) [inst_1 : Decidable P],
  (if P then s else s') ⊆ s ∪ s'
-- Mathlib.FieldTheory.Differential.Basic
Differential.instSubtypeMemIntermediateFieldOfFiniteDimensional : {F : Type u_2} →
  [inst : Field F] →
    [Differential F] →
      [CharZero F] →
        {K : Type u_3} →
          [inst_3 : Field K] →
            [inst_4 : Algebra F K] → (B : IntermediateField F K) → [FiniteDimensional F ↥B] → Differential ↥B
-- Lean.Data.Options
Lean.OptionDeprecation : Type
-- Init.Data.String.Lemmas.Slice
String.Slice.back?_eq : ∀ {s : String.Slice}, s.back? = s.copy.toList.getLast?
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderiv_inv' : ∀ {σ : Type u_1} {R : Type u_2} {i : σ} [inst : Field R] (f : MvPowerSeries σ R),
  (MvPowerSeries.pderiv R i) f⁻¹ = -f⁻¹ ^ 2 * (MvPowerSeries.pderiv R i) f
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageFactorisation.copy_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.ImageFactorisation f) (m : F.F.I ⟶ Y) (e : X ⟶ F.F.I)
  (hm : autoParam (m = F.F.m) CategoryTheory.Limits.ImageFactorisation.copy._auto_1)
  (he : autoParam (e = F.F.e) CategoryTheory.Limits.ImageFactorisation.copy._auto_3),
  (F.copy m e hm he).F = F.F.copy m e ⋯ ⋯
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.var.inj : ∀ {a a_1 : ℕ}, Mathlib.Tactic.ITauto.IProp.var a = Mathlib.Tactic.ITauto.IProp.var a_1 → a = a_1
-- Std.Http.Data.Status
/-- 203 Non-Authoritative Information
 -/
Std.Http.Status.nonAuthoritativeInformation : Std.Http.Status
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeInterpStrLit : String → Option String
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biprod.desc_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {T : C} {f : X ⟶ T} {g : Y ⟶ T},
  CategoryTheory.Limits.biprod.desc f g =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f +
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd g
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.ker_self_comp_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F),
  (A ∘ₗ LinearMap.adjoint A).ker = (LinearMap.adjoint A).ker
-- Mathlib.Topology.Algebra.ConstMulAction
AddAction.IsPretransitive.t1Space_iff : ∀ {α : Type u_2} (G : Type u_4) [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] (x : α) [AddAction.IsPretransitive G α], T1Space α ↔ IsClosed {x}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_eq_getD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, t[a]! = t.getD a default
-- Init.Try
Lean.Try.instInhabitedConfig : Inhabited Lean.Try.Config
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.curryLeft_apply : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂) (x : M 0)
  (m : (i : Fin n) → M i.succ), (f.curryLeft x) m = f (Fin.cons x m)
-- Init.Data.Int.Basic
/-- Decides whether two integers are equal. Usually accessed via the `DecidableEq Int` instance.

This function is overridden by the compiler with an efficient implementation. This definition is the
logical model.

Examples:
* `show (7 : Int) = (3 : Int) + (4 : Int) by decide`
* `if (6 : Int) = (3 : Int) * (2 : Int) then "yes" else "no" = "yes"`
* `(¬ (6 : Int) = (3 : Int)) = true`
 -/
Int.instDecidableEq : DecidableEq ℤ
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.unit'.eq_1 : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α} (h : IsUnit a),
  h.unit' = { val := a, inv := a⁻¹, val_inv := ⋯, inv_val := ⋯ }
-- Mathlib.FieldTheory.SeparableDegree
/-- If `x` and `y` are both separable elements, then `x * y` is also a separable element.  -/
Field.isSeparable_mul : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x y : E},
  IsSeparable F x → IsSeparable F y → IsSeparable F (x * y)
-- Mathlib.AlgebraicTopology.CechNerve
/-- The augmented Čech nerve construction, as a functor from `Arrow C`.  -/
CategoryTheory.SimplicialObject.augmentedCechNerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
      CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.SimplicialObject.Augmented C)
-- Mathlib.Topology.Category.LightProfinite.Sequence
LightProfinite.instMetrizableSpaceOnePointNat : TopologicalSpace.MetrizableSpace (OnePoint ℕ)
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.zero_right : ∀ (b : Ordinal.{u_1}), Ordinal.CNF b 0 = []
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
/-- Cycle graph over `Fin n`  -/
SimpleGraph.cycleGraph : (n : ℕ) → SimpleGraph (Fin n)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Fix.ind_aux : ∀ {F : Type u → Type u} [q : QPF F] (a : (QPF.P F).A) (f : (QPF.P F).B a → (QPF.P F).W),
  QPF.Fix.mk (QPF.abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦WType.mk a f⟧
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The cofork is in fact a coequalizer.  -/
CategoryTheory.IsRegularEpi.isColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.IsRegularEpi f] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.instZero : {α : Type u_1} → Zero (Multiset α)
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_ne_zero_iff_odd : ∀ {n : ℕ}, ↑n ≠ 0 ↔ Odd n
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- The ring tactic normal form of `c.subject`  -/
Mathlib.Tactic.Determinant.Cert.norm : {u : Lean.Level} → {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → Mathlib.Tactic.Determinant.Cert rα → Q(«$α»)
-- Mathlib.Algebra.Ring.Invertible
neg_add_eq_mul_invOf_mul_same_iff : ∀ {R : Type u_1} [inst : Ring R] {a b : R} [inst_1 : Invertible a] [inst_2 : Invertible b],
  -(b + a) = a * ⅟b * a ↔ -1 = ⅟a * b + ⅟b * a
-- Mathlib.Data.Ordmap.Invariants
Ordnode.BalancedSz.dec : DecidableRel Ordnode.BalancedSz
-- Mathlib.Algebra.Polynomial.Lifts
/-- The subring of polynomials that lift.  -/
Polynomial.liftsRing : {R : Type u} → [inst : Ring R] → {S : Type v} → [inst_1 : Ring S] → (R →+* S) → Subring (Polynomial S)
-- Init.Data.SInt.Bitwise
Int16.zero_xor : ∀ {a : Int16}, 0 ^^^ a = a