mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.BooleanAlgebra.Set
Set.nonempty_compl : ∀ {α : Type u_1} {s : Set α}, sᶜ.Nonempty ↔ s ≠ Set.univ
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_then_not_ite' : ∀ (c0 c1 : Bool) {a b : Bool}, (bif c0 then !bif c1 then !a else b else a) = bif c0 && !c1 then !b else a
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Coplanar.eq_1 : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P), Coplanar k s = (Module.rank k ↥(vectorSpan k s) ≤ 2)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.ChosenPullbacksAlong.snd
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom) S.hom) T.hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.snd R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom)
      (CategoryTheory.ChosenPullbacksAlong.snd S.hom T.hom)
-- Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
/-- Given subcomplexes `S` and `T` of simplicial sets, this if a `Functor.PushoutObjObj`
structure for the chosen binary products on `SSet`, with point `S.unionProd T`.  -/
SSet.Subcomplex.unionProd.pushoutObjObj : {X Y : SSet} →
  (S : X.Subcomplex) → (T : Y.Subcomplex) → (CategoryTheory.MonoidalCategory.curriedTensor SSet).PushoutObjObj S.ι T.ι
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.id_map₂ : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  (CategoryTheory.StrictlyUnitaryPseudofunctor.id B).map₂ η = η
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsAddCyclic.of_exponent_eq_card : ∀ {α : Type u_1} [inst : AddCommGroup α] [Finite α], AddMonoid.exponent α = Nat.card α → IsAddCyclic α
-- Mathlib.Topology.ShrinkingLemma
/-- `chainSup hu c hc ne hfin hU` is an upper bound of the chain `c`.  -/
ShrinkingLemma.PartialRefinement.le_chainSup : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  {c : Set (ShrinkingLemma.PartialRefinement u s p)} (hc : IsChain (fun x1 x2 => x1 ≤ x2) c) (ne : c.Nonempty)
  (hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite) (hU : s ⊆ ⋃ i, u i) {v : ShrinkingLemma.PartialRefinement u s p},
  v ∈ c → v ≤ ShrinkingLemma.PartialRefinement.chainSup c hc ne hfin hU
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- Reindex the indexing type of an effective epi family.
 -/
CategoryTheory.EffectiveEpiFamily.reindex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} {α' : Type u_3} (X : α → C)
  (π : (a : α) → X a ⟶ B) (e : α' ≃ α),
  (CategoryTheory.EffectiveEpiFamily (fun a => X (e a)) fun a => π (e a)) → CategoryTheory.EffectiveEpiFamily X π
-- Mathlib.Order.FixedPoints
OrderHom.isFixedPt_lfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), Function.IsFixedPt (⇑f) (OrderHom.lfp f)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.invFun_eq_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  {f : α ≃*o β}, f.invFun = ⇑f.symm
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLTD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β) (fallback : (a : α) × β a),
  Std.DTreeMap.Internal.Impl.getEntryLTD k t fallback = (Std.DTreeMap.Internal.Impl.getEntryLT? k t).getD fallback
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.initial_eval : ∀ {α : Type u₁} {I : α → Type u₂} [inst : (s : α) → CategoryTheory.Category.{v₂, u₂} (I s)]
  [∀ (s : α), CategoryTheory.IsCofiltered (I s)] (s : α), (CategoryTheory.Pi.eval I s).Initial
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_union_of_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k m₁ = true → Std.DTreeMap.Internal.Impl.contains k (m₁.union m₂ ⋯ ⋯) = true
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorRefVecBlastNot : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.RefVec fun {len} => Std.Tactic.BVDecide.BVExpr.bitblast.blastNot
-- Mathlib.RingTheory.Etale.StandardEtale
/-- The class of standard etale algebras,
defined to be the existence of a `StandardEtalePresentation`.  -/
Algebra.IsStandardEtale : (R : Type u_4) → (S : Type u_5) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Prop
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_eq_zero_iff : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι)
  {x : G i}, RestrictedProduct.single A i x = 0 ↔ x = 0
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableOn_singleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E}, DifferentiableOn 𝕜 f {x}
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_inv_hom : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) (E : L.LeftExtension F) (c : C),
  (CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso G F L E c).inv.hom =
    CategoryTheory.CategoryStruct.id (G.obj (E.right.obj c))
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.multiset_sum_sum_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  (f : Multiset (α →₀ M)) (h : α → M → N),
  (∀ (a : α), h a 0 = 0) →
    (∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) → f.sum.sum h = (Multiset.map (fun g => g.sum h) f).sum
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofPartialTermInfo.injEq : ∀ (i i_1 : Lean.Elab.PartialTermInfo),
  (Lean.Elab.Info.ofPartialTermInfo i = Lean.Elab.Info.ofPartialTermInfo i_1) = (i = i_1)
-- Mathlib.Topology.Order.IntermediateValue
/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and the set `s ∩ [a, b)` has no maximal point, then `b ∈ s`.  -/
IsClosed.mem_of_ge_of_forall_exists_gt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {a b : α}
  {s : Set α}, IsClosed (s ∩ Set.Icc a b) → a ∈ s → a ≤ b → (∀ x ∈ s ∩ Set.Ico a b, (s ∩ Set.Ioc x b).Nonempty) → b ∈ s
-- Mathlib.Data.Matrix.Basis
/-- Linear maps from finite matrices are equal if they agree on the standard basis.

See note [partially-applied ext lemmas].  -/
Matrix.ext_linearMap : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) {α : Type u_7} {β : Type u_8} [inst : DecidableEq m]
  [inst_1 : DecidableEq n] [Finite m] [Finite n] [inst_4 : Semiring R] [inst_5 : AddCommMonoid α]
  [inst_6 : AddCommMonoid β] [inst_7 : Module R α] [inst_8 : Module R β] ⦃f g : Matrix m n α →ₗ[R] β⦄,
  (∀ (i : m) (j : n), f ∘ₗ Matrix.singleLinearMap R i j = g ∘ₗ Matrix.singleLinearMap R i j) → f = g
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq' : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : CompleteLattice α],
  CompletelyDistribLattice.MinimalAxioms α → ∀ (f : (a : ι) → κ a → α), ⨅ i, ⨆ j, f i j = ⨆ g, ⨅ i, f i (g i)
-- Lean.Data.Name
Lean.Name.getString! : Lean.Name → String
-- Init.Data.Array.Erase
Array.eraseP_append_right : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} (ys : Array α),
  (∀ b ∈ xs, ¬p b = true) → (xs ++ ys).eraseP p = xs ++ ys.eraseP p
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.roots_T_real_nodup : ∀ (n : ℕ), (Multiset.map (fun k => Real.cos ((2 * ↑k + 1) * Real.pi / (2 * ↑n))) (Multiset.range n)).Nodup
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If a power series converges at `w`, it converges absolutely at all `z` of smaller norm.  -/
summable_powerSeries_of_norm_lt : ∀ {α : Type u_1} [inst : NormedDivisionRing α] [CompleteSpace α] {f : ℕ → α} {w z : α},
  (CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i) → ‖z‖ < ‖w‖ → Summable fun n => f n * z ^ n
-- Lean.Server.InfoUtils
Lean.Elab.Info.isTerm : Lean.Elab.Info → Bool
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countableOrCountablyGenerated_left_of_prod_left_of_nonempty : ∀ {β : Type u_2} {α : Type u_3} {γ : Type u_4} [inst : MeasurableSpace γ] [Nonempty β]
  [h : MeasurableSpace.CountableOrCountablyGenerated (α × β) γ], MeasurableSpace.CountableOrCountablyGenerated α γ
-- Init.Data.UInt.Lemmas
UInt8.lt_or_lt_of_ne : ∀ {a b : UInt8}, a ≠ b → a < b ∨ b < a
-- Mathlib.Geometry.Euclidean.Triangle
EuclideanGeometry.angle_lt_iff_dist_lt : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c : P},
  ¬Collinear ℝ {a, b, c} → (EuclideanGeometry.angle a c b < EuclideanGeometry.angle a b c ↔ dist a b < dist a c)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.ext_iff : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] {𝒜 : ιA → σA} {ℳ : ιM → σM} [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ]
  {I J : HomogeneousSubmodule 𝒜 ℳ}, I = J ↔ I.toSubmodule = J.toSubmodule
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
_private.Mathlib.Topology.ContinuousMap.Bounded.Basic.0.BoundedContinuousFunction.dist_nonneg' : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β}, 0 ≤ dist f g
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
/-- The unit isomorphism of the equivalence
`Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c`.  -/
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) ≅
            CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor.comp
              CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.guitartExact_iff_isConnected_rightwards : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B),
  w.GuitartExact ↔
    ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), CategoryTheory.IsConnected (w.StructuredArrowRightwards g)
-- Aesop.Search.SearchM
Aesop.SearchM.Context.normSimpContext : Aesop.SearchM.Context → Aesop.NormSimpContext
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.hasForgetToCoalgebra : {R : Type u} → [inst : CommRing R] → CategoryTheory.HasForget₂ (BialgCat R) (CoalgCat R)
-- Mathlib.Order.Filter.CardinalInter
Filter.cardinalInterFilter_top : ∀ {α : Type u} {c : Cardinal.{u}}, CardinalInterFilter ⊤ c
-- Mathlib.CategoryTheory.Action.Basic
/-- Restricting scalars along equal maps is naturally isomorphic.  -/
Action.resCongr : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_3} →
      {H : Type u_4} →
        [inst_1 : Monoid G] → [inst_2 : Monoid H] → {f f' : G →* H} → f = f' → (Action.res V f ≅ Action.res V f')
-- Batteries.Recycling.MonadSatisfying.Basic
/-- If a monad has `MonadSatisfying m`, then we can lift a `h : SatisfiesM (m := m) p x` predicate
to monadic value `satisfying x p : m { x // p x }`.

Reader, state, and exception monads have `MonadSatisfying` instances if the base monad does.
 -/
MonadSatisfying : (m : Type u → Type v) → [inst : Functor m] → [LawfulFunctor m] → Type (max (u + 1) v)
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_ι_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C}
  (c : CategoryTheory.Limits.Cocone K) (F : CategoryTheory.Functor C D) {X : D} (f : F.obj c.pt ⟶ X) (j : J),
  (c.toCostructuredArrowCocone F f).ι.app j = CategoryTheory.CostructuredArrow.homMk (c.ι.app j) ⋯
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_mul_of_left_mem_nonZeroDivisors : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.leadingCoeff f ∈ nonZeroDivisors R → m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.HasExt.standard : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C], CategoryTheory.HasExt C
-- Init.Ext
Subtype.ext_iff : ∀ {α : Sort u} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_lt : ∀ {a b : UInt64}, a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256
-- Mathlib.Data.Set.Basic
Set.union_nonempty : ∀ {α : Type u} {s t : Set α}, (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty
-- Batteries.Data.Vector.Lemmas
Vector.idRun_scanrM : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {f : α → β → Id β} {as : Vector α n},
  (Vector.scanrM f init as).run = Vector.scanr (fun x1 x2 => (f x1 x2).run) init as
-- Mathlib.Data.Set.Lattice
/-- This rather trivial consequence of `iInter₂_subset` is convenient with `apply`, and has `i` and
`j` explicit for this purpose.  -/
Set.iInter₂_subset_of_subset : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set α} (i : ι) (j : κ i),
  s i j ⊆ t → ⋂ i, ⋂ j, s i j ⊆ t
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNormedAddCommGroup : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] → [inst_1 : NormedAddCommGroup β] → NormedAddCommGroup (ZeroAtInftyContinuousMap α β)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.join_red_of_step : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red.Step L₁ L₂ → Relation.Join FreeGroup.Red L₁ L₂
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidIso.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (toMulEquiv toMulEquiv_1 : α ≃* β) (e_toMulEquiv : toMulEquiv = toMulEquiv_1)
  (map_le_map_iff' : ∀ {a b : α}, toMulEquiv.toFun a ≤ toMulEquiv.toFun b ↔ a ≤ b),
  { toMulEquiv := toMulEquiv, map_le_map_iff' := map_le_map_iff' } =
    { toMulEquiv := toMulEquiv_1, map_le_map_iff' := ⋯ }
-- Mathlib.Data.Nat.Log
Nat.log.eq_1 : ∀ (b n : ℕ), Nat.log b n = if b ≤ 1 then 0 else (Nat.log.go n b n).2
-- Mathlib.Order.Preorder.Chain
Flag.instOrderBotSubtypeMem : {α : Type u_1} → [inst : Preorder α] → [OrderBot α] → (s : Flag α) → OrderBot ↥s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.comp_fst_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {X Y Z : CategoryTheory.Limits.CategoricalPullback F G} (f : X.Hom Y) (g : Y.Hom Z) {Z_1 : A} (h : Z.fst ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).fst h =
    CategoryTheory.CategoryStruct.comp f.fst (CategoryTheory.CategoryStruct.comp g.fst h)
-- Mathlib.Data.Set.Prod
Set.eqOn_prodMap_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f f' : α → γ} {g g' : β → δ} {s : Set α} {t : Set β},
  s.Nonempty → t.Nonempty → (Set.EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t) ↔ Set.EqOn f f' s ∧ Set.EqOn g g' t)
-- Mathlib.Order.Filter.Pointwise
Filter.smul_set_mem_smul_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter β} {s : Set β} {a : α}, s ∈ f → a • s ∈ a • f
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.NonnegCoeffs.below.num : ∀ {motive : (a : Lean.Grind.CommRing.Poly) → a.NonnegCoeffs → Prop} (c : ℤ) (a : c ≥ 0),
  Lean.Grind.CommRing.Poly.NonnegCoeffs.below ⋯
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_sub : ∀ (n₁ n₂ : ℤ), (n₁ - n₂).negOnePow = n₁.negOnePow * n₂.negOnePow
-- Lean.Elab.MutualDef
Lean.Elab.Term.instTypeNameAsyncBodyInfo : TypeName Lean.Elab.Term.AsyncBodyInfo
-- Mathlib.MeasureTheory.Measure.Prod
/-- The product of two non-null sets is null measurable
if and only if both of them are null measurable.  -/
MeasureTheory.Measure.nullMeasurableSet_prod_of_ne_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set α} {t : Set β},
  μ s ≠ 0 →
    ν t ≠ 0 →
      (MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
        MeasureTheory.NullMeasurableSet s μ ∧ MeasureTheory.NullMeasurableSet t ν)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.contSupp.match_1.eq_5 : ∀ (motive : Turing.PartrecToTM2.Cont' → Sort u_1)
  (h_1 : (fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.cons₁ fs k))
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive k.cons₂)
  (h_3 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.comp f k))
  (h_4 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.fix f k))
  (h_5 : Unit → motive Turing.PartrecToTM2.Cont'.halt),
  (match Turing.PartrecToTM2.Cont'.halt with
    | Turing.PartrecToTM2.Cont'.cons₁ fs k => h_1 fs k
    | k.cons₂ => h_2 k
    | Turing.PartrecToTM2.Cont'.comp f k => h_3 f k
    | Turing.PartrecToTM2.Cont'.fix f k => h_4 f k
    | Turing.PartrecToTM2.Cont'.halt => h_5 ()) =
    h_5 ()
-- Mathlib.Algebra.Order.Group.MinMax
max_inv_inv' : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] (a b : α), max a⁻¹ b⁻¹ = (min a b)⁻¹
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The associator for tensor product of R-algebras, as an algebra isomorphism.  -/
Algebra.TensorProduct.assoc : (R : Type uR) →
  (S : Type uS) →
    (T : Type u_2) →
      (A : Type uA) →
        (C : Type uC) →
          (D : Type uD) →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring S] →
                [inst_2 : Algebra R S] →
                  [inst_3 : Semiring A] →
                    [inst_4 : Algebra R A] →
                      [inst_5 : Algebra S A] →
                        [inst_6 : IsScalarTower R S A] →
                          [inst_7 : Semiring C] →
                            [inst_8 : Algebra R C] →
                              [inst_9 : Algebra S C] →
                                [inst_10 : IsScalarTower R S C] →
                                  [inst_11 : Semiring D] →
                                    [inst_12 : Algebra R D] →
                                      [inst_13 : CommSemiring T] →
                                        [inst_14 : Algebra R T] →
                                          [inst_15 : Algebra S T] →
                                            [inst_16 : Algebra T A] →
                                              [inst_17 : IsScalarTower R T A] →
                                                [inst_18 : IsScalarTower S T A] →
                                                  TensorProduct R (TensorProduct S A C) D ≃ₐ[T]
                                                    TensorProduct S A (TensorProduct R C D)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₃.fun_cases_unfolding : ∀ (w x y : UInt8) (motive : Option Char → Prop),
  ((ByteArray.utf8DecodeChar?.isInvalidContinuationByte x || ByteArray.utf8DecodeChar?.isInvalidContinuationByte y) =
        true →
      motive none) →
    (¬(ByteArray.utf8DecodeChar?.isInvalidContinuationByte x || ByteArray.utf8DecodeChar?.isInvalidContinuationByte y) =
            true →
        have r := ByteArray.utf8DecodeChar?.assemble₃Unchecked w x y;
        r < 2048 → motive none) →
      (¬(ByteArray.utf8DecodeChar?.isInvalidContinuationByte x ||
                ByteArray.utf8DecodeChar?.isInvalidContinuationByte y) =
              true →
          have r := ByteArray.utf8DecodeChar?.assemble₃Unchecked w x y;
          ¬r < 2048 → 55296 ≤ r ∧ r ≤ 57343 → motive none) →
        (¬(ByteArray.utf8DecodeChar?.isInvalidContinuationByte x ||
                  ByteArray.utf8DecodeChar?.isInvalidContinuationByte y) =
                true →
            let r := ByteArray.utf8DecodeChar?.assemble₃Unchecked w x y;
            ¬r < 2048 → ∀ (h : ¬(55296 ≤ r ∧ r ≤ 57343)), motive (some { val := r, valid := ⋯ })) →
          motive (ByteArray.utf8DecodeChar?.assemble₃ w x y)
-- Mathlib.Algebra.Ring.Subring.Basic
RingEquiv.ofLeftInverse_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {g : S → R} {f : R →+* S}
  (h : Function.LeftInverse g ⇑f) (x : R), ↑((RingEquiv.ofLeftInverse h) x) = f x
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_zsmul_add' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIocMod hp (m • p + a) b = m • p + toIocMod hp a b
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instFaithfulVAddOfNonempty : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] [Nonempty ι]
  [∀ (i : ι), FaithfulVAdd M (α i)], FaithfulVAdd M ((i : ι) × α i)
-- Mathlib.AlgebraicGeometry.Sites.Small
AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology : ∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : P.IsMultiplicative] [inst_2 : P.RespectsIso]
  [inst_3 : Q.IsStableUnderComposition] [inst_4 : Q.IsStableUnderBaseChange] [inst_5 : Q.HasOfPostcompProperty Q],
  P ≤ Q →
    AlgebraicGeometry.Scheme.smallGrothendieckTopology P S =
      (AlgebraicGeometry.Scheme.smallPretopology P Q).toGrothendieck