mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.append.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (x : RBTree.RBNode α)
  (h_1 : (x : RBTree.RBNode α) → motive RBTree.RBNode.nil x) (h_2 : (x : RBTree.RBNode α) → motive x RBTree.RBNode.nil)
  (h_3 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.red c y d))
  (h_4 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.black a x b) (RBTree.RBNode.node RBTree.RBColor.black c y d))
  (h_5 :
    (a l : RBTree.RBNode α) →
      (v : α) →
        (r : RBTree.RBNode α) →
          a = RBTree.RBNode.node RBTree.RBColor.black l v r →
            (b : RBTree.RBNode α) →
              (x : α) →
                (c : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.black l v r) (RBTree.RBNode.node RBTree.RBColor.red b x c))
  (h_6 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c l : RBTree.RBNode α) →
          (v : α) →
            (r : RBTree.RBNode α) →
              c = RBTree.RBNode.node RBTree.RBColor.black l v r →
                motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.black l v r)),
  (match RBTree.RBNode.nil, x with
    | RBTree.RBNode.nil, x => h_1 x
    | x, RBTree.RBNode.nil => h_2 x
    | RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d => h_3 a x b c y d
    | RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d => h_4 a x b c y d
    | a@h:(RBTree.RBNode.node RBTree.RBColor.black l v r), RBTree.RBNode.node RBTree.RBColor.red b x c =>
      h_5 a l v r h b x c
    | RBTree.RBNode.node RBTree.RBColor.red a x b, c@h:(RBTree.RBNode.node RBTree.RBColor.black l v r) =>
      h_6 a x b c l v r h) =
    h_1 x
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.δ_comp_toMk₁_of_le : ∀ {n : ℕ} (i : Fin (n + 3)) (j : Fin (n + 2)) (h : i ≤ j.castSucc),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.toMk₁ i) =
    SimplexCategory.toMk₁ (i.castPred ⋯)
-- Mathlib.Algebra.Quandle
/-- Proof of right inverse  -/
Rack.right_inv : ∀ {α : Type u} [self : Rack α] (x : α), Function.RightInverse (Rack.invAct x) (Shelf.act x)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.coe_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  Function.Injective DFunLike.coe
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.StrictMono.funext : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {N : Type u_5} [inst_1 : AddCommGroup N] [inst_2 : Module R N]
  {M : Type u_6} [IsHausdorff I N] {f g : M → N} {a : ℕ → ℕ},
  StrictMono a → (∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)) → f = g
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_eq_some_iff_exists_beq_and_mem_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {v : β},
  Std.DHashMap.Const.get? m k = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ Std.DHashMap.Const.toList m
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.isMultiplicative_sigma : ∀ {k : ℕ}, (ArithmeticFunction.sigma k).IsMultiplicative
-- Mathlib.Data.Set.Basic
Set.powerset_nonempty : ∀ {α : Type u} {s : Set α}, (𝒫 s).Nonempty
-- Init.Data.Vector.Lemmas
Vector.contains_map : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} [inst : BEq β] {xs : Vector α n} {x : β} {f : α → β},
  (Vector.map f xs).contains x = xs.any fun a => x == f a
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_eq_top : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι],
  MeasureTheory.IsStoppingTime f τ → MeasurableSet {ω | τ ω = ⊤}
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.toHomeomorph : {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] → (A ≃A[R] B) → A ≃ₜ B
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The canonical inclusion `M → TrivSqZeroExt R M`.  -/
TrivSqZeroExt.inr : {R : Type u} → {M : Type v} → [Zero R] → M → TrivSqZeroExt R M
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) (ψ : F₂ ⟶ F₃)
  [CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.CategoryStruct.comp φ ψ)],
  CategoryTheory.Presheaf.IsLocallyInjective J φ
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galRestrict'.congr_simp : ∀ (A : Type u_1) {K : Type u_2} {L : Type u_3} {L₂ : Type u_4} (B : Type u_6) (B₂ : Type u_7) [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : Algebra K L] [inst_10 : Algebra A L]
  [inst_11 : IsScalarTower A K L] [inst_12 : Algebra K L₂] [inst_13 : Algebra A L₂] [inst_14 : IsScalarTower A K L₂]
  [inst_15 : Algebra B L] [inst_16 : IsScalarTower A B L] [inst_17 : IsIntegralClosure B A L] [inst_18 : Algebra B₂ L₂]
  [inst_19 : IsScalarTower A B₂ L₂] [inst_20 : IsIntegralClosure B₂ A L₂] (f f_1 : L →ₐ[K] L₂),
  f = f_1 → galRestrict' A B B₂ f = galRestrict' A B B₂ f_1
-- Std.Data.DHashMap.Internal.RawLemmas
/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `get_insertIfNew`.  -/
Std.DHashMap.Internal.Raw₀.contains_of_contains_insertIfNew' : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {k a : α} {v : β k},
      (m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearMap.adjoint_rTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] [inst_7 : FiniteDimensional 𝕜 E]
  [inst_8 : FiniteDimensional 𝕜 F] [inst_9 : FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F),
  LinearMap.adjoint (LinearMap.rTensor G f) = LinearMap.rTensor G (LinearMap.adjoint f)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.ringEquivOpMop_apply : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring R) (a : ↥S),
  S.ringEquivOpMop a = MulOpposite.op (S.addEquivOp a)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.comap_comap : ∀ {R : Type u} {S : Type v} {T : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : NonUnitalNonAssocRing T] (s : NonUnitalSubring T) (g : S →ₙ+* T) (f : R →ₙ+* S),
  NonUnitalSubring.comap f (NonUnitalSubring.comap g s) = NonUnitalSubring.comap (g.comp f) s
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- If `C.d i j` and `C.d i' j` are both allowed, then we must have `i = i'`,
and so the differentials only differ by an `eqToHom`.
 -/
HomologicalComplex.eqToHom_comp_d : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i i' j : ι}
  (rij : c.Rel i j) (rij' : c.Rel i' j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (C.d i' j) = C.d i j
-- Mathlib.Topology.Algebra.PontryaginDual
instTopologicalSpacePontryaginDual : (A : Type u_1) → [inst : Monoid A] → [inst_1 : TopologicalSpace A] → TopologicalSpace (PontryaginDual A)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx?.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → ℕ → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : ℕ) →
          ((x : ℕ) → motive Std.DTreeMap.Internal.Impl.leaf x) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l r : Std.DTreeMap.Internal.Impl α β) →
                      (n : ℕ) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n) →
              motive x x_1
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.instCoePowerSeries : {R : Type u_1} → [inst : Semiring R] → Coe (PowerSeries R) (LaurentSeries R)
-- Aesop.Stats.Basic
Aesop.GoalKind.noConfusionType : Sort v✝ → Aesop.GoalKind → Aesop.GoalKind → Sort v✝
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.curryRingEquiv.eq_1 : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N],
  AddMonoidAlgebra.curryRingEquiv = { toEquiv := AddMonoidAlgebra.curryAddEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯ }
-- Mathlib.Data.Nat.Hyperoperation
/-- Implementation of the hyperoperation sequence
where `hyperoperation n m k` is the `n`th hyperoperation between `m` and `k`.
 -/
hyperoperation : ℕ → ℕ → ℕ → ℕ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- An alternative constructor for `IsStableUnderCobaseChange`.  -/
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.RespectsIso],
  (∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasPushout f g],
      P f → P (CategoryTheory.Limits.pushout.inr f g)) →
    P.IsStableUnderCobaseChange
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `G` is an equivalence, then a right extension of `F` along `L` is universal iff
the corresponding left extension of `G ⋙ F` along `G ⋙ L` is.  -/
CategoryTheory.Functor.RightExtension.isUniversalPrecompEquiv : {C : Type u_1} →
  {C' : Type u_2} →
    {H : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (L : CategoryTheory.Functor C D) →
                  (F : CategoryTheory.Functor C H) →
                    (G : CategoryTheory.Functor C' C) →
                      [G.IsEquivalence] →
                        (e : L.RightExtension F) →
                          CategoryTheory.CostructuredArrow.IsUniversal e ≃
                            CategoryTheory.CostructuredArrow.IsUniversal
                              ((CategoryTheory.Functor.RightExtension.precomp L F G).obj e)
-- Mathlib.Order.LatticeIntervals
Set.Ici.orderBot : {α : Type u_1} → [inst : Preorder α] → {a : α} → OrderBot ↑(Set.Ici a)
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.hasForgetToBoolAlg : CategoryTheory.HasForget₂ FinBoolAlg BoolAlg
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
AlgebraicTopology.DoldKan.hσ'_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {q n a m : ℕ} (ha : n = a + q) (hnm : AlgebraicTopology.DoldKan.c.Rel m n),
  AlgebraicTopology.DoldKan.hσ' q n m hnm =
    CategoryTheory.CategoryStruct.comp ((-1) ^ a • X.σ ⟨a, ⋯⟩) (CategoryTheory.eqToHom ⋯)
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalExprApplyNewGoals : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.ApplyNewGoals
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_preimage_im : ∀ (s : Set ℝ), frontier (Complex.im ⁻¹' s) = Complex.im ⁻¹' frontier s
-- Mathlib.Order.CompleteLattice.Basic
Antitone.sInf : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : CompleteLattice β] {s : Set (α → β)},
  (∀ f ∈ s, Antitone f) → Antitone (sInf s)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The domain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.WhiskerLeft.srcM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.WhiskerLeft → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Algebra.Category.MonCat.Limits
/-- Construction of a limit cone in `MonCat`.
(Internal use only; use the limits API.)
 -/
MonCat.HasLimits.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J MonCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] → CategoryTheory.Limits.Cone F
-- Lean.Meta.LazyDiscrTree
/-- An unprocessed entry in the lazy discrimination tree.
 -/
Lean.Meta.LazyDiscrTree.LazyEntry : Type u_1 → Type u_1
-- Std.Sat.AIG.CachedLemmas
Std.Sat.AIG.mkGateCached.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.mkGateCached input =
    if input.lhs.gate < input.rhs.gate then Std.Sat.AIG.mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs }
    else Std.Sat.AIG.mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }
-- Mathlib.Analysis.PSeries
sum_Ioo_inv_sq_le : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (k n : ℕ),
  ∑ i ∈ Finset.Ioo k n, (↑i ^ 2)⁻¹ ≤ 2 / (↑k + 1)
-- Init.Data.Nat.Lemmas
Nat.pow_lt_pow_iff_right : ∀ {a n m : ℕ}, 1 < a → (a ^ n < a ^ m ↔ n < m)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  AddMonCat.FilteredColimits.colimit F = AddMonCat.of (AddMonCat.FilteredColimits.M F)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.obj_μ_zero_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (m₁ m₂ : M)
  (X : C) [inst_3 : F.Monoidal],
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit M) m₂).app
        ((F.obj m₁).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.LaxMonoidal.μ F m₁
              (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)
                m₂)).app
          X)
        (CategoryTheory.CategoryStruct.comp
          ((F.map
                (CategoryTheory.MonoidalCategoryStruct.associator m₁
                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit M) m₂).inv).app
            X)
          ((CategoryTheory.Functor.OplaxMonoidal.δ F
                (CategoryTheory.MonoidalCategoryStruct.tensorObj m₁
                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit M))
                m₂).app
            X))) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit M) m₂).app
        ((F.obj m₁).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor m₂).hom).app ((F.obj m₁).obj X))
        ((F.obj m₂).map ((F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor m₁).inv).app X)))
-- Lean.Elab.MutualInductive
/-- Heuristic: users don't tend to want types that are universe polymorphic across both `Prop` and `Type _`.
This can be disabled by setting the option `bootstrap.inductiveCheckResultingUniverse` to false,
unless one of the inductive commands requires it (for instance `structure` due to projections).
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.checkResultingUniversePolymorphism : Array Lean.Elab.Command.InductiveView → Lean.Level → ℕ → List Lean.InductiveType → Lean.Elab.TermElabM Unit
-- Aesop.RuleSet
Aesop.BaseRuleSet.mk.sizeOf_spec : ∀ (normRules : Aesop.Index Aesop.NormRuleInfo) (unsafeRules : Aesop.Index Aesop.UnsafeRuleInfo)
  (safeRules : Aesop.Index Aesop.SafeRuleInfo) (unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name))
  (forwardRules : Aesop.ForwardIndex) (forwardRuleNames : Lean.PHashSet Aesop.RuleName)
  (rulePatterns : Aesop.RulePatternIndex) (erased : Lean.PHashSet Aesop.RuleName)
  (ruleNames : Lean.PHashMap Lean.Name (Aesop.UnorderedArraySet Aesop.RuleName)),
  sizeOf
      { normRules := normRules, unsafeRules := unsafeRules, safeRules := safeRules, unfoldRules := unfoldRules,
        forwardRules := forwardRules, forwardRuleNames := forwardRuleNames, rulePatterns := rulePatterns,
        erased := erased, ruleNames := ruleNames } =
    1 + sizeOf normRules + sizeOf unsafeRules + sizeOf safeRules + sizeOf unfoldRules + sizeOf forwardRules +
            sizeOf forwardRuleNames +
          sizeOf rulePatterns +
        sizeOf erased +
      sizeOf ruleNames
-- Mathlib.Data.Fin.Fin2
_private.Mathlib.Data.Fin.Fin2.0.Fin2.toNat.match_1.splitter : (motive : (x : ℕ) → Fin2 x → Sort u_1) →
  (x : ℕ) →
    (x_1 : Fin2 x) → ((n : ℕ) → motive (n + 1) Fin2.fz) → ((n : ℕ) → (i : Fin2 n) → motive (n + 1) i.fs) → motive x x_1
-- Mathlib.MeasureTheory.Measure.AddContent
/-- An additive content with values in `ℝ≥0∞` is said to be sigma-sub-additive if for any sequence
of sets `f` in `C` such that `⋃ i, f i ∈ C`, we have `m (⋃ i, f i) ≤ ∑' i, m (f i)`.  -/
MeasureTheory.AddContent.IsSigmaSubadditive : {α : Type u_1} → {C : Set (Set α)} → MeasureTheory.AddContent ENNReal C → Prop
-- Std.Time.Zoned.ZoneRules
/-- Indicates if the time is wall clock or standard time.
 -/
Std.Time.TimeZone.LocalTimeType.wall : Std.Time.TimeZone.LocalTimeType → Std.Time.TimeZone.StdWall
-- Mathlib.RingTheory.Localization.BaseChange
Algebra.isPushout_of_isLocalization : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A] (T : Type u_5) (B : Type u_6) [inst_4 : CommSemiring T]
  [inst_5 : CommSemiring B] [inst_6 : Algebra R T] [inst_7 : Algebra T B] [inst_8 : Algebra R B] [inst_9 : Algebra A B]
  [inst_10 : IsScalarTower R T B] [inst_11 : IsScalarTower R A B] [IsLocalization (Algebra.algebraMapSubmonoid T S) B],
  Algebra.IsPushout R T A B
-- Init.Control.Lawful.Instances
OptionT.run_restoreM : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (x : stM m (OptionT m) α), (restoreM x).run = pure x
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.comap_map : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (s : Subfield K),
  Subfield.comap f (Subfield.map f s) = s
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- The relative perfect closure of `F` in `E` is purely inseparable over `F`.  -/
perfectClosure.isPurelyInseparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IsPurelyInseparable F ↥(perfectClosure F E)
-- Mathlib.Topology.Maps.Strict.Basic
/-- Assume that `f : X → Y` is a quotient map. Then `g : Y → Z` is strict
if and only if `g ∘ f` is strict.  -/
Topology.IsQuotientMap.isStrictMap_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z},
  Topology.IsQuotientMap f → (Topology.IsStrictMap g ↔ Topology.IsStrictMap (g ∘ f))
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_comap_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S], Function.Surjective ⇑f → ∀ (I : Ideal S), Ideal.map f (Ideal.comap f I) = I
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.exists_genWeightSpace_le_ker_of_isNoetherian : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsNoetherian R M] (χ : L → R) (x : L),
  ∃ k,
    ↑(LieModule.genWeightSpace M χ) ≤
      LinearMap.ker (((LieModule.toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.step : {α : Type u} →
  {β : α → Type v} → Std.DTreeMap.Internal.Zipper α β → Std.IterStep (Std.IterM Id ((a : α) × β a)) ((a : α) × β a)
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
/-- In a normed space, linear independence of `v` implies positive definiteness of `gram 𝕜 v`.  -/
Matrix.posDef_gram_of_linearIndependent : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [Finite n] {v : n → E}, LinearIndependent 𝕜 v → (Matrix.gram 𝕜 v).PosDef
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.fieldRange_eq_map : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L),
  f.fieldRange = Subfield.map f ⊤
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.center_eq_top : ∀ (M : Type u_1) [inst : CommMonoid M], Submonoid.center M = ⊤
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hexagon_forward : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  (X Y Z : CategoryTheory.Arrow C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding X
            (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
        (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding X Y).hom Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y
          (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding X Z).hom))
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Ioo_eq_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a < b → Set.Iic a ∪ Set.Ioo a b = Set.Iio b
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.fintypeMultiples : {M : Type u_1} → [inst : AddMonoid M] → {a : M} → [Fintype M] → Fintype ↥(AddSubmonoid.multiples a)
-- Mathlib.RingTheory.RingHom.Surjective
RingHom.surjective_respectsIso : RingHom.RespectsIso fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.toNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T₁ T₂ : CategoryTheory.Monad C} → CategoryTheory.MonadHom T₁ T₂ → CategoryTheory.NatTrans T₁.toFunctor T₂.toFunctor
-- Init.Data.List.Lemmas
List.ne_nil_of_length_eq_add_one : ∀ {α : Type u_1} {l : List α} {n : ℕ}, l.length = n + 1 → l ≠ []