mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal.hσ'₀ : ∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (f₁ :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x)),
  (∀ (x : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })),
      f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op))
          (f₀ x)) →
    ∀ (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      SSet.Truncated.liftOfStrictSegal.f₂ f₀ f₁ hδ₁ hδ₀ hY
          ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_15✝ _proof_12✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_15✝ _proof_12✝).op)) (f₁ x)
-- Lean.Elab.InfoTree.Types
/-- Info for an option reference (e.g. in `set_option`).  -/
Lean.Elab.OptionInfo : Type
-- Mathlib.Topology.Algebra.Order.Group
/-- In a linearly ordered multiplicative group, the integer powers of an element are dense
iff they are the whole group.  -/
denseRange_zpow_iff_surjective : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G] {a : G}, (DenseRange fun x => a ^ x) ↔ Function.Surjective fun x => a ^ x
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Isomorphisms that exhibits the essential image of `ι` as closed under day
convolution.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObjIsoConvolution : (C : Type u₁) →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    (V : Type u₂) →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            {D : Type u₃} →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] →
                  (d d' : D) →
                    (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).obj
                        (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObj
                          C V d d') ≅
                      CategoryTheory.MonoidalCategory.DayConvolution.convolution
                        ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                              D).obj
                          d)
                        ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                              D).obj
                          d')
-- Mathlib.Topology.Order
/-- A topological space is nontrivial if it is not the indiscrete topology.  -/
NontrivialTopology : (α : Type u_2) → [TopologicalSpace α] → Prop
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- The natural transformation `H ⟶ F` that exists for every adjoint triple `F ⊣ G ⊣ H` where `G`
is fully faithful, given here as the preimage of `adj₂.counit ≫ adj₁.unit : H ⋙ G ⟶ F ⋙ G`
under whiskering with `G`.  -/
CategoryTheory.Adjunction.Triple.rightToLeft : {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] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            {H : CategoryTheory.Functor C D} → CategoryTheory.Adjunction.Triple F G H → [G.Full] → [G.Faithful] → H ⟶ F
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.neg_toGerm : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddGroup γ] [inst_3 : IsTopologicalAddGroup γ] (f : α →ₘ[μ] γ), (-f).toGerm = -f.toGerm
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
/-- The pivot of the resulting echelon form.  -/
Echelon.Decomposition.pivot : {m : Type u_1} →
  [inst : Fintype m] →
    [inst_1 : LinearOrder m] →
      {n : Type u_2} →
        [inst_2 : LinearOrder n] →
          {R : Type u_3} → [inst_3 : CommRing R] → {A : Matrix m n R} → Echelon.Decomposition A → m → WithTop n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {km : α}, t.minKey? = some km → t.getKey? km = some km
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β k}, (t.insertIfNew k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.isComplex₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ComposableArrows C 1), S.IsComplex
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.diff_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.diff t₂ = t₁ \ t₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.eraseMany!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ α] (t : Std.DTreeMap.Internal.Impl α β)
  (l : ρ),
  t.eraseMany! l =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun a __s =>
            let r := __s;
            have r := ⟨Std.DTreeMap.Internal.Impl.erase! a ↑r, ⋯⟩;
            pure (ForInStep.yield r)
      have r : t.IteratedSlowErasureFrom := __s
      pure r).run
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_add : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (x y : ↥S), ↑(x + y) = ↑x + ↑y
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithTop.decidableLE.match_1.eq_2 : ∀ {α : Type u_1} (motive : WithTop α → WithTop α → Sort u_2) (a : α) (h_1 : (x : WithTop α) → motive none x)
  (h_2 : (a : α) → motive (some a) none) (h_3 : (a b : α) → motive (some a) (some b)),
  (match some a, none with
    | none, x => h_1 x
    | some a, none => h_2 a
    | some a, some b => h_3 a b) =
    h_2 a
-- Mathlib.Algebra.Group.Submonoid.Pointwise
/-- Pointwise negation of additive submonoids as an order isomorphism  -/
AddSubmonoid.negOrderIso : {G : Type u_2} → [inst : AddGroup G] → AddSubmonoid G ≃o AddSubmonoid G
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {s : CategoryTheory.Limits.Cone F} {G : CategoryTheory.Functor K C} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (e : J ≌ K) (w : e.functor.comp G ≅ F),
  P.conePointsIsoOfEquivalence Q e w =
    {
      hom :=
        Q.lift
          ((CategoryTheory.Limits.Cone.equivalenceOfReindexing e.symm
                  ((e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G)).functor.obj
            s),
      inv := P.lift ((CategoryTheory.Limits.Cone.equivalenceOfReindexing e w).functor.obj t), hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.differentiableAt_eta_tprod : ∀ {z : ℂ},
  z ∈ UpperHalfPlane.upperHalfPlaneSet → DifferentiableAt ℂ (fun x => ∏' (n : ℕ), (1 - ModularForm.eta_q n x)) z
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_X_pow_sub : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {n : ℕ}, p.degree < ↑n → (Polynomial.X ^ n - p).Monic
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.ofAscListAux₁.match_5.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : α) (xs : List α) (h_1 : Unit → motive [])
  (h_2 : (x : α) → (xs : List α) → motive (x :: xs)),
  (match x :: xs with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_2 x xs
-- Mathlib.Data.NNReal.Defs
NNReal.algebraMap_eq_coe : ⇑(algebraMap NNReal ℝ) = NNReal.toReal
-- Mathlib.Order.Category.PartOrd
_private.Mathlib.Order.Category.PartOrd.0.PartOrd.Hom.mk.injEq : ∀ {X Y : PartOrd} (hom' hom'_1 : ↑X →o ↑Y), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.toPartialEquiv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        {I : ModelWithCorners 𝕜 E H₁} →
                          {J : ModelWithCorners 𝕜 F H₂} →
                            {M : Type u_8} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        {n : WithTop ℕ∞} → PartialDiffeomorph I J M N n → PartialEquiv M N
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.Indep.union_isBasis_union_of_contract_isBasis : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.Indep I → (M.contract I).IsBasis J X → M.IsBasis (J ∪ I) (X ∪ I)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.toWord.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j : ι} (w : Monoid.CoprodI.NeWord M i j),
  w.toWord = { toList := w.toList, ne_one := ⋯, chain_ne := ⋯ }
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- **Dirichlet's Theorem** on primes in arithmetic progression: if `q` is a positive
integer and `a : ℕ` is coprime to `q`, then there are infinitely many prime numbers `p`
such that `p ≡ a mod q`.  -/
Nat.forall_exists_prime_gt_and_modEq : ∀ (n : ℕ) {q a : ℕ}, q ≠ 0 → a.Coprime q → ∃ p > n, Nat.Prime p ∧ p ≡ a [MOD q]
-- Mathlib.Topology.ClusterPt
Filter.Tendsto.mapClusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [F.NeBot],
  Filter.Tendsto u F (nhds x) → MapClusterPt x F u
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGE_obj_bot : ∀ {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), t.eTruncGE.obj ⊥ = CategoryTheory.Functor.id C
-- Mathlib.Analysis.LocallyConvex.AbsConvex
closedAbsConvexHull_isClosed : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] [inst_4 : TopologicalSpace E] (s : Set E),
  (closedAbsConvexHull 𝕜).IsClosed s = (AbsConvex 𝕜 s ∧ IsClosed s)
-- Mathlib.Data.Rel
/-- Restrict the domain of a relation to a subtype.  -/
SetRel.restrictDomain : {α : Type u_1} → {β : Type u_2} → SetRel α β → (s : Set α) → SetRel (↑s) β
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The integral of an almost-everywhere strongly measurable function over `UnitAddCircle` is
equal to the integral over an interval $(t, t + 1]$ in `ℝ` of its lift to `ℝ`.  -/
UnitAddCircle.integral_preimage : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (t : ℝ) (f : UnitAddCircle → E),
  ∫ (a : ℝ) in Set.Ioc t (t + 1), f ↑a = ∫ (b : UnitAddCircle), f b
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_homOfLE_isoImage_ι_hom : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V) (W : TopologicalSpace.Opens ↥↑V),
  CategoryTheory.CategoryStruct.comp (X.homOfLE e ∣_ W) (AlgebraicGeometry.Scheme.Hom.isoImage V.ι W).hom =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.isoImage U.ι ((TopologicalSpace.Opens.map (X.homOfLE e).base).obj W)).hom
      (X.homOfLE ⋯)
-- Mathlib.Data.EReal.Basic
EReal.coe_zero : ↑0 = 0
-- Mathlib.Order.Monotone.Odd
/-- An odd function on a linear ordered additive commutative group is strictly antitone on the whole
group provided that it is strictly antitone on `Set.Ici 0`.  -/
strictAnti_of_odd_strictAntiOn_nonneg : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G]
  [inst_3 : AddCommGroup H] [inst_4 : PartialOrder H] [IsOrderedAddMonoid H] {f : G → H},
  (∀ (x : G), f (-x) = -f x) → StrictAntiOn f (Set.Ici 0) → StrictAnti f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.fvarId : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.CodeDecl pu → Lean.FVarId
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.IsPreconnected.mk : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J],
  (∀ {α : Type u₁} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j : J),
      Nonempty (F ≅ (CategoryTheory.Functor.const J).obj (F.obj j))) →
    CategoryTheory.IsPreconnected J
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α}, k ∉ m₁ → (m₁ ∩ m₂).get? k = none
-- Mathlib.Logic.Embedding.Basic
/-- Embedding of a `Subtype`.  -/
Function.Embedding.subtype : {α : Sort u_1} → (p : α → Prop) → Subtype p ↪ α
-- Mathlib.Algebra.Order.Monovary
/-- Two functions antivary iff the rearrangement inequality holds.  -/
antivary_iff_smul_rearrangement : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β},
  Antivary f g ↔ ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.go.eq_def : ∀ (aig : Std.Sat.AIG ℕ) (upper : ℕ) (h : upper < aig.decls.size) (state : Std.Sat.AIG.toCNF.State✝ aig),
  Std.Sat.AIG.toCNF.go✝ aig upper h state =
    if hmarked : (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ state))[upper] = true then ⟨state, ⋯⟩
    else
      let decl := aig.decls[upper];
      match heq : decl with
      | Std.Sat.AIG.Decl.false => Std.Sat.AIG.toCNF.State.addFalse✝ state upper h heq
      | Std.Sat.AIG.Decl.atom idx => Std.Sat.AIG.toCNF.State.addAtom✝ state upper h heq
      | Std.Sat.AIG.Decl.gate lhs rhs =>
        have this := ⋯;
        match Std.Sat.AIG.toCNF.go✝ aig lhs.gate ⋯ state with
        | ⟨lstate, hlstate⟩ =>
          match Std.Sat.AIG.toCNF.go✝ aig rhs.gate ⋯ lstate with
          | ⟨rstate, hrstate⟩ =>
            have this_1 := ⋯;
            match Std.Sat.AIG.toCNF.State.addGate✝ rstate upper h heq ⋯ ⋯ with
            | ⟨ret, hretstate⟩ => ⟨ret, ⋯⟩
-- Mathlib.Algebra.Algebra.Spectrum.Basic
resolventSet_neg : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A),
  resolventSet R (-a) = -resolventSet R a
-- Mathlib.Data.Finset.Card
List.toFinset_card_of_nodup : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α}, l.Nodup → l.toFinset.card = l.length
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.norm_pi_le_of_le : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {M : ι → Type u_10}
  [inst_4 : (i : ι) → SeminormedAddCommGroup (M i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (M i)] {C : ℝ}
  {L : (i : ι) → E →L[𝕜] M i}, (∀ (i : ι), ‖L i‖ ≤ C) → 0 ≤ C → ‖ContinuousLinearMap.pi L‖ ≤ C
-- Mathlib.Data.Nat.EvenOddRec
Nat.evenOddRec_even : ∀ {P : ℕ → Sort u_1} (h0 : P 0) (h_even : (i : ℕ) → P i → P (2 * i)) (h_odd : (i : ℕ) → P i → P (2 * i + 1)),
  h_even 0 h0 = h0 → ∀ (n : ℕ), Nat.evenOddRec h0 h_even h_odd (2 * n) = h_even n (Nat.evenOddRec h0 h_even h_odd n)
-- ProofWidgets.Util
/-- Certain monad transformers such as `ReaderT` and `StateT`/`StateRefT`
provide additional *context* (read-only) and *state* (mutable).
`MonadSaveCtx m n` means that `m` is a stack of contexts/states on top of `n`.
It provides a way to suspend an `m`-action by saving the "current" value of this stack.

For example, `m = Lean.MetaM` is a stack of contexts and states on top of `n = EIO Lean.Exception`.
Thus we have `saveCtxM : Lean.MetaM α → Lean.MetaM (EIO Lean.Exception α)`.  -/
MonadSaveCtx : (Type → Type) → outParam (Type → Type) → Type 1
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.partialOrder : {α : Type u_1} →
  [inst : AddCommMonoid α] →
    [inst_1 : PartialOrder α] → [IsOrderedCancelAddMonoid α] → {s : AddSubmonoid α} → PartialOrder (AddLocalization s)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- The category of `κ`-filtered partially ordered types,
with morphisms given by order embeddings.  -/
CategoryTheory.CardinalDirectedPoset : (κ : Cardinal.{u}) → [Fact κ.IsRegular] → Type (u + 1)
-- Mathlib.Data.Sign.Basic
sign_intCast : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [Nontrivial α] [inst_4 : DecidableLT α]
  (n : ℤ), SignType.sign ↑n = SignType.sign n
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.ofList_symm : ∀ {α : Type u_1}, FreeMonoid.ofList.symm = FreeMonoid.toList
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.SplitCandidate.some.injEq : ∀ (c : Lean.Meta.Grind.SplitInfo) (numCases : ℕ) (isRec tryPostpone : Bool) (c_1 : Lean.Meta.Grind.SplitInfo)
  (numCases_1 : ℕ) (isRec_1 tryPostpone_1 : Bool),
  (Lean.Meta.Grind.SplitCandidate.some✝ c numCases isRec tryPostpone =
      Lean.Meta.Grind.SplitCandidate.some✝ c_1 numCases_1 isRec_1 tryPostpone_1) =
    (c = c_1 ∧ numCases = numCases_1 ∧ isRec = isRec_1 ∧ tryPostpone = tryPostpone_1)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The restriction from `EuclideanSpace 𝕜 J` to `EuclideanSpace 𝕜 I` when `I ⊆ J`.  -/
EuclideanSpace.restrict₂ : {ι' : Type u_2} →
  {𝕜 : Type u_3} → [inst : RCLike 𝕜] → {I J : Finset ι'} → I ⊆ J → EuclideanSpace 𝕜 ↥J →L[𝕜] EuclideanSpace 𝕜 ↥I
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Stats.mk.sizeOf_spec : ∀ (numNodes numNull numCollisions maxDepth : ℕ),
  sizeOf { numNodes := numNodes, numNull := numNull, numCollisions := numCollisions, maxDepth := maxDepth } =
    1 + sizeOf numNodes + sizeOf numNull + sizeOf numCollisions + sizeOf maxDepth
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Complex.deriv_log : ∀ {x : ℂ}, x ∈ Complex.slitPlane → deriv Complex.log x = x⁻¹
-- Lean.Meta.LazyDiscrTree
/-- Eliminate loose bound variables via beta-reduction.

This is primarily used to reduce pi-terms `∀(x : P), T` into
non-dependent functions `P → T`.  The latter has a more specific
discrimination tree key `.arrow..` and this improves the accuracy of the
discrimination tree.

Clone of `Lean.Meta.DiscrTree.elimLooseBVarsByBeta`.  See it for more
discussion.
 -/
Lean.Meta.LazyDiscrTree.MatchClone.elimLooseBVarsByBeta : Lean.Expr → Lean.CoreM Lean.Expr
-- Init.Data.Sum.Lemmas
Sum.forall : ∀ {α : Type u_1} {β : Type u_2} {p : α ⊕ β → Prop},
  (∀ (x : α ⊕ β), p x) ↔ (∀ (a : α), p (Sum.inl a)) ∧ ∀ (b : β), p (Sum.inr b)
-- Mathlib.RingTheory.Coalgebra.Quotient
/-- `Submodule.mkQ` as a coalgebra homomorphism.  -/
Coalgebra.Quotient.mkQCoalgHom : {R : Type u_1} →
  {C : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup C] →
        [inst_2 : Module R C] →
          [inst_3 : CoalgebraStruct R C] → (I : Submodule R C) → [inst_4 : I.IsCoideal] → C →ₗc[R] C ⧸ I
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Inhabited α] [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∩ t₂).get! k = default
-- Mathlib.CategoryTheory.Monad.Limits
/-- A monadic functor creates colimits if it preserves colimits.  -/
CategoryTheory.monadicCreatesColimitsOfPreservesColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (R : CategoryTheory.Functor D C) →
          [CategoryTheory.MonadicRightAdjoint R] →
            [CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R] →
              CategoryTheory.CreatesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by projection onto the first factor.  -/
ContinuousMonoidHom.fst : (A : Type u_2) →
  (B : Type u_3) →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → A × B →ₜ* A
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_maxKey?_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)}, Std.Internal.List.containsKey k l = true → (Std.Internal.List.maxKey? l).isSome = true
-- Lean.Meta.Instances
Lean.Meta.Instances.mk.inj : ∀ {discrTree : Lean.Meta.InstanceTree} {instanceNames : Lean.PHashMap Lean.Name Lean.Meta.InstanceEntry}
  {erased : Lean.PHashSet Lean.Name} {discrTree_1 : Lean.Meta.InstanceTree}
  {instanceNames_1 : Lean.PHashMap Lean.Name Lean.Meta.InstanceEntry} {erased_1 : Lean.PHashSet Lean.Name},
  { discrTree := discrTree, instanceNames := instanceNames, erased := erased } =
      { discrTree := discrTree_1, instanceNames := instanceNames_1, erased := erased_1 } →
    discrTree = discrTree_1 ∧ instanceNames = instanceNames_1 ∧ erased = erased_1
-- Mathlib.Data.Seq.Basic
Stream'.Seq.mem_map : ∀ {α : Type u} {β : Type v} (f : α → β) {a : α} {s : Stream'.Seq α}, a ∈ s → f a ∈ Stream'.Seq.map f s
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.toZMod_eq_residueField_comp_residue : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)],
  PadicInt.toZMod = PadicInt.residueField.toRingHom.comp (IsLocalRing.residue ℤ_[p])
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.instConcreteCategoryContinuousMapCarrierToTop : CategoryTheory.ConcreteCategory CompactlyGenerated fun x1 x2 => C(↑x1.toTop, ↑x2.toTop)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- A set of points is cospherical if they are equidistant from some
point. In two dimensions, this is the same thing as being
concyclic.  -/
EuclideanGeometry.Cospherical : {P : Type u_2} → [MetricSpace P] → Set P → Prop