mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instDivInvMonoid : {α : Type u_1} → [DivInvMonoid α] → DivInvMonoid αᵃᵒᵖ
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.lift_app_coe : ∀ {X Y : SSet} (f : X ⟶ Y) {B : Y.Subcomplex} (hf : SSet.Subcomplex.range f ≤ B) {n : SimplexCategoryᵒᵖ} (x : X.obj n),
  ↑((CategoryTheory.ConcreteCategory.hom ((SSet.Subcomplex.lift f hf).app n)) x) =
    (CategoryTheory.ConcreteCategory.hom (f.app n)) x
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.ContinuousRiemannianMetric.mk.inj : ∀ {B : Type u_4} {inst : TopologicalSpace B} {F : Type u_5} {inst_1 : NormedAddCommGroup F} {inst_2 : NormedSpace ℝ F}
  {E : B → Type u_6} {inst_3 : TopologicalSpace (Bundle.TotalSpace F E)} {inst_4 : (b : B) → TopologicalSpace (E b)}
  {inst_5 : (b : B) → AddCommGroup (E b)} {inst_6 : (b : B) → Module ℝ (E b)} {inst_7 : FiberBundle F E}
  {inst_8 : VectorBundle ℝ F E} {inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ}
  {symm : ∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v}
  {pos : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v}
  {isVonNBounded : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1}}
  {continuous : Continuous fun b => ⟨b, inner b⟩} {inner_1 : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ}
  {symm_1 : ∀ (b : B) (v w : E b), ((inner_1 b) v) w = ((inner_1 b) w) v}
  {pos_1 : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner_1 b) v) v}
  {isVonNBounded_1 : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner_1 b) v) v < 1}}
  {continuous_1 : Continuous fun b => ⟨b, inner_1 b⟩},
  { inner := inner, symm := symm, pos := pos, isVonNBounded := isVonNBounded, continuous := continuous } =
      { inner := inner_1, symm := symm_1, pos := pos_1, isVonNBounded := isVonNBounded_1, continuous := continuous_1 } →
    inner = inner_1
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a base map `b₁ : M → B₁`, and
another base map `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending smoothly
on `m`, one can apply `ϕ m` to `v m`, and the resulting map is `C^n`.

Note that the smoothness of `ϕ` cannot always be stated as smoothness of a map into a manifold,
as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` are smooth manifolds only when `b₁` and `b₂` are
globally smooth, but we want to apply this lemma with only local information. Therefore, we
formulate it using smoothness of `ϕ` read in coordinates.

Version for `ContMDiffWithinAt`. We also give a version for `ContMDiffAt`, but no version for
`ContMDiffOn` or `ContMDiff` as our assumption, written in coordinates, only makes sense around
a point.

For a version with `B₁ = B₂` and `b₁ = b₂`, in which smoothness can be expressed without
`inCoordinates`, see `ContMDiffWithinAt.clm_bundle_apply`.
 -/
ContMDiffWithinAt.clm_apply_of_inCoordinates : ∀ {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {E₁ : B₁ → Type u_7}
  {E₂ : B₂ → Type u_8} [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B₁) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B₁) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B₁) → TopologicalSpace (E₁ x)]
  [inst_7 : (x : B₂) → AddCommGroup (E₂ x)] [inst_8 : (x : B₂) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_9} [inst_13 : NormedAddCommGroup EB₁]
  [inst_14 : NormedSpace 𝕜 EB₁] {HB₁ : Type u_10} [inst_15 : TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁}
  [inst_16 : TopologicalSpace B₁] [inst_17 : ChartedSpace HB₁ B₁] {EB₂ : Type u_11} [inst_18 : NormedAddCommGroup EB₂]
  [inst_19 : NormedSpace 𝕜 EB₂] {HB₂ : Type u_12} [inst_20 : TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂}
  [inst_21 : TopologicalSpace B₂] [inst_22 : ChartedSpace HB₂ B₂] {EM : Type u_13} [inst_23 : NormedAddCommGroup EM]
  [inst_24 : NormedSpace 𝕜 EM] {HM : Type u_14} [inst_25 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  [inst_26 : TopologicalSpace M] [inst_27 : ChartedSpace HM M] {n : WithTop ℕ∞} [inst_28 : FiberBundle F₁ E₁]
  [inst_29 : VectorBundle 𝕜 F₁ E₁] [inst_30 : FiberBundle F₂ E₂] [inst_31 : VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁}, ⋯
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_smul : ∀ {𝕜 : 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_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {s : Set M} {x : M} {a : M → 𝕜},
  MDiffAt[s] a x →
    ∀ {g : M → F}, MDiffAt[s] g x → UniqueMDiffAt[s] x → d[s] (a • g) x = a x • d[s] g x + (d[s] a x).smulRight (g x)
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_max_def : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R),
  max x y = Tropical.trop (max (Tropical.untrop x) (Tropical.untrop y))
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_nsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIocDiv hp (a - m • p) b = toIocDiv hp a b + ↑m
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
intEquivOfZMultiplesEqTop_apply : ∀ {G : Type u_2} [inst : Infinite G] [inst_1 : AddGroup G] (g : G) (hg : AddSubgroup.zmultiples g = ⊤) (a : ℤ),
  (intEquivOfZMultiplesEqTop g hg) a = a • g
-- Mathlib.GroupTheory.Submonoid.Inverses
/-- The submonoid of pointwise inverse of `S` is `MulEquiv` to `S`.  -/
Submonoid.leftInvEquiv : {M : Type u_1} → [inst : CommMonoid M] → (S : Submonoid M) → S ≤ IsUnit.submonoid M → ↥S.leftInv ≃* ↥S
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhdsGT_one_neBot : (nhdsWithin 1 (Set.Ioi 1)).NeBot
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.instIsLeftAdjointCommMonCatUnderMonoidAlgebra : ∀ (R : CommRingCat), R.monoidAlgebra.IsLeftAdjoint
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.Λ'.normal.injEq : ∀ {Γ : Type u_1} {Λ : Type u_2} (a a_1 : Λ), (Turing.TM0to1.Λ'.normal a = Turing.TM0to1.Λ'.normal a_1) = (a = a_1)
-- Lean.Declaration
Lean.QuotVal.mk.injEq : ∀ (toConstantVal : Lean.ConstantVal) (kind : Lean.QuotKind) (toConstantVal_1 : Lean.ConstantVal)
  (kind_1 : Lean.QuotKind),
  ({ toConstantVal := toConstantVal, kind := kind } = { toConstantVal := toConstantVal_1, kind := kind_1 }) =
    (toConstantVal = toConstantVal_1 ∧ kind = kind_1)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotencyClass_le_one_of_isSimple_of_isNilpotent`. -/
nilpotencyClass_le_one_of_isSimple_of_isNilpotent : ∀ {G : Type u_1} [inst : Group G] [IsSimpleGroup G] [Group.IsNilpotent G], Group.nilpotencyClass G ≤ 1
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- Mapping an integral closure along an `AlgEquiv` gives the integral closure.  -/
integralClosure_map_algEquiv : ∀ {R : Type u_1} {A : Type u_2} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing S]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] (f : A ≃ₐ[R] S),
  Subalgebra.map (↑f) (integralClosure R A) = integralClosure R S
-- Mathlib.Algebra.Notation.Defs
VSub.ext : ∀ {G : outParam (Type u_1)} {P : Type u_2} {x y : VSub G P}, VSub.vsub = VSub.vsub → x = y
-- Mathlib.Data.Finsupp.Defs
Finsupp.equivFunOnFinite_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] [inst_1 : Finite α] (a : α →₀ M) (a_1 : α),
  Finsupp.equivFunOnFinite a a_1 = a a_1
-- Mathlib.Data.Prod.TProd
List.TProd.fst_mk : ∀ {ι : Type u} {α : ι → Type v} (i : ι) (l : List ι) (f : (i : ι) → α i), (List.TProd.mk (i :: l) f).1 = f i
-- Mathlib.Order.RelSeries
/-- Any `LTSeries` can be refined to a `CovBy`-`RelSeries`
in a bidirectionally well-founded order.  -/
LTSeries.exists_relSeries_covBy : ∀ {α : Type u_3} [inst : PartialOrder α] [WellFoundedLT α] [WellFoundedGT α] (s : LTSeries α),
  ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ i 0 = 0 ∧ i (Fin.last s.length) = Fin.last t.length
-- Init.Data.UInt.Bitwise
UInt8.xor_eq_zero_iff : ∀ {a b : UInt8}, a ^^^ b = 0 ↔ a = b
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
_private.Mathlib.RingTheory.Bialgebra.MonoidAlgebra.0.MonoidAlgebra.mapDomainOfBialgHomFun : {R : Type u_1} →
  {G : Type u_5} →
    {H : Type u_6} →
      [inst : CommRing R] →
        [IsDomain R] → [inst_2 : Group G] → [inst_3 : Group H] → (MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) → G → H
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
separableClosure_inf_perfectClosure : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  separableClosure F E ⊓ perfectClosure F E = ⊥
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.image_apply_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (x : ↑s), ↑((e.image s) x) = e ↑x
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.mk.inj : ∀ {X Y : AlgebraicGeometry.Scheme} {toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace},
  { toLRSHom' := toLRSHom' } = { toLRSHom' := toLRSHom'_1 } → toLRSHom' = toLRSHom'_1
-- Std.Sync.Notify
Std.Notify.mk.injEq : ∀ (state state_1 : Std.Mutex Std.Notify.State), ({ state := state } = { state := state_1 }) = (state = state_1)
-- Mathlib.Analysis.Normed.Operator.NormedSpace
LinearIsometryEquiv.enorm_toContinuousLinearMap : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] [NontrivialTopology E] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_7 : RingHomInvPair σ₁₂ σ₂₁] [inst_8 : RingHomInvPair σ₂₁ σ₁₂] [inst_9 : RingHomIsometric σ₁₂]
  (e : E ≃ₛₗᵢ[σ₁₂] F), ‖↑↑e‖ₑ = 1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_eq_toList_rco : ∀ {m n : ℕ}, (m<...=n).toList = ((m + 1)...n + 1).toList
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length'.eq_1 : ∀ {α : Type u} (s : Stream'.Seq α), s.length' = if h : s.Terminates then ↑(s.length h) else ⊤
-- Mathlib.NumberTheory.Cyclotomic.Basic
IntermediateField.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot : ∀ (S : Set ℕ) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  (∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n) →
    IsCyclotomicExtension S K ↥(IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
-- Batteries.Util.Panic
/-- Panic with a specific default value `v`.  -/
Batteries.panicWith : {α : Sort u_1} → α → String → α
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.ret.sizeOf_spec : ∀ (x : Lean.IR.Arg), sizeOf (Lean.IR.FnBody.ret x) = 1 + sizeOf x
-- Mathlib.Algebra.Ring.Subring.Defs
/-- `Subring R` is the type of subrings of `R`. A subring of `R` is a subset `s` that is a
multiplicative submonoid and an additive subgroup. Note in particular that it shares the
same 0 and 1 as R.  -/
Subring : (R : Type u) → [NonAssocRing R] → Type u
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.map.congr_simp : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] (f f_1 : (a : α) → β a → γ a),
  f = f_1 → ∀ (m m_1 : Std.ExtDHashMap α β), m = m_1 → Std.ExtDHashMap.map f m = Std.ExtDHashMap.map f_1 m_1
-- Mathlib.Topology.UniformSpace.Defs
/-- A function `f : α → β` is *uniformly continuous* on `s : Set α` if `(f x, f y)` tends to
the diagonal as `(x, y)` tends to the diagonal while remaining in `s ×ˢ s`.
In other words, if `x` is sufficiently close to `y`, then `f x` is close to
`f y` no matter where `x` and `y` are located in `s`.  -/
UniformContinuousOn : {α : Type ua} → {β : Type ub} → [UniformSpace α] → [UniformSpace β] → (α → β) → Set α → Prop
-- Mathlib.RingTheory.Coprime.Basic
/-- `IsCoprime` is not a useful definition for `Nat`; consider using `Nat.Coprime` instead.  -/
Nat.isCoprime_iff : ∀ {m n : ℕ}, IsCoprime m n ↔ m = 1 ∨ n = 1
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n log n)`. Fold over the elements of a heap in increasing order,
by repeatedly pulling the minimum element out of the heap.
 -/
Batteries.BinomialHeap.Imp.Heap.fold : {α : Type u_1} → {β : Type u_2} → (α → α → Bool) → Batteries.BinomialHeap.Imp.Heap α → β → (β → α → β) → β
-- Init.Data.String.Slice
String.Slice.SplitIterator.operating.inj : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  {inst : String.Slice.Pattern.ToForwardSearcher pat σ} {currPos : s.Pos}
  {searcher : Std.Iter (String.Slice.Pattern.SearchStep s)} {currPos_1 : s.Pos}
  {searcher_1 : Std.Iter (String.Slice.Pattern.SearchStep s)},
  String.Slice.SplitIterator.operating currPos searcher = String.Slice.SplitIterator.operating currPos_1 searcher_1 →
    currPos = currPos_1 ∧ searcher = searcher_1
-- Mathlib.Data.Finset.Card
Finset.card_ne_zero : ∀ {α : Type u_1} {s : Finset α}, s.card ≠ 0 ↔ s.Nonempty
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.keyAtIdx?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {i : ℕ}, t₁.keyAtIdx? i = t₂.keyAtIdx? i
-- Mathlib.Algebra.Order.Hom.Basic
map_div_rev : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [GroupSeminormClass F α β] (f : F) (x y : α), f (x / y) = f (y / x)
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- **Alias** of the reverse direction of `SimpleGraph.neighborFinset_eq_empty`. -/
SimpleGraph.IsIsolated.neighborFinset_eq_empty : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)],
  G.IsIsolated v → G.neighborFinset v = ∅
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
panicking if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryGT! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Raw α β cmp → α → (a : α) × β a
-- Mathlib.GroupTheory.Congruence.BigOperators
/-- Multiplicative congruence relations preserve finite product.  -/
Con.finsetProd : ∀ {ι : Type u_1} {M : Type u_2} [inst : CommMonoid M] (c : Con M) (s : Finset ι) {f g : ι → M},
  (∀ i ∈ s, c (f i) (g i)) → c (s.prod f) (s.prod g)
-- Mathlib.Data.ZMod.QuotientGroup
AddAction.orbitZMultiplesEquiv_symm_apply' : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] (a : α) [inst_1 : AddAction α β] (b : β) (k : ℤ),
  (AddAction.orbitZMultiplesEquiv a b).symm ↑k = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.IsSubordinate.mono : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} {f : BumpCovering ι X s} {U V : ι → Set X},
  f.IsSubordinate U → (∀ (i : ι), U i ⊆ V i) → f.IsSubordinate V
-- Lean.Elab.PreDefinition.WF.Unfold
/-- Generalization of `splitMatch` that can handle `casesOn`  -/
_private.Lean.Elab.PreDefinition.WF.Unfold.0.Lean.Elab.WF.splitMatchOrCasesOn : Lean.MVarId → Lean.Expr → Lean.Meta.MatcherInfo → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Order.Hom.Basic
/-- Embeddings of partial orders that preserve `<` also preserve `≤`.  -/
RelEmbedding.orderEmbeddingOfLTEmbedding : {α : Type u_2} →
  {β : Type u_3} →
    [inst : PartialOrder α] → [inst_1 : PartialOrder β] → ((fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2) → α ↪o β
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_mapₘ : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → δ a},
  (Std.DHashMap.Internal.toListModel (↑(m.mapₘ f)).buckets).Perm
    (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.galoisConnection_toGrothendieck_toPrecoverage : ∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_3, u_2} C],
  GaloisConnection CategoryTheory.Precoverage.toGrothendieck CategoryTheory.GrothendieckTopology.toPrecoverage
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.edgeSetSumEquiv.match_1.congr_eq_4 : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}
  (motive : (x x_1 : V ⊕ W) → (G ⊕g H).Adj x x_1 → Sort u_3) (x x_1 : V ⊕ W) (x_2 : (G ⊕g H).Adj x x_1)
  (h_1 : (u v : V) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)) → motive (Sum.inl u) (Sum.inl v) h)
  (h_2 : (u v : W) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)) → motive (Sum.inr u) (Sum.inr v) h)
  (h_3 : (u : V) → (v : W) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)) → motive (Sum.inl u) (Sum.inr v) h)
  (h_4 : (u : W) → (v : V) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)) → motive (Sum.inr u) (Sum.inl v) h) (u : W)
  (v : V) (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)),
  x = Sum.inr u →
    x_1 = Sum.inl v →
      x_2 ≍ h →
        (match x, x_1, x_2 with
          | Sum.inl u, Sum.inl v, h => h_1 u v h
          | Sum.inr u, Sum.inr v, h => h_2 u v h
          | Sum.inl u, Sum.inr v, h => h_3 u v h
          | Sum.inr u, Sum.inl v, h => h_4 u v h) ≍
          h_4 u v h
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.ofScalar : {R : Type u_1} → {X : Type u_2} → R → FreeAlgebra.Pre R X
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {T : CategoryTheory.Monad C} {A B : T.Algebra}
  {f : A.A ⟶ B.A}
  {h :
    autoParam (CategoryTheory.CategoryStruct.comp (T.map f) B.a = CategoryTheory.CategoryStruct.comp A.a f)
      CategoryTheory.Monad.Algebra.Hom.h._autoParam}
  {f_1 : A.A ⟶ B.A}
  {h_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (T.map f_1) B.a = CategoryTheory.CategoryStruct.comp A.a f_1)
      CategoryTheory.Monad.Algebra.Hom.h._autoParam},
  { f := f, h := h } = { f := f_1, h := h_1 } → f = f_1
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_one_eq_measureReal : ∀ {X : Type u_5} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {s : Set X}, ∫ (x : X) in s, 1 ∂μ = μ.real s
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Naturality of the oplax functoriality constraint, on the left.  -/
CategoryTheory.OplaxFunctor.mapComp_naturality_left_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (X : ↑(self.obj a)),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)).toNatTrans.app X)
      ((self.mapComp f' g).toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X)
      ((self.map g).toFunctor.map ((self.map₂ η).toNatTrans.app X))
-- Mathlib.Data.ENat.Lattice
/-- **Alias** of `ENat.iInf_eq_natCast_iff`. -/
ENat.iInf_eq_coe_iff : ∀ {ι : Sort u_1} {f : ι → ℕ∞} {n : ℕ}, ⨅ i, f i = ↑n ↔ (∃ i, f i = ↑n) ∧ ∀ (i : ι), ↑n ≤ f i
-- Mathlib.Data.Set.Card
Set.exists_superset_subset_encard_eq : ∀ {α : Type u_1} {s t : Set α} {k : ℕ∞}, s ⊆ t → s.encard ≤ k → k ≤ t.encard → ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.evaluation_preservesFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesFiniteLimits (PresheafOfModules.evaluation R X)
-- Lean.Expr
Lean.mkApp5 : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Data.Finset.Image
/-- The `Finset` version of `Equiv.symm_image_subset`.  -/
Finset.map_symm_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {f : α ≃ β},
  Finset.map f.symm.toEmbedding t ⊆ s ↔ t ⊆ Finset.map f.toEmbedding s
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Augmented.stdSimplex_obj_right : ∀ (Δ : SimplexCategory), (SSet.Augmented.stdSimplex.obj Δ).right = ⊤_ Type u
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredWithTopPropSetWithTop : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (κ' : Cardinal.{u})
  [inst_1 : Fact κ'.IsRegular], CategoryTheory.IsCardinalFiltered (Subtype (J.PropSetWithTop κ')) κ'
-- Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Polynomial.Bivariate.aeval_aeval_eq_aeval_algEquivAdjoin : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_3}
  [inst_3 : CommRing B] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B] {x : A} (y : B)
  (hx : Transcendental R x) (p : Polynomial (Polynomial R)),
  (Polynomial.aeval ((algebraMap A B) x)) ((Polynomial.aeval (Polynomial.C ⟨y, ⋯⟩)) p) =
    (Polynomial.aeval y) ((Polynomial.Bivariate.Transcendental.algEquivAdjoin hx) p)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableAt.smul : ∀ {𝕜 : 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} {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V}, MDiffAt f x → MDiffAt g x → MDiffAt (f • g) x
-- Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
/-- The fan that is induced by a wide pullback cone.  -/
CategoryTheory.Limits.WidePullbackCone.toFan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      {B : C} →
        {objs : ι → C} →
          (arrows : (j : ι) → objs j ⟶ B) →
            CategoryTheory.Limits.WidePullbackCone arrows → CategoryTheory.Limits.Fan objs
-- Mathlib.Probability.Decision.Risk.Basic
/-- See `avgRisk_const_right'` for a similar result when `P` is not a Markov kernel.  -/
ProbabilityTheory.avgRisk_const_right : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧) [ProbabilityTheory.IsMarkovKernel P]
  (ν : MeasureTheory.Measure 𝓨) (π : MeasureTheory.Measure Θ),
  ProbabilityTheory.avgRisk ℓ P (ProbabilityTheory.Kernel.const 𝓧 ν) π = ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂ν ∂π
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.instNoPrefixPatternModelForallCharProp : ∀ {p : Char → Prop} [inst : DecidablePred p], String.Slice.Pattern.Model.NoPrefixPatternModel p
-- Mathlib.Data.Sign.Defs
_private.Mathlib.Data.Sign.Defs.0.SignType.fin3Equiv.match_1.eq_1 : ∀ (motive : SignType → Sort u_1) (h_1 : Unit → motive SignType.zero) (h_2 : Unit → motive SignType.pos)
  (h_3 : Unit → motive SignType.neg),
  (match SignType.zero with
    | SignType.zero => h_1 ()
    | SignType.pos => h_2 ()
    | SignType.neg => h_3 ()) =
    h_1 ()
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg : {α : Type} →
  {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → m α → m α
-- Mathlib.Topology.LocallyConstant.Algebra
/-- Evaluation as a `RingHom`  -/
LocallyConstant.evalRingHom : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : Semiring Y] → X → LocallyConstant X Y →+* Y