mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_sub_zsmul : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddGroup G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℤ), f (x - n • a) = f x - n • b
-- Init.Data.Ord.Basic
Ordering.gt.sizeOf_spec : sizeOf Ordering.gt = 1
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.simpConfig : Aesop.Frontend.TacticConfig → Lean.Meta.Simp.Config
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- If `f` is an injective linear map, then the family `f ∘ v` is linearly independent
if and only if the family `v` is linearly independent.  -/
LinearMap.linearIndependent_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  f.ker = ⊥ → (LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_restrict_of_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : Zero β] [inst_2 : Zero γ]
  {g : β → γ},
  g 0 = 0 →
    ∀ (f : MeasureTheory.SimpleFunc α β) (s : Set α),
      MeasureTheory.SimpleFunc.map g (f.restrict s) = (MeasureTheory.SimpleFunc.map g f).restrict s
-- Init.Data.String.Basic
String.endExclusive_sliceFrom : ∀ {s : String} {p : s.Pos}, (s.sliceFrom p).endExclusive = s.endPos
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.srange_snd : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] [Nonempty M], (AddHom.snd M N).srange = ⊤
-- Mathlib.Algebra.Homology.QuasiIso
quasiIso_iff_of_arrow_mk_iso : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L K' L' : HomologicalComplex C c}
  (φ : K ⟶ L) (φ' : K' ⟶ L') (e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ')
  [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i] [inst_4 : ∀ (i : ι), K'.HasHomology i]
  [inst_5 : ∀ (i : ι), L'.HasHomology i], QuasiIso φ ↔ QuasiIso φ'
-- Mathlib.Order.WithBot
WithTop.eq_untop_iff : ∀ {α : Type u_1} {a : α} {b : WithTop α} (h : b ≠ ⊤), a = b.untop h ↔ ↑a = b
-- Mathlib.Tactic.Ring.Basic
/-- Applies `Nat.cast` to a nat monomial to produce a monomial in `α`.

* `↑c = c` if `c` is a numeric literal
* `↑(a ^ n * b) = ↑a ^ n * ↑b`
 -/
Mathlib.Tactic.Ring.ExProd.evalNatCast : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {v : Lean.Level} →
        {β : Q(Type v)} →
          (sβ : Q(CommSemiring «$β»)) →
            {a : Q(ℕ)} →
              Mathlib.Tactic.Ring.ExProd sβ a →
                Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.ExProd sα) q(↑«$a»))
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.StrongTrans.Modification η θ)
  {b c : B} {a' : C} (f : a' ⟶ F.obj b) (g : b ⟶ c) {Z : a' ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (θ.app b) (G.map g)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (F.map g) (Γ.app c)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g).hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (η.naturality g).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (Γ.app b) (G.map g))) h)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.normedSpace : {α : Type u_1} →
  {E : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : CompactSpace α] →
        [inst_2 : SeminormedAddCommGroup E] →
          {𝕜 : Type u_5} → [inst_3 : NormedField 𝕜] → [NormedSpace 𝕜 E] → NormedSpace 𝕜 C(α, E)
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_empty : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R}, PointedCone.dual p ∅ = ⊤
-- Lean.Meta.Tactic.Grind.Types
/-- Solver terms attached to this E-node.  -/
Lean.Meta.Grind.ENode.sTerms : Lean.Meta.Grind.ENode → Lean.Meta.Grind.SolverTerms
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
/-- The type of `n`-alternating maps on `M : ModuleCat R` to `N : ModuleCat R`.  -/
ModuleCat.AlternatingMap : {R : Type u} → [inst : CommRing R] → ModuleCat R → ModuleCat R → ℕ → Type (max (max v u v) 0)
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.B₀_sa : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → star B₀ = B₀
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Config.mk : Bool → Bool → Bool → Lean.Meta.Sym.Config
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The second simplicial identity  -/
SimplexCategory.δ_comp_σ_of_le_assoc : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    ∀ {Z : SimplexCategory} (h : { len := n + 1 } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.castSucc)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j.succ) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) h)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of two strictly antitone functions is strictly antitone.  -/
StrictAnti.mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
  [MulLeftStrictMono α] [MulRightStrictMono α], StrictAnti f → StrictAnti g → StrictAnti fun x => f x * g x
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.ext_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  {f g : ZeroAtInftyContinuousMap α β}, f = g ↔ ∀ (x : α), f x = g x
-- Batteries.Data.Char.Basic
Char.ofNatAux.eq_1 : ∀ (n : ℕ) (h : n.isValidChar), Char.ofNatAux n h = { val := { toBitVec := n#'⋯ }, valid := h }
-- Mathlib.Data.List.Destutter
List.destutter_eq_nil : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {l : List α}, List.destutter R l = [] ↔ l = []
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZifV2.mk : Std.Time.TimeZone.TZif.TZifV1 → Option String → Std.Time.TimeZone.TZif.TZifV2
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_indicator_of_disjoint_on_support_of_mem : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : γ → Set β)
  (f : β → α),
  ∀ i ∈ ⋃ d, s d,
    Pairwise (Function.onFun Disjoint fun j => s j ∩ Function.support f) → ∑' (d : γ), (s d).indicator f i = f i
-- Mathlib.Topology.Filter
Filter.tendsto_nhds : ∀ {α : Type u_2} {β : Type u_3} {la : Filter α} {lb : Filter β} {f : α → Filter β},
  Filter.Tendsto f la (nhds lb) ↔ ∀ s ∈ lb, ∀ᶠ (a : α) in la, s ∈ f a
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (n : ℤ) (X : C),
  (t.triangleLTGE n).obj X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {a : α}, t.contains a = false → t.get! a = default
-- Mathlib.CategoryTheory.Bicategory.SingleObj
/-- The monoidal functor from the endomorphisms of the single object
when we promote a monoidal category to a single object bicategory,
to the original monoidal category.

We subsequently show this is an equivalence.
 -/
CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)) C
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The left map in the oplax left unitality square.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapₗ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          (F : CategoryTheory.Functor C D) → F ⟶ F.comp (CategoryTheory.MonoidalCategory.tensorUnitLeft D)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.union_insert_right_equiv_insert_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {p : α × β}, m₁.WF → m₂.WF → (m₁ ∪ m₂.insert p.1 p.2).Equiv ((m₁ ∪ m₂).insert p.1 p.2)
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- The condition that a cochain complex `K` is strictly `≥ n`.  -/
CochainComplex.IsStrictlyGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CochainComplex C ℤ → ℤ → Prop
-- Mathlib.Data.Set.NAry
Set.image2_mk_eq_prod : ∀ {α : Type u_1} {β : Type u_3} {s : Set α} {t : Set β}, Set.image2 Prod.mk s t = s ×ˢ t
-- Mathlib.Combinatorics.Quiver.SingleObj
/-- Equip `SingleObj α` with a reverse operation.  -/
Quiver.SingleObj.hasReverse : {α : Type u_1} → (α → α) → Quiver.HasReverse (Quiver.SingleObj α)
-- Init.Data.Array.Zip
Array.extract_zipWith : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {as : Array α} {bs : Array α_1} {i j : ℕ},
  (Array.zipWith f as bs).extract i j = Array.zipWith f (as.extract i j) (bs.extract i j)
-- Mathlib.Order.WithBot
/-- Deconstruct a `x : WithTop α` to the underlying value in `α`, given a proof that `x ≠ ⊤`.  -/
WithTop.untop : {α : Type u_1} → (x : WithTop α) → x ≠ ⊤ → α
-- Lean.Meta.Order
/-- Given a function `f : α → α`, an instance `inst : CCPO α`
and a monotonicity proof `hmono : monotone f`, constructs a least fixpoint of `f`
with respect to the instance `inst`. The `packedType` is assumed to contain the type `α`.
Can handle `CompleteLattice` as well.
 -/
Lean.Meta.mkFixOfMonFun : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Hom.Monoid
strictMono_iff_map_pos : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F)
  [iamhc : AddMonoidHomClass F α β], StrictMono ⇑f ↔ ∀ (a : α), 0 < a → 0 < f a
-- Init.Core
/-- `a ∪ b` is the union of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∪` in identifiers is `union`. -/
«term_∪_» : Lean.TrailingParserDescr
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn_9.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} (t : List (IO.Ref Aesop.GoalUnsafe))
  (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t) (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t)
  (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  Aesop.GoalUnsafe.brecOn_9 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_12 t (Aesop.GoalUnsafe.brecOn_9.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.clift_comp_mk : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : FreeAddMonoid (M ⊕ N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0)
  (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0)
  (hM :
    ∀ (x y : M),
      f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y)))
  (hN :
    ∀ (x y : N),
      f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))),
  (AddMonoid.Coprod.clift f hM₁ hN₁ hM hN).comp AddMonoid.Coprod.mk = f
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.IsReduced.eq_1 : ∀ {α : Type u} (L : List (α × Bool)), FreeAddGroup.IsReduced L = List.IsChain (fun a b => a.1 = b.1 → a.2 = b.2) L
-- Mathlib.Topology.Order.Lattice
Continuous.inf' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Min L]
  [ContinuousInf L] {f g : X → L}, Continuous f → Continuous g → Continuous (f ⊓ g)
-- Mathlib.Tactic.NormNum.Core
/-- An extension for `norm_num`.
 -/
Mathlib.Meta.NormNum.NormNumExt : Type
-- Aesop.Forward.State
/-- Hypotheses or pattern substitutions that have been added to the cluster
state, but have not yet been added to the `variableMap`.  -/
Aesop.ClusterState.slotQueues : Aesop.ClusterState → Array (Array Aesop.RawHyp)
-- Lean.Elab.DocString
Lean.Doc.State.mk.sizeOf_spec : ∀ (scopes : List Lean.Elab.Command.Scope) (openDecls : List Lean.OpenDecl) (lctx : Lean.LocalContext)
  (localInstances : Lean.LocalInstances) (options : Lean.Options),
  sizeOf
      { scopes := scopes, openDecls := openDecls, lctx := lctx, localInstances := localInstances, options := options } =
    1 + sizeOf scopes + sizeOf openDecls + sizeOf lctx + sizeOf localInstances + sizeOf options
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.RawView.mk.injEq : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (tree : Std.DTreeMap.Internal.Impl α β) (k_1 : α) (v_1 : β k_1)
  (tree_1 : Std.DTreeMap.Internal.Impl α β),
  ({ k := k, v := v, tree := tree } = { k := k_1, v := v_1, tree := tree_1 }) = (k = k_1 ∧ v ≍ v_1 ∧ tree = tree_1)
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜), HasDerivAt 0 0 x
-- Mathlib.Tactic.Linter.ValidatePRTitle
/-- Check if `word` looks like an abbreviation, like `JSON` or `E2` or `W3C`.
 -/
_private.Mathlib.Tactic.Linter.ValidatePRTitle.0.isAbbreviation : String.Slice → Bool
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_map : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {γ : Type u_5}
  {mγ : MeasurableSpace γ} {ν : MeasureTheory.Measure γ} [inst_3 : MeasureTheory.IsFiniteMeasure ν] {f : γ → α},
  AEMeasurable X (MeasureTheory.Measure.map f ν) →
    AEMeasurable Y (MeasureTheory.Measure.map f ν) →
      AEMeasurable f ν →
        ⇑(ProbabilityTheory.condDistrib Y X (MeasureTheory.Measure.map f ν)) =ᵐ[MeasureTheory.Measure.map (X ∘ f) ν]
          ⇑(ProbabilityTheory.condDistrib (Y ∘ f) (X ∘ f) ν)
-- Mathlib.RingTheory.Smooth.AdicCompletion
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.liftAdicCompletionAux.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (m : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (m : ℕ) → motive m.succ.succ),
  (match m.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | m.succ.succ => h_3 m) =
    h_3 m
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : J),
  CategoryTheory.Limits.colimit.ι F j = (CategoryTheory.Limits.colimit.cocone F).ι.app j
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- `symm` is `true` when rewriting from right to left  -/
Mathlib.Tactic.LibraryRewrite.RewriteInterface.symm : Mathlib.Tactic.LibraryRewrite.RewriteInterface → Bool
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.instAssociativeHMul : ∀ (α : Type u) [inst : Lean.Grind.Semiring α], Std.Associative fun x1 x2 => x1 * x2
-- Std.Time.Time.Unit.Hour
/-- Creates an `Offset` from an integer.
 -/
Std.Time.Hour.Offset.ofInt : ℤ → Std.Time.Hour.Offset
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isEquivalent_atBot_lead : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Asymptotics.IsEquivalent Filter.atBot (fun x => Polynomial.eval x P) fun x => P.leadingCoeff * x ^ P.natDegree
-- Init.Data.UInt.Bitwise
UInt64.not_and_self : ∀ {a : UInt64}, ~~~a &&& a = 0
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_mkRat_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionRing α] (a : ℤ) {b : ℕ}, ↑b ≠ 0 → ↑(mkRat a b) = ↑a / ↑b
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.lift.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : Type u₁} [inst_1 : CategoryTheory.Groupoid G]
  (φ : CategoryTheory.Functor C G),
  CategoryTheory.FreeGroupoid.lift φ =
    CategoryTheory.Quotient.lift (CategoryTheory.FreeGroupoid.homRel C) (Quiver.FreeGroupoid.lift φ.toPrefunctor) ⋯
-- Mathlib.MeasureTheory.Function.L2Space
_private.Mathlib.MeasureTheory.Function.L2Space.0.MeasureTheory.«term⟪_,_⟫» : Lean.ParserDescr
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_rotateRight : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ},
  (x.rotateRight r).getLsbD i =
    bif decide (i < w - r % w) then x.getLsbD (r % w + i) else decide (i < w) && x.getLsbD (i - (w - r % w))
-- Init.Data.String.Lemmas.IsEmpty
String.toByteArray_eq_empty_iff : ∀ {s : String}, s.toByteArray = ByteArray.empty ↔ s = ""
-- Init.Data.Array.Lemmas
Array.getElem_extract_loop_ge_aux : ∀ {α : Type u_1} {i : ℕ} {xs ys : Array α} {size start : ℕ},
  i ≥ ys.size → i < (Array.extract.loop xs size start ys).size → start + i - ys.size < xs.size
-- Mathlib.Data.List.Indexes
List.mapIdx_append_one : ∀ {α : Type u} {β : Type v} {f : ℕ → α → β} {l : List α} {e : α},
  List.mapIdx f (l ++ [e]) = List.mapIdx f l ++ [f l.length e]
-- Mathlib.Analysis.Calculus.Implicit
/-- Implicit function theorem. If `f : E → F` and `g : E → G` are two maps strictly differentiable
at `a`, their derivatives `f'`, `g'` are surjective, and the kernels of these derivatives are
complementary subspaces of `E`, then `x ↦ (f x, g x)` defines an open partial homeomorphism between
`E` and `F × G`. In particular, `{x | f x = f a}` is locally homeomorphic to `G`.  -/
ImplicitFunctionData.toOpenPartialHomeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    {G : Type u_4} →
                      [inst_7 : NormedAddCommGroup G] →
                        [inst_8 : NormedSpace 𝕜 G] →
                          [inst_9 : CompleteSpace G] → ImplicitFunctionData 𝕜 E F G → OpenPartialHomeomorph E (F × G)
-- Init.Data.SInt.Lemmas
Int64.le_of_eq : ∀ {a b : Int64}, a = b → a ≤ b
-- Mathlib.Analysis.Convex.Join
segment_subset_convexJoin : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s t : Set E} {x y : E}, x ∈ s → y ∈ t → segment 𝕜 x y ⊆ convexJoin 𝕜 s t
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_addNatEmb_Ici : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.map (Fin.addNatEmb m) (Finset.Ici i) = Finset.Ici (i.addNat m)
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimTargetInfo.arg? : Lean.Elab.Tactic.ElimTargetInfo✝ → Option Lean.Meta.GeneralizeArg
-- Init.Data.Nat.Basic
Nat.eq_zero_of_le_zero : ∀ {n : ℕ}, n ≤ 0 → n = 0
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- The oplax lineator morphism.  -/
CategoryTheory.Functor.OplaxLeftLinear.δₗ : {D : Type u_1} →
  {D' : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} D} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} →
        (F : CategoryTheory.Functor D D') →
          {C : Type u_3} →
            {inst_2 : CategoryTheory.Category.{v_3, u_3} C} →
              {inst_3 : CategoryTheory.MonoidalCategory C} →
                {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} →
                  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} →
                    [self : F.OplaxLeftLinear C] →
                      (c : C) →
                        (d : D) →
                          F.obj (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d) ⟶
                            CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit : {n : ℕ} →
  Array Std.Tactic.BVDecide.LRAT.Internal.Assignment →
    Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  k ∈ Std.ExtHashSet.ofList l ↔ l.contains k = true