mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.step.match_3.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Lean.PersistentHashMap.Zipper α β → Sort u_3)
  (h_1 : Unit → motive Lean.PersistentHashMap.Zipper.done)
  (h_2 :
    (es : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      (z' : Lean.PersistentHashMap.Zipper α β) → motive (Lean.PersistentHashMap.Zipper.consEntries es z'))
  (h_3 :
    (keys : Subarray α) →
      (vals : Subarray β) →
        (hsz : Std.Slice.size keys = Std.Slice.size vals) →
          (z' : Lean.PersistentHashMap.Zipper α β) →
            motive (Lean.PersistentHashMap.Zipper.consCollision keys vals hsz z')),
  (match Lean.PersistentHashMap.Zipper.done with
    | Lean.PersistentHashMap.Zipper.done => h_1 ()
    | Lean.PersistentHashMap.Zipper.consEntries es z' => h_2 es z'
    | Lean.PersistentHashMap.Zipper.consCollision keys vals hsz z' => h_3 keys vals hsz z') =
    h_1 ()
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
CategoryTheory.ObjectProperty.IsLocal.toIsClosedUnderIsomorphisms : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C}
  (K : CategoryTheory.Precoverage C) [self : P.IsLocal K], P.IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.zero_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (a : α), 0 a = 0
-- Init.Data.UInt.Bitwise
USize.toUInt64_and : ∀ (a b : USize), (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.of_le_isUnit : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R}, S ≤ IsUnit.submonoid R → IsLocalization S R
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.nonsingular_iff_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    (W.Nonsingular P ↔
      W.Equation P ∧ ((MvPolynomial.eval P) W.polynomialX ≠ 0 ∨ (MvPolynomial.eval P) W.polynomialY ≠ 0))
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.snd_mapComp_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c : B × C} (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.Bicategory.Prod.snd B C).mapComp f g).inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.2 g.2)
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_3.eq_3 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : (CategoryTheory.WithTerminal C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3)
  (x :
    Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star) ⟶
      Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star))
  (x_1 : Opposite.op CategoryTheory.WithTerminal.star ⟶ Opposite.op CategoryTheory.WithTerminal.star)
  (h_1 :
    (x y : C) →
      (f :
          Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of y)) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of x))) →
        (x_2 : Opposite.op (CategoryTheory.WithTerminal.of x) ⟶ Opposite.op (CategoryTheory.WithTerminal.of y)) →
          motive (Opposite.op (CategoryTheory.WithTerminal.of x)) (Opposite.op (CategoryTheory.WithTerminal.of y)) f
            x_2)
  (h_2 :
    (a : C) →
      (x :
          Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of a)) ⟶
            Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star)) →
        (x_2 : Opposite.op CategoryTheory.WithTerminal.star ⟶ Opposite.op (CategoryTheory.WithTerminal.of a)) →
          motive (Opposite.op CategoryTheory.WithTerminal.star) (Opposite.op (CategoryTheory.WithTerminal.of a)) x x_2)
  (h_3 :
    (x :
        Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star) ⟶
          Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star)) →
      (x_2 : Opposite.op CategoryTheory.WithTerminal.star ⟶ Opposite.op CategoryTheory.WithTerminal.star) →
        motive (Opposite.op CategoryTheory.WithTerminal.star) (Opposite.op CategoryTheory.WithTerminal.star) x x_2),
  (match Opposite.op CategoryTheory.WithTerminal.star, Opposite.op CategoryTheory.WithTerminal.star, x, x_1 with
    | Opposite.op (CategoryTheory.WithTerminal.of x), Opposite.op (CategoryTheory.WithTerminal.of y), f, x_2 =>
      h_1 x y f x_2
    | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op (CategoryTheory.WithTerminal.of a), x, x_2 =>
      h_2 a x x_2
    | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op CategoryTheory.WithTerminal.star, x, x_2 => h_3 x x_2) =
    h_3 x x_1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.toQuaternion_ofQuaternion : ∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R} (q : QuaternionAlgebra R c₁ 0 c₂),
  CliffordAlgebraQuaternion.toQuaternion (CliffordAlgebraQuaternion.ofQuaternion q) = q
-- Mathlib.GroupTheory.Coxeter.Basic
/-- A Coxeter system `CoxeterSystem M W` is a structure recording the isomorphism between
a group `W` and the Coxeter group associated to a Coxeter matrix `M`.  -/
CoxeterSystem : {B : Type u_1} → CoxeterMatrix B → (W : Type u_2) → [Group W] → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.preservesColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ] {A B X Y : C}
  (i : A ⟶ B),
  I i →
    ∀ (f : X ⟶ Y) (hf : HomotopicalAlgebra.RelativeCellComplex (fun x => I.homFamily) f),
      CategoryTheory.Limits.PreservesColimit hf.F (CategoryTheory.coyoneda.obj (Opposite.op A))
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.RootPositiveForm.mk.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (form form_1 : LinearMap.BilinForm R M) (e_form : form = form_1) (symm : LinearMap.IsSymm form)
  (isOrthogonal_reflection : ∀ (i : ι), LinearMap.IsOrthogonal form ⇑(P.reflection i))
  (exists_eq : ∀ (i j : ι), ∃ s, (algebraMap S R) s = (form (P.root i)) (P.root j))
  (exists_pos_eq : ∀ (i : ι), ∃ s > 0, (algebraMap S R) s = (form (P.root i)) (P.root i)),
  { form := form, symm := symm, isOrthogonal_reflection := isOrthogonal_reflection, exists_eq := exists_eq,
      exists_pos_eq := exists_pos_eq } =
    { form := form_1, symm := ⋯, isOrthogonal_reflection := ⋯, exists_eq := ⋯, exists_pos_eq := ⋯ }
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_const_mul_of_integrable : ∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {A : Type u_8}
  [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {f : X → A},
  MeasureTheory.Integrable f μ → ∀ {c : A}, ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKey?.induct_unfolding : ∀ {α : Type u} {β : α → Type v} (motive : Std.DTreeMap.Internal.Impl α β → Option α → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf none →
    (∀ (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) (some k)) →
      (∀ (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKey? →
            motive (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKey?) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a a.minKey?
-- Init.Data.Order.PackageFactories
Std.FactoryInstances.instLawfulOrderLeftLeaningMinOfOrd : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α], Std.LawfulOrderLeftLeaningMin α
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.compactSpace_iff_quasiCompact : ∀ (X : AlgebraicGeometry.Scheme),
  CompactSpace ↥X ↔ AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.terminal.from X)
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.point_mem_finset_logSizeBallSeq : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ),
  (PairReduction.logSizeBallSeq J hJ a c i).finset.Nonempty →
    (PairReduction.logSizeBallSeq J hJ a c i).point ∈ (PairReduction.logSizeBallSeq J hJ a c i).finset
-- Mathlib.Algebra.Regular.ULift
ULift.isRegular_up : ∀ {R : Type v} [inst : Mul R] {a : R}, IsRegular { down := a } ↔ IsRegular a
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany?_zero : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a : α},
  Std.PRange.succMany? 0 a = some a
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- More flexible variant of `mapComp`. (See `Bicategory.Functor.Strict`
for applications to strict bicategories.)  -/
CategoryTheory.LaxFunctor.mapComp' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.LaxFunctor B C) →
          {b₀ b₁ b₂ : B} →
            (f : b₀ ⟶ b₁) →
              (g : b₁ ⟶ b₂) →
                (fg : b₀ ⟶ b₂) →
                  autoParam (CategoryTheory.CategoryStruct.comp f g = fg) CategoryTheory.LaxFunctor.mapComp'._auto_1 →
                    (CategoryTheory.CategoryStruct.comp (F.map f) (F.map g) ⟶ F.map fg)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.mk.inj : ∀ {α : Type u} {β : Type v} {inst : BEq α} {inst_1 : Hashable α} {root root_1 : Lean.PersistentHashMap.Node α β},
  { root := root } = { root := root_1 } → root = root_1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_neg_add_iff_add_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, b ≤ -a + c ↔ a + b ≤ c
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradient_const' : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (c : 𝕜), gradient (Function.const F c) = 0
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.tensorObj_carrier : ∀ {R : Type u} [inst : CommRing R] (M N : ModuleCat R),
  ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj M N) = TensorProduct R ↑M ↑N
-- Mathlib.Logic.Embedding.Basic
/-- A version of `Option.map` for `Function.Embedding`s.  -/
Function.Embedding.optionMap : {α : Type u_1} → {β : Type u_2} → (α ↪ β) → Option α ↪ Option β
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
/-- Shows `piToPiTop` is an isomorphism, whose inverse is precisely the pi product
of the induced projections. This shows that `fundamentalGroupoidFunctor` preserves products.
 -/
FundamentalGroupoidFunctor.piIso : {I : Type u} →
  (X : I → TopCat) →
    CategoryTheory.Grpd.of ((i : I) → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))) ≅
      FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i)))
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.exists_subset_card_eq : ∀ {α : Type u} {s : Set α}, s.Infinite → ∀ (n : ℕ), ∃ t, ↑t ⊆ s ∧ t.card = n
-- Mathlib.FieldTheory.Finite.GaloisField
Polynomial.splits_X_pow_nat_card_sub_X : ∀ {K : Type u_1} [inst : Field K], (Polynomial.X ^ Nat.card K - Polynomial.X).Splits
-- Batteries.Data.AssocList
Batteries.AssocList.forM.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [inst : Monad m] (f : α → β → m PUnit.{u_1 + 1}) (a : α)
  (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.forM f (Batteries.AssocList.cons a b es) = do
    f a b
    Batteries.AssocList.forM f es
-- Mathlib.Analysis.Calculus.FDeriv.Mul
hasStrictFDerivAt_list_prod' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸 : Type u_6} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] [Finite ι] {l : List ι} {x : ι → 𝔸},
  HasStrictFDerivAt (fun x => (List.map x l).prod)
    (∑ i,
      (List.map x (List.take (↑i) l)).prod •
        MulOpposite.op (List.map x (List.drop (↑i).succ l)).prod • ContinuousLinearMap.proj l[i])
    x
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
sub_mem_posTangentConeAt_of_segment_subset : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {x y : E},
  segment ℝ x y ⊆ s → y - x ∈ posTangentConeAt s x
-- Mathlib.Probability.Kernel.Composition.Lemmas
MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ],
  μ.compProd κ = (μ.bind ⇑(ProbabilityTheory.Kernel.copy α)).bind ⇑(ProbabilityTheory.Kernel.id.parallelComp κ)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.piecewise_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β) (s : Set α) (t : Set β) [inst : (x : α) → Decidable (x ∈ s)]
  [inst_1 : (y : β) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t),
  ↑(e.piecewise e' s t H H').symm = t.piecewise ↑e.symm ↑e'.symm
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
/-- An object `X` is cofibrant if `⊥_ C ⟶ X` is a cofibration.  -/
HomotopicalAlgebra.IsCofibrant : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [HomotopicalAlgebra.CategoryWithCofibrations C] → [CategoryTheory.Limits.HasInitial C] → C → Prop
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- Given a submersive presentation of `S` as `R`-algebra, any indexing type `κ` complementary to
the `σ` in `ι` indexes a basis of `Ω[S⁄R]`.
See `SubmersivePresentation.basisKaehler` for the special case `κ = (Set.range P.map)ᶜ`.
 -/
Algebra.SubmersivePresentation.basisKaehlerOfIsCompl : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                (P : Algebra.SubmersivePresentation R S ι σ) →
                  {κ : Type u_5} →
                    {f : κ → ι} →
                      Function.Injective f → IsCompl (Set.range f) (Set.range P.map) → Module.Basis κ S Ω[S⁄R]
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- The Möbius function of the incidence algebra as a bare function defined recursively.  -/
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.muFun : (𝕜 : Type u_2) →
  {α : Type u_5} →
    [AddCommGroup 𝕜] → [One 𝕜] → [inst : Preorder α] → [LocallyFiniteOrder α] → [DecidableEq α] → α → α → 𝕜
-- Std.Http.Test.Helpers
Std.Http.Internal.Test.r505 : String
-- Mathlib.Topology.Separation.AlexandrovDiscrete
nhdsKer_eq_of_t1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] (s : Set X), nhdsKer s = s
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.funLike : {R : Type u_1} → [inst : NonUnitalRing R] → FunLike (RingNorm R) R ℝ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_insertMany_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α] {l : ρ} {k : α}, k ∈ m → k ∈ m.insertMany l
-- Lean.Elab.Command
Lean.Elab.Command.State.messages : Lean.Elab.Command.State → Lean.MessageLog
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.isStrictlyPositive_iff_isStrictlyPositive_sqrt_and_eq_sqrt_mul_sqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A},
  IsStrictlyPositive a ↔ IsStrictlyPositive (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal
ENNReal.aefinStronglyMeasurable_of_aemeasurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  ∫⁻ (x : α), f x ∂μ ≠ ⊤ → AEMeasurable f μ → MeasureTheory.AEFinStronglyMeasurable f μ
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.coe_πs' : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o₁ o₂ : Ordinal.{u}}
  (h : o₁ ≤ o₂) (f : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁) ℤ),
  ((Profinite.NobelingProof.πs' C h) f).toFun = f.toFun ∘ Profinite.NobelingProof.ProjRestricts C ⋯
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.instReprWeekday.repr.match_1.eq_5 : ∀ (motive : Std.Time.Weekday → Sort u_1) (h_1 : Unit → motive Std.Time.Weekday.monday)
  (h_2 : Unit → motive Std.Time.Weekday.tuesday) (h_3 : Unit → motive Std.Time.Weekday.wednesday)
  (h_4 : Unit → motive Std.Time.Weekday.thursday) (h_5 : Unit → motive Std.Time.Weekday.friday)
  (h_6 : Unit → motive Std.Time.Weekday.saturday) (h_7 : Unit → motive Std.Time.Weekday.sunday),
  (match Std.Time.Weekday.friday with
    | Std.Time.Weekday.monday => h_1 ()
    | Std.Time.Weekday.tuesday => h_2 ()
    | Std.Time.Weekday.wednesday => h_3 ()
    | Std.Time.Weekday.thursday => h_4 ()
    | Std.Time.Weekday.friday => h_5 ()
    | Std.Time.Weekday.saturday => h_6 ()
    | Std.Time.Weekday.sunday => h_7 ()) =
    h_5 ()
-- Mathlib.Probability.Independence.Conditional
/-- A family of sets of sets `π : ι → Set (Set Ω)` is conditionally independent given `m'` with
respect to a measure `μ` if for any finite set of indices `s = {i_1, ..., i_n}`, for any sets
`f i_1 ∈ π i_1, ..., f i_n ∈ π i_n`, then `μ⟦⋂ i in s, f i | m'⟧ =ᵐ[μ] ∏ i ∈ s, μ⟦f i | m'⟧`.
See `ProbabilityTheory.iCondIndepSets_iff`.
It will be used for families of π-systems.  -/
ProbabilityTheory.iCondIndepSets : {Ω : Type u_1} →
  {ι : Type u_2} →
    (m' : MeasurableSpace Ω) →
      {mΩ : MeasurableSpace Ω} →
        [StandardBorelSpace Ω] →
          m' ≤ mΩ →
            (ι → Set (Set Ω)) →
              (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.iCondIndepSets._auto_1) →
                [MeasureTheory.IsFiniteMeasure μ] → Prop
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_union_of_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ → k ∈ m₁ ∪ m₂
-- Mathlib.Order.CountableSupClosed
/-- If a set is closed under binary infima, then its countable supremum closure is also closed under
binary infima.  -/
InfClosed.countableSupClosure : ∀ {α : Type u_2} {s : Set α} [inst : Order.Frame α], InfClosed s → InfClosed (countableSupClosure s)
-- Lean.Elab.Quotation
/-- Transform sequence of pushes and appends into acceptable code  -/
Lean.Elab.Term.Quotation.ArrayStxBuilder : Type
-- Lean.Parser.Command
Lean.Parser.Command.noncomputable.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- Locally constant maps are the same as continuous maps when the target is equipped with the discrete
topology
 -/
CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap : (Y : Type u_1) → (X : Type u_2) → [inst : TopologicalSpace Y] → LocallyConstant Y X ≅ C(Y, ↑(TopCat.discrete.obj X))
-- Init.Grind.Lemmas
Lean.Grind.or_eq_of_eq_false_right : ∀ {a b : Prop}, b = False → (a ∨ b) = a
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.symm_iff : ∀ {L : Type u_2} [inst : LieRing L] {h e f : L}, IsSl2Triple (-h) f e ↔ IsSl2Triple h e f
-- Batteries.Util.ProofWanted
/-- Parses the surface syntax of `instance_wanted`, generates a name if absent, forwards to the
shared `elabWanted`, validates the payload is a typeclass, and registers the declared name in
`wantedInstancesExt` so subsequent wanted declarations auto-include it.  -/
elabInstanceWanted : Lean.Elab.Command.CommandElab
-- Mathlib.FieldTheory.LinearDisjoint
/-- Linear disjointness of an intermediate field with a tower of field embeddings is preserved by
algebra homomorphisms.  -/
IntermediateField.LinearDisjoint.map' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ (K : Type u_1) [inst_7 : Field K] [inst_8 : Algebra F K] [inst_9 : Algebra L K] [inst_10 : IsScalarTower F L K]
      [inst_11 : Algebra E K] [inst_12 : IsScalarTower F E K] [IsScalarTower L E K],
      (IntermediateField.map (IsScalarTower.toAlgHom F E K) A).LinearDisjoint L
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.orderTop_abs : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [IsOrderedAddMonoid R] (x : Lex (HahnSeries Γ R)), (ofLex |x|).orderTop = (ofLex x).orderTop
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.repr : {R : Type u} → [inst : Semiring R] → [Repr R] → [DecidableEq R] → Repr (Polynomial R)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).isEmpty = false ↔
      ∃ k, ∃ (h : m.contains k = true), (f (m.getKey k h) (Std.DHashMap.Internal.Raw₀.Const.get m k h)).isSome = true)
-- Mathlib.Tactic.Linter.UnusedInstancesInType
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.Parameter.mk.sizeOf_spec : ∀ (fvar? type? : Option Lean.Expr) (idx : ℕ) (appearsInTypeProof : Bool),
  sizeOf { fvar? := fvar?, type? := type?, idx := idx, appearsInTypeProof := appearsInTypeProof } =
    1 + sizeOf fvar? + sizeOf type? + sizeOf idx + sizeOf appearsInTypeProof
-- Mathlib.Algebra.Group.Basic
eq_add_of_sub_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a - c = b → a = b + c
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zsmul_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive] (A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F) (r : ℤ)
  (α : A₁ ⟶ A₂), (r • α).f = r • α.f
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.LocalizerMorphism.smallShiftedHomMap.congr_simp : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {M : Type w'}
  [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C₁ M] [inst_4 : CategoryTheory.HasShift C₂ M]
  [inst_5 : Φ.functor.CommShift M] {X₁ Y₁ : C₁} {X₂ Y₂ : C₂}
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] (eX eX_1 : Φ.functor.obj X₁ ≅ X₂),
  eX = eX_1 →
    ∀ (eY eY_1 : Φ.functor.obj Y₁ ≅ Y₂),
      eY = eY_1 →
        ∀ {m : M} (f f_1 : CategoryTheory.Localization.SmallShiftedHom W₁ X₁ Y₁ m),
          f = f_1 → Φ.smallShiftedHomMap eX eY f = Φ.smallShiftedHomMap eX_1 eY_1 f_1