mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.instInhabitedTransported : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] → (e : C ≌ D) → Inhabited (CategoryTheory.Monoidal.Transported e)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- Evidence that `lanLiftLeftLift f g` is a Kan lift.  -/
CategoryTheory.Bicategory.lanLiftIsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : b ⟶ a) →
        (g : c ⟶ a) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] →
            (CategoryTheory.Bicategory.lanLiftLeftLift f g).IsKan
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instPreservesColimitOverSchemeTopMorphismPropertyOverForget : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {S : AlgebraicGeometry.Scheme} {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J]
  (F : CategoryTheory.Functor J (P.Over ⊤ S))
  [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f).left]
  [(F.comp
        ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp
          ((CategoryTheory.Over.forget S).comp AlgebraicGeometry.Scheme.forget))).IsLocallyDirected]
  [Quiver.IsThin J] [Small.{u, u_1} J],
  CategoryTheory.Limits.PreservesColimit F (CategoryTheory.MorphismProperty.Over.forget P ⊤ S)
-- Mathlib.Algebra.Module.Defs
smul_add_one_sub_smul : ∀ {M : Type u_3} [inst : AddCommMonoid M] {R : Type u_5} [inst_1 : Ring R] [inst_2 : Module R M] {r : R} {m : M},
  r • m + (1 - r) • m = m
-- Init.Data.SInt.Lemmas
Int32.toBitVec_toInt8 : ∀ (x : Int32), x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
MulAction.IsPretransitive.of_partition : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α},
  (∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b) →
    (∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b) → MulAction.stabilizer M s ≠ ⊤ → MulAction.IsPretransitive M α
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_fun_comm : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {g : α → F} [ContinuousNeg E] {f₁ f₂ : α → E},
  (fun a => f₁ a - f₂ a) =o[𝕜; l] g ↔ (fun a => f₂ a - f₁ a) =o[𝕜; l] g
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.add_lt_of_le_of_neg : ∀ {α : Type u} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {a b c : α},
  b ≤ c → a < 0 → b + a < c
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- If the first two signs are the same, then `signVariations` is unchanged by `eraseLead`  -/
Polynomial.signVariations_eraseLead : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] (P : Polynomial R),
  SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff → P.eraseLead.signVariations = P.signVariations
-- Mathlib.Tactic.Linter.UpstreamableDecl
/-- The `upstreamableDecl` linter detects declarations that could be moved to a file higher up in the
import hierarchy. If this is the case, it emits a warning.

By default, this linter will not fire on definitions, nor private declarations:
see options `linter.upstreamableDecl.defs` and `linter.upstreamableDecl.private`.

This is intended to assist with splitting files.
 -/
Mathlib.Linter.linter.upstreamableDecl : Lean.Option Bool
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.fvar.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (args : Array (Lean.Compiler.LCNF.Arg pu))
  (fvarId_1 : Lean.FVarId) (args_1 : Array (Lean.Compiler.LCNF.Arg pu)),
  (Lean.Compiler.LCNF.LetValue.fvar fvarId args = Lean.Compiler.LCNF.LetValue.fvar fvarId_1 args_1) =
    (fvarId = fvarId_1 ∧ args = args_1)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.toLinearEquiv_tensorTensorTensorComm : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  [inst_7 : Semiring D] [inst_8 : Algebra R D],
  ↑(Algebra.TensorProduct.tensorTensorTensorComm R R R R A B C D) = TensorProduct.tensorTensorTensorComm R A B C D
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- An orthonormal basis of the Euclidean mixed space.  -/
NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      OrthonormalBasis (NumberField.mixedEmbedding.index K) ℝ (NumberField.mixedEmbedding.euclidean.mixedSpace K)
-- Mathlib.Algebra.CharP.Algebra
/-- If `R` has characteristic `0`, then so does `FreeAlgebra R X`.  -/
FreeAlgebra.charZero : ∀ {R : Type u_3} {X : Type u_4} [inst : CommSemiring R] [CharZero R], CharZero (FreeAlgebra R X)
-- Mathlib.Data.Set.Finite.Lattice
/-- A finite union of sets which are all bounded below is still bounded below.  -/
Set.Finite.bddBelow_biUnion : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [IsCodirectedOrder α] [Nonempty α] {I : Set β} {S : β → Set α},
  I.Finite → (BddBelow (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddBelow (S i))
-- Mathlib.Topology.Instances.EReal.Lemmas
continuous_coe_real_ereal : Continuous Real.toEReal
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_source_mem_nhdsWithin' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s : Set M} [inst_5 : ChartedSpace H M] {x x' : M},
  x' ∈ (extChartAt I x).source → (extChartAt I x).source ∈ nhdsWithin x' s
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The integrand in `next` is integrable.  -/
ODE.FunSpace.intervalIntegrable_comp_compProj : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K →
    ∀ (α : ODE.FunSpace t₀ x₀ r L) (t : ↑(Set.Icc tmin tmax)),
      IntervalIntegrable (fun t' => f t' (α.compProj t')) MeasureTheory.volume ↑t₀ ↑t
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.ext : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {F G : f₀.Homotopy f₁}, (∀ (x : ↑unitInterval × X), F x = G x) → F = G
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.pushforward_curry_uncurry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} {f : I ⟶ J}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  {X : CategoryTheory.Over I} {A : CategoryTheory.Over J}
  (v : A ⟶ (CategoryTheory.ExponentiableMorphism.pushforward f).obj X),
  CategoryTheory.ExponentiableMorphism.pushforwardCurry (CategoryTheory.ExponentiableMorphism.pushforwardUncurry v) = v
-- Std.Data.HashMap.Lemmas
Std.HashMap.all_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulHashable α] [EquivBEq α]
  {p : α → Bool}, m.keys.all p = m.all fun a x => p a
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_comap_eq : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S) (t : Subring S),
  Subring.map f (Subring.comap f t) = t ⊓ f.range
-- Mathlib.Algebra.Group.Hom.Defs
/-- `M →+ N` denotes the type of additive monoid homomorphisms from `M` to `N`.  -/
«term_→+_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.injective_inclusionSpan : ∀ {R : Type u_1} {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (p : Submodule R M),
  Function.Injective ⇑(Submodule.inclusionSpan S p)
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_zero : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), Multiset.erase 0 a = 0
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.map_diagonal_star : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddMonoid α] [inst_2 : StarAddMonoid α] (x : n → α),
  (Matrix.diagonal x).map star = Matrix.diagonal (star x)
-- Mathlib.Topology.Algebra.Ring.Ideal
/-- This is not `@[simp]` since otherwise it causes timeouts downstream as `simp` tries and fails to
generate an `IsClosed` instance.
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234852.20heartbeats.20of.20the.20linter
 -/
Ideal.closure_eq_of_isClosed : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [inst_2 : IsTopologicalRing R] (I : Ideal R),
  IsClosed ↑I → I.closure = I
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- The functor sending a representation to its complex of inhomogeneous chains.  -/
groupHomology.chainsFunctor : (k G : Type u) →
  [inst : CommRing k] → [inst_1 : Group G] → CategoryTheory.Functor (Rep.{u, u, u} k G) (ChainComplex (ModuleCat k) ℕ)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
_private.Mathlib.Analysis.Normed.Algebra.Spectrum.0.QuasispectrumRestricts.termσₙ : Lean.ParserDescr
-- Mathlib.Data.Part
Part.sub_mem_sub : ∀ {α : Type u_1} [inst : Sub α] (a b : Part α) (ma mb : α), ma ∈ a → mb ∈ b → ma - mb ∈ a - b
-- Lean.Message
Lean.MessageData.ofLazy.sizeOf_spec : ∀ (f : Option Lean.PPContext → BaseIO Dynamic) (hasSyntheticSorry : Lean.MetavarContext → Bool),
  sizeOf (Lean.MessageData.ofLazy f hasSyntheticSorry) = 1
-- Mathlib.Data.Setoid.Partition
/-- Makes an equivalence relation from a set of disjoints sets covering α.  -/
Setoid.setoidOfDisjointUnion : {α : Type u_1} → {c : Set (Set α)} → ⋃₀ c = Set.univ → c.PairwiseDisjoint id → Setoid α
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.instPreservesColimitsOfShapeDiscreteObjFunctorEval : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] (J : Type w) (F : CategoryTheory.Functor C A),
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J)
    ((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F)
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.nhdsKer_singleton : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α] (a : α),
  nhdsKer {a} = Set.Iic a
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.eq_comp_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X},
  g = CategoryTheory.CategoryStruct.comp f α.inv ↔ CategoryTheory.CategoryStruct.comp g α.hom = f
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.All.eq_1 : ∀ {α : Type u_1} (p : α → Prop), RBTree.RBNode.All p RBTree.RBNode.nil = True
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.mk.sizeOf_spec : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (toSlashInvariantForm : SlashInvariantForm Γ k)
  (holo' : MDiff ⇑toSlashInvariantForm)
  (bdd_at_cusps' : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm.toFun k),
  sizeOf { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := bdd_at_cusps' } =
    1 + sizeOf toSlashInvariantForm
-- Lean.Meta.Match.Basic
Lean.Meta.Match.counterExamplesToMessageData : Array Lean.Meta.Match.CounterExample → Lean.MessageData
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_bijective : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S],
  Function.Bijective RingEquiv.symm
-- Mathlib.RepresentationTheory.Action
Representation.linearizeMap_toLinearMap : ∀ {k : Type u} {G : Type v} [inst : Monoid G] [inst_1 : Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y),
  (Representation.linearizeMap f).toLinearMap =
    MonoidAlgebra.mapDomainLinearMap k k ⇑(CategoryTheory.ConcreteCategory.hom f.hom)
-- Mathlib.Topology.UniformSpace.Pi
cauchy_pi_iff' : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] {l : Filter ((i : ι) → α i)} [l.NeBot],
  Cauchy l ↔ ∀ (i : ι), Cauchy (Filter.map (Function.eval i) l)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_one : ∀ {R : Type u} {M : Type v} [inst : One R] [inst_1 : Zero M], TrivSqZeroExt.fst 1 = 1
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.merge.eq_3 : ∀ {α : Type u_1} (le : α → α → Bool) (a₁ : α) (c₁ sibling : Batteries.PairingHeapImp.Heap α),
  Batteries.PairingHeapImp.Heap.merge le (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling)
      Batteries.PairingHeapImp.Heap.nil =
    Batteries.PairingHeapImp.Heap.node a₁ c₁ Batteries.PairingHeapImp.Heap.nil
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- (Implementation): Auxiliary lemma for `CategoryTheory.PreOneHypercover.isoMk`.  -/
CategoryTheory.PreOneHypercover.isoMk_aux_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j))
  {i j : E.I₀} (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (k : E.I₁ i j) {Z : C}
  (h : E.Y (s₁.symm ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (s₁ k))) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (h₁ k).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp
            (h₁ (s₁.symm ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv h))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ k).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A restatement of `MetricSpace.tendsto_atTop` in terms of the norm.  -/
NormedAddCommGroup.tendsto_atTop : ∀ {α : Type u_2} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] {β : Type u_5} [inst_2 : SeminormedAddCommGroup β]
  {f : α → β} {b : β}, Filter.Tendsto f Filter.atTop (nhds b) ↔ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → ‖f n - b‖ < ε
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.matrix_components : ∀ {J : Type} [inst : Finite J] {K : Type} [inst_1 : Finite K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (j : J) (k : K),
  CategoryTheory.Limits.biproduct.components (CategoryTheory.Limits.biproduct.matrix m) j k = m j k
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm : ∀ {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E] {f : α → E}
  (p : ENNReal),
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ (φ : α → 𝕜), MeasureTheory.eLpNorm (φ • f) p μ ≤ MeasureTheory.eLpNorm φ ⊤ μ * MeasureTheory.eLpNorm f p μ
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.instIsLocalizationPlusInjectiveObjectQuotientInverseImageQuasiIsoMapCochainComplexPlusι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopyCategory.Plus.quotient (CategoryTheory.InjectiveObject C)).IsLocalization
    ((CochainComplex.Plus.quasiIso C).inverseImage (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.equivBool_apply_right : CategoryTheory.Limits.WalkingPair.equivBool CategoryTheory.Limits.WalkingPair.right = false
-- Lean.Meta.ReduceEval
_private.Lean.Meta.ReduceEval.0.Lean.Meta.evalList : {α : Type} → [Lean.Meta.ReduceEval α] → Lean.Expr → Lean.MetaM (List α)
-- Mathlib.Topology.Bornology.Absorbs
Set.Finite.absorbs_sUnion : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {T : Set (Set α)},
  T.Finite → (Absorbs M s (⋃₀ T) ↔ ∀ t ∈ T, Absorbs M s t)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.linearIndependent_single_of_ne_zero : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : Ring 𝕜] [IsDomain 𝕜] {M : Type u_5}
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] [Module.IsTorsionFree 𝕜 M] {v : ι → M},
  (∀ (i : ι), v i ≠ 0) → LinearIndependent 𝕜 fun i => PiLp.single p i (v i)
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
_private.Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints.0.UpperHalfPlane.fixedPt.eq_1 : ∀ (g : GL (Fin 2) ℝ) (hell : g.IsElliptic),
  UpperHalfPlane.fixedPt g hell =
    { coe := (↑(↑g 0 0) - ↑(↑g 1 1)) / (2 * ↑(↑g 1 0)) + Complex.I * (↑√(-(↑g).discr) / (2 * ↑|↑g 1 0|)),
      coe_im_pos := ⋯ }
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
ContinuousLinearMap.coe_restrictScalars : ∀ {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} [inst : Semiring A] [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module A M₁] [inst_4 : Module R M₁] [inst_5 : TopologicalSpace M₁]
  [inst_6 : AddCommMonoid M₂] [inst_7 : Module A M₂] [inst_8 : Module R M₂] [inst_9 : TopologicalSpace M₂]
  [inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A] (f : M₁ →L[A] M₂), ↑(ContinuousLinearMap.restrictScalars R f) = ↑R ↑f
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.range_pullbackFst : ∀ {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)
-- Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
/-- The projection from a trivial fiber bundle to its base is continuous.  -/
IsHomeomorphicTrivialFiberBundle.continuous_proj : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B}, IsHomeomorphicTrivialFiberBundle F proj → Continuous proj
-- Mathlib.Data.Fintype.Card
/-- Note: this lemma is specifically about `Fintype.ofIsEmpty`. For a statement about
arbitrary `Fintype` instances, use `Fintype.card_eq_zero`.  -/
Fintype.card_ofIsEmpty : ∀ {α : Type u_1} [inst : IsEmpty α], Fintype.card α = 0
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.toAddMonoid_injective : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u₁}
  [inst_2 : AddCommMonoid γ], Function.Injective DirectSum.toAddMonoid
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The function from multivariable polynomials in one type,
with coefficients in multivariable polynomials in another type,
to multivariable polynomials in the sum of the two types.

See `sumRingEquiv` for the ring isomorphism.
 -/
MvPolynomial.iterToSum : (R : Type u) →
  (S₁ : Type v) →
    (S₂ : Type w) → [inst : CommSemiring R] → MvPolynomial S₁ (MvPolynomial S₂ R) →+* MvPolynomial (S₁ ⊕ S₂) R
-- Mathlib.RingTheory.IsGaloisGroup.Basic
Subgroup.smul_algebraMap : ∀ {G : Type u_1} (B : Type u_3) [inst : Group G] [inst_1 : Semiring B] [inst_2 : MulSemiringAction G B] {C : Type u_4}
  [inst_3 : CommSemiring C] [inst_4 : Algebra C B] {H : Subgroup G} [SMulCommClass (↥H) C B] {g : G},
  g ∈ H → ∀ (x : C), g • (algebraMap C B) x = (algebraMap C B) x
-- Mathlib.Analysis.Quaternion
Quaternion.continuous_im : Continuous fun q => q.im
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `F⟮x⟯` has dimension `≤1` over `F` for every `x ∈ E` then `F = E`.  -/
IntermediateField.bot_eq_top_of_finrank_adjoin_le_one : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E],
  (∀ (x : E), Module.finrank F ↥F⟮x⟯ ≤ 1) → ⊥ = ⊤
-- Mathlib.Computability.RegularExpressions
/-- `P.deriv a` matches `x` if `P` matches `a :: x`, the Brzozowski derivative of `P` with respect
to `a`  -/
RegularExpression.deriv : {α : Type u_1} → [DecidableEq α] → RegularExpression α → α → RegularExpression α
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.IsLimit.homIso_symm_apply : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) (Z : C)
  (h :
    { h // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp h (f j₁) = CategoryTheory.CategoryStruct.comp h (f j₂) }),
  (CategoryTheory.Limits.Trident.IsLimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Trident.IsLimit.lift' ht ↑h ⋯)
-- Mathlib.Logic.Nonempty
Function.Surjective.nonempty : ∀ {α : Sort u_1} {β : Sort u_2} [h : Nonempty β] {f : α → β}, Function.Surjective f → Nonempty α
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.reindex_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) {ι : Type w'}
  (e : ι ≃ E.I₀) (i : ι), (E.reindex e).f i = E.f (e i)
-- Mathlib.Computability.Ackermann
add_lt_ack : ∀ (m n : ℕ), m + n < ack m n
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.SubobjectRepresentableBy.hasTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω), CategoryTheory.Limits.HasTerminal C
-- Mathlib.CategoryTheory.Sites.Canonical
/-- Construct the finest (largest) Grothendieck topology for which the given presheaf is a sheaf.  -/
CategoryTheory.Sheaf.finestTopologySingle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ (Type w) → CategoryTheory.GrothendieckTopology C
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Recursive part of `findEq`.  -/
_private.Mathlib.Tactic.Simproc.ExistsAndEq.0.ExistsAndEq.findEq.go : {u : Lean.Level} →
  {α : Q(Sort u)} →
    Q(«$α») → Q(Prop) → ExistsAndEq.Path → Lean.MetaM (List ExistsAndEq.VarQ × Lean.LocalContext × Q(Prop) × Q(«$α»))
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.below.pair : ∀ {motive : (a : ℕ → ℕ) → Nat.Primrec a → Prop} {f g : ℕ → ℕ} (a : Nat.Primrec f) (a_1 : Nat.Primrec g),
  Nat.Primrec.below a → motive f a → Nat.Primrec.below a_1 → motive g a_1 → Nat.Primrec.below ⋯
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- Measures `ν` on `α` and `μ` on the `Quotient` of `α` mod `G` satisfy
`QuotientMeasureEqMeasurePreimage` if: for any fundamental domain `t`, and any measurable subset
`U` of the quotient, `μ U = ν ((π ⁻¹' U) ∩ t)`.  -/
MeasureTheory.QuotientMeasureEqMeasurePreimage : {G : Type u_1} →
  {α : Type u_3} →
    [inst : Group G] →
      [inst_1 : MulAction G α] →
        [inst_2 : MeasurableSpace α] →
          autoParam (MeasureTheory.Measure α) MeasureTheory.QuotientMeasureEqMeasurePreimage._auto_1 →
            MeasureTheory.Measure (Quotient (MulAction.orbitRel G α)) → Prop
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.getStack : Lean.PrettyPrinter.FormatterM (Array Std.Format)
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_le_castSucc_iff : ∀ {n : ℕ} {a b : Fin n}, a.castSucc ≤ b.castSucc ↔ a ≤ b
-- Mathlib.Data.Finset.Preimage
Finset.image_preimage_of_bijective : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {f : α → β} (s : Finset β) (hf : Function.Bijective f),
  Finset.image f (s.preimage f ⋯) = s
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- The functor `shrinkCoyoneda : Cᵒᵖ ⥤ C ⥤ Type w` for a locally `w`-small category `C`
is fully faithful.  -/
CategoryTheory.fullyFaithfulShrinkCoyoneda : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] → CategoryTheory.shrinkCoyoneda.{w, v, u}.FullyFaithful