mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.zipWithAll.eq_1 : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} (f : Option α → Option β → γ) (as : Array α) (bs : Array β),
  Array.zipWithAll f as bs = Array.zipWithAll.go✝ f as bs 0 #[]
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.self_le_maxKey_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (cmp k ((t.insert k v).maxKey ⋯)).isLE = true
-- Mathlib.Topology.Algebra.SeparationQuotient.Hom
SeparationQuotient.liftContinuousMonoidHom.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : CommMonoid M]
  [inst_3 : ContinuousMul M] [inst_4 : CommMonoid N] (f : M →ₜ* N) (hf : ∀ (x y : M), Inseparable x y → f x = f y),
  SeparationQuotient.liftContinuousMonoidHom f hf =
    { toFun := SeparationQuotient.lift (⇑f) hf, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.uniformity_dist : ∀ {α : Type u} [self : PseudoMetricSpace α], uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε}
-- Mathlib.Combinatorics.Enumerative.Schroder
_private.Mathlib.Combinatorics.Enumerative.Schroder.0.Nat.largeSchroder.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.FiniteAdeleRing.algebraMap_apply : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (k : K) (v : IsDedekindDomain.HeightOneSpectrum R),
  ((algebraMap K (IsDedekindDomain.FiniteAdeleRing R K)) k) v =
    { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm k) }
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.map_objAppend1 : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α γ : TypeVec.{u} n} (g : α.Arrow γ) (a : P.A) (f' : (P.drop.B a).Arrow α)
  (f : P.last.B a → P.W α),
  MvFunctor.map (g ::: P.wMap g) (P.objAppend1 a f' f) = P.objAppend1 a (TypeVec.comp g f') fun x => P.wMap g (f x)
-- Init.Data.Bool
Bool.decide_eq_false : ∀ {b : Bool} {x : Decidable (b = false)}, decide (b = false) = !b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.inclusion_rfl : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] {S₁ : AffineSubspace k P₁} [inst_4 : Nonempty ↥S₁],
  AffineSubspace.inclusion ⋯ = AffineMap.id k ↥S₁
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.prodIso_hom : ∀ {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex),
  (A.prodIso B).hom =
    CategoryTheory.CartesianMonoidalCategory.lift
      (SSet.Subcomplex.lift
        (CategoryTheory.CategoryStruct.comp (A.prod B).ι (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) ⋯)
      (SSet.Subcomplex.lift
        (CategoryTheory.CategoryStruct.comp (A.prod B).ι (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) ⋯)
-- Aesop.Tree.Data
Aesop.MVarCluster.instNonempty : Nonempty Aesop.MVarCluster
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Structure which contains the data and properties for a morphism `h` satisfying
`Presieve.bind S R h`.  -/
CategoryTheory.Presieve.BindStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (S : CategoryTheory.Presieve X) →
        (⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y) → {Z : C} → (Z ⟶ X) → Type (max u₁ v₁)
-- Mathlib.Topology.Constructions.SumProd
prod_mem_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y} {x : X}
  {y : Y}, s ∈ nhds x → t ∈ nhds y → s ×ˢ t ∈ nhds (x, y)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- A morphism property `P` satisfies `P.RespectsRight Q` if it is stable under post-composition
with morphisms satisfying `Q`, i.e. whenever `P` holds for `f` and `Q` holds for `i` then `P`
holds for `f ≫ i`.  -/
CategoryTheory.MorphismProperty.RespectsRight : {C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorObj_comm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  {Z : C} (h : CategoryTheory.SmallObject.functorObj f πX ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjLeft f πX)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ρFunctorObj f πX) h)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.lift_card_closure_le_card_term : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M},
  Cardinal.lift.{max u w, w} (Cardinal.mk ↥((FirstOrder.Language.Substructure.closure L).toFun s)) ≤
    Cardinal.mk (L.Term ↑s)
-- Mathlib.Algebra.Order.Floor.Div
/-- Do not use this. Use `zero_floorDiv` instead.  -/
FloorDiv.zero_floorDiv : ∀ {α : Type u_2} {β : Type u_3} {inst : AddCommMonoid α} {inst_1 : PartialOrder α} {inst_2 : AddCommMonoid β}
  {inst_3 : PartialOrder β} {inst_4 : SMulZeroClass α β} [self : FloorDiv α β] (a : α), 0 ⌊/⌋ a = 0
-- Mathlib.Analysis.BoxIntegral.Basic
/-- A continuous function is box-integrable with respect to any locally finite measure.

This is true for any volume with bounded variation.  -/
BoxIntegral.integrable_of_continuousOn : ∀ {ι : Type u} {E : Type v} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : Fintype ι]
  (l : BoxIntegral.IntegrationParams) [CompleteSpace E] {I : BoxIntegral.Box ι} {f : (ι → ℝ) → E},
  ContinuousOn f (BoxIntegral.Box.Icc I) →
    ∀ (μ : MeasureTheory.Measure (ι → ℝ)) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ],
      BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul
-- Std.Data.Internal.List.Associative
Std.Internal.List.size_filter_not_contains_add_size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α},
  Std.Internal.List.DistinctKeys l₁ →
    (List.filter (fun p => !l₂.contains p.fst) l₁).length + (List.filter (fun p => l₂.contains p.fst) l₁).length =
      l₁.length
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.valueGroup_def : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : MonoidWithZero B] (f : A →*₀ B),
  f.valueGroup = Subgroup.closure ↑f.valueMonoid
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.curryLinearEquiv_apply : ∀ {α : Type u_9} {β : Type u_10} (R : Type u_11) {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (a : α × β →₀ M), (Finsupp.curryLinearEquiv R) a = a.curry
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.div_of_ne_zero : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0),
  I / J = ⟨↑I / ↑J, ⋯⟩
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagInfo.target : Lean.Meta.Grind.EMatchDiagInfo → Lean.Meta.Grind.EMatchDiagNode
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
/-- If `R : ProjectiveResolution X`, this is the cochain complex indexed by `ℤ`
obtained by extending by zero the chain complex `R.complex` indexed by `ℕ`.  -/
CategoryTheory.ProjectiveResolution.cochainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Preadditive C] → {X : C} → CategoryTheory.ProjectiveResolution X → CochainComplex C ℤ
-- Mathlib.Algebra.Ring.Pointwise.Finset
Finset.add_mul_subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Distrib α] (s t u : Finset α), (s + t) * u ⊆ s * u + t * u
-- Mathlib.CategoryTheory.EqToHom
/-- `eqToHom h` is heterogeneously equal to the identity of its domain.  -/
CategoryTheory.eqToHom_heq_id_dom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X Y : C) (h : X = Y),
  CategoryTheory.eqToHom h ≍ CategoryTheory.CategoryStruct.id X
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime.eq_def : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ)
  (N : ι) (x : ℕ),
  MeasureTheory.upperCrossingTime a b f N x =
    match (motive := ℕ → Ω → ι) x with
    | 0 => ⊥
    | n.succ => fun ω =>
      MeasureTheory.hittingBtwn f (Set.Ici b)
        (MeasureTheory.lowerCrossingTimeAux a f (MeasureTheory.upperCrossingTime a b f N n ω) N ω) N ω
-- Mathlib.Algebra.Group.Hom.Defs
/-- Group homomorphisms preserve division.  -/
MonoidHom.map_mul_inv : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] (f : α →* β) (g h : α),
  f (g * h⁻¹) = f g * (f h)⁻¹
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.ComposableArrows.sc.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} (S S_1 : CategoryTheory.ComposableArrows C n) (e_S : S = S_1) (hS : S.IsComplex) (i i_1 : ℕ) (e_i : i = i_1)
  (hi : i + 2 ≤ n), S.sc hS i hi = S_1.sc ⋯ i_1 ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Taking the multicoequalizer over the multispan index is equivalent to taking the coequalizer
over the two morphisms `∐ I.left ⇉ ∐ I.right`. This is the diagram of the latter for colimiting
cofans.  -/
CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        {c : CategoryTheory.Limits.Cofan I.left} →
          CategoryTheory.Limits.Cofan I.right →
            CategoryTheory.Limits.IsColimit c → CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
-- Aesop.Index.Basic
Aesop.IndexingMode.brecOn.go : {motive_1 : Aesop.IndexingMode → Sort u} →
  {motive_2 : Array Aesop.IndexingMode → Sort u} →
    {motive_3 : List Aesop.IndexingMode → Sort u} →
      (t : Aesop.IndexingMode) →
        ((t : Aesop.IndexingMode) → t.below → motive_1 t) →
          ((t : Array Aesop.IndexingMode) → Aesop.IndexingMode.below_1 t → motive_2 t) →
            ((t : List Aesop.IndexingMode) → Aesop.IndexingMode.below_2 t → motive_3 t) → motive_1 t ×' t.below
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_symm_toIsometryEquiv : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑e.toIsometryEquiv.symm = ⇑e.symm
-- Init.Data.Nat.Lemmas
Nat.mul_right_cancel_iff : ∀ {m : ℕ}, 0 < m → ∀ {n k : ℕ}, n * m = k * m ↔ n = k
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.ext_iff : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] {f g : P1 →ᵃ[k] P2}, f = g ↔ ∀ (p : P1), f p = g p
-- Aesop.Forward.PremiseIndex
Aesop.instInhabitedPremiseIndex.default : Aesop.PremiseIndex
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.fold_eq_foldl_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.DHashMap.Raw.fold (fun d a x => f d a) init ↑m = List.foldl f init (↑m).keys
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.coe_smul : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  {M : Type u_3} [inst_3 : Zero R] [inst_4 : SMulZeroClass M R] [inst_5 : ContinuousConstSMul M R] (m : M)
  (f : ContinuousMapZero X R), ⇑(m • f) = m • ⇑f
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_mkSlice_roc : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = (Std.Slice.toArray xs).extract (lo + 1) (hi + 1)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.singleton_injective : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α], Function.Injective fun x => {x}
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_one : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R] [inst_1 : One R], QuaternionAlgebra.imJ 1 = 0
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_add : ∀ {a b : ℕ} (hab : a + b < 2 ^ 64), UInt64.ofNatLT (a + b) hab = UInt64.ofNatLT a ⋯ + UInt64.ofNatLT b ⋯
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.map_zero : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} [inst_2 : OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J}
  (self : d.Extension val₀ j),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) self.val = val₀
-- Mathlib.Data.Rel.Cover
SetRel.IsCover.mono : ∀ {X : Type u_1} {U : SetRel X X} {s N₁ N₂ : Set X}, N₁ ⊆ N₂ → U.IsCover s N₁ → U.IsCover s N₂
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_eq_empty_iff_eq_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R},
  p.vars = ∅ ↔ p = MvPolynomial.C (MvPolynomial.coeff 0 p)
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Product of subrings is isomorphic to their product as rings.  -/
Subring.prodEquiv : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocRing R] → [inst_1 : NonAssocRing S] → (s : Subring R) → (t : Subring S) → ↥(s.prod t) ≃+* ↥s × ↥t
-- Mathlib.RingTheory.Ideal.Operations
/-- `Submonoid.map` as an `AlgHom`, when applied to an `AlgHom`.  -/
Submodule.mapAlgHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → Submodule R A →ₐ[Ideal R] Submodule R B
-- Mathlib.Topology.Compactness.Compact
/-- For every open cover of a compact set, there exists a finite subcover.  -/
IsCompact.elim_finite_subcover_image : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set X} {b : Set ι} {c : ι → Set X},
  IsCompact s → (∀ i ∈ b, IsOpen (c i)) → s ⊆ ⋃ i ∈ b, c i → ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.IsSchemeTheoreticallyDominant.isReduced : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsSchemeTheoreticallyDominant f]
  [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.IsReduced X], AlgebraicGeometry.IsReduced Y
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β], ⇑0 = 0
-- Mathlib.Order.LiminfLimsup
/-- If `f : α → α` is a morphism of complete lattices, then the limsup of its iterates of any
`a : α` is a fixed point.  -/
CompleteLatticeHom.apply_limsup_iterate : ∀ {α : Type u_1} [inst : CompleteLattice α] (f : CompleteLatticeHom α α) (a : α),
  f (Filter.limsup (fun n => (⇑f)^[n] a) Filter.atTop) = Filter.limsup (fun n => (⇑f)^[n] a) Filter.atTop
-- Init.Data.List.MinMaxOn
List.maxOn?_nil : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β}, List.maxOn? f [] = none
-- Mathlib.Tactic.Abel
/-- A type synonym used by `abel` to represent `n • x + a` in an additive commutative group.  -/
Mathlib.Tactic.Abel.termg_eq : ∀ {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x a : α), Mathlib.Tactic.Abel.termg n x a = n • x + a
-- Mathlib.Algebra.Order.Group.Defs
lt_inv_self_iff : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {a : α}, a < a⁻¹ ↔ a < 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraRing.reverse_eq_id : ∀ {R : Type u_1} [inst : CommRing R], CliffordAlgebra.reverse = LinearMap.id
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.pullback_symm_apply_snd : ∀ {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : TopologicalSpace F] [inst_3 : TopologicalSpace B]
  [inst_4 : ∀ (_b : B), Nonempty (E _b)] {K : Type U} [inst_5 : FunLike K B' B] [inst_6 : ContinuousMapClass K B' B]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (f : K) (y : B' × F),
  (↑(e.pullback f).symm y).snd = e.symm (f y.1) y.2
-- Mathlib.Data.Nat.Choose.Basic
Nat.multichoose_one : ∀ (k : ℕ), Nat.multichoose 1 k = 1
-- Mathlib.CategoryTheory.GradedObject.Associator
CategoryTheory.GradedObject.ι_mapBifunctorAssociator_hom : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)}
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J}
  (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_6 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [inst_8 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_9 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
  [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J)
  (h : r (i₁, i₂, i₃) = j),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j) =
    CategoryTheory.CategoryStruct.comp (((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
      (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
-- Mathlib.Data.Set.Card
Set.ncard_le_one_iff_subsingleton : ∀ {α : Type u_1} {s : Set α} [Finite ↑s], s.ncard ≤ 1 ↔ s.Subsingleton
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_involutive : ∀ {R : Type u_1} [inst : Semiring R], Function.Involutive Polynomial.mirror
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.allTR.loop.congr_simp : ∀ (n : ℕ) (f f_1 : (i : ℕ) → i < n → Bool),
  f = f_1 → ∀ (i i_1 : ℕ) (e_i : i = i_1) (a : i ≤ n), Nat.allTR.loop✝ n f i a = Nat.allTR.loop✝ n f_1 i_1 ⋯
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.mk : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R →+* R₂} →
          {σ₂₁ : R₂ →+* R} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {E : Type u_11} →
                  {E₂ : Type u_12} →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] →
                          [inst_7 : Module R₂ E₂] →
                            (toLinearEquiv : E ≃ₛₗ[σ₁₂] E₂) → (∀ (x : E), ‖toLinearEquiv x‖ = ‖x‖) → E ≃ₛₗᵢ[σ₁₂] E₂
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.weakEquivalences_unop_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {X Y : Cᵒᵖ} (f : X ⟶ Y), HomotopicalAlgebra.WeakEquivalence f.unop ↔ HomotopicalAlgebra.WeakEquivalence f
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Semiring.powFn? : Lean.Meta.Grind.Arith.CommRing.Semiring → Option Lean.Expr
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_div_ratCast : ∀ (q : ℚ) {x : ℝ}, Irrational (x / ↑q) → Irrational x
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nsmul_subset_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] {s t : Set α} {m n : ℕ}, s ⊆ t → 0 ∈ t → m ≤ n → m • s ⊆ n • t
-- Mathlib.Algebra.Algebra.Subalgebra.Prod
Subalgebra.prod_top : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B], ⊤.prod ⊤ = ⊤
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- `qrSign` is multiplicative in the second argument.  -/
qrSign.mul_right : ∀ (m n₁ n₂ : ℕ) [NeZero n₁] [NeZero n₂], qrSign m (n₁ * n₂) = qrSign m n₁ * qrSign m n₂
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The range of a surjective monoid homomorphism is the whole of the codomain.  -/
MonoidHom.range_eq_top_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_7} [inst_1 : Group N] (f : G →* N), Function.Surjective ⇑f → f.range = ⊤
-- Mathlib.Topology.ContinuousMap.Algebra
algebraMap_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_2} [inst_1 : CommSemiring R] {A : Type u_3}
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : IsTopologicalSemiring A] (k : R)
  (a : α), ((algebraMap R C(α, A)) k) a = k • 1
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonTextDocumentChangeRegistrationOptions.fromJson : Lean.Json → Except String Lean.Lsp.TextDocumentChangeRegistrationOptions
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.whiskerLeft_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g h : b ⟶ c)
  [inst_1 : CategoryTheory.BicategoricalCoherence g h],
  CategoryTheory.BicategoricalCoherence.iso =
    CategoryTheory.Bicategory.whiskerLeftIso f CategoryTheory.BicategoricalCoherence.iso
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mk : {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] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                (left : A) → (right : B) → (L.obj left ⟶ R.obj right) → CategoryTheory.Comma L R