mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_eq_iSup : ∀ {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}),
  (Ordinal.type WellOrderingRel).bsup (Ordinal.bfamilyOfFamily f) = iSup f
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
/-- Given a finset `s` and a function `f : α → ℝ≥0∞` with sum `1` on `s`,
such that `f a = 0` for `a ∉ s`, we get a `PMF`.  -/
PMF.ofFinset : {α : Type u_1} → (f : α → ENNReal) → (s : Finset α) → ∑ a ∈ s, f a = 1 → (∀ a ∉ s, f a = 0) → PMF α
-- Init.Internal.Order.Lemmas
Lean.Order.Seq.monotone_seq : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] [LawfulMonad m] (f : γ → m α) (g : γ → m (α → β)),
  Lean.Order.monotone g → Lean.Order.monotone f → Lean.Order.monotone fun x => g x <*> f x
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
/-- A tensorial operation on sections of a vector bundle respects sums (since it respects binary
addition).  -/
TensorialAt.sum : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {A : Type u_9} [inst_13 : AddCommGroup A]
  [inst_14 : Module 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M} [VectorBundle 𝕜 F V],
  TensorialAt I F Φ x →
    ∀ {ι : Type u_10} {s : Finset ι} (σ : ι → (x : M) → V x),
      (∀ i ∈ s, MDiffAt (T% σ) x) → (Φ fun x' => ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)
-- Mathlib.GroupTheory.GroupExtension.Defs
MonoidHom.ofInjective.congr_simp : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} (hf : Function.Injective ⇑f),
  MonoidHom.ofInjective hf = MonoidHom.ofInjective hf
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.addCommGroup.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R],
  MonoidAlgebra.addCommGroup =
    { toAddMonoid := MonoidAlgebra.instAddMonoid,
      neg := fun a => MonoidAlgebra.coeffEquiv.2 (-MonoidAlgebra.coeffEquiv.toFun a),
      sub := fun a a_1 =>
        MonoidAlgebra.coeffEquiv.2 (MonoidAlgebra.coeffEquiv.toFun a - MonoidAlgebra.coeffEquiv.toFun a_1),
      toZSMul := ZSMul.ofSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯,
      neg_add_cancel := ⋯, add_comm := ⋯ }
-- Mathlib.Probability.Independence.BoundedContinuousFunction
pi_indepFun_of_prod_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4} {H : Type u_7}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] [inst_4 : TopologicalSpace H] [inst_5 : MeasurableSpace H] [BorelSpace H]
  [HasOuterApproxClosed H] {X : (s : S) → Ω → E s} {U : Ω → H} [inst_8 : Fintype S] [MeasureTheory.IsFiniteMeasure P],
  (∀ (s : S), AEMeasurable (X s) P) →
    AEMeasurable U P →
      (∀ (f : (s : S) → BoundedContinuousFunction (E s) ℝ) (g : BoundedContinuousFunction H ℝ),
          ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P =
            (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P) →
        ProbabilityTheory.IndepFun (fun ω s => X s ω) U P
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.map_const : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (μ : MeasureTheory.Measure α)
  (c : β), MeasureTheory.Measure.map (fun x => c) μ = μ Set.univ • MeasureTheory.Measure.dirac c
-- Mathlib.Data.Vector3
vectorAllP_nil : ∀ {α : Type u_1} (p : α → Prop), VectorAllP p [] = True
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- The color class of a given color.
 -/
SimpleGraph.Coloring.colorClass : {V : Type u} → {G : SimpleGraph V} → {α : Type u_2} → G.Coloring α → α → Set V
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_dvd_prime_iff_eq : ∀ {p q : ℕ}, Nat.Prime p → Nat.Prime q → (p ∣ q ↔ p = q)
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.alternatingFaceMapComplex_obj_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  ((AlgebraicTopology.alternatingFaceMapComplex C).obj X).X n = X.obj (Opposite.op { len := n })
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.not_lt_norm : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsLinearOrder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
  (lhs rhs : Lean.Grind.Linarith.Expr) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.norm_cert rhs lhs p = true →
    ¬Lean.Grind.Linarith.Expr.denote ctx lhs < Lean.Grind.Linarith.Expr.denote ctx rhs →
      Lean.Grind.Linarith.Poly.denote' ctx p ≤ 0
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castAdd_Ici : ∀ {n : ℕ} (m : ℕ) [inst : NeZero m] (i : Fin n), Fin.castAdd m '' Set.Ici i = Set.Ico (Fin.castAdd m i) (Fin.natAdd n 0)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.intermediateField : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (F : IntermediateField K L) [Finite G]
  [hGKL : IsGaloisGroup G K L], IsGaloisGroup (↥(fixingSubgroup G ↑F)) (↥F) L
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.isCompl_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p q : ↥f.invtSubmodule}, IsCompl p q ↔ IsCompl ↑p ↑q
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Postcomposition with a linear isometry preserves the operator norm.  -/
ContinuousLinearMap.opNNNorm_linearIsometryEquiv_mul : ∀ {𝕜 : Type u_1} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (e : E ≃ₗᵢ[𝕜] E) (f : E →L[𝕜] E), ‖↑↑e * f‖₊ = ‖f‖₊
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `antilipschitzWith_neg_iff`. -/
AntilipschitzWith.of_neg : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal}
  {f : α → E}, AntilipschitzWith K (-f) → AntilipschitzWith K f
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.instToJsonOptions : Lean.ToJson Lean.Lsp.CreateFile.Options
-- Init.Data.SInt.Bitwise
Int64.toInt8_not : ∀ (a : Int64), (~~~a).toInt8 = ~~~a.toInt8
-- Init.Data.Nat.Basic
Nat.succ_le_succ_iff : ∀ {a b : ℕ}, a.succ ≤ b.succ ↔ a ≤ b
-- Mathlib.RingTheory.SimpleRing.Principal
IsPrincipalIdealRing.of_isSimpleRing : ∀ {R : Type u_1} [inst : CommRing R] [IsSimpleRing R], IsPrincipalIdealRing R
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp'_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃))
      (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃))
        (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯) h))
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.reps_zero_empty : FixedDetMatrices.reps 0 = ∅
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then if `v` is adjacent to `w` in `G` then `w ∈ t`.  -/
SimpleGraph.IsBipartiteWith.mem_of_mem_adj : ∀ {V : Type u_1} {v w : V} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t → v ∈ s → G.Adj v w → w ∈ t
-- Init.Data.SInt.Lemmas
Int16.toBitVec_minValue : Int16.minValue.toBitVec = BitVec.intMin 16
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.MemLp.of_le_mul' : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_5} {ε' : Type u_6}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : TopologicalSpace ε'] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'} {c : NNReal},
  MeasureTheory.MemLp g p μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ) → MeasureTheory.MemLp f p μ
-- Mathlib.Lean.Expr.Basic
/-- Get the last field of a name as a string.
Doesn't raise an error when the last component is a numeric field.  -/
Lean.Name.lastComponentAsString : Lean.Name → String
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.succMany?_decode : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] {n' : ℕ}
  [m : HasModel✝ α β] {x : β},
  Std.PRange.succMany? n' (HasModel.decode✝ x) = Option.map HasModel.decode✝ (Std.PRange.succMany? n' x)
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.image_coe_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithBot.some '' Set.Ioc b a = Set.Ioc ↑b ↑a
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln.eq_9 : ∀ (k : ℕ) (cf : Nat.Partrec.Code),
  Nat.Partrec.Code.evaln k.succ cf.rfind' = fun n => do
    guard (n ≤ k)
    Nat.unpaired
        (fun a m => do
          let x ← Nat.Partrec.Code.evaln (k + 1) cf (Nat.pair a m)
          if x = 0 then pure m else Nat.Partrec.Code.evaln k cf.rfind' (Nat.pair a (m + 1)))
        n
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Set.Finite.of_summable_const : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : TopologicalSpace α] [Archimedean α] [OrderClosedTopology α] {b : α},
  0 < b → (Summable fun x => b) → Set.univ.Finite
-- Init.Data.Array.Find
Array.find?_eq_map_findFinIdx?_getElem : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, Array.find? p xs = Option.map (fun x => xs[x]) (Array.findFinIdx? p xs)
-- Mathlib.Data.Rat.Lemmas
Rat.inv_natCast_den_of_pos : ∀ {a : ℕ}, 0 < a → (↑a)⁻¹.den = a
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Returns `some k` if `e` `@OfNat.ofNat Nat _ (instOfNatNat k)`  -/
Lean.Meta.Grind.Arith.isNatNum? : Lean.Expr → Option ℕ
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.map_sin : ∀ {A : Type u_1} {A' : Type u_2} [inst : Ring A] [inst_1 : Ring A'] [inst_2 : Algebra ℚ A] [inst_3 : Algebra ℚ A']
  (f : A →+* A'), (PowerSeries.map f) (PowerSeries.sin A) = PowerSeries.sin A'
-- Mathlib.Algebra.Quaternion
Quaternion.imI_mul : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R),
  (a * b).imI = a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.inl.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  OrderMonoidHom.inl α β = { toMonoidHom := MonoidHom.inl α β, monotone' := ⋯ }
-- Mathlib.Topology.Order.OrderClosed
closure_Ici : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] (a : α),
  closure (Set.Ici a) = Set.Ici a
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The iterated derivative of the difference of two functions is the difference of the iterated
derivatives.
 -/
iteratedFDerivWithin_sub_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {x : E} {i : ℕ} {f g : E → F},
  ContDiffWithinAt 𝕜 (↑i) f s x →
    ContDiffWithinAt 𝕜 (↑i) g s x →
      UniqueDiffOn 𝕜 s →
        x ∈ s → iteratedFDerivWithin 𝕜 i (f - g) s x = iteratedFDerivWithin 𝕜 i f s x - iteratedFDerivWithin 𝕜 i g s x
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.norm_expSeries_summable' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸] (x : 𝔸), Summable fun n => ‖(↑n.factorial)⁻¹ • x ^ n‖
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.instNormedSpace : {ι : Type u_1} →
  [inst : Fintype ι] →
    {𝕜 : Type u_2} →
      {E : ι → Type u_3} →
        [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_2 : NormedField 𝕜] →
            [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] → NormedSpace 𝕜 (PiTensorProduct 𝕜 fun i => E i)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyFunctor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y),
  (CategoryTheory.ShortComplex.homologyFunctor C).map f = CategoryTheory.ShortComplex.homologyMap f
-- Mathlib.Algebra.Order.Archimedean.Basic
AddUnits.instAddArchimedean : ∀ (M : Type u_5) [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [Archimedean M], Archimedean (AddUnits M)
-- Mathlib.Condensed.Functors
instFullCompHausCondensedSetCompHausToCondensed : compHausToCondensed.Full
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] {l : List α},
  t.size ≤ (t.insertManyIfNewUnit l).size
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.comapComp_hom_app : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} {K : Type w₂}
  (f : K → J) (g : J → I) (X : (i : I) → C i) (b : K),
  (CategoryTheory.Pi.comapComp C f g).hom.app X b = CategoryTheory.CategoryStruct.id (X (g (f b)))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm_eq_norm : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : K),
  NumberField.mixedEmbedding.norm ((NumberField.mixedEmbedding K) x) = ↑|(Algebra.norm ℚ) x|
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.codeSupp'.match_1.eq_7 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (f : Turing.ToPartrec.Code)
  (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.zero' → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.succ → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.tail → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (c f fs : Turing.ToPartrec.Code) → c = f.cons fs → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (c f g : Turing.ToPartrec.Code) → c = f.comp g → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (c f g : Turing.ToPartrec.Code) → c = f.case g → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (c f : Turing.ToPartrec.Code) → c = f.fix → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match f.fix, k with
    | c@h:Turing.ToPartrec.Code.zero', k => h_1 c h k
    | c@h:Turing.ToPartrec.Code.succ, k => h_2 c h k
    | c@h:Turing.ToPartrec.Code.tail, k => h_3 c h k
    | c@h:(f.cons fs), k => h_4 c f fs h k
    | c@h:(f.comp g), k => h_5 c f g h k
    | c@h:(f.case g), k => h_6 c f g h k
    | c@h:f.fix, k => h_7 c f h k) =
    h_7 f.fix f ⋯ k
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- The natural map that reindexes a matrix's rows and columns with equivalent types is an
equivalence.  -/
CStarMatrix.reindexₐ : {m : Type u_1} →
  {n : Type u_2} →
    (R : Type u_7) →
      (A : Type u_8) →
        [inst : Fintype m] →
          [inst_1 : Fintype n] →
            [inst_2 : Semiring R] →
              [inst_3 : AddCommMonoid A] →
                [inst_4 : Mul A] →
                  [inst_5 : Module R A] → [inst_6 : Star A] → m ≃ n → CStarMatrix m m A ≃⋆ₐ[R] CStarMatrix n n A
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- Given the nondegenerate bilinear form `B` and the linear map `φ`,
`leftAdjointOfNondegenerate` provides the left adjoint of `φ` with respect to `B`.
The lemma proving this property is `BilinForm.isAdjointPairLeftAdjointOfNondegenerate`.  -/
LinearMap.BilinForm.leftAdjointOfNondegenerate : {V : Type u_5} →
  {K : Type u_6} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          [FiniteDimensional K V] → (B : LinearMap.BilinForm K V) → B.Nondegenerate → (V →ₗ[K] V) → V →ₗ[K] V
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.filterMap_equiv_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {f : α → β → Bool},
  Std.ExtTreeMap.filterMap (fun k => Option.guard fun v => f k v) t = Std.ExtTreeMap.filter f t
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Implementation; see `CostructuredArrow.prodEquivalence`.  -/
CategoryTheory.CostructuredArrow.prodInverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C' : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] →
            {D' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] →
                (S : CategoryTheory.Functor C D) →
                  (S' : CategoryTheory.Functor C' D') →
                    (T : D) →
                      (T' : D') →
                        CategoryTheory.Functor
                          (CategoryTheory.CostructuredArrow S T × CategoryTheory.CostructuredArrow S' T')
                          (CategoryTheory.CostructuredArrow (S.prod S') (T, T'))
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.sumIDeriv_apply : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R),
  Polynomial.sumIDeriv p = ∑ i ∈ Finset.range (p.natDegree + 1), (⇑Polynomial.derivative)^[i] p
-- Mathlib.NumberTheory.Divisors
Nat.dvd_of_mem_divisors : ∀ {n m : ℕ}, n ∈ m.divisors → n ∣ m
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_sub : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f g : α → E},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ g
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instNeg : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Neg (ModularForm Γ k)
-- Init.Data.List.Basic
List.foldr_cons : ∀ {α : Type u} {β : Type v} {a : α} {l : List α} {f : α → β → β} {b : β},
  List.foldr f b (a :: l) = f a (List.foldr f b l)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.mk_start_snd_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, ¬p.Nil → s(v, p.snd) ∈ p.edges
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.Y_eq_iff' : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 → (P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3 ↔ P 1 / P 2 ^ 3 = W.toAffine.negY (Q 0 / Q 2 ^ 2) (Q 1 / Q 2 ^ 3))
-- Mathlib.Analysis.Normed.Ring.Basic
Finset.norm_prod_le : ∀ {ι : Type u_4} {α : Type u_5} [inst : NormedCommRing α] [NormOneClass α] (s : Finset ι) (f : ι → α),
  ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖
-- Lean.HeadIndex
Lean.HeadIndex.mvar : Lean.MVarId → Lean.HeadIndex
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.Internal.Impl.map f t).isEmpty = t.isEmpty
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
TopologicalSpace.compactlyGenerated.eq_1 : ∀ (X : Type w) [inst : TopologicalSpace X],
  TopologicalSpace.compactlyGenerated X =
    TopologicalSpace.coinduced
      (fun x =>
        match x with
        | ⟨⟨fst, i⟩, s⟩ => i s)
      inferInstance
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.IsDetpBalanced.symm : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {a b : R}, A.IsDetpBalanced a b → A.IsDetpBalanced b a
-- Lean.Meta.CoeAttr
Lean.Meta.CoeFnType.ofNat : ℕ → Lean.Meta.CoeFnType
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromSource.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C}
  {Q : CategoryTheory.MorphismProperty C}, (∀ {X Y : C} (f : X ⟶ Y), Q f → P X → P Y) → P.InheritedFromSource Q
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- The discriminant of a constant polynomial is `1`.  -/
Polynomial.discr_C : ∀ {R : Type u_1} [inst : CommRing R] (r : R), (Polynomial.C r).discr = 1
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_exp_neg_Ioi : ∀ (c : ℝ), MeasureTheory.IntegrableOn (fun x => Real.exp (-x)) (Set.Ioi c) MeasureTheory.volume
-- Mathlib.Topology.Separation.Basic
t1Space_iff_exists_open : ∀ {X : Type u_1} [inst : TopologicalSpace X], T1Space X ↔ Pairwise fun x y => ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U
-- Mathlib.Data.Finset.Insert
Finset.instUniqueSubtypeMemSingleton : {α : Type u_1} → (i : α) → Unique ↥{i}
-- Mathlib.Algebra.Group.Defs
AddCancelCommMonoid.toIsLeftCancelAdd : ∀ {M : Type u} [self : AddCancelCommMonoid M], IsLeftCancelAdd M
-- Init.Data.SInt.Lemmas
Int16.ofIntClamp_bitVecToInt : ∀ (n : BitVec 16), Int16.ofIntClamp n.toInt = Int16.ofBitVec n
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The lifted map `s.X ⟶ (gluing 𝒰 f g).glued` in order to show that `(gluing 𝒰 f g).glued` is
indeed the pullback.

Given a pullback cone `s`, we have the maps `s.fst ⁻¹' Uᵢ ⟶ Uᵢ` and
`s.fst ⁻¹' Uᵢ ⟶ s.X ⟶ Y` that we may lift to a map `s.fst ⁻¹' Uᵢ ⟶ Uᵢ ×[Z] Y`.

to glue these into a map `s.X ⟶ Uᵢ ×[Z] Y`, we need to show that the maps agree on
`(s.fst ⁻¹' Uᵢ) ×[s.X] (s.fst ⁻¹' Uⱼ) ⟶ Uᵢ ×[Z] Y`. This is achieved by showing that both of these
maps factors through `gluedLiftPullbackMap`.
 -/
AlgebraicGeometry.Scheme.Pullback.gluedLift : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          (s : CategoryTheory.Limits.PullbackCone f g) → s.pt ⟶ (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).glued
-- Mathlib.Data.Multiset.ZeroCons
Multiset.Rel.cons : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {a : α} {b : β} {as : Multiset α} {bs : Multiset β},
  r a b → Multiset.Rel r as bs → Multiset.Rel r (a ::ₘ as) (b ::ₘ bs)