mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Match.MatcherApp.Transform
/-- Performs a possibly type-changing transformation to a `MatcherApp`.

* `onParams` is run on each parameter and discriminant
* `onMotive` runs on the body of the motive, and is passed the motive parameters
  (one for each `MatcherApp.discrs`)
* `onAlt` runs on each alternative, and is passed the expected type of the alternative,
   as inferred from the motive
* `onRemaining` runs on the remaining arguments (and may change their number)

If `useSplitter` is true, the matcher is replaced with the splitter.
NB: Not all operations on `MatcherApp` can handle one `matcherName` is a splitter.

If `addEqualities` is true, then equalities connecting the discriminant to the parameters of the
alternative (like in `match h : x with …`) are be added, if not already there.

This function works even if the type of alternatives do *not* fit the inferred type. This
allows you to post-process the `MatcherApp` with `MatcherApp.inferMatchType`, which will
infer a type, given all the alternatives.
 -/
Lean.Meta.MatcherApp.transform : {n : Type → Type} →
  [MonadLiftT Lean.MetaM n] →
    [MonadControlT Lean.MetaM n] →
      [inst : Monad n] →
        [Lean.MonadError n] →
          [Lean.MonadEnv n] →
            [Lean.MonadLog n] →
              [Lean.AddMessageContext n] →
                [Lean.MonadOptions n] →
                  Lean.Meta.MatcherApp →
                    optParam Bool false →
                      optParam Bool false →
                        optParam (Lean.Expr → n Lean.Expr) pure →
                          (optParam (Array Lean.Expr → Lean.Expr → n Lean.Expr) fun x e => pure e) →
                            (optParam (ℕ → Lean.Expr → Lean.Meta.MatcherApp.TransformAltFVars → Lean.Expr → n Lean.Expr)
                                fun x x_1 x_2 e => pure e) →
                              optParam (Array Lean.Expr → n (Array Lean.Expr)) pure → n Lean.Meta.MatcherApp
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_id_comp_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C)
  {Z : CochainComplex (ModuleCat k) ℕ} (h : groupCohomology.inhomogeneousCochains C ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.cochainsMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ)) h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap (MonoidHom.id G) φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap (MonoidHom.id G) ψ) h)
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.id_map : ∀ (P : PFunctor.{uA, uB}) {α : Type v₁} (x : ↑P α), P.map id x = x
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.α_inv : {C : Type u} → (X Y Z : CategoryTheory.FreeMonoidalCategory C) → (X.tensor (Y.tensor Z)).Hom ((X.tensor Y).tensor Z)
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitAppArgs.go' : Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Expr
-- Mathlib.Data.Finite.Defs
Set.not_finite : ∀ {α : Type u} {s : Set α}, ¬s.Finite ↔ s.Infinite
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.map'_id : ∀ {β : Type u_2} [inst : MulOneClass β], ↑(WithZero.map' (MonoidHom.id β)) = MonoidHom.id (WithZero β)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isSome_get?_iff_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, (Std.DTreeMap.Raw.Const.get? t a).isSome = true ↔ a ∈ t
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- Dual to `Monad.ReflectsColimitOfIsSplitPair`.  -/
CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisorsLeft_eq_nonZeroSMulDivisors : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀], nonZeroDivisorsLeft M₀ = nonZeroSMulDivisors M₀ M₀
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.restrictVar.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (l : ℕ) (F : L.Functions l)
  (ts : Fin l → L.Term α) (f : ↥(FirstOrder.Language.func F ts).varFinset → β),
  (FirstOrder.Language.func F ts).restrictVar f =
    FirstOrder.Language.func F fun i => (ts i).restrictVar (f ∘ Set.inclusion ⋯)
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
/-- The relation on the `ι`-indexed tensor power of `M` where two tensors are equal
if they are related by a permutation of `ι`.  -/
SymmetricPower.Rel : (R ι : Type u) →
  [inst : CommSemiring R] →
    (M : Type v) →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → (PiTensorProduct R fun x => M) → (PiTensorProduct R fun x => M) → Prop
-- Mathlib.Data.ZMod.Defs
/-- Distributive structure on `Fin n`.  -/
Fin.instDistrib : (n : ℕ) → Distrib (Fin n)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₅_def : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution.u₅✝ S =
    -⋯.unit ^ 2 * FermatLastTheoremForThreeGen.Solution.u₁✝ S * (FermatLastTheoremForThreeGen.Solution.u₂✝ S)⁻¹
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.exists_of_maximal_cliqueFree_not_adj : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} [inst : DecidableEq α],
  Maximal (fun H => H.CliqueFree (n + 1)) G →
    ∀ {x y : α}, x ≠ y → ¬G.Adj x y → ∃ s, x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s)
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
MeasureTheory.withDensitySMulLI.congr_simp : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {E : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → NNReal} (f_meas : Measurable f),
  MeasureTheory.withDensitySMulLI μ f_meas = MeasureTheory.withDensitySMulLI μ f_meas
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFiniteType f] {x : ↥X},
  AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x → IsClopen {AlgebraicGeometry.Scheme.Hom.asFiber f x}
-- Init.Data.Int.Gcd
Int.le_lcm_right : ∀ {a : ℤ} (b : ℤ), a ≠ 0 → b ≤ ↑(a.lcm b)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.rightUnitor_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Lax.LaxTrans.rightUnitor η).inv.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_diff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k (m₁.diff m₂ ⋯) =
        (Std.DTreeMap.Internal.Impl.contains k m₁ && !Std.DTreeMap.Internal.Impl.contains k m₂)
-- Lean.Compiler.Specialize
Lean.Compiler.instBEqSpecializeAttributeKind : BEq Lean.Compiler.SpecializeAttributeKind
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.pair : ∀ {O : Set (ℕ →. ℕ)} {f h : ℕ →. ℕ},
  Nat.RecursiveIn O f → Nat.RecursiveIn O h → Nat.RecursiveIn O fun n => Nat.pair <$> f n <*> h n
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.instNoSuffixPatternModel : ∀ {pat : String.Slice}, String.Slice.Pattern.Model.NoSuffixPatternModel pat
-- Mathlib.Topology.Constructions
Filter.Tendsto.finTail : ∀ {Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [inst : (i : Fin (n + 1)) → TopologicalSpace (A i)]
  {f : Y → (j : Fin (n + 1)) → A j} {l : Filter Y} {x : (j : Fin (n + 1)) → A j},
  Filter.Tendsto f l (nhds x) → Filter.Tendsto (fun a => Fin.tail (f a)) l (nhds (Fin.tail x))
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.ComputableSmall.Target : (α : Type v) → [self : Std.Internal.ComputableSmall α] → Type u
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.submartingale_of_condExp_sub_nonneg_nat : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] [inst_3 : PartialOrder E]
  [IsOrderedAddMonoid E] [ClosedIciTopology E] [IsOrderedModule ℝ E] [MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Ω → E},
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (i : ℕ), 0 ≤ᵐ[μ] μ[f (i + 1) - f i | ↑𝒢 i]) → MeasureTheory.Submartingale f 𝒢 μ
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_of_ge : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b ≤ a → Finset.uIcc a b = Finset.Icc b a
-- Mathlib.Data.Sym.Sym2
/-- The members of an unordered pair are members of the corresponding unordered list.  -/
Sym2.mem_toMultiset : ∀ {α : Type u_4} {x : α} {z : Sym2 α}, x ∈ z.toMultiset ↔ x ∈ z
-- Mathlib.Logic.Function.Conjugate
/-- If `f : α → β` semiconjugates `ga : α → α` to `gb : β → β`,
`ga'` is a right inverse of `ga`, and `gb'` is a left inverse of `gb`,
then `f` semiconjugates `ga'` to `gb'` as well.  -/
Function.Semiconj.inverses_right : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga ga' : α → α} {gb gb' : β → β},
  Function.Semiconj f ga gb → Function.RightInverse ga' ga → Function.LeftInverse gb' gb → Function.Semiconj f ga' gb'
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.reorder.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.reorder c = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.reorder c_1) =
    (c = c_1)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_C_mul_le : ∀ {R : Type u} [inst : Semiring R] (a : R) (f : Polynomial R), (Polynomial.C a * f).natDegree ≤ f.natDegree
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).π =
    CategoryTheory.Limits.cokernel.π
      (CategoryTheory.Limits.kernel.ι
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g)
          (CategoryTheory.Limits.cokernel.π S.f)))
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The state for the `CoherenceM ρ` monad.  -/
Mathlib.Tactic.BicategoryLike.State : Type
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.of.eq_1 : ∀ (M : Type u) [inst : AddCommGroup M], AddCommGrpCat.of M = { carrier := M, str := inst }
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : x.isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l l_1 : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_2 r : Std.DTreeMap.Internal.Impl α β) →
                    l_1 = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r))
                          h)
  (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l_1 r : Std.DTreeMap.Internal.Impl α β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
      false),
  x = Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) →
    x_1 ≍ h →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
        | Std.DTreeMap.Internal.Impl.inner size k v l l_2@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r),
          h_3 => h_2 size k v l l_2 size_2 k_2 v_2 l_3 r h h_3) ≍
        h_2 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ h
-- Mathlib.Data.Multiset.Fintype
Multiset.coe_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} {x : m.ToType}, x.fst ∈ m
-- Init.Data.List.MinMax
List.min?.eq_2 : ∀ {α : Type u} [inst : Min α] (a : α) (as : List α), (a :: as).min? = some (List.foldl min a as)
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In a commutative semiring `R`, `Subsemiring.sumSq R` is the subsemiring of sums of squares in `R`.
 -/
Subsemiring.sumSq : (T : Type u_2) → [inst : CommSemiring T] → Subsemiring T
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.functorComp_inv_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J)
  (X : CategoryTheory.Discrete I),
  (CategoryTheory.Discrete.functorComp f g).inv.app X = CategoryTheory.CategoryStruct.id (f (g X.as))
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_startpoint : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → ¬p.Nil → p.toSubgraph.neighborSet u = {p.snd}
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesMap_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 : ι) [inst_2 : K.HasHomology i],
  HomologicalComplex.cyclesMap (CategoryTheory.CategoryStruct.id K) i = CategoryTheory.CategoryStruct.id (K.cycles i)
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationAdjunctionRight_counit_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) (Y : CategoryTheory.Functor C D)
  (x : C),
  ((CategoryTheory.evaluationAdjunctionRight D c).counit.app Y).app x =
    CategoryTheory.Limits.Sigma.desc fun h => Y.map h
-- Mathlib.Analysis.Meromorphic.Basic
/-- `Meromorphic` is invariant under translation.  -/
Meromorphic.meromorphic_fun_comp_sub_const_iff_meromorphic : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜}, (Meromorphic fun z => f (z - c)) ↔ Meromorphic f
-- Init.Data.Vector.Lemmas
Vector.findRevM?_mk : ∀ {m : Type → Type} {α : Type} {n : ℕ} [inst : Monad m] {xs : Array α} (h : xs.size = n) (f : α → m Bool),
  Vector.findRevM? f (Vector.mk xs h) = Array.findRevM? f xs
-- Mathlib.Data.Set.Function
Set.LeftInvOn.congr_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} {f₁' : β → α},
  Set.LeftInvOn f₁' f₁ s → Set.EqOn f₁ f₂ s → Set.LeftInvOn f₁' f₂ s
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.brecOn_2.eq : ∀ {motive_1 : Lean.Lsp.Ipc.ModuleHierarchy → Sort u} {motive_2 : Array Lean.Lsp.Ipc.ModuleHierarchy → Sort u}
  {motive_3 : List Lean.Lsp.Ipc.ModuleHierarchy → Sort u} (t : List Lean.Lsp.Ipc.ModuleHierarchy)
  (F_1 : (t : Lean.Lsp.Ipc.ModuleHierarchy) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_2 t → motive_3 t),
  Lean.Lsp.Ipc.ModuleHierarchy.brecOn_2 t F_1 F_2 F_3 = F_3 t (Lean.Lsp.Ipc.ModuleHierarchy.brecOn_2.go t F_1 F_2 F_3).2
-- Mathlib.Data.Nat.Choose.Basic
Nat.descFactorial_eq_factorial_mul_choose : ∀ (n k : ℕ), n.descFactorial k = k.factorial * n.choose k
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.periodic_weierstrassP : ∀ (L : PeriodPair) (l : ↥L.lattice), Function.Periodic L.weierstrassP ↑l
-- Mathlib.Algebra.Homology.BifunctorHomotopy
HomologicalComplex.mapBifunctorMapHomotopy.hom₂.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : 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_3} D] [inst_3 : CategoryTheory.Preadditive C₁]
  [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁}
  {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} (f₁ : K₁ ⟶ L₁) {K₂ L₂ : HomologicalComplex C₂ c₂}
  {f₂ f₂' : K₂ ⟶ L₂} (h₂ : Homotopy f₂ f₂') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J]
  [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c]
  (j j' : J),
  HomologicalComplex.mapBifunctorMapHomotopy.hom₂ f₁ h₂ F c j j' =
    (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).totalDesc fun i₁ i₂ x =>
      c₁.ε₂ c₂ c (i₁, c₂.prev i₂) •
        CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂))
          (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (h₂.hom i₂ (c₂.prev i₂)))
            (L₁.ιMapBifunctorOrZero L₂ F c i₁ (c₂.prev i₂) j'))
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.card_bot : ∀ {G : Type u_1} [inst : AddGroup G], Nat.card ↥⊥ = 1
-- Init.Data.BitVec.Lemmas
BitVec.toFin_natCast : ∀ {w : ℕ} (n : ℕ), (↑n).toFin = ↑n
-- Std.Http.Server.Config
/-- Maximum allowed total body size per request in bytes (default: 64 MiB).
 -/
Std.Http.Config.maxBodySize : Std.Http.Config → ℕ
-- Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
/-- A measurable embedding of a standard Borel space into `ℝ`.  -/
MeasureTheory.embeddingReal : (Ω : Type u_2) → [inst : MeasurableSpace Ω] → [StandardBorelSpace Ω] → Ω → ℝ
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso_inv_app_app_app : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (X X_1 : C) (X_2 : D),
  (((CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso C D).inv.app X).app X_1).app X_2 =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso X_2 X X_1).inv
-- Init.Data.SInt.Float32
/-- Truncates a floating-point number to the nearest 8-bit signed integer, rounding towards zero.

If the `Float` is larger than the maximum value for `Int8` (including `Inf`), returns the maximum value of
`Int8` (i.e. `Int8.maxValue`). If it is smaller than the minimum value for `Int8` (including `-Inf`),
returns the minimum value of `Int8` (i.e. `Int8.minValue`). If it is `NaN`, returns `0`.

This function does not reduce in the kernel.
 -/
Float32.toInt8 : Float32 → Int8
-- Mathlib.CategoryTheory.Join.Opposites
/-- Characterize `Join.opEquivInverse` with respect to the right inclusion  -/
CategoryTheory.Join.inclRightCompOpEquivInverse : (C : Type u₁) →
  (D : Type u₂) →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (CategoryTheory.Join.inclRight Dᵒᵖ Cᵒᵖ).comp (CategoryTheory.Join.opEquiv C D).inverse ≅
          (CategoryTheory.Join.inclLeft C D).op
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D₁ : Type u_1} {D₂ : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D₁] [inst_3 : CategoryTheory.Category.{v_2, u_2} D₂]
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [inst_4 : L₁.IsLocalization W₁]
  [inst_5 : L₂.IsLocalization W₂] [Φ.IsLeftDerivabilityStructure],
  CategoryTheory.TwoSquare.GuitartExact (CategoryTheory.CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).inv
-- Mathlib.Algebra.Group.Defs
AddLeftCancelSemigroup.ext_iff : ∀ {G : Type u} {x y : AddLeftCancelSemigroup G}, x = y ↔ Add.add = Add.add
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M]
  [toHasGroupoid : HasGroupoid M (contDiffGroupoid n I)], IsManifold I n M
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.covarianceBilinDual_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} [inst_1 : NormedSpace ℝ E]
  [inst_2 : BorelSpace E], ProbabilityTheory.covarianceBilinDual 0 = 0
-- Lean.Meta.Tactic.Revert
/-- Reverts all local declarations starting from `fvarId`.  -/
Lean.MVarId.revertFrom : Lean.MVarId → Lean.FVarId → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Init.Grind.Config
/-- When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
 -/
Lean.Grind.Config.abstractProof : Lean.Grind.Config → Bool
-- Mathlib.Data.FinEnum
FinEnum.instInt16 : FinEnum Int16
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_incl_top : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), LieSubmodule.map N.incl ⊤ = N
-- Mathlib.Algebra.CubicDiscriminant
Cubic.map_toPoly : ∀ {R : Type u_1} {S : Type u_2} {P : Cubic R} [inst : Semiring R] [inst_1 : Semiring S] {φ : R →+* S},
  (Cubic.map φ P).toPoly = Polynomial.map φ P.toPoly
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Set.Mem.eq_1 : ∀ {α : Type u} (s : Set α) (a : α), s.Mem a = s a
-- Lean.Parser.Command
Lean.Parser.Command.InternalSyntax.endLocalScopeSyntax : ℕ → Lean.Command
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsRadical.inf : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, I.IsRadical → J.IsRadical → (I ⊓ J).IsRadical
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.of_finite : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] [MeasurableSingletonClass α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α},
  s.Finite → ∀ {f : α → E}, MeasureTheory.IntegrableOn f s μ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.foldrM_eq_foldrM_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → δ → m δ}
  {init : δ}, Std.ExtDTreeMap.foldrM (fun a x d => f a d) init t = List.foldrM f init t.keys