mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.cancel_left : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {g : M₂ →SL[σ₂₃] M₃} {f₁ f₂ : M₁ →SL[σ₁₂] M₂},
  Function.Injective ⇑g → g ∘SL f₁ = g ∘SL f₂ → f₁ = f₂
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.contains a = false → m[a]? = none
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.rfind : ∀ {n : ℕ} {f : List.Vector ℕ (n + 1) → ℕ},
  Nat.Partrec' ↑f → Nat.Partrec' fun v => Nat.rfind fun n_1 => Part.some (decide (f (n_1 ::ᵥ v) = 0))
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.toHom_comp_symm_toHom : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G'),
  f.toHom.comp f.symm.toHom = SimpleGraph.Hom.id
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mkPiAlgebra_apply : ∀ {R : Type uR} {ι : Type uι} [inst : CommSemiring R] {A : Type u_1} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : Fintype ι] (m : ι → A), (MultilinearMap.mkPiAlgebra R ι A) m = ∏ i, m i
-- Mathlib.Geometry.Manifold.IsManifold.Basic
modelWithCornersSelf_coe_symm : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], ↑(modelWithCornersSelf 𝕜 E).symm = id
-- Lean.Parser.Do
Lean.Parser.Term.doRepeat.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Batteries.Data.Char.Basic
Char.maxSurrogate.eq_1 : Char.maxSurrogate = 57343
-- Init.Meta.Defs
/-- Extracts the items from a tactic configuration,
either a `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`, or these wrapped in null nodes.

New metaprograms should use `Lean.Elab.ConfigEval.foldConfigM` instead.
 -/
Lean.Parser.Tactic.getConfigItems : Lean.Syntax → Lean.TSyntaxArray `Lean.Parser.Tactic.configItem
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalars_comp : ∀ {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} {P : Type u_18} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M]
  [inst_5 : Module R N] [inst_6 : Module S M] [inst_7 : Module S N] [inst_8 : LinearMap.CompatibleSMul M N R S]
  [inst_9 : AddCommMonoid P] [inst_10 : Module S P] [inst_11 : Module R P] [inst_12 : LinearMap.CompatibleSMul N P R S]
  [inst_13 : LinearMap.CompatibleSMul M P R S] (f : N →ₗ[S] P) (g : M →ₗ[S] N), ↑R (f ∘ₗ g) = ↑R f ∘ₗ ↑R g
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.isRkFinite_ground_iff_rankFinite : ∀ {α : Type u_1} {M : Matroid α}, M.IsRkFinite M.E ↔ M.RankFinite
-- Mathlib.SetTheory.ZFC.PSet
PSet.Equiv.exists_right : ∀ {x : PSet.{u_1}} {y : PSet.{u_2}}, x.Equiv y → ∀ (j : y.Type), ∃ i, (x.Func i).Equiv (y.Func j)
-- Mathlib.RingTheory.Perfectoid.BDeRham
instCommRingBDeRhamPlus : (R : Type u_1) →
  [inst : CommRing R] →
    (p : ℕ) →
      [inst_1 : Fact (Nat.Prime p)] →
        [inst_2 : Fact ¬IsUnit ↑p] → [inst_3 : IsAdicComplete (Ideal.span {↑p}) R] → CommRing (BDeRhamPlus R p)
-- Lean.Structure
/-- Computes and caches the C3 linearization. Assumes parents have already been set with `setStructureParents`.
If `relaxed` is false, then if the linearization cannot be computed, conflicts are recorded in the return value.
 -/
Lean.computeStructureResolutionOrder : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → Bool → m Lean.StructureResolutionOrderResult
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureRat_prop : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ) (n : ℕ),
  (MvPolynomial.bind₁ (wittStructureRat p Φ)) (wittPolynomial p ℚ n) =
    (MvPolynomial.bind₁ fun i => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℚ n)) Φ
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries_one : ∀ (G : Type u_1) [inst : Group G], Subgroup.upperCentralSeries G 1 = Subgroup.center G
-- Mathlib.Algebra.DirectSum.Ring
/-- On negative integers, the canonical map from ℤ to a graded ring is the negative extension of
the canonical map from ℕ to the underlying graded semiring.  -/
DirectSum.GRing.intCast_negSucc_ofNat : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} {inst_1 : (i : ι) → AddCommGroup (A i)}
  [self : DirectSum.GRing A] (n : ℕ), DirectSum.GRing.intCast (Int.negSucc n) = -DirectSum.GSemiring.natCast (n + 1)
-- Mathlib.Algebra.DirectSum.Basic
/-- `of i` is the natural inclusion map from `β i` to `⨁ i, β i`.  -/
DirectSum.of : {ι : Type v} →
  (β : ι → Type w) →
    [inst : (i : ι) → AddCommMonoid (β i)] → [DecidableEq ι] → (i : ι) → β i →+ DirectSum ι fun i => β i
-- Mathlib.GroupTheory.Coset.Card
Subgroup.card_mul_eq_card_subgroup_mul_card_quotient : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) (t : Set α),
  Nat.card ↑(t * ↑s) = Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' t)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsPathGraph3Compl.adj : ∀ {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α}, G.IsPathGraph3Compl v w₁ w₂ → G.Adj w₁ w₂
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticSeverity.information.sizeOf_spec : sizeOf Lean.Lsp.DiagnosticSeverity.information = 1
-- Mathlib.GroupTheory.Congruence.Defs
/-- A version of `Con.induction_on` for predicates which takes two arguments.  -/
Con.induction_on₂ : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {c : Con M} {d : Con N}
  {C : c.Quotient → d.Quotient → Prop} (p : c.Quotient) (q : d.Quotient), (∀ (x : M) (y : N), C ↑x ↑y) → C p q
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_insertIfNew_le : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insertIfNew k v).size ≤ m.size + 1
-- Init.Data.UInt.Basic
instOrOpUInt8 : OrOp UInt8
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.trans : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {x y z : M},
  AddConGen.Rel r x y → AddConGen.Rel r y z → AddConGen.Rel r x z
-- Mathlib.Algebra.Order.Group.Lattice
nsmul_two_semiclosed : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] {a : α}, 0 ≤ 2 • a → 0 ≤ a
-- Init.Core
Function.comp_def : ∀ {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} (f : β → δ) (g : α → β), f ∘ g = fun x => f (g x)
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_id_obj_unop : ∀ {X : TopCat} (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).obj (Opposite.unop U) = Opposite.unop U
-- Mathlib.Algebra.Quaternion
Quaternion.instNNRatCast : {R : Type u_1} → [inst : Field R] → NNRatCast (Quaternion R)
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- Same thing as `H × H'`. We introduce it for technical reasons,
see note [Manifold type tags].  -/
ModelProd : Type u_5 → Type u_6 → Type (max u_5 u_6)
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDFReal_zero_var : ∀ (m : ℝ), ProbabilityTheory.gaussianPDFReal m 0 = 0
-- Mathlib.Condensed.Discrete.Module
LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology LightProfinite) (Type u)).Full
-- Mathlib.Combinatorics.Quiver.SingleObj
_private.Mathlib.Combinatorics.Quiver.SingleObj.0.Quiver.SingleObj.listToPath.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (l : List α) → motive (a :: l)) → motive x
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  (X : CategoryTheory.Grothendieck F),
  ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).obj X).fiber =
    CategoryTheory.AsSmall.up.obj X.fiber
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- In a proper pseudometric space, all spheres are compact.  -/
isCompact_sphere : ∀ {α : Type u_3} [inst : PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ), IsCompact (Metric.sphere x r)
-- Mathlib.Algebra.Ring.Semireal.Defs
isSemireal_iff_not_isSumSq_neg_one : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : One R] [inst_2 : Mul R], IsSemireal R ↔ ¬IsSumSq (-1)
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation) `b`. See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.b : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} → (self : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) → D.obj self.i ⟶ X
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.w_support : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {D : ℝ},
  0 < D → Function.support (ExistsContDiffBumpBase.w D) = Metric.ball 0 D
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instFirstCountableTopology : ∀ {M : Type u_1} [inst : TopologicalSpace M] [FirstCountableTopology M], FirstCountableTopology Mᵈᵃᵃ
-- Mathlib.RingTheory.RingHom.OpenImmersion
RingHom.IsStandardOpenImmersion.algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [IsLocalization.Away r S], (algebraMap R S).IsStandardOpenImmersion
-- Mathlib.Geometry.Convex.Cone.Basic
Submodule.toConvexCone_le_toConvexCone : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {C₁ C₂ : Submodule R M}, C₁.toConvexCone ≤ C₂.toConvexCone ↔ C₁ ≤ C₂
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_zero_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β] (s : Finset α),
  s • 0 ⊆ 0
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- An extension of rings `R ⊆ S` is quadratic if `S` is a free `R`-algebra of rank `2`.
 -/
Algebra.IsQuadraticExtension : (R : Type u_2) →
  (S : Type u_3) → [inst : CommSemiring R] → [StrongRankCondition R] → [inst_2 : Semiring S] → [Algebra R S] → Prop
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The tensor product of two objects with right duals has a right dual,
given by the tensor product of the duals in the opposite order.  -/
CategoryTheory.hasRightDualTensor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        [CategoryTheory.HasRightDual X] →
          [CategoryTheory.HasRightDual Y] →
            CategoryTheory.HasRightDual (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_sup_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Injective ⇑f →
    ∀ (S T : AddSubsemigroup M), AddSubsemigroup.comap f (AddSubsemigroup.map f S ⊔ AddSubsemigroup.map f T) = S ⊔ T
-- Mathlib.Topology.Homotopy.Basic
/-- A `HomotopyRel f₀ f₁ S` is a homotopy between `f₀` and `f₁` which is fixed on the points in `S`.
 -/
ContinuousMap.HomotopyRel : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → C(X, Y) → Set X → Type (max u v)
-- Init.Grind.Interactive
Lean.Parser.Category.grind_ref : Lean.Parser.Category
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.emb_strictMono : ∀ {n : ℕ} (self : OrderedFinpartition n) (m : Fin self.length), StrictMono (self.emb m)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote_norm : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.Poly.denote ctx p.norm = Lean.Grind.Linarith.Poly.denote ctx p
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.continuousOn_tan : ContinuousOn Real.tan {x | Real.cos x ≠ 0}
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- A `SheafedSpace C` is a topological space equipped with a sheaf of `C`s.  -/
AlgebraicGeometry.SheafedSpace : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max (max u (u_1 + 1)) v)
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.opEquiv_symm_apply : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring Rᵐᵒᵖ), (RelIso.symm Subring.opEquiv) S = S.unop
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- For `p` prime, an element of `R` is a `p`-th root of unity if and only if it is either a
primitive `p`-th root of unity or `1`.  -/
mem_nthRootsFinset_iff_of_prime : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {p : ℕ},
  Nat.Prime p → ∀ {η : R}, η ∈ Polynomial.nthRootsFinset p 1 ↔ IsPrimitiveRoot η p ∨ η = 1
-- Init.Prelude
/-- `rfl : a = a` is the unique constructor of the equality type. This is the
same as `Eq.refl` except that it takes `a` implicitly instead of explicitly.

This is a more powerful theorem than it may appear at first, because although
the statement of the theorem is `a = a`, Lean will allow anything that is
definitionally equal to that type. So, for instance, `2 + 2 = 4` is proven in
Lean by `rfl`, because both sides are the same up to definitional equality.
 -/
rfl : ∀ {α : Sort u} {a : α}, a = a
-- Lean.Compiler.InlineAttrs
Lean.Compiler.hasAlwaysInlineAttribute : Lean.Environment → Lean.Name → Bool
-- Mathlib.Algebra.CharP.MixedCharZero
/-- A ring is a `ℚ`-algebra iff it has equal characteristic zero.  -/
EqualCharZero.nonempty_algebraRat_iff : ∀ (R : Type u_1) [inst : CommRing R], Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instLTRequestID : LT Lean.JsonRpc.RequestID
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coeFnMonoidHom.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Monoid β]
  [inst_3 : ContinuousMul β], ContinuousMap.coeFnMonoidHom = { toFun := fun f => ⇑f, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Each function of a uniformly equicontinuous family is uniformly continuous.  -/
UniformEquicontinuous.uniformContinuous : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α},
  UniformEquicontinuous F → ∀ (i : ι), UniformContinuous (F i)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.wellPowered_of_isSeparator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Balanced C] (G : C), CategoryTheory.IsSeparator G → CategoryTheory.WellPowered.{v₁, v₁, u₁} C
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.mk.injEq : ∀ {R : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Star R] (toNonUnitalSubsemiring : NonUnitalSubsemiring R)
  (star_mem' : ∀ {a : R}, a ∈ toNonUnitalSubsemiring.carrier → star a ∈ toNonUnitalSubsemiring.carrier)
  (toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R)
  (star_mem'_1 : ∀ {a : R}, a ∈ toNonUnitalSubsemiring_1.carrier → star a ∈ toNonUnitalSubsemiring_1.carrier),
  ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := star_mem' } =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := star_mem'_1 }) =
    (toNonUnitalSubsemiring = toNonUnitalSubsemiring_1)
-- Mathlib.Analysis.Matrix.PosDef
/-- A positive semi-definite matrix `M` induces a norm `‖x‖ = sqrt (re xᴴMx)`.  -/
Matrix.toSeminormedAddCommGroup : {n : Type u_2} →
  {𝕜 : Type u_3} → [Fintype n] → [inst : RCLike 𝕜] → (M : Matrix n n 𝕜) → M.PosSemidef → SeminormedAddCommGroup (n → 𝕜)
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.instBoundedOrderSubtypeSubmoduleMemSublatticeInvtRootSubmodule : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] → (P : RootPairing ι R M N) → BoundedOrder ↥P.invtRootSubmodule
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.lift₂_iso_hom_app_app₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (hF : W₁.IsInvertedBy₂ W₂ F)
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [inst_5 : L₁.IsLocalization W₁]
  [inst_6 : L₂.IsLocalization W₂] [inst_7 : W₁.ContainsIdentities] [inst_8 : W₂.ContainsIdentities] (X₁ : C₁) (X₂ : C₂),
  ((CategoryTheory.Localization.Lifting₂.iso L₁ L₂ W₁ W₂ F (CategoryTheory.Localization.lift₂ F hF L₁ L₂)).hom.app
          X₁).app
      X₂ =
    (CategoryTheory.Localization.Lifting.iso L₂ W₂ (F.obj X₁)
            ((CategoryTheory.Localization.lift₂ F hF L₁ L₂).obj (L₁.obj X₁))).hom.app
      X₂
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instIsTopologicalAddGroup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddCommGroup β]
  [inst_3 : IsTopologicalAddGroup β], IsTopologicalAddGroup C(α, β)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vadd_finset_eq_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {s : Finset β}
  {a : α} [inst_3 : Fintype β], a +ᵥ s = Finset.univ ↔ s = Finset.univ
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideCoequalizer.hom_ext_iff : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] [Nonempty J] {W : C}
  {k l : CategoryTheory.Limits.wideCoequalizer f ⟶ W},
  k = l ↔
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) k =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) l
-- Mathlib.Topology.Order.LeftRightNhds
/-- If `S` is order-connected and contains two points `x < y`,
then `S` is a punctured right neighbourhood of `x`.  -/
Set.OrdConnected.mem_nhdsGT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {S : Set α} {x y : α},
  S.OrdConnected → x ∈ S → y ∈ S → x < y → S ∈ nhdsWithin x (Set.Ioi x)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_4.eq_4 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Var)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match Lean.Grind.CommRing.Expr.var x with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.intCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_4 x
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.trans.congr_simp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_5 : RingHomInvPair σ₂₃ σ₃₂] [inst_6 : RingHomInvPair σ₃₂ σ₂₃]
  {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_7 : RingHomInvPair σ₁₃ σ₃₁] [inst_8 : RingHomInvPair σ₃₁ σ₁₃]
  [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4}
  [inst_11 : TopologicalSpace M₁] [inst_12 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_13 : TopologicalSpace M₂]
  [inst_14 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_15 : TopologicalSpace M₃] [inst_16 : AddCommMonoid M₃]
  [inst_17 : Module R₁ M₁] [inst_18 : Module R₂ M₂] [inst_19 : Module R₃ M₃] (e₁ e₁_1 : M₁ ≃SL[σ₁₂] M₂),
  e₁ = e₁_1 → ∀ (e₂ e₂_1 : M₂ ≃SL[σ₂₃] M₃), e₂ = e₂_1 → e₁.trans e₂ = e₁_1.trans e₂_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanCompIso_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospanCompIso F f g).app CategoryTheory.Limits.WalkingCospan.right =
    CategoryTheory.Iso.refl (((CategoryTheory.Limits.cospan f g).comp F).obj CategoryTheory.Limits.WalkingCospan.right)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.naturality_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) [G.IsLocallyFull K] {X Y : C} (i : G.obj X ⟶ G.obj Y)
  (x : (fun X => X) ((G.op.comp ℱ).obj (Opposite.op Y))),
  (CategoryTheory.ConcreteCategory.hom (ℱ'.obj.map i.op))
      ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) x) =
    (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) ((CategoryTheory.ConcreteCategory.hom (ℱ.map i.op)) x)
-- Mathlib.Topology.Order
generateFrom_inter : ∀ {α : Type u} (a b : TopologicalSpace α), TopologicalSpace.generateFrom ({s | IsOpen s} ∩ {s | IsOpen s}) = a ⊔ b
-- Aesop.Script.SScript
Aesop.Script.SScript.onGoal : ℕ → Aesop.Script.Step → Aesop.Script.SScript → Aesop.Script.SScript
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Equifibered.of_isIso : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G)
  [CategoryTheory.IsIso α], CategoryTheory.NatTrans.Equifibered α
-- Mathlib.Data.EReal.Basic
EReal.coe_toReal : ∀ {x : EReal}, x ≠ ⊤ → x ≠ ⊥ → ↑x.toReal = x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.mk_π_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X)
  (snd : W ⟶ Y) (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g),
  (CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app CategoryTheory.Limits.WalkingCospan.left = fst
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Concise textual representation of the source location of a recursive call   -/
Lean.Elab.WF.GuessLex.RecCallWithContext.posString : Lean.Elab.WF.GuessLex.RecCallWithContext → Lean.MetaM String