mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- The map from `ι` to objects in `C`  -/
CategoryTheory.Mat_.X : {C : Type u₁} → (self : CategoryTheory.Mat_ C) → self.ι → C
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.WeaklyRegular.innerRegular : ∀ {α : Type u_1} {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α}
  [self : μ.WeaklyRegular], μ.InnerRegularWRT IsClosed IsOpen
-- Mathlib.Data.Fintype.EquivFin
/-- If `s : Set α` is a proper subset of `α` and `f : s → α` is surjective, then `α` is infinite.  -/
Infinite.of_surjective_from_set : ∀ {α : Type u_1} {s : Set α}, s ≠ Set.univ → ∀ {f : ↑s → α}, Function.Surjective f → Infinite α
-- Batteries.Control.AlternativeMonad
/-- `map` commutes with `orElse`. The stronger statement with `bind` generally isn't true  -/
LawfulAlternative.map_orElse : ∀ {m : Type u_1 → Type u_2} {inst : Alternative m} [self : LawfulAlternative m] {α β : Type u_1} (x y : m α)
  (f : α → β), f <$> (x <|> y) = (f <$> x <|> f <$> y)
-- Mathlib.Algebra.Order.Star.Basic
star_mul_self_pos : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [Nontrivial R] {x : R}, IsRegular x → 0 < star x * x
-- Mathlib.RingTheory.Ideal.Maps
/-- `Module.annihilator R M` is the ideal of all elements `r : R` such that `r • M = 0`.  -/
Module.annihilator : (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Ideal R
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.toList_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp},
  (Std.DTreeMap.Const.toArray t).toList = Std.DTreeMap.Const.toList t
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkImpCached_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (idx : ℕ) (aig : Std.Sat.AIG α) (input : aig.BinaryInput)
  {h : idx < aig.decls.size} {h2 : idx < (aig.mkImpCached input).aig.decls.size},
  (aig.mkImpCached input).aig.decls[idx] = aig.decls[idx]
-- Init.Data.Rat.Lemmas
Rat.sub_add_cancel : ∀ {a b : ℚ}, a - b + b = a
-- Mathlib.Tactic.GCongr.ForwardAttr
/-- Environment extensions for `gcongrForward` declarations  -/
Mathlib.Tactic.GCongr.forwardExt : Lean.PersistentEnvExtension Lean.Name (Lean.Name × Mathlib.Tactic.GCongr.ForwardExt)
  (List Lean.Name × List (Lean.Name × Mathlib.Tactic.GCongr.ForwardExt))
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_congr' : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β},
  f₁ =ᶠ[l₁] f₂ → (Filter.Tendsto f₁ l₁ l₂ ↔ Filter.Tendsto f₂ l₁ l₂)
-- Lean.Hygiene
_private.Lean.Hygiene.0.Lean.mkInaccessibleUserNameAux : Bool → Lean.Name → ℕ → Lean.Name
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.extendScalarsOfSurjective_apply : ∀ {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A ≃ₐ[R] B),
  (AlgEquiv.extendScalarsOfSurjective h) f = { toEquiv := ↑f, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
thickening_thickening : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 < ε → 0 < δ → ∀ (s : Set E), Metric.thickening ε (Metric.thickening δ s) = Metric.thickening (ε + δ) s
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_nonUnitalSubalgebra : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (s : Set A),
  Algebra.adjoin R ↑(NonUnitalAlgebra.adjoin R s) = Algebra.adjoin R s
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.cancel_right : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] {g₁ g₂ f : CentroidHom α},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Algebra.Group.Units.Defs
/-- For `a, b` in a Dedekind-finite monoid such that `a * b = 1`, makes a unit out of `a`.  -/
Units.mkOfMulEqOne : {α : Type u} → [inst : Monoid α] → [IsDedekindFiniteMonoid α] → (a b : α) → a * b = 1 → αˣ
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.invFun_eq_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {f : M ≃* N}, f.invFun = ⇑f.symm
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.forget_reflects_isos : ∀ {R : Type u} [inst : CommRing R], (CategoryTheory.forget (CoalgCat R)).ReflectsIsomorphisms
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncFinset_apply : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)} (p : MvPowerSeries σ R),
  (MvPowerSeries.truncFinset R s) p = ∑ x ∈ s, (MvPolynomial.monomial x) ((MvPowerSeries.coeff x) p)
-- Mathlib.AlgebraicGeometry.Restrict
/-- Open subset of a scheme as a scheme.  -/
AlgebraicGeometry.Scheme.Opens.toScheme : {X : AlgebraicGeometry.Scheme} → X.Opens → AlgebraicGeometry.Scheme
-- Mathlib.Topology.Algebra.MulAction
instContinuousSMulForall : ∀ {M : Type u_1} [inst : TopologicalSpace M] {ι : Type u_5} {γ : ι → Type u_6}
  [inst_1 : (i : ι) → TopologicalSpace (γ i)] [inst_2 : (i : ι) → SMul M (γ i)] [∀ (i : ι), ContinuousSMul M (γ i)],
  ContinuousSMul M ((i : ι) → γ i)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fundamentalDomain_ae_parallelepiped : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [inst_2 : Fintype ι] [inst_3 : MeasurableSpace E] (μ : MeasureTheory.Measure E) [BorelSpace E] [μ.IsAddHaarMeasure],
  ZSpan.fundamentalDomain b =ᵐ[μ] parallelepiped ⇑b
-- Mathlib.CategoryTheory.Comma.Basic
/-- The functor `Comma L R ⥤ Comma L' R'` induced by three functors `F₁`, `F₂`, `F`
and two natural transformations `F₁ ⋙ L' ⟶ L ⋙ F` and `R ⋙ F ⟶ F₂ ⋙ R'`.  -/
CategoryTheory.Comma.map : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {A' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                {B' : Type u₅} →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                    {T' : Type u₆} →
                      [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] →
                        {L : CategoryTheory.Functor A T} →
                          {R : CategoryTheory.Functor B T} →
                            {L' : CategoryTheory.Functor A' T'} →
                              {R' : CategoryTheory.Functor B' T'} →
                                {F₁ : CategoryTheory.Functor A A'} →
                                  {F₂ : CategoryTheory.Functor B B'} →
                                    {F : CategoryTheory.Functor T T'} →
                                      (F₁.comp L' ⟶ L.comp F) →
                                        (R.comp F ⟶ F₂.comp R') →
                                          CategoryTheory.Functor (CategoryTheory.Comma L R) (CategoryTheory.Comma L' R')
-- Mathlib.Order.Filter.Prod
Filter.tendsto_fst : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, Filter.Tendsto Prod.fst (f ×ˢ g) f
-- Mathlib.CategoryTheory.Limits.Creates
/-- `liftColimit t` is the cocone for `K` given by lifting the colimit `t` for `K ⋙ F`.  -/
CategoryTheory.liftColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [CategoryTheory.CreatesColimit K F] →
                  {c : CategoryTheory.Limits.Cocone (K.comp F)} →
                    CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.Cocone K
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
/-- `CliffordAlgebra.reverse` as a `LinearEquiv`.  -/
CliffordAlgebra.reverseEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {Q : QuadraticForm R M} → CliffordAlgebra Q ≃ₗ[R] CliffordAlgebra Q
-- Mathlib.Order.RelIso.Basic
/-- A relation isomorphism is an equivalence that is also a relation embedding.  -/
RelIso : {α : Type u_5} → {β : Type u_6} → (α → α → Prop) → (β → β → Prop) → Type (max u_5 u_6)
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_eq_zero_iff_addCommute : ∀ {G : Type u_1} [inst : AddGroup G] {g₁ g₂ : G}, ⁅g₁, g₂⁆ = 0 ↔ AddCommute g₁ g₂
-- Mathlib.LinearAlgebra.Transvection.Generation
LinearEquiv.finrank_fixedSubmodule_dilatransvection_mul_le : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] (e f : V ≃ₗ[K] V),
  f ∈ LinearEquiv.dilatransvections K V →
    Module.finrank K ↥(↑(f * e)).fixedSubmodule ≤ 1 + Module.finrank K ↥(↑e).fixedSubmodule
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.MemLp.of_nnnorm_le_mul : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : α → E} {g : α → F} {c : NNReal},
  MeasureTheory.MemLp g p μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) → MeasureTheory.MemLp f p μ
-- Mathlib.Algebra.Group.Basic
IsRightCancelAdd.toGrindAddRightCancel : ∀ (α : Type u_5) [inst : AddSemigroup α] [IsRightCancelAdd α], Lean.Grind.AddRightCancel α
-- Mathlib.Data.Set.Operations
Set.mem_ofPred : ∀ {α : Type u} {a : α} {p : α → Prop}, a ∈ {x | p x} ↔ p a
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instT0SpaceOfT1Space : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T1Space α], T0Space (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Data.Fin.SuccPred
Fin.castAdd_inj : ∀ {n m : ℕ} {a b : Fin m}, Fin.castAdd n a = Fin.castAdd n b ↔ a = b
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_toVal : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x : R), (WithVal.toVal v x).ofVal = x
-- Mathlib.GroupTheory.OreLocalization.Cardinality
AddOreLocalization.numeratorHom_surjective_of_finite : ∀ {R : Type u} [inst : AddMonoid R] (S : AddSubmonoid R) [inst_1 : AddOreLocalization.AddOreSet S] [Finite ↥S],
  Function.Surjective ⇑AddOreLocalization.numeratorHom
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_eq_C : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {p : ℕ},
  0 < p → ∀ {f : MvPolynomial σ R} {r : R}, (MvPolynomial.expand p) f = MvPolynomial.C r ↔ f = MvPolynomial.C r
-- Mathlib.Topology.Compactness.Lindelof
eq_closed_inter_countable : ∀ {X : Type u} [inst : TopologicalSpace X] [HereditarilyLindelofSpace X] {ι : Type u_2} (C : ι → Set X),
  (∀ (i : ι), IsClosed (C i)) → ∃ t, t.Countable ∧ ⋂ i ∈ t, C i = ⋂ i, C i
-- Mathlib.Data.Nat.Find
Nat.findGreatest_spec : ∀ {m : ℕ} {P : ℕ → Prop} [inst : DecidablePred P] {n : ℕ}, m ≤ n → P m → P (Nat.findGreatest P n)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` creates colimits, then `F : C ⥤ Dᵒᵖ` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) → [CategoryTheory.CreatesColimits F.leftOp] → CategoryTheory.CreatesLimits F
-- Mathlib.RingTheory.Ideal.Maps
/-- A non-computable version of `RingHom.liftOfRightInverse` for when no computable right
inverse is available, that uses `Function.surjInv`.  -/
RingHom.liftOfSurjective : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : Ring A] →
        [inst_1 : Ring B] →
          [inst_2 : Ring C] →
            (f : A →+* B) → Function.Surjective ⇑f → { g // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C)
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.isoModSerre.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P P_1 : CategoryTheory.ObjectProperty C) (e_P : P = P_1) [inst_2 : P.IsSerreClass] ⦃X Y : C⦄ (x x_1 : X ⟶ Y),
  x = x_1 → P.isoModSerre x = P_1.isoModSerre x_1
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- The graph isomorphism from a graph `G` that `IsCompleteMultipartite` to the corresponding
`completeMultipartiteGraph` (see also `isCompleteMultipartite_iff`)  -/
SimpleGraph.IsCompleteMultipartite.iso : {α : Type u} →
  {G : SimpleGraph α} →
    (h : G.IsCompleteMultipartite) → G ≃g SimpleGraph.completeMultipartiteGraph fun c => { x // h.setoid c.out x }
-- Lean.Language.Basic
Lean.Language.SyntaxGuarded.mk.inj : ∀ {α : Type} {stx : Lean.Syntax} {val : α} {stx_1 : Lean.Syntax} {val_1 : α},
  { stx := stx, val := val } = { stx := stx_1, val := val_1 } → stx = stx_1 ∧ val = val_1
-- Init.Data.SInt.Bitwise
UInt8.toInt8_and : ∀ (a b : UInt8), (a &&& b).toInt8 = a.toInt8 &&& b.toInt8
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_eq_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set β} {a : α}, a +ᵥ s = ∅ ↔ s = ∅
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.DenseMatrix.mk : {n m : ℕ} → Array (Array ℚ) → Mathlib.Tactic.Linarith.SimplexAlgorithm.DenseMatrix n m
-- Init.Data.UInt.BasicAux
UInt32.ofNatLT_lt_of_lt : ∀ {n m : ℕ} (h1 : n < UInt32.size), m < UInt32.size → n < m → UInt32.ofNatLT n h1 < UInt32.ofNat m
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C)
  (X_1 : CategoryTheory.Discrete PUnit.{u + 1}),
  ((CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso C).hom.app X).hom.hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.withInductiveLocalDecls.match_4.splitter : (motive : Option (Lean.Expr × Subarray Lean.Expr) → Sort u_1) →
  (x : Option (Lean.Expr × Subarray Lean.Expr)) →
    (Unit → motive none) →
      ((origParam : Lean.Expr) → (s' : Subarray Lean.Expr) → motive (some (origParam, s'))) → motive x
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Equivalence.pi_functor : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i),
  (CategoryTheory.Equivalence.pi E).functor = CategoryTheory.Functor.pi fun i => (E i).functor
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_empty : ∀ {α : Type u_1} (M : Matroid α), M.eRk ∅ = 0
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Spec.map_residueFieldIso_inv_eq_fromSpecResidueField : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Spec.residueFieldIso R x).inv)
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField))) =
    (AlgebraicGeometry.Spec R).fromSpecResidueField x
-- Lean.DocString.Types
Lean.Doc.Inline.brecOn_2.eq : ∀ {i : Type u} {motive_1 : Lean.Doc.Inline i → Sort u_1} {motive_2 : Array (Lean.Doc.Inline i) → Sort u_1}
  {motive_3 : List (Lean.Doc.Inline i) → Sort u_1} (t : List (Lean.Doc.Inline i))
  (F_1 : (t : Lean.Doc.Inline i) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_2 t → motive_3 t),
  Lean.Doc.Inline.brecOn_2 t F_1 F_2 F_3 = F_3 t (Lean.Doc.Inline.brecOn_2.go t F_1 F_2 F_3).2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_toReal_neg : ∀ (θ : Real.Angle), |(-θ).toReal| = |θ.toReal|
-- Mathlib.Order.KrullDimension
Order.coheight_eq_coe_add_one_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
  Order.coheight x = ↑n + 1 ↔ Order.coheight x < ⊤ ∧ (∃ y > x, Order.coheight y = ↑n) ∧ ∀ y > x, Order.coheight y ≤ ↑n
-- Mathlib.CategoryTheory.HomCongr
/-- If `Y₁` is isomorphic to `Y₂`, then there is a bijection between `X ≅ Y₁` and `X ≅ Y₂`.  -/
CategoryTheory.Iso.isoCongrRight : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y₁ Y₂ : C} → (Y₁ ≅ Y₂) → (X ≅ Y₁) ≃ (X ≅ Y₂)
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_jointly_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'}
  [inst_3 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_4 : CategoryTheory.ConcreteCategory A FC]
  {P : CategoryTheory.Functor Cᵒᵖ A}
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)]
  [CategoryTheory.LocallySmall.{w, v, u} C] (p : CategoryTheory.ToType (Φ.presheafFiber.obj P)),
  ∃ X x z, (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z = p
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.spineToSimplex_interval : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path n) (j l : ℕ) (hjl : j + l ≤ n),
  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.subinterval j l hjl).op)) (sx.spineToSimplex f) =
    sx.spineToSimplex (f.interval j l hjl)
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- An upper-block-triangular matrix is invertible if its diagonal is.  -/
Matrix.fromBlocksZero₂₁Invertible : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (B : Matrix m n α) →
                    (D : Matrix n n α) → [Invertible A] → [Invertible D] → Invertible (Matrix.fromBlocks A B 0 D)
-- Lean.Elab.Tactic.Induction
/-- Return `true` if the first LHS of the given alternative contains `@`.  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.altHasExplicitModifier : Lean.Syntax → Bool
-- Init.Data.Rat.Basic
/-- Form the quotient `n / d` where `n d : Int`.  -/
Rat.divInt : ℤ → ℤ → ℚ
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- Extensionality lemma in terms of `UpperHalfPlane.re` and `UpperHalfPlane.im`.  -/
UpperHalfPlane.ext_re_im : ∀ {a b : UpperHalfPlane}, a.re = b.re → a.im = b.im → a = b
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instBEqOrigin : BEq Mathlib.Meta.FunProp.Origin
-- Std.Http.Internal.Encode
/-- Serializes a type `t` to a `ChunkedBuffer` containing its canonical HTTP representation for protocol
version `v`.
 -/
Std.Http.Internal.Encode : Std.Http.Version → Type → Type
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
/-- Gets the orthogonal direction of one vector relative to another.  -/
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.ortho : {V : Type u_1} → [inst : NormedAddCommGroup V] → [InnerProductSpace ℝ V] → V → V → V
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.isGLB_of_u_image : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : Preorder β] (gi : GaloisInsertion l u)
  {s : Set β} {a : α}, IsGLB (u '' s) a → IsGLB s (l a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.φ_three : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R),
  W.φ 3 = Polynomial.C Polynomial.X * Polynomial.C W.Ψ₃ ^ 2 - Polynomial.C W.preΨ₄ * W.ψ₂ ^ 2
-- Init.MetaTypes
/-- Do not unfold anything.  -/
Lean.Meta.TransparencyMode.none : Lean.Meta.TransparencyMode
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- Given a family of morphisms `f : X i ⟶ S`, and `M : F.obj (.mk (op S))`,
this is the object in `F.DescentData f` that is obtained by pulling back `M`
over the `X i`.  -/
CategoryTheory.Pseudofunctor.DescentData.ofObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} → {X : ι → C} → {f : (i : ι) → X i ⟶ S} → ↑(F.obj { as := Opposite.op S }) → F.DescentData f
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.inf_le_right : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : SemilatticeInf β] [inst_3 : ContinuousInf β] (f g : α →ₘ[μ] β), f ⊓ g ≤ g
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instDiv : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → Div (LowerSet α)
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.dense_preimage_mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G}
  {s : Set (G ⧸ N)}, Dense (QuotientAddGroup.mk ⁻¹' s) ↔ Dense s
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.ι_jointly_surjective : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J]
  [inst_4 : Small.{u, w} J] (x : ↥(CategoryTheory.Limits.colimit F)),
  ∃ i xi, (CategoryTheory.Limits.colimit.ι F i) xi = x
-- Init.Data.String.PosRaw
String.Pos.Raw.add_char_eq : ∀ (p : String.Pos.Raw) (c : Char), p + c = { byteIdx := p.byteIdx + c.utf8Size }
-- Std.Http.Data.URI.Basic
/-- Removes all occurrences of a query parameter by key name.
 -/
Std.Http.URI.Query.eraseEncoded : Std.Http.URI.Query → Std.Http.URI.EncodedQueryParam → Std.Http.URI.Query
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- Boundaryless manifolds have empty boundary.  -/
ModelWithCorners.Boundaryless.boundary_eq_empty : ∀ {𝕜 : 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] [BoundarylessManifold I M], ModelWithCorners.boundary M = ∅
-- Mathlib.RingTheory.Localization.Pi
/-- Let `M` be a submonoid of a direct product of commutative rings `R i`, and let `M' i` denote
the projection of `M` onto each factor. Then the canonical map from the localization of the direct
product `Π i, R i` at `M` to the direct product of the localizations of each `R i` at `M' i`
is bijective.  -/
IsLocalization.bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom : ∀ {ι : Type u_1} (R : ι → Type u_2) (S : ι → Type u_3) [inst : (i : ι) → CommSemiring (R i)]
  [inst_1 : (i : ι) → CommSemiring (S i)] [inst_2 : (i : ι) → Algebra (R i) (S i)] (S' : Type u_4)
  [inst_3 : CommSemiring S'] [inst_4 : Algebra ((i : ι) → R i) S'] (M : Submonoid ((i : ι) → R i))
  [inst_5 : ∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)] [inst_6 : IsLocalization M S']
  [Finite ι], Function.Bijective ⇑(IsLocalization.lift ⋯)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α}, t.contains k = true → t.getKey? k = some k
-- Init.Data.Vector.Lemmas
Vector.getElem?_replace_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a b : α} {xs : Vector α n} {i : ℕ},
  xs[i]? ≠ some a → (xs.replace a b)[i]? = xs[i]?