mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.foldl.eq_def : ∀ {σ : Sort u_1} {α : Type u_2} (f : σ → α → σ) (x : σ) (x_1 : RBTree.RBNode.Stream α),
  RBTree.RBNode.Stream.foldl f x x_1 =
    match x, x_1 with
    | b, RBTree.RBNode.Stream.nil => b
    | b, RBTree.RBNode.Stream.cons v r tail => RBTree.RBNode.Stream.foldl f (RBTree.RBNode.foldl f (f b v) r) tail
-- Init.Data.BitVec.Lemmas
/-- Signed addition overflow reassociation.
If `(x + y)` and `(y + z)` do not overflow, then `(x + y) + z` overflows iff `x + (y + z)` overflows.
 -/
BitVec.saddOverflow_assoc : ∀ {w : ℕ} {x y z : BitVec w},
  ¬x.saddOverflow y = true → ¬y.saddOverflow z = true → (x + y).saddOverflow z = x.saddOverflow (y + z)
-- Mathlib.Analysis.Analytic.Constructions
formalMultilinearSeries_geometric_apply_norm : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [NormOneClass A] (n : ℕ), ‖formalMultilinearSeries_geometric 𝕜 A n‖ = 1
-- Mathlib.CategoryTheory.Adjunction.Parametrized
/-- Given bifunctors `F : C₁ ⥤ C₂ ⥤ C₃` and `G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂`,
an adjunction with parameter `F ⊣₂ G` consists of the data of
adjunctions `F.obj X₁ ⊣ G.obj (op X₁)` for all `X₁ : C₁` which
satisfy a naturality condition with respect to `X₁`.  -/
CategoryTheory.ParametrizedAdjunction : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃) →
              CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂) → Type (max (max (max (max u₁ u₂) u₃) v₂) v₃)
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousAt_unique : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [inst : Unique ι]
  {F : ι → X → α} {x : X}, EquicontinuousAt F x ↔ ContinuousAt (F default) x
-- Mathlib.Topology.Gluing
/-- The canonical map from the glue of a family of open subsets `α` into `α`.
This map is an open embedding (`fromOpenSubsetsGlue_isOpenEmbedding`),
and its range is `⋃ i, (U i : Set α)` (`range_fromOpenSubsetsGlue`).
 -/
TopCat.GlueData.fromOpenSubsetsGlue : {α : Type u} →
  [inst : TopologicalSpace α] →
    {J : Type u} → (U : J → TopologicalSpace.Opens α) → (TopCat.GlueData.ofOpenSubsets U).glued ⟶ TopCat.of α
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)]
  {j : J} {k : K} {Z : C} (h : G.obj (j, k) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G (j, k)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k)
        h)
-- Std.Data.DHashMap.Raw
/-- Returns an array of all values present in the hash map in some order.  -/
Std.DHashMap.Raw.valuesArray : {α : Type u} → {β : Type v} → (Std.DHashMap.Raw α fun x => β) → Array β
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.iInter : ∀ {ι : Sort u_1} {α : Type u_2} [inst : LE α] {f : ι → Set α},
  (∀ (i : ι), CountableInfClosed (f i)) → CountableInfClosed (⋂ i, f i)
-- Mathlib.Order.Monotone.Defs
Antitone.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  Antitone f = ∀ ⦃a b : α⦄, a ≤ b → f b ≤ f a
-- Aesop.Tree.Data
Aesop.GoalData.addedInIteration : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Aesop.Iteration
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.mul_neg : ∀ {α : Type u} [inst : Ring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {a b : α}, a < 0 → 0 < b → b * a < 0
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.IsExtension.mk : ∀ {R : Type u_1} {N : 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 : LieRing N] [inst_4 : LieAlgebra R N] [inst_5 : LieRing M]
  [inst_6 : LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M},
  i.ker = ⊥ → p.range = ⊤ → i.range = LieIdeal.toLieSubalgebra R L p.ker → LieAlgebra.IsExtension i p
-- Mathlib.Order.BooleanSubalgebra
/-- A Boolean subalgebra of a lattice inherits a Boolean algebra structure.  -/
BooleanSubalgebra.instBooleanAlgebraCoe : {α : Type u_2} → [inst : BooleanAlgebra α] → (L : BooleanSubalgebra α) → BooleanAlgebra ↥L
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.toList_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} {f : α → β → γ},
  (Std.DHashMap.Const.toList (Std.DHashMap.map f m)).Perm
    (List.map (fun p => (p.1, f p.1 p.2)) (Std.DHashMap.Const.toList m))
-- Mathlib.Order.CompleteLattice.Basic
biInf_congr : ∀ {α : Type u_1} {ι : Sort u_4} [inst : InfSet α] {f g : ι → α} {p : ι → Prop},
  (∀ (i : ι), p i → f i = g i) → ⨅ i, ⨅ (_ : p i), f i = ⨅ i, ⨅ (_ : p i), g i
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- **Alias** of `MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto_ae`. -/
Filter.Tendsto.integrableAtFilter_ae : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {f : α → E} {l : Filter α} [l.IsMeasurablyGenerated],
  StronglyMeasurableAtFilter f l μ →
    μ.FiniteAtFilter l →
      ∀ {b : E}, Filter.Tendsto f (l ⊓ MeasureTheory.ae μ) (nhds b) → MeasureTheory.IntegrableAtFilter f l μ
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The normal closure of `s` is a normal subgroup.  -/
Subgroup.normalClosure_normal : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, (Subgroup.normalClosure s).Normal
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.lift_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cocycle K F 1) (β : CochainComplex.HomComplex.Cochain K G 0)
  (eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0) (p q : ℤ)
  (hpq : p + 1 = q),
  (CochainComplex.mappingCone.lift φ α β eq).f p =
    CategoryTheory.CategoryStruct.comp ((↑α).v p q hpq) ((CochainComplex.mappingCone.inl φ).v q p ⋯) +
      CategoryTheory.CategoryStruct.comp (β.v p p ⋯) ((CochainComplex.mappingCone.inr φ).f p)
-- Mathlib.Order.CompleteLattice.Basic
iSup_le_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {a : α}, iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The valuation equals relation, defined as `x =ᵥ y ↔ x ≤ᵥ y ∧ y ≤ᵥ x`.  -/
ValuativeRel.«term_=ᵥ_» : Lean.TrailingParserDescr
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.deleteMin_fst : ∀ {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {le : α → α → Bool},
  Option.map (fun x => x.1) (Batteries.BinomialHeap.Imp.Heap.deleteMin le s) =
    Batteries.BinomialHeap.Imp.Heap.head? le s
-- Mathlib.Analysis.CStarAlgebra.Classes
CStarAlgebra.toCStarRing : ∀ {A : Type u_1} [self : CStarAlgebra A], CStarRing A
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionRule.mk.sizeOf_spec : ∀ (spec : Std.Time.TimeZone.TransitionSpec) (time : Std.Time.Second.Offset),
  sizeOf { spec := spec, time := time } = 1 + sizeOf spec + sizeOf time
-- Mathlib.RingTheory.KrullDimension.Basic
/-- The ring-theoretic Krull dimension is the Krull dimension of its spectrum ordered by inclusion.
 -/
ringKrullDim : (R : Type u_1) → [CommSemiring R] → WithBot ℕ∞
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_ediv_assoc : ∀ (a : ℤ) {b c : ℤ}, c ∣ b → a * b / c = a * (b / c)
-- Mathlib.CategoryTheory.Category.PartialFun
/-- The forgetful functor from `Type` to `PartialFun` which forgets that the maps are total.  -/
typeToPartialFun : CategoryTheory.Functor (Type u) PartialFun
-- Lean.Data.LBool
Lean.LBool.instToString : ToString Lean.LBool
-- Mathlib.Probability.Distributions.Uniform
PMF.toMeasure_uniformOfFintype_apply : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] (s : Set α) [inst_2 : MeasurableSpace α],
  MeasurableSet s →
    ∀ [inst_3 : Fintype ↑s], (PMF.uniformOfFintype α).toMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.widthInfty_pos_iff : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [DiscreteTopology ↥𝒢.periods] [𝒢.HasDetPlusMinusOne],
  0 < 𝒢.widthInfty ↔ IsCusp OnePoint.infty 𝒢
-- Init.Data.SInt.Lemmas
Int32.toInt16_ofNat' : ∀ {n : ℕ}, (Int32.ofNat n).toInt16 = Int16.ofNat n
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.fst_comp_inl : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  (OrderMonoidHom.fst α β).comp (OrderMonoidHom.inl α β) = OrderMonoidHom.id α
-- Mathlib.Order.Cofinal
OrderIso.map_isCofinal_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {s : Set α},
  IsCofinal (⇑e '' s) ↔ IsCofinal s
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr.mk.injEq : ∀ (p : Lean.Grind.CommRing.Poly) (h : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof) (p_1 : Lean.Grind.CommRing.Poly)
  (h_1 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof),
  ({ p := p, h := h } = { p := p_1, h := h_1 }) = (p = p_1 ∧ h = h_1)
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_le_iff : ∀ {M : Type u_1} (s : Set M) [inst : Add M] (G : SimpleGraph M),
  SimpleGraph.addCayley s ≤ G ↔ ∀ g ∈ s, ∀ (a : M), a + g ≠ a → G.Adj (a + g) a
-- Mathlib.CategoryTheory.Limits.FintypeCat
/-- Any functor from a finite category to `Type*` that only involves finite objects,
has a finite limit.  -/
CategoryTheory.Limits.FintypeCat.finiteLimitOfFiniteDiagram : {J : Type} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] →
      (K : CategoryTheory.Functor J (Type u_1)) →
        [∀ (j : J), Finite (K.obj j)] → Fintype (CategoryTheory.Limits.limit K)
-- Mathlib.Order.Filter.Basic
/-- Eta-expanded form of `Filter.EventuallyEq.div` -/
Filter.EventuallyEq.fun_div : ∀ {α : Type u} {β : Type v} [inst : Div β] {f f' g g' : α → β} {l : Filter α},
  f =ᶠ[l] g → f' =ᶠ[l] g' → (fun i => f i / f' i) =ᶠ[l] fun i => g i / g' i
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mk_of_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (x : M),
  AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inl x)) = AddMonoid.Coprod.inl x
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.explicit.inj : ∀ {ref : Lean.Syntax} {a : Lean.Elab.Tactic.RCases.RCasesPatt} {ref_1 : Lean.Syntax}
  {a_1 : Lean.Elab.Tactic.RCases.RCasesPatt},
  Lean.Elab.Tactic.RCases.RCasesPatt.explicit ref a = Lean.Elab.Tactic.RCases.RCasesPatt.explicit ref_1 a_1 →
    ref = ref_1 ∧ a = a_1
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.generalizingMap_iff_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_3}
  {U : ι → TopologicalSpace.Opens α},
  TopologicalSpace.IsOpenCover U → (GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap (f ∘ Subtype.val))
-- Mathlib.Data.Stream.Init
Stream'.cons_injective_right : ∀ {α : Type u} (x : α), Function.Injective (Stream'.cons x)
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The morphism `homotopyCofiber φ ⟶ K` that is induced by a morphism `α : G ⟶ K`
and a homotopy `hα : Homotopy (φ ≫ α) 0`.  -/
HomologicalComplex.homotopyCofiber.desc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G K : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] →
                  (α : G ⟶ K) →
                    Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0 → (HomologicalComplex.homotopyCofiber φ ⟶ K)
-- Std.Data.DHashMap.Internal.AssocList.Basic
_private.Std.Data.DHashMap.Internal.AssocList.Basic.0.Std.DHashMap.Internal.AssocList.toList.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Std.DHashMap.Internal.AssocList α β → Sort u_3) →
      (x : Std.DHashMap.Internal.AssocList α β) →
        (Unit → motive Std.DHashMap.Internal.AssocList.nil) →
          ((a : α) →
              (b : β a) →
                (es : Std.DHashMap.Internal.AssocList α β) → motive (Std.DHashMap.Internal.AssocList.cons a b es)) →
            motive x
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_comm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α), lcm a b = lcm b a
-- Mathlib.Topology.ContinuousOn
ContinuousOn.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β × γ} {s : Set α}, ContinuousOn f s → ContinuousOn (fun x => (f x).2) s
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.π_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X Y : F.Elements}
  (f : X ⟶ Y), (CategoryTheory.CategoryOfElements.π F).map f = ↑f
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.lt_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β) {x : α} {y : β}, x < e.symm y ↔ e x < y
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.comp_whiskerLeft_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {W X Y Z : CategoryTheory.Mon C} (M : Bimod W X) (N : Bimod X Y) {P P' : Bimod Y Z} (f : P ⟶ P'),
  (M.tensorBimod N).whiskerLeft f =
    CategoryTheory.CategoryStruct.comp (M.associatorBimod N P).hom
      (CategoryTheory.CategoryStruct.comp (M.whiskerLeft (N.whiskerLeft f)) (M.associatorBimod N P').inv)
-- Lean.Meta.Match.AltTelescopes
_private.Lean.Meta.Match.AltTelescopes.0.Lean.Meta.Match.forallAltTelescope.go : {α : Type} →
  Lean.Expr →
    ℕ →
      (Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.Expr → Lean.MetaM α) →
        Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Array Bool → ℕ → Lean.Expr → Lean.MetaM α
-- Mathlib.Order.InitialSeg
InitialSeg.map_rel_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {a b : α} (f : InitialSeg r s),
  s (f a) (f b) ↔ r a b
-- Init.Data.Option.Lemmas
Option.pmap_or : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o o' : Option α}
  {h : ∀ (a : α), o.or o' = some a → p a},
  Option.pmap f (o.or o') h =
    match o, h with
    | none, h => Option.pmap f o' ⋯
    | some a, h => some (f a ⋯)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.coe_orderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (f : α →+o β), ⇑↑f = ⇑f
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.range_path_union_range_path : ∀ {x y : Circle}, x ≠ y → Set.range ⇑(x.path y) ∪ Set.range ⇑(y.path x) = Set.univ
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coeToMvPowerSeries.ringHom_apply : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (φ : MvPolynomial σ R),
  MvPolynomial.coeToMvPowerSeries.ringHom φ = ↑φ
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.nonempty_of_prod_ne_one : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} {f : ι → M} [inst : CommMonoid M], ∏ x ∈ s, f x ≠ 1 → s.Nonempty
-- Init.Data.Sum.Lemmas
Sum.elim_const_const : ∀ {γ : Sort u_1} {α : Type u_2} {β : Type u_3} (c : γ),
  Sum.elim (Function.const α c) (Function.const β c) = Function.const (α ⊕ β) c
-- Mathlib.Probability.Independence.Conditional
/-- Two functions are conditionally independent if the two measurable space structures they generate
are conditionally independent. For a function `f` with codomain having measurable space structure
`m`, the generated measurable space structure is `m.comap f`.
See `ProbabilityTheory.condIndepFun_iff`.
We use the notation `X ⟂ᵢ[Z, hZ; μ] Y` to write that `X` and `Y` are conditionally independent
given (the σ-algebra generated by) `Z` (scoped in `ProbabilityTheory`).  -/
ProbabilityTheory.«term_⟂ᵢ[_,_;_]_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.c₄.eq_1 : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.c₄ = W.b₂ ^ 2 - 24 * W.b₄
-- Mathlib.Algebra.Group.Action.End
AddAction.coe_toPermHom : ∀ (G : Type u_1) (α : Type u_5) [inst : AddGroup G] [inst_1 : AddAction G α],
  ⇑(AddAction.toPermHom G α) = AddAction.toPerm
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.prod_group_smul : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (g : G) (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.ReducedWord.prod φ (g • w).toReducedWord =
    HNNExtension.of g * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (fg' : i' ⟶ k')
  (h' : CategoryTheory.CategoryStruct.comp f' g' = fg')
  (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g')
  (β : CategoryTheory.ComposableArrows.mk₁ fg ⟶ CategoryTheory.ComposableArrows.mk₁ fg') (n : ℤ),
  autoParam (β.app 0 = α.app 0) CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap._auto_1 →
    autoParam (β.app 1 = α.app 2) CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap._auto_3 →
      ∀ {Z : C} (h_1 : X.cycles f' g' n ⟶ Z),
        CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n)
            (CategoryTheory.CategoryStruct.comp (X.cyclesMap f g f' g' α n) h_1) =
          CategoryTheory.CategoryStruct.comp ((X.H n).map β)
            (CategoryTheory.CategoryStruct.comp (X.toCycles f' g' fg' h' n) h_1)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_neg : ∀ (x : ℝ), Real.arsinh (-x) = -Real.arsinh x
-- Mathlib.Order.WithBot
WithTop.IsWellOrder.gt : ∀ {α : Type u_1} [inst : Preorder α] [IsWellOrder α fun x1 x2 => x1 > x2], IsWellOrder (WithTop α) fun x1 x2 => x1 > x2
-- Mathlib.Order.UpperLower.Closure
lowerClosure_le : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {t : LowerSet α}, lowerClosure s ≤ t ↔ s ⊆ ↑t
-- Mathlib.Algebra.Ring.Subgroup
AddSubgroup.zero_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (s : AddSubgroup M),
  0 • s = ⊥
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.add : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [inst : AddSemigroup α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c₁ → Function.Antiperiodic f c₂ → Function.Periodic f (c₁ + c₂)
-- Init.Data.UInt.Bitwise
UInt16.neg_one_shiftLeft_and_shiftLeft : ∀ {a b : UInt16}, (-1) <<< b &&& a <<< b = a <<< b
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The minimal non-unital subalgebra that includes `s`.  -/
NonUnitalStarAlgebra.adjoin : (R : Type u) →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module R A] →
              [IsScalarTower R A A] → [SMulCommClass R A A] → [StarModule R A] → Set A → NonUnitalStarSubalgebra R A
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.DBuilderName.regular : Aesop.BuilderName → Aesop.Frontend.DBuilderName
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_eq_get_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {he : t.isEmpty = false},
  t.min he = t.min?.get ⋯
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_loops_eq : ∀ {α : Type u_1} (M : Matroid α) (C : Set α), (M.contract C).loops = M.closure C \ C
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Context.maxResultSize : Lean.Meta.SynthInstance.Context → ℕ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMap_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology],
  CategoryTheory.ShortComplex.rightHomologyMap (CategoryTheory.CategoryStruct.id S) =
    CategoryTheory.CategoryStruct.id S.rightHomology
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.find_shiftr : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) (x : X), K.shiftr.find x = K.find x + 1
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.of_f : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] {i j : ι} (hij : i ≤ j) (x : G i),
  (AddCommGroup.DirectLimit.of G f j) ((f i j hij) x) = (AddCommGroup.DirectLimit.of G f i) x
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.instCanLiftSetCoeIsOpen : ∀ {α : Type u_2} [inst : TopologicalSpace α], CanLift (Set α) (TopologicalSpace.Opens α) SetLike.coe IsOpen
-- Mathlib.Order.Interval.Basic
/-- Consider a nonempty interval `[a, b]` as the set `[a, b]`.  -/
NonemptyInterval.coeHom : {α : Type u_1} → [inst : PartialOrder α] → NonemptyInterval α ↪o Set α
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instZSMul.eq_1 : ∀ {M : Type u_1} [inst : AddGroup M] (c : AddCon M),
  c.instZSMul = { smul := fun z x => Quotient.map' (fun x => z • x) ⋯ x }
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.tsupport_iteratedLineDerivOp_subset : ∀ {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : NormedSpace ℝ E] {n : ℕ} (m : Fin n → E) (f : SchwartzMap E F),
  tsupport ⇑(LineDeriv.iteratedLineDerivOp m f) ⊆ tsupport ⇑f
-- Mathlib.Topology.CantorBendixson
/-- Every perfect subset of a set is contained in its perfect kernel.  -/
Perfect.subset_perfectKernel : ∀ {X : Type u} [inst : TopologicalSpace X] {s P : Set X}, Perfect P → P ⊆ s → P ⊆ CantorBendixson.perfectKernel s
-- Mathlib.Order.SetAccumulate
Set.biUnion_accumulate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α] (x : α),
  ⋃ y, ⋃ (_ : y ≤ x), Set.accumulate s y = ⋃ y, ⋃ (_ : y ≤ x), s y
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestExactTac : Lean.Elab.Tactic.Try.TryTactic
-- Init.Conv
/-- An occurrence specification, either `*` or a list of numbers. The default is `[1]`.  -/
Lean.Parser.Tactic.Conv.occs : Lean.ParserDescr