mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.forIn'_eq_forIn'_toList : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toList init fun a ha acc => f a ⋯ acc
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_congr : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k k' : α}, (k == k') = true → m.getKey? k = m.getKey? k'
-- Init.Data.List.Basic
List.tail?_cons : ∀ {α : Type u} {a : α} {l : List α}, (a :: l).tail? = some l
-- Mathlib.Combinatorics.SetFamily.LYM
/-- The **Lubell-Yamamoto-Meshalkin inequality**, also known as the **LYM inequality**.

If `𝒜` is an antichain, then the sum of the proportion of elements it takes from each layer is less
than `1`.  -/
Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : Fintype α] {𝒜 : Finset (Finset α)},
  IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜 →
    ∑ r ∈ Finset.range (Fintype.card α + 1), ↑(𝒜.slice r).card / ↑((Fintype.card α).choose r) ≤ 1
-- Mathlib.NumberTheory.ZetaValues
hasSum_one_div_nat_pow_mul_cos : ∀ {k : ℕ},
  k ≠ 0 →
    ∀ {x : ℝ},
      x ∈ Set.Icc 0 1 →
        HasSum (fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * Real.pi * ↑n * x))
          ((-1) ^ (k + 1) * (2 * Real.pi) ^ (2 * k) / 2 / ↑(2 * k).factorial *
            Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
-- Mathlib.Topology.DiscreteQuotient
/-- Any locally constant function induces a discrete quotient.  -/
LocallyConstant.discreteQuotient : {α : Type u_1} → {X : Type u_2} → [inst : TopologicalSpace X] → LocallyConstant X α → DiscreteQuotient X
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.eq_1 : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {β : ι → Type u_8}
  [m : (x : ι) → MeasurableSpace (β x)] (f : (x : ι) → Ω → β x) (κ : ProbabilityTheory.Kernel α Ω)
  (μ : MeasureTheory.Measure α),
  ProbabilityTheory.Kernel.iIndepFun f κ μ =
    ProbabilityTheory.Kernel.iIndep (fun x => MeasurableSpace.comap (f x) (m x)) κ μ
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.zero.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.NatModule α],
  Lean.Grind.IntModule.OfNatModule.zero = Lean.Grind.IntModule.OfNatModule.Q.mk (0, 0)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_add_const_Icc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x + a) ⁻¹' Set.Icc b c = Set.Icc (b - a) (c - a)
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- An abbreviation for `IsLocalRing.maximalIdeal 𝒪[K]` of a valued field `K`, enabling the notation
`𝓂[K]` for the maximal ideal in `𝒪[K]` of a valued field `K`.  -/
Valued.«term𝓂[_]» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomLeft : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᴹᵒᵖ D] {d d' : D} (f : d ⟶ d') (c : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight { unmop := c } f
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.pullback₂_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C}
  [inst_1 : J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T)
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f],
  (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f E).toPreZeroHypercover =
    CategoryTheory.PreZeroHypercover.pullback₂ f E.toPreZeroHypercover
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Transfer `MonObj` along an isomorphism.  -/
CategoryTheory.MonObj.ofIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M X : C} → [CategoryTheory.MonObj M] → (M ≅ X) → CategoryTheory.MonObj X
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Returns `fun (x_0 : varTypes[0]) ... (x_n : varTypes[n]) => b`.
`b` contains `varTypes.size` loose bound variables.
 -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.mkLambdaWithBodyAndVarType : Array Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.absolutelyContinuous_inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant], μ.AbsolutelyContinuous μ.inv
-- Mathlib.RingTheory.Unramified.Finite
Algebra.FormallyUnramified.lmul_elem : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Algebra.FormallyUnramified R S] [inst_4 : Algebra.EssFiniteType R S],
  (Algebra.TensorProduct.lmul' R) (Algebra.FormallyUnramified.elem R S) = 1
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- **Alias** of `Submodule.isSymmetricProjection_projection_of_isOrtho`.

---

**Alias** of the reverse direction of `Submodule.isSymmetricProjection_projection_iff`. -/
Submodule.IsCompl.projection_isSymmetricProjection_of_isOrtho : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} (hUV : IsCompl U V), U ⟂ V → (U.projection V hUV).IsSymmetricProjection
-- Mathlib.Analysis.Convex.Gauge
mem_openSegment_of_gauge_lt_one : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E},
  Absorbent ℝ s → gauge s x < 1 → ∃ y ∈ s, x ∈ openSegment ℝ 0 y
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- In an additive group with a left invariant measure `μ` and a right invariant
measure `ν`, one can express integrals with respect to `μ` as integrals with respect to `ν` up to a
constant scaling factor (given in the statement as `∫ x, g x ∂μ` where `g` is a fixed reference
function) and an explicit density `y ↦ 1/∫ z, g (-z + y) ∂ν`.  -/
MeasureTheory.Measure.integral_isAddLeftInvariant_isAddRightInvariant_combo : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] {μ ν : MeasureTheory.Measure G}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.IsFiniteMeasureOnCompacts ν] [μ.IsAddLeftInvariant]
  [ν.IsAddRightInvariant] [ν.IsOpenPosMeasure] {f g : G → ℝ},
  Continuous f →
    HasCompactSupport f →
      Continuous g →
        HasCompactSupport g →
          0 ≤ g →
            ∀ {x₀ : G},
              g x₀ ≠ 0 → ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (-z + y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.fun_vadd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : TopologicalSpace 𝕜] [inst_2 : VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜} {g : α → β},
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun i => f i +ᵥ g i
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.indepSet_of_mem : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {s t : Set Ω} (S T : Set (Set Ω)),
  s ∈ S →
    t ∈ T →
      MeasurableSet s →
        MeasurableSet t →
          ∀ (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IndepSets.indepSet_of_mem._auto_1)
            [MeasureTheory.IsZeroOrProbabilityMeasure μ],
            ProbabilityTheory.IndepSets S T μ → ProbabilityTheory.IndepSet s t μ
-- Mathlib.Algebra.Algebra.TransferInstance
Equiv.algEquiv_apply : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommSemiring R] (e : α ≃ β) [inst_1 : Semiring β]
  [inst_2 : Algebra R β] (a : α), (Equiv.algEquiv R e) a = e a
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_eq_some_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {km : α},
  t.min? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.EssSurj.mk : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}, (∀ (Y : D), F.essImage Y) → F.EssSurj
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.Edge.CompStruct.tensor_simplex_snd : ∀ {X Y : SSet.Truncated 2}
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  (hx : e₀₁.CompStruct e₁₂ e₀₂)
  {y₀ y₁ y₂ : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  {e'₀₁ : SSet.Truncated.Edge y₀ y₁} {e'₁₂ : SSet.Truncated.Edge y₁ y₂} {e'₀₂ : SSet.Truncated.Edge y₀ y₂}
  (hy : e'₀₁.CompStruct e'₁₂ e'₀₂), (hx.tensor hy).simplex.2 = hy.simplex
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.FG.prod : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {S : Subalgebra R A} {T : Subalgebra R B}, S.FG → T.FG → (S.prod T).FG
-- Mathlib.Data.Num.ZNum
PosNum.cast_sub' : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (m n : PosNum), ↑(m.sub' n) = ↑m - ↑n
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instIsAddTorsionFree : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddMonoid M] [IsAddTorsionFree M], IsAddTorsionFree (ι →₀ M)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.cooper_unsat' : ∀ {a c b d e α β x : ℤ},
  d > 1 →
    d ∣ c * x + e →
      α * c + β * d = 1 →
        -1 * x + a ≤ 0 → x + b ≤ 0 → -b < Int.Internal.Linear.cdiv (a - -α * e % d) d * d + -α * e % d → False
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.map_Z : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S T : J.Cover X} {I₁ I₂ : S.Arrow} (r : I₁.Relation I₂) (f : S ⟶ T), (r.map f).Z = r.Z
-- Mathlib.CategoryTheory.Abelian.Projective.Basic
/-- The preadditive co-Yoneda functor on `P` preserves homology if `P` is projective.  -/
CategoryTheory.preservesHomology_preadditiveCoyonedaObj_of_projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (P : C)
  [hP : CategoryTheory.Projective P], (CategoryTheory.preadditiveCoyonedaObj P).PreservesHomology
-- Mathlib.Data.Finsupp.Order
Finsupp.addLeftReflectLE : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [AddLeftReflectLE α],
  AddLeftReflectLE (ι →₀ α)
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instMulActionQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : Monoid S] →
      [inst_1 : Add M] → [inst_2 : MulAction S M] → (c : ModuleCon S M) → MulAction S (ModuleCon.Quotient M c)
-- Mathlib.Topology.ContinuousMap.Algebra
MonoidHom.compLeftContinuous.eq_1 : ∀ (α : Type u_1) {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
  [inst_2 : Monoid β] [inst_3 : ContinuousMul β] [inst_4 : TopologicalSpace γ] [inst_5 : Monoid γ]
  [inst_6 : ContinuousMul γ] (g : β →* γ) (hg : Continuous ⇑g),
  MonoidHom.compLeftContinuous α g hg =
    { toFun := fun f => { toFun := ⇑g, continuous_toFun := hg }.comp f, map_one' := ⋯, map_mul' := ⋯ }
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.instCoeTSyntaxConsSyntaxNodeKindMkStr1Nil_lean : Coe (Lean.TSyntax `rcasesPat) (Lean.TSyntax `rintroPat)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_liftAt_one_self : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}
  {v : α → M} {xs : Fin (n + 1) → M},
  (FirstOrder.Language.BoundedFormula.liftAt 1 n φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.castSucc)
-- Mathlib.Tactic.CancelDenoms.Core
/-- Given `e`, a term with rational division, produces a natural number `n` and a proof of `n*e = e'`,
where `e'` has no division. Assumes "well-behaved" division.
 -/
Mathlib.Tactic.CancelDenoms.derive : Lean.Expr → Lean.MetaM (ℕ × Lean.Expr)
-- Mathlib.Data.Nat.Totient
Nat.totient_eq_zero : ∀ {n : ℕ}, n.totient = 0 ↔ n = 0
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.map_comp : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q},
  (f.map hy k).comp f.toMonoidHom = k.toMonoidHom.comp g
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.entryAtIdxD : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → ℕ → (a : α) × β a → (a : α) × β a
-- Mathlib.CategoryTheory.Products.Basic
/-- The "evaluation of `F` at `X`" functor,
as a functor `C × (C ⥤ D) ⥤ D`.
 -/
CategoryTheory.evaluationUncurried : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor (C × CategoryTheory.Functor C D) D
-- Init.Conv
/-- `conv => cs` runs `cs` in sequence on the target `t`,
resulting in `t'`, which becomes the new target subgoal.  -/
Lean.Parser.Tactic.Conv.convConvSeq : Lean.ParserDescr
-- Init.Data.Array.Lemmas
Array.setIfInBounds_comm : ∀ {α : Type u_1} (a b : α) {i j : ℕ} {xs : Array α},
  i ≠ j → (xs.setIfInBounds i a).setIfInBounds j b = (xs.setIfInBounds j b).setIfInBounds i a
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.toContinuousLinearMap_mul : ∀ {R₁ : Type u_1} [inst : Semiring R₁] (M₁ : Type u_4) [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] (e e' : M₁ ≃L[R₁] M₁), ↑(e * e') = ↑e * ↑e'
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurableSet_mulSupport : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : One β]
  [MeasurableSingletonClass β], Measurable f → MeasurableSet (Function.mulSupport f)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.trans_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) (x : X), (h₁.trans h₂) x = h₂ (h₁ x)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_tensor_associator_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z X' : C}
  (f : X ⟶ X') {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X' Y) Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id Y))
          (CategoryTheory.CategoryStruct.id Z))
        h)
-- Init.Data.String.Lemmas.Pattern.Find.String
String.Slice.contains_slice_iff : ∀ {t s : String.Slice}, s.contains t = true ↔ t.copy.toList <:+: s.copy.toList
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.instDecidableEqDyadic.decEq.match_1.eq_1 : ∀ (motive : Dyadic → Dyadic → Sort u_1) (h_1 : Unit → motive Dyadic.zero Dyadic.zero)
  (h_2 : (n k : ℤ) → (hn : n % 2 = 1) → motive Dyadic.zero (Dyadic.ofOdd n k hn))
  (h_3 : (n k : ℤ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n k hn) Dyadic.zero)
  (h_4 :
    (a a_1 : ℤ) →
      (a_2 : a % 2 = 1) → (b b_1 : ℤ) → (b_2 : b % 2 = 1) → motive (Dyadic.ofOdd a a_1 a_2) (Dyadic.ofOdd b b_1 b_2)),
  (match Dyadic.zero, Dyadic.zero with
    | Dyadic.zero, Dyadic.zero => h_1 ()
    | Dyadic.zero, Dyadic.ofOdd n k hn => h_2 n k hn
    | Dyadic.ofOdd n k hn, Dyadic.zero => h_3 n k hn
    | Dyadic.ofOdd a a_1 a_2, Dyadic.ofOdd b b_1 b_2 => h_4 a a_1 a_2 b b_1 b_2) =
    h_1 ()
-- Mathlib.Topology.Ultrafilter
isClosed_iff_ultrafilter : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X],
  IsClosed s ↔ ∀ (x : X) (u : Ultrafilter X), ↑u ≤ nhds x → s ∈ u → x ∈ s
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalFactorizationRing.factor₂.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Polynomial.UniversalFactorizationRing.factor₂ m k hn p =
    (↑((MvPolynomial.universalFactorizationMapLiftEquiv R (Polynomial.UniversalFactorizationRing m k hn p) n m k hn
            (Polynomial.UniversalFactorizationRing.monicDegreeEq m k hn p))
          ⟨Polynomial.UniversalFactorizationRing.fromTensor m k hn p, ⋯⟩)).2
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.topMap_id : ∀ (R : CommRingCat),
  AlgebraicGeometry.Spec.topMap (CategoryTheory.CategoryStruct.id R) =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec.topObj R)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_diff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.Const.get! (m₁.diff m₂ ⋯) k =
        if Std.DTreeMap.Internal.Impl.contains k m₂ = true then default else Std.DTreeMap.Internal.Impl.Const.get! m₁ k
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
/-- A stochastic process `X` with independent increments, such that `X t` is Gaussian for
all `t` and such that `X ⊥ = 0` almost surely is a Gaussian process.  -/
ProbabilityTheory.HasIndepIncrements.isGaussianProcess : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : LinearOrder T] [inst_1 : OrderBot T] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E]
  [inst_4 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {X : T → Ω → E},
  (∀ (t : T), ProbabilityTheory.HasGaussianLaw (X t) P) →
    (∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0) → ProbabilityTheory.HasIndepIncrements X P → ProbabilityTheory.IsGaussianProcess X P
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
/-- A `parallelepiped` is the convex hull of its vertices  -/
parallelepiped_eq_convexHull : ∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] (v : ι → E),
  parallelepiped v = (convexHull ℝ) (∑ i, {0, v i})
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₁_inverse : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'}
  {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₁ hF).inverse = e'.inverse.comp eA.inverse
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ≫ θ` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.MkEval.mkEvalComp : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEval m] →
    Mathlib.Tactic.BicategoryLike.Mor₂ →
      Mathlib.Tactic.BicategoryLike.Mor₂ →
        Mathlib.Tactic.BicategoryLike.NormalExpr →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mem_compl : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U : TopologicalSpace.Opens α} {x : α}, x ∈ Uᶜ ↔ ∃ V, Disjoint V U ∧ x ∈ V
-- Mathlib.Topology.Order.IsLUB
DenseRange.exists_seq_strictMono_tendsto : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {β : Type u_3}
  [inst_3 : LinearOrder β] [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] {f : β → α},
  DenseRange f →
    Monotone f →
      ∀ (x : α), ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Set.Iio x) ∧ Filter.Tendsto (f ∘ u) Filter.atTop (nhds x)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.action.inj : ∀ {action action_1 : Lean.Syntax},
  Lean.Elab.Term.Do.Code.action action = Lean.Elab.Term.Do.Code.action action_1 → action = action_1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.closure_normLeOne_subset : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  closure (NumberField.mixedEmbedding.fundamentalCone.normLeOne K) ⊆
    NumberField.mixedEmbedding.normAtAllPlaces ⁻¹' NumberField.mixedEmbedding.fundamentalCone.compactSet K
-- Lean.Data.KVMap
Lean.KVMap.getNat : Lean.KVMap → Lean.Name → optParam ℕ 0 → ℕ
-- Mathlib.Order.Filter.Lift
Filter.tendsto_lift' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {h : Set α → Set β} {m : γ → β} {l : Filter γ},
  Filter.Tendsto m l (f.lift' h) ↔ ∀ s ∈ f, ∀ᶠ (a : γ) in l, m a ∈ h s
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
fderivWithin_fderivWithin_eq_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E} {f : E → F}
  {x : E},
  t ∈ nhdsWithin x s →
    ContDiffWithinAt 𝕜 2 f t x →
      UniqueDiffOn 𝕜 s →
        UniqueDiffOn 𝕜 t → x ∈ s → fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)}
  (φ : X ⟶ Y),
  (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₁ =
    CategoryTheory.Arrow.Hom.left (CategoryTheory.Arrow.Hom.left φ)
-- Mathlib.Data.Fin.SuccPred
/-- By moving `succ` to the outside of this expression, we create opportunities for further
simplification using `succAbove_zero` or `succ_succAbove_zero`.  -/
Fin.succ_succAbove_one : ∀ {n : ℕ} [inst : NeZero n] (i : Fin (n + 1)), i.succ.succAbove 1 = (i.succAbove 0).succ
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.map_surjective : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (B : Type u_3)
  [inst_3 : CommRing B] [inst_4 : Algebra S B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R S B],
  Function.Surjective ⇑(KaehlerDifferential.map R S B B)
-- Std.Sat.AIG.Basic
/-- The public constructor of `Fanin`.
 -/
Std.Sat.AIG.Fanin.mk : ℕ → Bool → Std.Sat.AIG.Fanin
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instSDiffOfTransCmp : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → SDiff (Std.ExtDTreeMap α β cmp)
-- Init.Grind.Order
Lean.Grind.Order.eq_mp_not : ∀ {p q : Prop}, p = q → ¬p → ¬q