mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- the objects in the coverings of the fibre products  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.Y : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {S : C} → (self : F.PreOneHypercoverDenseData S) → ⦃i₁ i₂ : self.I₀⦄ → self.I₁ i₁ i₂ → C₀
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare km k).isLE = true
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.mem_units_iff : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (x : Mˣ), x ∈ S.units ↔ ↑x ∈ S ∧ ↑x⁻¹ ∈ S
-- Mathlib.Order.ModularLattice
IsModularLattice.exists_inf_eq_and_sup_eq : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {a b c : α} [inst_2 : BoundedOrder α] [ComplementedLattice α],
  a ≤ b → b ≤ c → ∃ b', b ⊓ b' = a ∧ b ⊔ b' = c
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.map_fst_toList_eq_keys : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α], List.map Prod.fst (Std.DHashMap.Raw.Const.toList ↑m) = (↑m).keys
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.homToEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C},
  α.homToEquiv =
    { toFun := fun f => CategoryTheory.CategoryStruct.comp f α.hom,
      invFun := fun g => CategoryTheory.CategoryStruct.comp g α.inv, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.iterate_mono : ∀ {f g : CircleDeg1Lift}, f ≤ g → ∀ (n : ℕ), (⇑f)^[n] ≤ (⇑g)^[n]
-- Mathlib.CategoryTheory.Localization.HasLocalization
CategoryTheory.MorphismProperty.instCategoryLocalization' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      [inst_1 : W.HasLocalization] → CategoryTheory.Category.{w, u} W.Localization'
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toBialgHom_eq_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A ≃ₐc[R] B), f.toBialgHom = ↑f
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Any regular monomorphism is a strong monomorphism.  -/
CategoryTheory.RegularMono.strongMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (h : CategoryTheory.RegularMono f),
  CategoryTheory.StrongMono f
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- Copy of a `CompactlySupportedContinuousMap` with a new `toFun` equal to the old one. Useful
to fix definitional equalities.  -/
CompactlySupportedContinuousMap.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Zero β] →
          (f : CompactlySupportedContinuousMap α β) → (f' : α → β) → f' = ⇑f → CompactlySupportedContinuousMap α β
-- Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
/-- The property that the subtype of arrows satisfying a property `P : MorphismProperty C`
is of cardinality `< κ`.  -/
CategoryTheory.MorphismProperty.HasCardinalLT : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Cardinal.{w} → Prop
-- Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic
AlgebraicGeometry.AlgebraicCycle.map_id : ∀ {X : AlgebraicGeometry.Scheme} {R : Type u_1} [inst : Semiring R] {N : Type u_2} [inst_1 : DecidableEq N]
  (wx : ↥X → N) (c : AlgebraicGeometry.AlgebraicCycle X R),
  AlgebraicGeometry.AlgebraicCycle.map (CategoryTheory.CategoryStruct.id X) wx wx c = c
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_empty : ∀ {α : Type u_2} {x : Bornology α}, Bornology.IsBounded ∅
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.comp_asNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e f g : C ≌ D} (α : e ⟶ f) (β : f ⟶ g),
  CategoryTheory.Equivalence.asNatTrans (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.asNatTrans α)
      (CategoryTheory.Equivalence.asNatTrans β)
-- Mathlib.RingTheory.Smooth.Locus
Algebra.smoothLocus_eq_univ : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Algebra.Smooth R A],
  Algebra.smoothLocus R A = Set.univ
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalCategoryStruct_tensorHom : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {X₁ Y₁ X₂ Y₂ : (i : I) → C i} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂)
  (i : I),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g i = CategoryTheory.MonoidalCategoryStruct.tensorHom (f i) (g i)
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivative_one : ∀ {R : Type u_1} [inst : CommSemiring R], (PowerSeries.derivative R) 1 = 0
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Icc_add_intCast : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (a : α),
  ⋃ n, Set.Icc (a + ↑n) (a + ↑n + 1) = Set.univ
-- Lean.Meta.Tactic.Grind.EMatch
/-- Internal "marker" for representing unassigned elements in the `assignment` field.
This is a small hack to avoid one extra level of indirection by using `Option Expr` at `assignment`.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.unassigned : Lean.Expr
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod.instSigmaFinite : ∀ {α : Type u_4} {β : Type u_5} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  {x_1 : MeasurableSpace β} {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite ν],
  MeasureTheory.SigmaFinite (μ.prod ν)
-- Init.Data.Slice.InternalLemmas
Std.Slice.Internal.iter_eq_toIteratorIter : ∀ {α β : Type v} {γ : Type u} [inst : Std.ToIterator (Std.Slice γ) Id α β] {s : Std.Slice γ},
  Std.Slice.Internal.iter s = Std.ToIterator.iter s
-- Mathlib.Data.Multiset.MapFold
Multiset.pmap_eq_map_attach : ∀ {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ a ∈ s, p a),
  Multiset.pmap f s H = Multiset.map (fun x => f ↑x ⋯) s.attach
-- Mathlib.RingTheory.ReesAlgebra
adjoin_monomial_eq_reesAlgebra : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R),
  Algebra.adjoin R ↑(Submodule.map (Polynomial.monomial 1) I) = reesAlgebra I
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.mul.go.match_1.splitter : (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) →
  (m₁ m₂ : Lean.Grind.CommRing.Mon) →
    ((m₁ : Lean.Grind.CommRing.Mon) → motive m₁ Lean.Grind.CommRing.Mon.unit) →
      ((m₂ : Lean.Grind.CommRing.Mon) →
          (m₂ = Lean.Grind.CommRing.Mon.unit → False) → motive Lean.Grind.CommRing.Mon.unit m₂) →
        ((pw₁ : Lean.Grind.CommRing.Power) →
            (m₁ : Lean.Grind.CommRing.Mon) →
              (pw₂ : Lean.Grind.CommRing.Power) →
                (m₂ : Lean.Grind.CommRing.Mon) →
                  motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)) →
          motive m₁ m₂
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.eq_zero_of_homogenize_eq_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {p : Polynomial R} {n : ℕ}, p.natDegree ≤ n → p.homogenize n = 0 → p = 0
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsNegApply.neg_apply`. -/
neg_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Neg β}
  {inst_2 : Neg F} [self : IsNegApply F α β] (f : F) (x : α), (-f) x = -f x
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_lt_iff_lt : ∀ {a b : ℤ} (ha₁ : Int32.minValue.toInt ≤ a) (ha₂ : a ≤ Int32.maxValue.toInt) (hb₁ : Int32.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int32.maxValue.toInt), Int32.ofIntLE a ha₁ ha₂ < Int32.ofIntLE b hb₁ hb₂ ↔ a < b
-- Mathlib.CategoryTheory.Sites.Coherent.Comparison
CategoryTheory.regularCoverage.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C],
  CategoryTheory.regularCoverage C =
    {
      coverings := fun B =>
        {S | ∃ X f, (S = CategoryTheory.Presieve.ofArrows (fun x => X) fun x => f) ∧ CategoryTheory.EffectiveEpi f},
      pullback := ⋯ }
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- Note: This does not hold for `n = ∞`. `f` being `C^∞` at `x` means that for every `n`, `f` is
`C^n` on some neighborhood of `x`, but this neighborhood can depend on `n`.  -/
contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M'],
  n ≠ ↑⊤ → (ContMDiffWithinAt I I' n f s x ↔ ∀ᶠ (x' : M) in nhdsWithin x (insert x s), ContMDiffWithinAt I I' n f s x')
-- Mathlib.Algebra.Ring.Action.Basic
MulSemiringAction.toDistribMulAction : {M : Type u} →
  {R : Type v} → {inst : Monoid M} → {inst_1 : Semiring R} → [self : MulSemiringAction M R] → DistribMulAction M R
-- Aesop.Tree.TreeM
Aesop.Tree.mk.inj : ∀ {root : Aesop.MVarClusterRef} {rootMetaState : Lean.Meta.SavedState} {numGoals numRapps : ℕ}
  {nextGoalId : Aesop.GoalId} {nextRappId : Aesop.RappId} {allIntroducedMVars : Std.HashSet Lean.MVarId}
  {root_1 : Aesop.MVarClusterRef} {rootMetaState_1 : Lean.Meta.SavedState} {numGoals_1 numRapps_1 : ℕ}
  {nextGoalId_1 : Aesop.GoalId} {nextRappId_1 : Aesop.RappId} {allIntroducedMVars_1 : Std.HashSet Lean.MVarId},
  { root := root, rootMetaState := rootMetaState, numGoals := numGoals, numRapps := numRapps, nextGoalId := nextGoalId,
        nextRappId := nextRappId, allIntroducedMVars := allIntroducedMVars } =
      { root := root_1, rootMetaState := rootMetaState_1, numGoals := numGoals_1, numRapps := numRapps_1,
        nextGoalId := nextGoalId_1, nextRappId := nextRappId_1, allIntroducedMVars := allIntroducedMVars_1 } →
    root = root_1 ∧
      rootMetaState = rootMetaState_1 ∧
        numGoals = numGoals_1 ∧
          numRapps = numRapps_1 ∧
            nextGoalId = nextGoalId_1 ∧ nextRappId = nextRappId_1 ∧ allIntroducedMVars = allIntroducedMVars_1
-- Mathlib.Analysis.Convex.Between
wbtw_iff_of_le : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {x y z : R},
  x ≤ z → (Wbtw R x y z ↔ x ≤ y ∧ y ≤ z)
-- Mathlib.Order.Heyting.Boundary
/-- **Leibniz rule** for the co-Heyting boundary.  -/
Coheyting.boundary_inf : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a b : α),
  Coheyting.boundary (a ⊓ b) = Coheyting.boundary a ⊓ b ⊔ a ⊓ Coheyting.boundary b
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_ret_fix : ∀ (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)) =
    Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main
      (Turing.TM2.Stmt.goto fun s =>
        bif Turing.PartrecToTM2.natEnd (s.getD default) then Turing.PartrecToTM2.Λ'.ret k
        else
          Turing.PartrecToTM2.Λ'.clear Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.K'.main
            (Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.fix f k)))
-- Mathlib.NumberTheory.Divisors
_private.Mathlib.NumberTheory.Divisors.0.Int.divisorsAntidiag.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Mathlib.Analysis.Calculus.Taylor
/-- **Taylor's theorem** with a polynomial bound on the remainder

We assume that `f` is `n+1`-times continuously differentiable on the closed set `Icc a b`.
The difference of `f` and its `n`-th Taylor polynomial can be estimated by
`C * (x - a)^(n+1) / n!` where `C` is a bound for the `n+1`-th iterated derivative of `f`.  -/
taylor_mean_remainder_bound : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b C x : ℝ} {n : ℕ},
  a ≤ b →
    ContDiffOn ℝ (↑n + 1) f (Set.Icc a b) →
      x ∈ Set.Icc a b →
        (∀ y ∈ Set.Icc a b, ‖iteratedDerivWithin (n + 1) f (Set.Icc a b) y‖ ≤ C) →
          ‖f x - taylorWithinEval f n (Set.Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n.factorial
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.closure_sUnion : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : Set (Set R)),
  NonUnitalSubring.closure (⋃₀ s) = ⨆ t ∈ s, NonUnitalSubring.closure t
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- `determinant` of `Matrix.kroneckerMapBilinear`.

This is primarily used with `R = ℕ` to prove `Matrix.det_kronecker`.  -/
Matrix.det_kroneckerMapBilinear : ∀ {R : Type u_1} {S : Type u_2} {α : Type u_3} {β : Type u_5} {γ : Type u_7} {m : Type u_10} {n : Type u_11}
  [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : DecidableEq m]
  [inst_5 : DecidableEq n] [inst_6 : NonAssocSemiring α] [inst_7 : NonAssocSemiring β] [inst_8 : CommRing γ]
  [inst_9 : Module R α] [inst_10 : Module S β] [inst_11 : Module R γ] [inst_12 : Module S γ]
  [inst_13 : SMulCommClass S R γ] (f : α →ₗ[R] β →ₗ[S] γ),
  (∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b') →
    ∀ (A : Matrix m m α) (B : Matrix n n β),
      (((Matrix.kroneckerMapBilinear f) A) B).det =
        (A.map fun a => (f a) 1).det ^ Fintype.card n * (B.map fun b => (f 1) b).det ^ Fintype.card m
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_sdiff_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iic a \ Set.Iic b = Set.Ioc b a
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_nnreal_smul_apply : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (c : NNReal),
  (c • μ).real s = ↑c * μ.real s
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The categorical product and the usual product agree
 -/
CommRingCat.piIsoPi : {ι : Type u} → (R : ι → CommRingCat) → ∏ᶜ R ≅ CommRingCat.of ((i : ι) → ↑(R i))
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueProds.toIsCancelMul : ∀ {G : Type u} [inst : Mul G] [UniqueProds G], IsCancelMul G
-- Mathlib.Analysis.Normed.Group.Basic
nontrivialTopology_iff_exists_norm_ne_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], NontrivialTopology E ↔ ∃ x, ‖x‖ ≠ 0
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₂ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.ShortComplex.π₂
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.coeffIntegerNormalization_mem_support : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (p : Polynomial S) (i : ℕ),
  IsLocalization.coeffIntegerNormalization M p i ≠ 0 → i ∈ p.support
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with subtraction.  -/
ContDiffWithinAt.laplacianWithin_sub : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E} {s : Set E},
  ContDiffWithinAt ℝ 2 f₁ s x →
    ContDiffWithinAt ℝ 2 f₂ s x →
      UniqueDiffOn ℝ s →
        x ∈ s →
          InnerProductSpace.laplacianWithin (f₁ - f₂) s x =
            InnerProductSpace.laplacianWithin f₁ s x - InnerProductSpace.laplacianWithin f₂ s x
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.mk : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : TopologicalSpace Z] →
            {proj : Z → B} →
              (toOpenPartialHomeomorph : OpenPartialHomeomorph Z (B × F)) →
                (baseSet : Set B) →
                  IsOpen baseSet →
                    toOpenPartialHomeomorph.source = proj ⁻¹' baseSet →
                      toOpenPartialHomeomorph.target = baseSet ×ˢ Set.univ →
                        (∀ p ∈ toOpenPartialHomeomorph.source, (↑toOpenPartialHomeomorph p).1 = proj p) →
                          Bundle.Trivialization F proj
-- Mathlib.LinearAlgebra.Matrix.Polynomial
Polynomial.coeff_det_X_add_C_card : ∀ {n : Type u_1} {α : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A B : Matrix n n α),
  (Polynomial.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.coeff (Fintype.card n) = A.det
-- Init.Data.Int.Gcd
Int.gcd_mul_left_sub_right : ∀ (m n k : ℤ), m.gcd (m * k - n) = m.gcd n
-- Init.Data.Order.Lemmas
/-- If a `Min α` instance satisfies typical properties in terms of a reflexive and antisymmetric `LE α`
instance, then the `LE α` instance represents a linear order.
 -/
Std.IsLinearOrder.of_refl_of_antisymm_of_lawfulOrderMin : ∀ {α : Type u} [LE α] [inst : LE α] [inst_1 : Min α] [Std.Refl fun x1 x2 => x1 ≤ x2] [Std.Antisymm fun x1 x2 => x1 ≤ x2]
  [Std.LawfulOrderMin α], Std.IsLinearOrder α
-- Mathlib.Data.ENNReal.Action
ENNReal.instSMulNNRealOfMulAction : {M : Type u_1} → [MulAction ENNReal M] → SMul NNReal M
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.matrixToStdBasis.eq_1 : ∀ (K : Type u_1) [inst : Field K],
  NumberField.mixedEmbedding.matrixToStdBasis K =
    Matrix.fromBlocks (Matrix.diagonal fun x => 1) 0 0
      ((Matrix.reindex (Equiv.prodComm (Fin 2) { w // w.IsComplex }) (Equiv.prodComm (Fin 2) { w // w.IsComplex }))
        (Matrix.blockDiagonal fun x => 2⁻¹ • !![1, 1; -Complex.I, Complex.I]))
-- Mathlib.Data.Num.Lemmas
PosNum.cast_one' : ∀ {α : Type u_1} [inst : One α] [inst_1 : Add α], ↑PosNum.one = 1
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_equiv_eq_map_symm' : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : N ≃+ G) (K : AddSubgroup G),
  AddSubgroup.comap f.toAddMonoidHom K = AddSubgroup.map f.symm.toAddMonoidHom K
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.instFullRingCatForget₂RingHomCarrierCarrier : (CategoryTheory.forget₂ CommRingCat RingCat).Full
-- Init.Notation
/-- `p,+,?` is shorthand for `sepBy1(p, ",", allowTrailingSep)`.
It parses 1 or more occurrences of `p` separated by `,`, possibly including
a trailing `,`, that is: `p | p, | p,p | p,p, | p,p,p | ...`.

It produces a `nullNode` containing a `SepArray` with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
 -/
«stx_,+,?» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.PowerSeries.Restricted
PowerSeries.isRestricted.mul : ∀ {R : Type u_1} [inst : NormedRing R] [IsUltrametricDist R] (c : ℝ) {f g : PowerSeries R},
  PowerSeries.IsRestricted c f → PowerSeries.IsRestricted c g → PowerSeries.IsRestricted c (f * g)
-- Std.Data.Internal.Cut
Std.Internal.instIsStrictCutCompareLt : ∀ {α : Type u} [inst : Ord α], Std.Internal.IsStrictCut compare fun x => Ordering.lt
-- Mathlib.Topology.Separation.Regular
NormalSpace.of_regularSpace_secondCountableTopology : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X], NormalSpace X
-- Mathlib.RingTheory.Invariant.Defs
Algebra.IsInvariant.isInvariant : ∀ {A : Type u_1} {B : Type u_2} {G : Type u_3} {inst : CommSemiring A} {inst_1 : Semiring B} {inst_2 : Algebra A B}
  {inst_3 : Group G} {inst_4 : MulSemiringAction G B} [self : Algebra.IsInvariant A B G] (b : B),
  (∀ (g : G), g • b = b) → ∃ a, (algebraMap A B) a = b
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.node.inj : ∀ {α : Type u} {cs cs_1 : Array (Lean.PersistentArrayNode α)},
  Lean.PersistentArrayNode.node cs = Lean.PersistentArrayNode.node cs_1 → cs = cs_1
-- Mathlib.RingTheory.RingHom.Smooth
/-- A ring homomorphism `f : R →+* S` is smooth if `S` is smooth as an `R` algebra.  -/
RingHom.Smooth : {R : Type u_1} → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.Data.WSeq.Basic
/-- auxiliary definition of `destruct_join` over weak sequences  -/
Stream'.WSeq.destruct_join.aux : {α : Type u} → Option (Stream'.WSeq α × Stream'.WSeq (Stream'.WSeq α)) → Computation (Option (α × Stream'.WSeq α))
-- Mathlib.Topology.Instances.CantorSet
quarter_mem_cantorSet : 1 / 4 ∈ cantorSet
-- Batteries.Data.String.Lemmas
String.extract_zero_endPos : ∀ (s : String), String.Pos.Raw.extract s 0 s.rawEndPos = s
-- Std.Http.Data.URI.Encoding
/-- Checks if all characters in a `ByteArray` are allowed in an encoded URI component. This is a fast check
that only verifies the character set, not full encoding validity.
 -/
Std.Http.URI.IsAllowedEncodedChars : (UInt8 → Bool) → ByteArray → Prop
-- Mathlib.MeasureTheory.Integral.IntegrableOn
ContinuousAt.stronglyMeasurableAtFilter : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace α]
  [OpensMeasurableSpace α] [SecondCountableTopologyEither α E] {f : α → E} {s : Set α} {μ : MeasureTheory.Measure α},
  IsOpen s → (∀ x ∈ s, ContinuousAt f x) → ∀ x ∈ s, StronglyMeasurableAtFilter f (nhds x) μ
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.counitAlgHom_apply : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (a : A),
  (Bialgebra.counitAlgHom R A) a = CoalgebraStruct.counit a
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- Auxiliary definition for `ran_isSheaf_of_isCocontinuous`  -/
CategoryTheory.RanIsSheafOfIsCocontinuous.isLimitMultifork : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {G : CategoryTheory.Functor C D} →
          {A : Type w} →
            [inst_2 : CategoryTheory.Category.{w', w} A] →
              {J : CategoryTheory.GrothendieckTopology C} →
                {K : CategoryTheory.GrothendieckTopology D} →
                  [G.IsCocontinuous J K] →
                    {F : CategoryTheory.Functor Cᵒᵖ A} →
                      CategoryTheory.Presheaf.IsSheaf J F →
                        {R : CategoryTheory.Functor Dᵒᵖ A} →
                          {α : G.op.comp R ⟶ F} →
                            (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension →
                              {X : D} → (S : K.Cover X) → CategoryTheory.Limits.IsLimit (S.multifork R)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLinkLocation.range : Lean.Elab.InlayHintLinkLocation → Lean.Syntax.Range
-- Lean.Level
Lean.Level.PP.Result.leaf : Lean.Name → Lean.Level.PP.Result
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TermElab : Type
-- Mathlib.Data.List.Perm.Basic
List.perm_insertIdx_iff : ∀ {α : Type u_1} {l₁ l₂ : List α} {n : ℕ} {a : α}, (l₁.insertIdx n a).Perm (l₂.insertIdx n a) ↔ l₁.Perm l₂
-- Mathlib.Algebra.Lie.OfAssociative
AlgEquiv.toLieEquiv_apply : ∀ {R : Type u} {A₁ : Type v} {A₂ : Type w} [inst : CommRing R] [inst_1 : Ring A₁] [inst_2 : Ring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁), e.toLieEquiv x = e x