mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.comp_continuousOn_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {γ : Type u_3}
  [inst_2 : TopologicalSpace γ] (h : α ≃ᵢ β) {f : γ → α} {s : Set γ}, ContinuousOn (⇑h ∘ f) s ↔ ContinuousOn f s
-- Mathlib.Order.Category.PartOrd
PartOrd.instCoeSortType : CoeSort PartOrd (Type u_1)
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsAddIndecomposable.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddMonoid M] (v : ι → M) (s : Set ι) (i : ι),
  IsAddIndecomposable v s i = (i ∈ s ∧ ∀ j ∈ s, ∀ k ∈ s, v i = v j + v k → v j = 0 ∨ v k = 0)
-- Mathlib.Logic.Function.Basic
/-- Replacing the value of a function at a given point by a given value.  -/
Function.update : {α : Sort u} → {β : α → Sort v} → [DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
-- Mathlib.Algebra.Group.Defs
AddCancelCommMonoid.toAddCancelMonoid : (M : Type u) → [AddCancelCommMonoid M] → AddCancelMonoid M
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
/-- `Equiv.divRight₀` as an order isomorphism.  -/
OrderIso.divRight₀ : {G₀ : Type u_1} →
  [inst : GroupWithZero G₀] → [inst_1 : PartialOrder G₀] → [MulPosReflectLT G₀] → (a : G₀) → 0 < a → G₀ ≃o G₀
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_le_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t → ∀ {fallback : α}, (cmp (t.minD fallback) k).isLE = true
-- Aesop.Rule.Name
Aesop.RuleName.builder : Aesop.RuleName → Aesop.BuilderName
-- Mathlib.Order.CompleteLattice.Defs
lt_iInf_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteSemilatticeInf α] {l : α} {f : ι → α},
  l < iInf f ↔ ∃ b, l < b ∧ ∀ (i : ι), b ≤ f i
-- Mathlib.Data.List.Pairwise
List.pairwise_iff : ∀ {α : Type u} (R : α → α → Prop) (a : List α),
  List.Pairwise R a ↔ a = [] ∨ ∃ a_1 l, (∀ a' ∈ l, R a_1 a') ∧ List.Pairwise R l ∧ a = a_1 :: l
-- Mathlib.Topology.Instances.Rat
NNRat.dist_eq : ∀ (p q : ℚ≥0), dist p q = dist ↑p ↑q
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.coe_toEquiv_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N), ⇑(↑f).symm = ⇑f.symm
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCohomologyRelation.symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} {γ₁ γ₂ : CategoryTheory.PresheafOfGroups.OneCochain G U}
  {α : CategoryTheory.PresheafOfGroups.ZeroCochain G U},
  CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₁ γ₂ α →
    CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₂ γ₁ α⁻¹
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.add_measure : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β} {μa' : MeasureTheory.Measure α} {μb' : MeasureTheory.Measure β},
  MeasureTheory.MeasurePreserving f μa μb →
    MeasureTheory.MeasurePreserving f μa' μb' → MeasureTheory.MeasurePreserving f (μa + μa') (μb + μb')
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheafCoconeOfSpecializes_pt : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C] {y : ↑X}
  (h : p₀ ⤳ y), (skyscraperPresheafCoconeOfSpecializes p₀ A h).pt = A
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkMatch : Lean.Syntax →
  Lean.Syntax →
    Lean.Syntax →
      Lean.Syntax →
        Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.CodeBlock) → Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.toUniversallyClosed : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsProper f],
  AlgebraicGeometry.UniversallyClosed f
-- Mathlib.Data.Finset.NAry
Finset.image₂_subset_iff_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {u : Finset γ}, Finset.image₂ f s t ⊆ u ↔ ∀ b ∈ t, Finset.image (fun a => f a b) s ⊆ u
-- Aesop.Nanos
Aesop.instOrdNanos : Ord Aesop.Nanos
-- Mathlib.Data.Set.Basic
Set.union_eq_left : ∀ {α : Type u} {s t : Set α}, s ∪ t = s ↔ t ⊆ s
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
tendsto_iff_forall_eval_tendsto_topDualPairing : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : ContinuousAdd 𝕜] [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E]
  [inst_6 : TopologicalSpace E] {l : Filter α} {f : α → WeakDual 𝕜 E} {x : WeakDual 𝕜 E},
  Filter.Tendsto f l (nhds x) ↔
    ∀ (y : E), Filter.Tendsto (fun i => ((topDualPairing 𝕜 E) (f i)) y) l (nhds (((topDualPairing 𝕜 E) x) y))
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.prime_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q : M}, Associated p q → (Prime p ↔ Prime q)
-- Mathlib.CategoryTheory.Limits.FullSubcategory
CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_of_preservesColimitsOfShape_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (J : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.HasColimitsOfShape J P.FullSubcategory]
  [P.IsClosedUnderIsomorphisms] [CategoryTheory.Limits.PreservesColimitsOfShape J P.ι], P.IsClosedUnderColimitsOfShape J
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
mul_inv_lt_inv_mul_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c d : α} [MulRightStrictMono α],
  a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b
-- Mathlib.CategoryTheory.Action.Basic
Action.instCategory : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → CategoryTheory.Category.{v_1, max (max u_2 u_1) v_1} (Action V G)
-- Init.Data.List.Nat.TakeDrop
/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
length `> i`. Version designed to rewrite from the small list to the big list.  -/
List.getElem_take : ∀ {α : Type u_1} {xs : List α} {j i : ℕ} {h : i < (List.take j xs).length}, (List.take j xs)[i] = xs[i]
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- A metric space has the Besicovitch covering property if there exist `N` and `τ > 1` such that
there are no satellite configurations of parameter `τ` with `N+1` points. This is the condition that
guarantees that the measurable Besicovitch covering theorem holds. It is satisfied by
finite-dimensional real vector spaces.  -/
HasBesicovitchCovering : (α : Type u_1) → [MetricSpace α] → Prop
-- Init.Data.List.Zip
_private.Init.Data.List.Zip.0.List.getElem?_zipWith.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (x : Option α) (x_1 : Option β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_2 : Option β) → motive x x_2),
  (∀ (a : α) (b : β), x = some a → x_1 = some b → False) →
    (match x, x_1 with
      | some a, some b => h_1 a b
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.smtSDiv_smtUDiv : ∀ {w : ℕ} (x y : BitVec w),
  x.smtSDiv y =
    bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then (-x).smtUDiv (-y) else -(-x).smtUDiv y
    else bif y.getLsbD (w - 1) then -x.smtUDiv (-y) else x.smtUDiv y
-- Aesop.Search.ExpandSafePrefix
Aesop.SafeExpansionM.State.mk.sizeOf_spec : ∀ (numRapps : ℕ), sizeOf { numRapps := numRapps } = 1 + sizeOf numRapps
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.eraseSimproc.sizeOf_spec : ∀ (toErase : Lean.Name), sizeOf (Lean.Elab.Tactic.ElabSimpArgResult.eraseSimproc toErase) = 1 + sizeOf toErase
-- Init.Tactics
/-- Theorems tagged with the `wf_preprocess` attribute are used during the processing of functions defined
by well-founded recursion. They are applied to the function's body to add additional hypotheses,
such as replacing `if c then _ else _` with `if h : c then _ else _` or `xs.map` with
`xs.attach.map`. Also see `wfParam`.

Warning: These rewrites are only applied to the declaration for the purpose of the logical
definition, but do not affect the compiled code. In particular they can cause a function definition
that diverges as compiled to be accepted without an explicit `partial` keyword, for example if they
remove irrelevant subterms or change the evaluation order by hiding terms under binders. Therefore
avoid tagging theorems with `[wf_preprocess]` unless they preserve also operational behavior.
 -/
Lean.Parser.Attr.wf_preprocess : Lean.ParserDescr
-- Mathlib.Order.Filter.Germ.Basic
/-- **Alias** of `Filter.Tendsto.congr_germ`. -/
Filter.Germ.Filter.Tendsto.congr_germ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f g : β → γ} {l : Filter α} {l' : Filter β},
  f =ᶠ[l'] g → ∀ {φ : α → β}, Filter.Tendsto φ l l' → ↑(f ∘ φ) = ↑(g ∘ φ)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.liftAux_tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  (φ : MultilinearMap R s E) (f : (i : ι) → s i), (PiTensorProduct.liftAux φ) ((PiTensorProduct.tprod R) f) = φ f
-- Mathlib.Data.Finset.Lattice.Prod
/-- See also `Finset.prodMk_sup'_sup'`.  -/
Finset.sup'_prodMap : ∀ {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  {s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β),
  (s ×ˢ t).sup' hst (Prod.map f g) = (s.sup' ⋯ f, t.sup' ⋯ g)
-- Mathlib.RingTheory.Finiteness.Small
Subalgebra.FG.small : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [Small.{u, u_1} R] {A : Subalgebra R S}, A.FG → Small.{u, u_2} ↥A
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- A permutation `c` is a cycle of `g` iff `k * c * k⁻¹` is a cycle of `k * g * k⁻¹`  -/
Equiv.Perm.mem_cycleFactorsFinset_conj : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (g k c : Equiv.Perm α),
  k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {F' : Type u_4}
  [inst_5 : NormedAddCommGroup F'] [inst_6 : NormedSpace 𝕜 F'] {H₁ : Type u_5} [inst_7 : TopologicalSpace H₁]
  {H₂ : Type u_6} [inst_8 : TopologicalSpace H₂] {H₃ : Type u_7} [inst_9 : TopologicalSpace H₃]
  {I : ModelWithCorners 𝕜 E H₁} {J : ModelWithCorners 𝕜 F H₂} (K : ModelWithCorners 𝕜 F' H₃) {M : Type u_8}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H₁ M] {N : Type u_9} [inst_12 : TopologicalSpace N]
  [inst_13 : ChartedSpace H₂ N] (P : Type u_10) [inst_14 : TopologicalSpace P] [inst_15 : ChartedSpace H₃ P]
  {n : WithTop ℕ∞} {f : M → N} {x : M},
  IsLocalDiffeomorphAt I J n f x →
    ∀ {g : N → P}, IsLocalDiffeomorphAt J K n g (f x) → IsLocalDiffeomorphAt I K n (g ∘ f) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit_empty_list_le : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {l : List α},
  (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)).size ≤ l.length
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.Braided.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {D : Type u₂} {inst_3 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_4 : CategoryTheory.MonoidalCategory D} {inst_5 : CategoryTheory.BraidedCategory D}
  {F : CategoryTheory.Functor C D} {x y : F.Braided},
  CategoryTheory.Functor.LaxMonoidal.ε F = CategoryTheory.Functor.LaxMonoidal.ε F →
    CategoryTheory.Functor.LaxMonoidal.μ F = CategoryTheory.Functor.LaxMonoidal.μ F →
      CategoryTheory.Functor.OplaxMonoidal.η F = CategoryTheory.Functor.OplaxMonoidal.η F →
        CategoryTheory.Functor.OplaxMonoidal.δ F = CategoryTheory.Functor.OplaxMonoidal.δ F → x = y
-- Mathlib.Algebra.Star.StarRingHom
/-- Any type satisfying `StarRingEquivClass` can be cast into `StarRingEquiv` via
`StarRingEquivClass.toStarRingEquiv`.  -/
StarRingEquivClass.instCoeHead : {F : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Add A] →
        [inst_1 : Mul A] →
          [inst_2 : Star A] →
            [inst_3 : Add B] →
              [inst_4 : Mul B] →
                [inst_5 : Star B] → [inst_6 : EquivLike F A B] → [StarRingEquivClass F A B] → CoeHead F (A ≃⋆+* B)
-- Mathlib.GroupTheory.Congruence.Defs
Con.instZPow.eq_1 : ∀ {M : Type u_1} [inst : Group M] (c : Con M), c.instZPow = { pow := fun x z => Quotient.map' (fun x => x ^ z) ⋯ x }
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.nextn.match_1.splitter : (motive : Substring.Raw → ℕ → String.Pos.Raw → Sort u_1) →
  (x : Substring.Raw) →
    (x_1 : ℕ) →
      (x_2 : String.Pos.Raw) →
        ((x : Substring.Raw) → (p : String.Pos.Raw) → motive x 0 p) →
          ((ss : Substring.Raw) → (i : ℕ) → (p : String.Pos.Raw) → motive ss i.succ p) → motive x x_1 x_2
-- Mathlib.Order.Filter.Ultrafilter.Defs
Filter.forall_neBot_le_iff : ∀ {α : Type u} {g : Filter α} {p : Filter α → Prop},
  Monotone p → ((∀ (f : Filter α), f.NeBot → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f)
-- Mathlib.RepresentationTheory.Basic
Representation.isTrivial_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) [ρ.IsTrivial] (g : G) (x : V), (ρ g) x = x
-- Aesop.Search.Main
Aesop.finalizeProof : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q Unit
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearMap.compAlternatingMap_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {N₂ : Type u_11} [inst_5 : AddCommMonoid N₂]
  [inst_6 : Module R N₂] (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) (m : ι → M), (g.compAlternatingMap f) m = g (f m)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The "first projection" of a CatCommSqOver as a functor.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.fstFunctor : {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 : Type u₄) →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    CategoryTheory.Functor (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
                      (CategoryTheory.Functor X A)
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_apply' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.Kernel α β) (a : α) {s : Set γ},
  MeasurableSet s → ((η.comp κ) a) s = ∫⁻ (b : β), (η b) s ∂κ a
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.orbit.coe_vadd : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G}
  {x : AddAction.orbitRel.Quotient G α} {a : ↑x.orbit}, ↑(g +ᵥ a) = g +ᵥ ↑a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- Given a vertex in the support of a path, give the path up until (and including) that vertex.  -/
SimpleGraph.Walk.takeUntil : {V : Type u} →
  {G : SimpleGraph V} → [DecidableEq V] → {v w : V} → (p : G.Walk v w) → (u : V) → u ∈ p.support → G.Walk v u
-- Mathlib.Data.ENNReal.BigOperators
/-- A sum is infinite iff one of the summands is infinite.  -/
ENNReal.sum_eq_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal}, ∑ x ∈ s, f x = ⊤ ↔ ∃ a ∈ s, f a = ⊤
-- Init.Data.List.Basic
List.mapTR.loop.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (a : List β), List.mapTR.loop f [] a = a.reverse
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.forM.eq_1 : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] (range : Std.Legacy.Range) (f : ℕ → m PUnit.{u_1 + 1}),
  range.forM f = Std.Legacy.Range.forM.loop✝ range f range.start
-- Mathlib.Order.UpperLower.Closure
IsUpperSet.disjoint_lowerClosure_left : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, IsUpperSet t → (Disjoint (↑(lowerClosure s)) t ↔ Disjoint s t)
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {F : CategoryTheory.Functor J C} →
            {c : CategoryTheory.Limits.Cocone F} →
              {X Y : C} →
                {p : X ⟶ Y} →
                  {f : F.obj ⊥ ⟶ X} →
                    {g : c.pt ⟶ Y} →
                      {j : J} →
                        (f' : F.obj j ⟶ X) →
                          autoParam (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) f' = f)
                              CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁._autoParam →
                            autoParam
                                (CategoryTheory.CategoryStruct.comp f' p =
                                  CategoryTheory.CategoryStruct.comp (c.ι.app j) g)
                                CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂._autoParam →
                              CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.sheafComposeNatTrans.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B)
  {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)}
  (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A)
  {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)}
  (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [inst_3 : J.HasSheafCompose F],
  CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂ =
    {
      app := fun P =>
        (adj₂.homEquiv (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).obj P)
              ((G₁.comp (CategoryTheory.sheafCompose J F)).obj P)).symm
          (CategoryTheory.Functor.whiskerRight (adj₁.unit.app P) F),
      naturality := ⋯ }
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Seq.erase0.match_1.eq_1 : ∀ (motive : Lean.Grind.AC.Seq → Sort u_1) (x : Lean.Grind.AC.Var)
  (h_1 : (x : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x))
  (h_2 : (x : Lean.Grind.AC.Var) → (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x s)),
  (match Lean.Grind.AC.Seq.var x with
    | Lean.Grind.AC.Seq.var x => h_1 x
    | Lean.Grind.AC.Seq.cons x s => h_2 x s) =
    h_1 x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
CategoryTheory.ShortComplex.ShortExact.comp_extClass_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {Y : C} {n : ℕ}
  (γ : CategoryTheory.Abelian.Ext S.X₁ Y n) {n' : ℕ} (h : 1 + n = n'),
  (CategoryTheory.Abelian.Ext.mk₀ S.g).comp (hS.extClass.comp γ h) ⋯ = 0
-- Lean.Elab.Do.PatternVar
Lean.Elab.Do.getPatternsVarsEx : Array Lean.Term → Lean.Elab.TermElabM (Array Lean.Ident)
-- Mathlib.Topology.Instances.PNat
PNat.instProperSpace : ProperSpace ℕ+
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LiftSourceTargetPropertyAt.congr_iff : ∀ {H : Type u_6} {G : Type u_8} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace G] {M : Type u_10}
  {N : Type u_12} [inst_2 : TopologicalSpace M] [inst_3 : TopologicalSpace N]
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop},
  Manifold.IsLocalSourceTargetProperty P →
    ∀ {f g : M → N} {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G},
      Set.EqOn f g φ.source → (P f φ ψ ↔ P g φ ψ)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback fallback' : α}, t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.comp_map : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {γ : Type x} {f : α → β} {g : β → γ}
  {x : Std.Iterators.HetT m α}, Std.Iterators.HetT.map (g ∘ f) x = Std.Iterators.HetT.map g (Std.Iterators.HetT.map f x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₂ → (t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instSMulCommClass : ∀ {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M}
  [inst_1 : OreLocalization.OreSet S] [inst_2 : MulAction M X] [inst_3 : SMul R X] [inst_4 : SMul R M]
  [inst_5 : IsScalarTower R M M] [inst_6 : IsScalarTower R M X] [inst_7 : SMul R' X] [inst_8 : SMul R' M]
  [inst_9 : IsScalarTower R' M M] [inst_10 : IsScalarTower R' M X] [SMulCommClass R R' M],
  SMulCommClass R R' (OreLocalization S X)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.equiv_symm_apply : ∀ {R : Type u_1} {A : Type u_2} (toProd : R × A), Unitization.equiv.symm toProd = Unitization.mk toProd
-- Mathlib.LinearAlgebra.Matrix.Basis
/-- A generalization of `LinearMap.toMatrix_id`.  -/
LinearMap.toMatrix_id_eq_basis_toMatrix : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (b' : Module.Basis ι' R M) [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι] [inst_5 : Finite ι'], (LinearMap.toMatrix b b') LinearMap.id = b'.toMatrix ⇑b
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- The pullback of `(𝟙 X, f)` and `(𝟙 X, g)`  -/
_private.Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers.0.CategoryTheory.NormalMonoCategory.P : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteProducts C] →
        [CategoryTheory.Limits.HasKernels C] →
          [CategoryTheory.IsNormalMonoCategory C] →
            {X Y : C} →
              (f g : X ⟶ Y) →
                [CategoryTheory.Mono (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) f)] →
                  [CategoryTheory.Mono (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) g)] → C