mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Control.Except
/-- Transforms a successful result with a function, doing nothing when an exception is thrown.

Examples:
* `(pure 2 : Except String Nat).map toString = pure 2`
* `(throw "Error" : Except String Nat).map toString = throw "Error"`
 -/
Except.map : {ε : Type u} → {α : Type u_1} → {β : Type u_2} → (α → β) → Except ε α → Except ε β
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.containsThenInsertIfNew.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β),
  m = m_1 →
    ∀ (a a_1 : α),
      a = a_1 → ∀ (b b_1 : β), b = b_1 → m.containsThenInsertIfNew a b = m_1.containsThenInsertIfNew a_1 b_1
-- Mathlib.Tactic.FunProp.Theorems
/-- theorem about specific function (either declared constant or free variable)  -/
Mathlib.Meta.FunProp.FunctionTheorem : Type
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₄_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.c₄ = -48 * W.a₄
-- Init.Data.BitVec.Lemmas
BitVec.le_ofFin : ∀ {n : ℕ} {x : BitVec n} {y : Fin (2 ^ n)}, x ≤ { toFin := y } ↔ x.toFin ≤ y
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.tail : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.DistinctKeys (⟨k, v⟩ :: l) → Std.Internal.List.DistinctKeys l
-- Mathlib.Topology.Algebra.Algebra
/-- If the subalgebra generated by a set `s` is dense in the ambient module, then two continuous
algebra maps equal on `s` are equal.  -/
ContinuousAlgHom.ext_on : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [T2Space B] {s : Set A}, Dense ↑(Algebra.adjoin R s) → ∀ {f g : A →A[R] B}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Std.Time.Zoned.Database.Windows
/-- Fetches the next timezone transition for a given timezone identifier and timestamp.
 -/
Std.Time.Database.Windows.getNextTransition : String → Int64 → Bool → IO (Option (Int64 × Std.Time.TimeZone))
-- Lean.Expr
Lean.instInhabitedBinderInfo.default : Lean.BinderInfo
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The category of commutative monoids and monoid morphisms.  -/
CommMonCat : Type (u + 1)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.seq_apply : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {β γ : Type v} (f : α →𝒄 Part (β → γ)) (g : α →𝒄 Part β) (x : α),
  (f.seq g) x = f x <*> g x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.mixedEmbedding.realSpace K),
  NumberField.mixedEmbedding.mixedSpaceOfRealSpace x = (fun w => x ↑w, fun w => ↑(x ↑w))
-- Mathlib.Topology.Constructions.SumProd
Topology.IsInducing.sumSwap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Topology.IsInducing Sum.swap
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instZero : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Zero β] → Zero (ZeroAtInftyContinuousMap α β)
-- Aesop.Search.SearchM
Aesop.SearchM.State.mk.injEq : ∀ {Q : Type} [inst : Aesop.Queue Q] (iteration : Aesop.Iteration) (queue : Q) (maxRuleApplicationDepthReached : Bool)
  (iteration_1 : Aesop.Iteration) (queue_1 : Q) (maxRuleApplicationDepthReached_1 : Bool),
  ({ iteration := iteration, queue := queue, maxRuleApplicationDepthReached := maxRuleApplicationDepthReached } =
      { iteration := iteration_1, queue := queue_1,
        maxRuleApplicationDepthReached := maxRuleApplicationDepthReached_1 }) =
    (iteration = iteration_1 ∧ queue = queue_1 ∧ maxRuleApplicationDepthReached = maxRuleApplicationDepthReached_1)
-- Mathlib.Data.Finsupp.Lex
Finsupp.toLex_monotone : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : LinearOrder α] [inst_2 : PartialOrder N], Monotone ⇑toLex
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.edist_vadd_Lp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f g : ↥(MeasureTheory.Lp E p μ)), edist (c +ᵥ f) (c +ᵥ g) = edist f g
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.equivOfIsos_inverse_obj_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} {f' g' : X' ⟶ Y'}
  (e₀ : X ≅ X') (e₁ : Y ≅ Y')
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom)
      CategoryTheory.Limits.Fork.equivOfIsos_inverse_obj_ι._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom)
      CategoryTheory.Limits.Fork.equivOfIsos_inverse_obj_ι._auto_3)
  (c : CategoryTheory.Limits.Fork f' g'),
  ((CategoryTheory.Limits.Fork.equivOfIsos e₀ e₁ comm₁ comm₂).inverse.obj c).ι =
    CategoryTheory.CategoryStruct.comp c.ι e₀.inv
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- The `src : CompSource` field is ignored when comparing `PComp`s. Two `PComp`s proving the same
comparison, with different sources, are considered equivalent.
 -/
Mathlib.Tactic.Linarith.PComp.cmp : Mathlib.Tactic.Linarith.PComp → Mathlib.Tactic.Linarith.PComp → Ordering
-- ProofWidgets.Cancellable
ProofWidgets.CancellableTask.task : ProofWidgets.CancellableTask → Task (Except Lean.Server.RequestError (ProofWidgets.LazyEncodable Lean.Json))
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instStarMul : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → Mul (G i)] →
                  [inst_5 : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] →
                    [inst_6 : (i : ι) → StarMul (G i)] →
                      [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] → StarMul (DirectLimit G f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β k}, a ∈ t.insertIfNew k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Mathlib.GroupTheory.Coprod.Basic
/-- `AddMonoid.Coprod.lift` as an equivalence.  -/
AddMonoid.Coprod.liftEquiv : {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : AddZeroClass M] →
        [inst_1 : AddZeroClass N] → [inst_2 : AddMonoid P] → (M →+ P) × (N →+ P) ≃ (AddMonoid.Coprod M N →+ P)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Equivariant additive monoid homomorphisms.  -/
«DistribMulActionHomLocal≺» : Lean.TrailingParserDescr
-- Init.Data.String.Basic
String.Slice.Pos.prevAux.go.eq_1 : ∀ {s : String.Slice} (off : ℕ) (h₁ : off < s.utf8ByteSize),
  String.Slice.Pos.prevAux.go off h₁ =
    if hbyte : (s.getUTF8Byte { byteIdx := off } h₁).IsUTF8FirstByte then { byteIdx := off }
    else
      have this := ⋯;
      match off, h₁, hbyte, this with
      | 0, h₁, hbyte, this => ⋯.elim
      | off.succ, h₁, hbyte, this => String.Slice.Pos.prevAux.go off ⋯
-- Mathlib.Algebra.Lie.Nilpotent
/-- Given a nilpotent Lie module `M` with lower central series `M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥`, this is
the natural number `k` (the number of inclusions).

For a non-nilpotent module, we use the junk value 0.  -/
LieModule.nilpotencyLength : (L : Type v) → (M : Type w) → [inst : LieRing L] → [inst_1 : AddCommGroup M] → [LieRingModule L M] → ℕ
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- The collection of names used for the `h :` discriminant annotations, in order.
Uniquified names are constructed after the first phase.  -/
Lean.PrettyPrinter.Delaborator.AppMatchState.hNames? : Lean.PrettyPrinter.Delaborator.AppMatchState → Array (Option Lean.Name)
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.brecOn_1.go : {motive_1 : Aesop.Script.StepTree → Sort u} →
  {motive_2 : Array Aesop.Script.StepTree → Sort u} →
    {motive_3 : List Aesop.Script.StepTree → Sort u} →
      (t : Array Aesop.Script.StepTree) →
        ((t : Aesop.Script.StepTree) → t.below → motive_1 t) →
          ((t : Array Aesop.Script.StepTree) → Aesop.Script.StepTree.below_1 t → motive_2 t) →
            ((t : List Aesop.Script.StepTree) → Aesop.Script.StepTree.below_2 t → motive_3 t) →
              motive_2 t ×' Aesop.Script.StepTree.below_1 t
-- Mathlib.ModelTheory.Definability
/-- Finite universal quantifiers preserve definablity.  -/
Set.Definable.forall_of_finite : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1} [Finite β]
  {S : Set (α ⊕ β → M)}, A.Definable L S → A.Definable L {v | ∀ (u : β → M), Sum.elim v u ∈ S}
-- Mathlib.RingTheory.FiniteType
/-- A group `G` is finitely generated if and only if `R[G]` is of finite type.  -/
MonoidAlgebra.finiteType_iff_group_fg : ∀ {R : Type u_1} {G : Type u_3} [inst : Group G] [inst_1 : CommRing R] [Nontrivial R],
  Algebra.FiniteType R (MonoidAlgebra R G) ↔ Group.FG G
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedSyntheticMVarKind.default : Lean.Elab.Term.SyntheticMVarKind
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β]
  (m : α) (n : β), (OrderMonoidHom.inlₗ α β) m * (OrderMonoidHom.inrₗ α β) n = toLex (m, n)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.isoSheafify.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D}
  (hP : CategoryTheory.Presheaf.IsSheaf J P), J.isoSheafify hP = J.isoSheafify hP
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Pi.multipliable : ∀ {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [inst : (x : α) → CommMonoid (X x)]
  [inst_1 : (x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} {f : ι → (x : α) → X x},
  Multipliable f L ↔ ∀ (x : α), Multipliable (fun i => f i x) L
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_map_right : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  {Y X :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)}
  (f : Y ⟶ X), ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).functor.map f).right = f.right
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.instInhabited : {α : Type u_1} → (rels : Set (FreeGroup α)) → Inhabited (PresentedGroup rels)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.inv_mk : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Group γ] [inst_3 : IsTopologicalGroup γ] (f : α → γ) (hf : MeasureTheory.AEStronglyMeasurable f μ),
  (MeasureTheory.AEEqFun.mk f hf)⁻¹ = MeasureTheory.AEEqFun.mk f⁻¹ ⋯
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_f_idem_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n : ℕ) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) h
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_inj : ∀ {a b : UInt16}, a.toBitVec = b.toBitVec ↔ a = b
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_eq_empty_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico a b = ∅ ↔ ¬a < b
-- Mathlib.Algebra.RingQuot
/-- The `•` function for `RingQuot`.  -/
RingQuot.smul : {R : Type uR} →
  [inst : Semiring R] →
    {S : Type uS} → [inst_1 : CommSemiring S] → (r : R → R → Prop) → [Algebra S R] → S → RingQuot r → RingQuot r
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.toInvtRootSubmodule.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [inst_5 : CharZero K]
  [inst_6 : LieAlgebra.IsKilling K L] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L),
  I.toInvtRootSubmodule = ⟨I.rootSpan, ⋯⟩
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- A proof of `False`.
Remark: We will later add support for a backtracking search inside of cutsat.
 -/
Lean.Meta.Grind.Arith.Cutsat.UnsatProof : Type
-- Init.Data.Nat.Bitwise.Basic
Nat.shiftRight_succ : ∀ (m n : ℕ), m >>> (n + 1) = m >>> n / 2
-- Mathlib.Algebra.Field.Subfield.Defs
/-- Two subfields are equal if they have the same elements.  -/
Subfield.ext : ∀ {K : Type u} [inst : DivisionRing K] {S T : Subfield K}, (∀ (x : K), x ∈ S ↔ x ∈ T) → S = T
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.builtinPropagatorsRef : IO.Ref Lean.Meta.Grind.BuiltinPropagators
-- Init.Data.Float.Float32
/-- Bit-for-bit conversion from `UInt32`. Interprets a `UInt32` as a `Float32`, ignoring the numeric
value and treating the `UInt32`'s bit pattern as a `Float32`.

`Float32`s and `UInt32`s have the same endianness on all supported platforms. IEEE 754 very
precisely specifies the bit layout of floats.

This function has a logical model in terms of `Float32.Model`.
 -/
Float32.ofBits : UInt32 → Float32
-- Mathlib.Dynamics.BirkhoffSum.Basic
/-- The sum of values of `g` on the first `n` points of the orbit of `x` under `f`.  -/
birkhoffSum : {α : Type u_1} → {M : Type u_2} → [AddCommMonoid M] → (α → α) → (α → M) → ℕ → α → M
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.dvd' : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Associated a b → b ∣ a
-- Aesop.Script.OptimizeSyntax
Aesop.optimizeSyntax : {m : Type → Type} →
  [Monad m] → [Lean.MonadQuotation m] → {kind : Lean.SyntaxNodeKinds} → Lean.TSyntax kind → m (Lean.TSyntax kind)
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntInt16SintOfNatNat : Lean.Grind.ToInt Int16 (Lean.Grind.IntInterval.sint 16)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.jacobiTheta₂'_functional_equation' : ∀ (z τ : ℂ), jacobiTheta₂' z τ = -2 * ↑Real.pi / (-Complex.I * τ) ^ (3 / 2) * HurwitzZeta.jacobiTheta₂'' z (-1 / τ)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqRhs.injEq : ∀ (gen gen_1 : Bool),
  (Lean.Meta.Grind.EMatchTheoremKind.eqRhs gen = Lean.Meta.Grind.EMatchTheoremKind.eqRhs gen_1) = (gen = gen_1)
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.mk.injEq : ∀ (toTop : TopCat) [is_compactly_generated : UCompactlyGeneratedSpace ↑toTop] (toTop_1 : TopCat)
  (is_compactly_generated_1 : UCompactlyGeneratedSpace ↑toTop_1),
  ({ toTop := toTop, is_compactly_generated := is_compactly_generated } =
      { toTop := toTop_1, is_compactly_generated := is_compactly_generated_1 }) =
    (toTop = toTop_1)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.pair_zip_pair : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (a₁ a₂ : α) (b₁ b₂ : β) (ha : a₁ ≤ a₂)
  (hb : b₁ ≤ b₂),
  (OmegaCompletePartialOrder.Chain.pair a₁ a₂ ha).zip (OmegaCompletePartialOrder.Chain.pair b₁ b₂ hb) =
    OmegaCompletePartialOrder.Chain.pair (a₁, b₁) (a₂, b₂) ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {e : (a : α) × β a} {k : α},
  Std.Internal.List.DistinctKeys l → (Std.Internal.List.getEntry? k l = some e ↔ (k == e.fst) = true ∧ e ∈ l)
-- Mathlib.CategoryTheory.EpiMono
/-- A composition of `SplitMono` is a `SplitMono`.  -/
CategoryTheory.SplitMono.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Z Y X : C} →
      {f : Z ⟶ Y} →
        {g : Y ⟶ X} →
          CategoryTheory.SplitMono f →
            CategoryTheory.SplitMono g → CategoryTheory.SplitMono (CategoryTheory.CategoryStruct.comp f g)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_union_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} (mem : k ∈ t₂), Std.DTreeMap.Const.get (t₁ ∪ t₂) k ⋯ = Std.DTreeMap.Const.get t₂ k mem
-- Mathlib.RingTheory.WittVector.Defs
WittVector.add_coeff_zero : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x y : WittVector p R),
  (x + y).coeff 0 = x.coeff 0 + y.coeff 0
-- Mathlib.Data.WSeq.Defs
/-- Zip two weak sequences into a single sequence of pairs  -/
Stream'.WSeq.zip : {α : Type u} → {β : Type v} → Stream'.WSeq α → Stream'.WSeq β → Stream'.WSeq (α × β)
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- Assume that each `R i` is a locally compact additive group with `A i` an open subgroup.
Assume also that all but finitely many `A i`s are compact.
Then the restricted product `Πʳ i, [R i, A i]` is a locally compact additive group.  -/
RestrictedProduct.locallyCompactSpace_of_addGroup : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))]
  [inst_2 : (i : ι) → AddGroup (R i)] [∀ (i : ι), AddSubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalAddGroup (R i)]
  [∀ (i : ι), LocallyCompactSpace (R i)],
  (∀ᶠ (i : ι) in Filter.cofinite, IsCompact ↑(B i)) →
    LocallyCompactSpace (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.Iterators.Types.ULiftIterator.Monadic.modifyStep.match_1.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
        (step : Std.IterStep (Std.IterM m β) β) →
          ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
            ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive step
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.iCyclesIso_inv_hom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hj : c.next i = j) (h : K.d i j = 0)
  [inst_2 : K.HasHomology i],
  CategoryTheory.CategoryStruct.comp (K.iCyclesIso i j hj h).inv (K.iCycles i) =
    CategoryTheory.CategoryStruct.id (K.X i)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.instSubsingletonImageMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g),
  Subsingleton (CategoryTheory.Limits.ImageMap sq)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.val_mulAutMulEquiv_apply : ∀ (G : Type u_2) [inst : Group G] [h : IsCyclic G] (a : MulAut G),
  ↑((IsCyclic.mulAutMulEquiv G) a) =
    (Multiplicative.toAdd
        ((MulAutMultiplicative (ZMod (Nat.card G)))
          ((zmodCyclicMulEquiv h).trans (MulEquiv.trans a (zmodCyclicMulEquiv h).symm))))
      1
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lcurry_apply : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] (f : TensorProduct R M N →ₛₗ[σ₁₂] P₂) (m : M)
  (n : N), (((TensorProduct.lcurry σ₁₂ M N P₂) f) m) n = f (m ⊗ₜ[R] n)
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.card_points : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [inst_1 : Configuration.ProjectivePlane P L]
  [inst_2 : Fintype P] [Finite L],
  Fintype.card P = Configuration.ProjectivePlane.order P L ^ 2 + Configuration.ProjectivePlane.order P L + 1
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenex.match_1.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (x : ℕ)
  (f : L.BoundedFormula α (x + 1)) (h_1 : (x : ℕ) → motive x FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (x l : ℕ) →
      (R : L.Relations l) → (ts : Fin l → L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (x : ℕ) → (f₁ f₂ : L.BoundedFormula α x) → motive x (f₁.imp f₂))
  (h_5 : (x : ℕ) → (f : L.BoundedFormula α (x + 1)) → motive x f.all),
  (match x, f.all with
    | x, FirstOrder.Language.BoundedFormula.falsum => h_1 x
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 x t₁ t₂
    | x, FirstOrder.Language.BoundedFormula.rel R ts => h_3 x l R ts
    | x, f₁.imp f₂ => h_4 x f₁ f₂
    | x, f.all => h_5 x f) =
    h_5 x f
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- See `MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card`
for a version that assumes `n ≤ #R`.  -/
MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero : ∀ {R : Type u_5} {σ : Type u_6} [inst : CommRing R] [IsDomain R] [Infinite R] {F : MvPolynomial σ R} {n : ℕ},
  F.IsHomogeneous n → (∀ (r : σ → R), (MvPolynomial.eval r) F = 0) → F = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  Std.DTreeMap.Const.get? (Std.DTreeMap.Const.insertManyIfNewUnit t l) k =
    if k ∈ t ∨ l.contains k = true then some () else none
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial.eq_1 : ∀ {R : Type u_1} (n : ℕ) [inst : Semiring R],
  SkewPolynomial.monomial n = SkewMonoidAlgebra.lsingle R (Multiplicative.ofAdd n)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, (m.insert k).get! a = if (k == a) = true ∧ k ∉ m then k else m.get! a
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.add : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u v : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : Add β]
  [ContinuousAdd β],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStronglyProgressive f v → MeasureTheory.IsStronglyProgressive f fun i ω => u i ω + v i ω