mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ι_mapBifunctor₁₂Desc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃}
  {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
  [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄}
  (f :
    (i₁ : ι₁) →
      (i₂ : ι₂) →
        (i₃ : ι₃) →
          c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ A))
  (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
      (HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc f) =
    f i₁ i₂ i₃ h
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToString.serialize : Std.Tactic.BVDecide.LRAT.IntAction → String
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorHom_comp_whiskerLeft_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z_1 : C} (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj W Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.comp g h)) h_1
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_monadMap_ExceptT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε : Type u}
  (f : {β : Type u} → m β → m β) {α : Type u} (x : ExceptT ε m α) (post : α → Pred)
  (epost : EPost.Cons✝ (ε → Pred) EPred),
  Std.Internal.Do.wp (MonadFunctor.monadMap (fun {β} => f) x) post epost =
    Std.Internal.Do.wp (f x.run) (Std.Internal.Do.EPost.Cons.pushExcept post epost) epost.tail
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Composing the zero multilinear map with a linear map in each argument.  -/
MultilinearMap.zero_compLinearMap : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] [inst_6 : (i : ι) → Module R (M₁' i)]
  (f : (i : ι) → M₁ i →ₗ[R] M₁' i), MultilinearMap.compLinearMap 0 f = 0
-- Mathlib.Analysis.Complex.Isometry
rotation_ne_conjLIE : ∀ (a : Circle), rotation a ≠ Complex.conjLIE
-- Lean.Compiler.IR.CompilerM
Lean.IR.LogEntry.message : Std.Format → Lean.IR.LogEntry
-- Aesop.Rule.Basic
Aesop.Rule : Type → Type
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.dist_eq_card : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → Dist (α i)] (f g : PiLp 0 α),
  dist f g = ↑⋯.toFinset.card
-- Init.Data.Bool
Bool.and_right_comm : ∀ (x y z : Bool), (x && y && z) = (x && z && y)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
IsRelPrime.moebius_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a b : α},
  IsRelPrime a b →
    UniqueFactorizationMonoid.moebius (a * b) =
      UniqueFactorizationMonoid.moebius a * UniqueFactorizationMonoid.moebius b
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the largest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.DTreeMap.Raw.maxKeyD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → α
-- Mathlib.Data.FinEnum
FinEnum.pempty : FinEnum PEmpty.{u_1 + 1}
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The functor `SimplexCategory ⥤ SSet` which sends `⦋n⦌` to the standard simplex `Δ[n]` is a
cosimplicial object in the category of simplicial sets. (This functor is essentially given by the
Yoneda embedding).  -/
Simplicial.«termΔ[_]» : Lean.ParserDescr
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidChangeTextDocumentParams : Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.DHashMap.Const.ofList l).getKeyD k' fallback = k
-- Mathlib.Topology.Constructions.SumProd
isOpenMap_sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z}, IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.toZModPow_eq_iff_ext : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {R : Type u_1} [inst : NonAssocSemiring R] {g g' : R →+* ℤ_[p]},
  (∀ (n : ℕ), (PadicInt.toZModPow n).comp g = (PadicInt.toZModPow n).comp g') ↔ g = g'
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.isReduced_of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsReduced Y],
  AlgebraicGeometry.IsReduced X
-- Mathlib.Algebra.Module.Presentation.Basic
/-- The presentation of an `A`-module `N` that is deduced from a presentation of
a module `M` and a linear equivalence `e : M ≃ₗ[A] N`.  -/
Module.Presentation.ofLinearEquiv : {A : Type u} →
  [inst : Ring A] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module A M] →
          Module.Presentation A M →
            {N : Type v'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → (M ≃ₗ[A] N) → Module.Presentation A N
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Construct the presieve given by the family of arrows indexed by `ι`.  -/
CategoryTheory.Presieve.ofArrows : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → {ι : Type u_1} → (Y : ι → C) → ((i : ι) → Y i ⟶ X) → CategoryTheory.Presieve X
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateWithAnchor.c : Lean.Meta.Grind.SplitCandidateWithAnchor → Lean.Meta.Grind.SplitInfo
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKeyD_alterKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} [EquivBEq α] {k k' fallback : α} {f : Option β → Option β}
  (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k' (Std.Internal.List.Const.alterKey k f l) fallback =
      if (k == k') = true then if (f (Std.Internal.List.getValue? k l)).isSome = true then k else fallback
      else Std.Internal.List.getKeyD k' l fallback
-- Init.Data.SInt.Lemmas
Int8.toBitVec_sub : ∀ {a b : Int8}, (a - b).toBitVec = a.toBitVec - b.toBitVec
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- If `E` is finite, then any nonempty collection of its subsets
with the exchange property is the collection of bases of a matroid on `E`.  -/
Matroid.ofIsBaseOfFinite : {α : Type u_1} →
  {E : Set α} →
    E.Finite →
      (IsBase : Set α → Prop) →
        (∃ B, IsBase B) → Matroid.ExchangeProperty IsBase → (∀ (B : Set α), IsBase B → B ⊆ E) → Matroid α
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Ico_of_strictMonoOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a ≤ b → ContinuousOn f (Set.Icc a b) → StrictMonoOn f (Set.Icc a b) → f '' Set.Ico a b = Set.Ico (f a) (f b)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_erase! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.erase! k t) a fallback =
        if compare k a = Ordering.eq then fallback else Std.DTreeMap.Internal.Impl.Const.getD t a fallback
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_mul_le_iff : ∀ {R : Type u} [inst : CommSemiring R] {x : R} {I J : Ideal R}, Ideal.span {x} * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J
-- Init.Notation
/-- `level` is a builtin syntax category for universe levels.
This is the `u` in `Sort u`: it can contain `max` and `imax`, addition with
constants, and variables.  -/
Lean.Parser.Category.level : Lean.Parser.Category
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.counit.congr_simp : ∀ (P : TopCat → Prop) [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_3 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  [inst_4 : CompHausLike.HasExplicitFiniteCoproducts P],
  CompHausLike.LocallyConstant.counit P hs = CompHausLike.LocallyConstant.counit P hs
-- Init.Data.Order.Opposite
/-- Inverts an {name}`LE` instance.

The result is an {lean}`LE α` instance where {lit}`a ≤ b` holds when {name}`le` would have
{lit}`b ≤ a` hold.

If {name}`le` obeys laws, then {lean}`le.opposite` obeys the opposite laws. For example, if
{name}`le` encodes a linear order, then {lean}`le.opposite` also encodes a linear order.
To automatically derive these laws, use {lit}`open Std.OppositeOrderInstances`.

For example, {name}`LE.opposite` can be used to derive maximum operations from minimum operations,
since finding the minimum in the opposite order is the same as finding the maximum in the original order:

```lean +warning
def min' [LE α] [DecidableLE α] (a b : α) : α :=
  if a ≤ b then a else b

open scoped Std.OppositeOrderInstances in
def max' [LE α] [DecidableLE α] (a b : α) : α :=
  letI : LE α := (inferInstance : LE α).opposite
  -- `DecidableLE` for the opposite order is derived automatically via `OppositeOrderInstances`
  min' a b
```

Without the `open scoped` command, Lean would not find the required {lit}`DecidableLE α`
instance for the opposite order.
 -/
LE.opposite : {α : Type u_1} → LE α → LE α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_filter_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k k' : α},
  t.getKey? k = some k' →
    Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.filter f t) k =
      Option.filter (fun x => f k' x) (Std.ExtDTreeMap.Const.get? t k)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex_fst : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A] {X : C}
  (data : F.PreOneHypercoverDenseData X) (P : CategoryTheory.Functor C₀ᵒᵖ A) (j : data.multicospanShape.R),
  (data.multicospanIndex P).fst j = P.map (data.p₁ j.snd).op
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.ext_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt)
  (w :
    autoParam (∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j))
      CategoryTheory.Limits.Cone.ext._auto_1),
  (CategoryTheory.Limits.Cone.ext φ w).inv.hom = φ.inv
-- Init.Data.Array.Find
Array.find?_some : ∀ {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α}, Array.find? p xs = some a → p a = true
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.range_subset : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  Set.range ⇑(algebraMap R A) ⊆ ↑S
-- Mathlib.Data.Finset.Lattice.Prod
/-- See also `Finset.inf'_prodMap`.  -/
Finset.prodMk_inf'_inf' : ∀ {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
  {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β),
  (s.inf' hs f, t.inf' ht g) = (s ×ˢ t).inf' ⋯ (Prod.map f g)
-- Mathlib.Logic.Function.Basic
Function.instSymmOnFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [Std.Symm r], Std.Symm (Function.onFun r f)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.any.match_1.splitter : {α : Type u_1} →
  (motive : List α → (α → Bool) → Sort u_2) →
    (x : List α) →
      (x_1 : α → Bool) →
        ((x : α → Bool) → motive [] x) → ((h : α) → (t : List α) → (p : α → Bool) → motive (h :: t) p) → motive x x_1
-- Mathlib.AlgebraicGeometry.Sites.Small
AlgebraicGeometry.Scheme.locallyCoverDense_of_le : ∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [P.IsStableUnderBaseChange] [P.IsMultiplicative] [P.RespectsIso] [Q.IsStableUnderComposition],
  P ≤ Q →
    (CategoryTheory.MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense
      (AlgebraicGeometry.Scheme.overGrothendieckTopology P S)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.alterₘ.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    (a : α) →
      (motive : Option (β a) → Sort u_2) →
        (x : Option (β a)) → (Unit → motive none) → ((b : β a) → motive (some b)) → motive x
-- Mathlib.Data.Set.Insert
Set.notMem_singleton_iff : ∀ {α : Type u_1} {a b : α}, a ∉ {b} ↔ a ≠ b
-- Mathlib.Lean.Environment
/-- Like `findConstVal?`, but also returns the declarations `ConstantKind`, which is known immediately.

Blocks on everything but the constant's body (if any), which is not accessible through the result.
 -/
Lean.Environment.findConstValWithKind? : Lean.Environment → Lean.Name → optParam Bool false → Option (Lean.ConstantVal × Lean.ConstantKind)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_mul_prod_comm : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] (f g h i : ι → M),
  (∏ a ∈ s, f a * g a) * ∏ a ∈ s, h a * i a = (∏ a ∈ s, f a * h a) * ∏ a ∈ s, g a * i a
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.eqToHom_comp_ι_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {j j' : J} (w : j = j') {Z : C} (h : ⨁ f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) h
-- Mathlib.RingTheory.Finiteness.Basic
/-- See also `Module.Finite.equiv_iff`.  -/
Submodule.fg_of_linearEquiv : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {P : Type u_3}
  [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (e : M ≃ₗ[R] P), ⊤.FG → ⊤.FG
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeriesBilinear.eq_3 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F),
  f.fpowerSeriesBilinear x 2 = f.uncurryBilinear
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBase.cardinalMk_sdiff_comm : ∀ {α : Type u} {M : Matroid α} {B B' : Set α} [M.InvariantCardinalRank],
  M.IsBase B → M.IsBase B' → Cardinal.mk ↑(B \ B') = Cardinal.mk ↑(B' \ B)
-- Init.GetElem
GetElem.mk : {coll : Type u} →
  {idx : Type v} →
    {elem : outParam (Type w)} →
      {valid : outParam (coll → idx → Prop)} →
        ((xs : coll) → (i : idx) → valid xs i → elem) → GetElem coll idx elem valid
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.Channel.Sync.forIn : {α : Type} →
  {m : Type → Type u_1} →
    {β : Type} →
      [Inhabited α] → [Monad m] → [MonadLiftT BaseIO m] → Std.Channel.Sync α → (α → β → m (ForInStep β)) → β → m β
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instAlgebra : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {K : Type u_5} →
        [inst_1 : CommSemiring K] → [inst_2 : Semiring β] → [Algebra K β] → Algebra K (MeasureTheory.SimpleFunc α β)
-- Lean.Data.LBool
Lean.LBool.true : Lean.LBool
-- Init.Meta.Defs
Array.getSepElems : {α : Type u_1} → Array α → Array α
-- Init.Data.String.Basic
String.Slice.startInclusive_sliceTo : ∀ {s : String.Slice} {pos : s.Pos}, (s.sliceTo pos).startInclusive = s.startInclusive
-- Mathlib.Data.ZMod.Basic
ZMod.ne_neg_self : ∀ {n : ℕ}, Odd n → ∀ {a : ZMod n}, a ≠ 0 → a ≠ -a
-- Mathlib.Algebra.Group.Basic
sub_left_inj : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, b - a = c - a ↔ b = c
-- Mathlib.Topology.Order.LeftRight
continuousWithinAt_Iio_iff_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : PartialOrder α] [inst_2 : TopologicalSpace β]
  {a : α} {f : α → β}, ContinuousWithinAt f (Set.Iio a) a ↔ ContinuousWithinAt f (Set.Iic a) a
-- Mathlib.Topology.Order.MonotoneConvergence
Pi.infConvergenceClass : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → TopologicalSpace (α i)]
  [∀ (i : ι), InfConvergenceClass (α i)], InfConvergenceClass ((i : ι) → α i)
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.ListBlank.modifyNth.match_1.eq_2 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (motive : ℕ → Turing.ListBlank Γ → Sort u_2) (n : ℕ) (L : Turing.ListBlank Γ)
  (h_1 : (L : Turing.ListBlank Γ) → motive 0 L) (h_2 : (n : ℕ) → (L : Turing.ListBlank Γ) → motive n.succ L),
  (match n.succ, L with
    | 0, L => h_1 L
    | n.succ, L => h_2 n L) =
    h_2 n L
-- Mathlib.Control.Monad.Writer
/-- reduce the equivalence between two writer monads to the equivalence between
their underlying monad  -/
WriterT.equiv : {m₁ : Type u₀ → Type v₀} →
  {m₂ : Type u₁ → Type v₁} →
    {α₁ ω₁ : Type u₀} → {α₂ ω₂ : Type u₁} → m₁ (α₁ × ω₁) ≃ m₂ (α₂ × ω₂) → WriterT ω₁ m₁ α₁ ≃ WriterT ω₂ m₂ α₂
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsRefl.groupSMul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_8}
  [inst_3 : Group α] [inst_4 : DistribMulAction α R] [inst_5 : SMulCommClass R α R] (a : α)
  {B : LinearMap.BilinForm R M}, B.IsRefl → (a • B).IsRefl
-- Mathlib.Topology.Order
continuous_induced_dom : ∀ {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace β}, Continuous f
-- Init.Data.UInt.Bitwise
UInt32.toUInt8_shiftLeft_mod : ∀ (a b : UInt32), (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fastGrowing.match_1.eq_1 : ∀ (o : ONote) (motive : (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → Sort u_1)
  (x : o.FundamentalSequenceProp (Sum.inl none))
  (h_1 : (x : o.FundamentalSequenceProp (Sum.inl none)) → motive (Sum.inl none) x)
  (h_2 : (a : ONote) → (h : o.FundamentalSequenceProp (Sum.inl (some a))) → motive (Sum.inl (some a)) h)
  (h_3 : (f : ℕ → ONote) → (h : o.FundamentalSequenceProp (Sum.inr f)) → motive (Sum.inr f) h),
  (match Sum.inl none, x with
    | Sum.inl none, x => h_1 x
    | Sum.inl (some a), h => h_2 a h
    | Sum.inr f, h => h_3 f h) =
    h_1 x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_eq_some_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, m.get? k = some v ↔ ∃ (h : k ∈ m), m.get k h = v
-- Mathlib.Algebra.Ring.Defs
/-- One is a left neutral element for multiplication  -/
NonAssocRing.one_mul : ∀ {α : Type u_1} [self : NonAssocRing α] (a : α), 1 * a = a
-- Lean.Environment
_private.Lean.Environment.0.Lean.instInhabitedAsyncConsts : Inhabited Lean.AsyncConsts✝
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_assoc : ∀ {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.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] (d : D) {Z : D'}
  (h : F.obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).hom h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxRightLinear.μᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp
        (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom) h)
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonUnitalCommSemiring` instance along a surjective function.  -/
Function.Surjective.nonUnitalCommSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : SMul ℕ S] →
                [inst_4 : NonUnitalCommSemiring R] →
                  f 0 = 0 →
                    (∀ (x y : R), f (x + y) = f x + f y) →
                      (∀ (x y : R), f (x * y) = f x * f y) →
                        (∀ (n : ℕ) (x : R), f (n • x) = n • f x) → NonUnitalCommSemiring S
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α}, k ∈ Std.DHashMap.filter f m ↔ ∃ (h : k ∈ m), f k (m.get k h) = true
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.flip_reflectionPerm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (a : ι),
  P.flip.reflectionPerm a = P.reflectionPerm a