mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_iSup_comap_of_surjective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_3}
  {f : L.Hom M N},
  Function.Surjective ⇑f →
    ∀ (S : ι → L.Substructure N),
      FirstOrder.Language.Substructure.map f (⨆ i, FirstOrder.Language.Substructure.comap f (S i)) = ⨆ i, S i
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- An additive product monoid algebra is a nested additive monoid algebra.  -/
AddMonoidAlgebra.curryRingEquiv : {R : Type u_1} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : AddMonoid M] →
          [inst_2 : AddMonoid N] → AddMonoidAlgebra R (M × N) ≃+* AddMonoidAlgebra (AddMonoidAlgebra R N) M
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.equivIsoColimit_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cocone F} (i : r ≅ t)
  (P : CategoryTheory.Limits.IsColimit r), (CategoryTheory.Limits.IsColimit.equivIsoColimit i) P = P.ofIsoColimit i
-- Mathlib.LinearAlgebra.Projection
Submodule.coe_prodEquivOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q), ↑(p.prodEquivOfIsCompl q h) = p.subtype.coprod q.subtype
-- Init.Data.Array.Erase
Array.eraseP_append : ∀ {α : Type u_1} {p : α → Bool} {xs ys : Array α},
  (xs ++ ys).eraseP p = if xs.any p = true then xs.eraseP p ++ ys else xs ++ ys.eraseP p
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
/-- The `fderivWithin` of the round-trip composition `(extChartAt I x) ∘ (extChartAt I x).symm`
at the chart point in `range I` equals the identity.  -/
fderivWithin_extChartAt_comp_extChartAt_symm_range : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M},
  fderivWithin 𝕜 (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x) =
    ContinuousLinearMap.id 𝕜 E
-- Init.Grind.Attr
/-- The `funCC` modifier marks global functions that support **function-valued congruence closure**.
Given an application `f a₁ a₂ … aₙ`, when `funCC := true`,
`grind` generates and tracks equalities for all partial applications:
- `f a₁`
- `f a₁ a₂`
- `…`
- `f a₁ a₂ … aₙ`
 -/
Lean.Parser.Attr.grindFunCC : Lean.ParserDescr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.Const.insertMany m l) k = Std.ExtDHashMap.Const.get? m k
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.zero_ne_one_of_field : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (ctx : Lean.Grind.Linarith.Context α) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.zero_ne_one_cert p = true →
    Lean.Grind.Linarith.Var.denote ctx 0 = One.one → Lean.Grind.Linarith.Poly.denote' ctx p ≠ 0
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G], ContinuousLinearMap.rTensor G 0 = 0
-- Lean.Data.JsonRpc
Lean.JsonRpc.Response.mk.injEq : ∀ {α : Type u} (id : Lean.JsonRpc.RequestID) (result : α) (id_1 : Lean.JsonRpc.RequestID) (result_1 : α),
  ({ id := id, result := result } = { id := id_1, result := result_1 }) = (id = id_1 ∧ result = result_1)
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.StartsWithResult.prefix.inj : ∀ {s s_1 : Lean.Grind.AC.Seq},
  Lean.Grind.AC.StartsWithResult.prefix✝ s = Lean.Grind.AC.StartsWithResult.prefix✝ s_1 → s = s_1
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable : ∀ {α : Type u_1} {E : Type u_2} {F' : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F') {C : ℝ},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * μ.real s) →
    ∀ (f : MeasureTheory.SimpleFunc α E),
      MeasureTheory.Integrable (⇑f) μ →
        ‖MeasureTheory.SimpleFunc.setToSimpleFunc T f‖ ≤ C * ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) * ‖x‖
-- Init.Prelude
/-- The maximum recursion depth.  -/
Lean.Macro.Context.maxRecDepth : Lean.Macro.Context → ℕ
-- Mathlib.Logic.Basic
/-- **Alias** of `exists_comm`. -/
exists_swap : ∀ {α : Sort u_2} {β : Sort u_1} {p : α → β → Prop}, (∃ a b, p a b) ↔ ∃ b a, p a b
-- Batteries.Data.Fin.Coding
Fin.encodeSubtype_succ_pos : ∀ {n : ℕ} {P : Fin (n + 1) → Prop} [inst : DecidablePred P] (h₀ : P 0) {i : Fin n} (h : P i.succ),
  Fin.encodeSubtype P ⟨i.succ, h⟩ = Fin.cast ⋯ (Fin.encodeSubtype (fun i => P i.succ) ⟨i, h⟩).succ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.length_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.keys.length = t.size
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.mk.injEq : ∀ (x : Lean.Grind.CommRing.Var) (k : ℕ) (x_1 : Lean.Grind.CommRing.Var) (k_1 : ℕ),
  ({ x := x, k := k } = { x := x_1, k := k_1 }) = (x = x_1 ∧ k = k_1)
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList_subset_of_dvd : ∀ {n k : ℕ}, n ∣ k → k ≠ 0 → n.primeFactorsList ⊆ k.primeFactorsList
-- Mathlib.Algebra.Group.Subgroup.Basic
AddAut.characteristic_apply_symm_apply_coe : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : H.Characteristic] (φ : AddAut G) (h : ↥H),
  ↑((AddEquiv.symm ((AddAut.characteristic H) φ)) h) = (AddEquiv.symm φ) ↑h
-- Mathlib.CategoryTheory.Countable
CategoryTheory.CountableCategory.instCountableObjAsType : ∀ (α : Type u) [inst : CategoryTheory.Category.{v, u} α] [inst_1 : CategoryTheory.CountableCategory α],
  Countable (CategoryTheory.CountableCategory.ObjAsType α)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_one_mem_boundaries₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (a : ↑A),
  (fun₀ | 1 => a) ∈ groupHomology.boundaries₁ A
-- Mathlib.Analysis.Convex.Strict.Extreme
/-- **Alias** of `StrictConvex.extremePoints_eq_sdiff_interior`. -/
StrictConvex.extremePoints_eq_diff_interior : ∀ {A : Type u_1} [inst : NormedAddCommGroup A] [inst_1 : NormedSpace ℝ A] [Nontrivial A] {S : Set A},
  StrictConvex ℝ S → Set.extremePoints ℝ S = S \ interior S
-- Mathlib.Analysis.MeanInequalitiesPow
NNReal.rpow_add_rpow_le : ∀ {p q : ℝ} (a b : NNReal), 0 < p → p ≤ q → (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_hadamard_diagonal : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : MulZeroOneClass α] (d : V → α), (SimpleGraph.adjMatrix α G).hadamard (Matrix.diagonal d) = 0
-- Mathlib.Topology.WithTopology
WithTopology.instSemilatticeSup.eq_1 : ∀ {X : Type u_1} (t : TopologicalSpace X) [inst : SemilatticeSup X],
  WithTopology.instSemilatticeSup t = Function.Injective.semilatticeSup WithTopology.ofTopology ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.Functor.toPseudofunctor_obj : ∀ {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] (F : CategoryTheory.Functor C D)
  (x : CategoryTheory.LocallyDiscrete C), F.toPseudofunctor.obj x = { as := F.obj x.as }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
/-- Returns `some (n, neZeroInst)` if `inst` is of the form `Fin.instOfNat n neZeroInst _`  -/
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.isFinInstOfNat? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Std.Data.DHashMap.RawLemmas
/-- Simpler variant of `getD_filterMap` when `LawfulBEq` is available.  -/
Std.DHashMap.Raw.Const.getD_filterMap' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [LawfulBEq α] {f : α → β → Option γ} {k : α} {fallback : γ},
  m.WF →
    Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.filterMap f m) k fallback =
      ((Std.DHashMap.Raw.Const.get? m k).bind (f k)).getD fallback
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.eq_of_revlex : ∀ (p₁ p₂ : Lean.Grind.CommRing.Power), p₁.revlex p₂ = Ordering.eq → p₁ = p₂
-- Mathlib.NumberTheory.BernoulliPolynomials
/-- Another version of `sum_range_pow`.  -/
Polynomial.sum_range_pow_eq_bernoulli_sub : ∀ (n p : ℕ),
  (↑p + 1) * ∑ k ∈ Finset.range n, ↑k ^ p = Polynomial.eval (↑n) (Polynomial.bernoulli p.succ) - bernoulli p.succ
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_zero_eq_constantCoeff : ∀ {R : Type u_1} [inst : Semiring R], ⇑(PowerSeries.coeff 0) = ⇑PowerSeries.constantCoeff
-- Init.Data.UInt.Lemmas
USize.toUInt32_ofFin : ∀ (n : Fin USize.size), (USize.ofFin n).toUInt32 = UInt32.ofNat ↑n
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instMonoidalCategoryStruct.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.AddGrp.instMonoidalCategoryStruct =
    {
      tensorObj := fun G H =>
        { X := CategoryTheory.MonoidalCategoryStruct.tensorObj G.X H.X,
          addGrp := CategoryTheory.AddGrpObj.tensorObj.instTensorObj },
      whiskerLeft := fun G x x_1 f =>
        CategoryTheory.AddGrp.homMk' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G.toAddMon f.hom),
      whiskerRight := fun {X₁ X₂} f G =>
        CategoryTheory.AddGrp.homMk' (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom G.toAddMon),
      tensorHom := fun {X₁ Y₁ X₂ Y₂} f g =>
        CategoryTheory.AddGrp.homMk' (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom),
      tensorUnit :=
        { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C,
          addGrp := CategoryTheory.AddGrpObj.instTensorAddUnit },
      associator := fun X Y Z =>
        (CategoryTheory.AddGrp.fullyFaithfulForget₂Mon C).preimageIso
          (CategoryTheory.MonoidalCategoryStruct.associator X.toAddMon Y.toAddMon Z.toAddMon),
      leftUnitor := fun G =>
        (CategoryTheory.AddGrp.fullyFaithfulForget₂Mon C).preimageIso
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.toAddMon),
      rightUnitor := fun G =>
        (CategoryTheory.AddGrp.fullyFaithfulForget₂Mon C).preimageIso
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.toAddMon) }
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.findMin_val : ∀ {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {le : α → α → Bool}
  {k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α}
  {res : Batteries.BinomialHeap.Imp.FindMin α},
  (Batteries.BinomialHeap.Imp.Heap.findMin le k s res).val = Batteries.BinomialHeap.Imp.Heap.headD le res.val s
-- Std.Http.Server
/-- Start a new HTTP/1.1 server on the given socket address. This function uses `Async` to handle tasks
and TCP connections, and returns a `Server` structure that can be used to cancel the server.
 -/
Std.Http.Server.serve : {σ : Type} →
  [Std.Http.Server.Handler σ] →
    Std.Net.SocketAddress → σ → optParam Std.Http.Config { } → optParam UInt32 1024 → Std.Async.Async Std.Http.Server
-- Aesop.Tree.Data
Aesop.MVarClusterData : Type → Type → Type
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Int.Internal.Linear.Poly.satisfiedLe : Int.Internal.Linear.Poly → Lean.Meta.Grind.GoalM Lean.LBool
-- Mathlib.Data.Rel
SetRel.instIsTransOfPredProdMatch_1PropOfIsTrans : ∀ {α : Type u_1} {R : α → α → Prop} [IsTrans α R], SetRel.IsTrans {(a, b) | R a b}
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_eq_get_get? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  {h : a ∈ m}, m.get a h = (m.get? a).get ⋯
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.instMonadCanonLinearM : Lean.Meta.Sym.Arith.MonadCanon Lean.Meta.Grind.Arith.Linear.LinearM
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_le_map_iff_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Injective ⇑f → ∀ {S T : Subsemigroup M}, Subsemigroup.map f S ≤ Subsemigroup.map f T ↔ S ≤ T
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.symm_bijective : ∀ {α : Type u_1} {β : Type u_2}, Function.Bijective PartialEquiv.symm
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : InfSet γ]
  {g : sInfHom β γ} {f₁ f₂ : sInfHom α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.iInter_of_antitone_of_frequently : ∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Type u_5} [inst_1 : Preorder ι] [Filter.atTop.IsCountablyGenerated]
  {s : ι → Set α}, Antitone s → (∃ᶠ (i : ι) in Filter.atTop, MeasurableSet (s i)) → MeasurableSet (⋂ i, s i)
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftsToColimit.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cocone (K.comp F)} {t : CategoryTheory.Limits.IsColimit c}
  (toLiftableCocone : CategoryTheory.LiftableCocone K F c)
  (makesColimit : CategoryTheory.Limits.IsColimit toLiftableCocone.liftedCocone)
  (toLiftableCocone_1 : CategoryTheory.LiftableCocone K F c)
  (makesColimit_1 : CategoryTheory.Limits.IsColimit toLiftableCocone_1.liftedCocone),
  ({ toLiftableCocone := toLiftableCocone, makesColimit := makesColimit } =
      { toLiftableCocone := toLiftableCocone_1, makesColimit := makesColimit_1 }) =
    (toLiftableCocone = toLiftableCocone_1 ∧ makesColimit ≍ makesColimit_1)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- A character is primitive if its level is equal to its conductor.  -/
DirichletCharacter.IsPrimitive : {R : Type u_1} → [inst : CommMonoidWithZero R] → {n : ℕ} → DirichletCharacter R n → Prop
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive commutative group, if it
admits a surjective map that preserves `0` and `+` to an additive commutative group.  -/
Function.Surjective.addCommGroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₂] →
      [inst_1 : Zero M₂] →
        [inst_2 : SMul ℕ M₂] →
          [inst_3 : Neg M₂] →
            [inst_4 : Sub M₂] →
              [inst_5 : SMul ℤ M₂] →
                [inst_6 : AddCommGroup M₁] →
                  (f : M₁ → M₂) →
                    Function.Surjective f →
                      f 0 = 0 →
                        (∀ (x y : M₁), f (x + y) = f x + f y) →
                          (∀ (x : M₁), f (-x) = -f x) →
                            (∀ (x y : M₁), f (x - y) = f x - f y) →
                              (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) →
                                (∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) → AddCommGroup M₂
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} [inst_2 : SizeOf C] [inst_3 : SizeOf D]
  (homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (unit : CategoryTheory.Functor.id C ⟶ F.comp G)
  (counit : G.comp F ⟶ CategoryTheory.Functor.id D)
  (homEquiv_unit :
    autoParam
      (∀ {X : C} {Y : D} {f : F.obj X ⟶ Y},
        (homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (unit.app X) (G.map f))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit._autoParam)
  (homEquiv_counit :
    autoParam
      (∀ {X : C} {Y : D} {g : X ⟶ G.obj Y},
        (homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (counit.app Y))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_counit._autoParam),
  sizeOf
      { homEquiv := homEquiv, unit := unit, counit := counit, homEquiv_unit := homEquiv_unit,
        homEquiv_counit := homEquiv_counit } =
    1 + sizeOf unit + sizeOf counit
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeD.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → List α → α → Sort u_2) (x : List α) (x_1 : α)
  (h_1 : (x : List α) → (x_2 : α) → motive 0 x x_2) (h_2 : (n : ℕ) → (l : List α) → (x : α) → motive n.succ l x),
  (match 0, x, x_1 with
    | 0, x, x_2 => h_1 x x_2
    | n.succ, l, x => h_2 n l x) =
    h_1 x x_1
-- Mathlib.Data.Sym.Sym2
Sym2.mem_mk_right : ∀ {α : Type u_1} (x y : α), y ∈ s(x, y)
-- Mathlib.Data.Set.Disjoint
Disjoint.union_left : ∀ {α : Type u_1} {s t u : Set α}, Disjoint s u → Disjoint t u → Disjoint (s ∪ t) u
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], (m₁ ∪ m₂)[k]! = m₂.getD k m₁[k]!
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.eq.sizeOf_spec : ∀ (lhs rhs : ℕ) (proof : Lean.Expr),
  sizeOf (Mathlib.Tactic.Order.AtomicFact.eq lhs rhs proof) = 1 + sizeOf lhs + sizeOf rhs + sizeOf proof
-- Init.Data.List.Nat.Basic
List.dropLast.match_1.congr_eq_3 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : List α) (h_1 : Unit → motive []) (h_2 : (head : α) → motive [head])
  (h_3 : (a : α) → (as : List α) → motive (a :: as)) (a : α) (as : List α),
  x = a :: as →
    (as = [] → False) →
      (match x with
        | [] => h_1 ()
        | [head] => h_2 head
        | a :: as => h_3 a as) ≍
        h_3 a as
-- Mathlib.CategoryTheory.Presentable.StrongGenerator
CategoryTheory.ObjectProperty.colimitsCardinalClosure_le_isCardinalPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.LocallySmall.{w, v, u} C],
  ∀ P ≤ CategoryTheory.isCardinalPresentable C κ, P.colimitsCardinalClosure κ ≤ CategoryTheory.isCardinalPresentable C κ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.contains_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (Std.DTreeMap.Raw.Const.unitOfList l cmp).contains k = l.contains k
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.equivOp_symm_apply_coe : ∀ {M : Type u_2} [inst : Mul M] (H : Subsemigroup M) (b : ↥H.op), ↑(H.equivOp.symm b) = MulOpposite.unop ↑b
-- Mathlib.CategoryTheory.Action.Limits
Action.instSubHom : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → [CategoryTheory.Preadditive V] → {X Y : Action V G} → Sub (X ⟶ Y)
-- Mathlib.Analysis.Convex.Quasiconvex
/-- If `f` is quasiconcave, then its over-levels are connected.  -/
QuasiconcaveOn.isPreconnected_preimage_subtype : ∀ {E : Type u_4} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] {β : Type u_5} [inst_5 : Preorder β] {f : E → β} {s : Set E} {t : β},
  QuasiconcaveOn ℝ s f → IsPreconnected (Subtype.val ⁻¹' f ⁻¹' Set.Ici t)
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.smul_cancel' : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] {r₁ : R} {r₂ : X} {s t : ↥S}, (r₁ * ↑s /ₒ t) • (r₂ /ₒ s) = r₁ • r₂ /ₒ t
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.rank_ratFunc_ratFunc : ∀ (k : Type u_3) (K : Type u_4) [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [Algebra.IsAlgebraic k K],
  Module.rank (RatFunc k) (RatFunc K) = Module.rank k K
-- Mathlib.Data.Int.GCD
_private.Mathlib.Data.Int.GCD.0.Nat.xgcdAux.match_1.splitter : (motive : (n : ℕ) → ((m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → Sort u_1) →
  (n : ℕ) →
    (ih : (m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) →
      ((ih : (m : ℕ) → m < 0 → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive 0 ih) →
        ((k : ℕ) → (ih : (m : ℕ) → m < k.succ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive k.succ ih) → motive n ih
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
LaurentPolynomial.instBialgebra : {R : Type u_11} →
  [inst : CommSemiring R] →
    {A : Type u_12} → [inst_1 : Semiring A] → [Bialgebra R A] → Bialgebra R (LaurentPolynomial A)
-- Mathlib.Topology.UnitInterval
_private.Mathlib.Topology.UnitInterval.0.Set.Icc.eq_convexComb.le_one : ∀ {a b : ℝ} {x y z : ↑(Set.Icc a b)}, x ≤ y → y ≤ z → (↑y - ↑x) / (↑z - ↑x) ≤ 1
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₁.eq_def : ∀ (a : List Char) (a_1 a_2 a_3 : String.Pos.Raw),
  String.Pos.Raw.extract.go₁ a a_1 a_2 a_3 =
    match a, a_1, a_2, a_3 with
    | [], x, x_1, x_2 => []
    | s@h:(c :: cs), i, b, e =>
      if i = b then String.Pos.Raw.extract.go₂ s i e else String.Pos.Raw.extract.go₁ cs (i + c) b e
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stepAux.match_1.eq_7 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4}
  (motive : Turing.TM2.Stmt Γ Λ σ → σ → ((k : K) → List (Γ k)) → Sort u_5) (v : σ) (S : (k : K) → List (Γ k))
  (h_1 :
    (k : K) →
      (f : σ → Γ k) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.push k f q) v S)
  (h_2 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.peek k f q) v S)
  (h_3 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.pop k f q) v S)
  (h_4 :
    (a : σ → σ) →
      (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.load a q) v S)
  (h_5 :
    (f : σ → Bool) →
      (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) →
        (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.branch f q₁ q₂) v S)
  (h_6 : (f : σ → Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.goto f) v S)
  (h_7 : (v : σ) → (S : (k : K) → List (Γ k)) → motive Turing.TM2.Stmt.halt v S),
  (match Turing.TM2.Stmt.halt, v, S with
    | Turing.TM2.Stmt.push k f q, v, S => h_1 k f q v S
    | Turing.TM2.Stmt.peek k f q, v, S => h_2 k f q v S
    | Turing.TM2.Stmt.pop k f q, v, S => h_3 k f q v S
    | Turing.TM2.Stmt.load a q, v, S => h_4 a q v S
    | Turing.TM2.Stmt.branch f q₁ q₂, v, S => h_5 f q₁ q₂ v S
    | Turing.TM2.Stmt.goto f, v, S => h_6 f v S
    | Turing.TM2.Stmt.halt, v, S => h_7 v S) =
    h_7 v S
-- Mathlib.Algebra.AddConstMap.Basic
/-- If `f : G → H` is an `AddConstMap`, then so is `fun x ↦ -f (-x)`.  -/
AddConstMap.conjNeg : {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddCommGroup G] → [inst_1 : AddCommGroup H] → {a : G} → {b : H} → AddConstMap G H a b ≃ AddConstMap G H a b
-- Mathlib.Data.Finset.CastCard
Finset.cast_card_union : ∀ {α : Type u_1} {R : Type u_2} {s t : Finset α} [inst : DecidableEq α] [inst_1 : AddGroupWithOne R],
  ↑(s ∪ t).card = ↑s.card + ↑t.card - ↑(s ∩ t).card
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.generator_denom_dvd_c_num : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → RatFunc.Luroth.g✝ E ∣ (RatFunc.Luroth.c✝ E).num