mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.DivMod.Basic
/-- Integer division using the T-rounding convention.

In [the T-rounding convention][t-rounding] (division with truncation), all rounding is towards zero.
Division by 0 is defined to be 0. In this convention, `Int.tmod a b + b * (Int.tdiv a b) = a`.

[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862

This function is overridden by the compiler with an efficient implementation. This definition is the
logical model.

Examples:
* `(7 : Int).tdiv (0 : Int) = 0`
* `(0 : Int).tdiv (7 : Int) = 0`
* `(12 : Int).tdiv (6 : Int) = 2`
* `(12 : Int).tdiv (-6 : Int) = -2`
* `(-12 : Int).tdiv (6 : Int) = -2`
* `(-12 : Int).tdiv (-6 : Int) = 2`
* `(12 : Int).tdiv (7 : Int) = 1`
* `(12 : Int).tdiv (-7 : Int) = -1`
* `(-12 : Int).tdiv (7 : Int) = -1`
* `(-12 : Int).tdiv (-7 : Int) = 1`
 -/
Int.tdiv : ℤ → ℤ → ℤ
-- Init.Data.BitVec.Lemmas
BitVec.toNat_toInt_of_msb : ∀ {w : ℕ} (b : BitVec w), b.msb = false → b.toInt.toNat = b.toNat
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A category with binary coproducts has a functorial `sup` operation on over categories.  -/
CategoryTheory.Over.coprod : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasBinaryCoproducts C] →
      {A : C} →
        CategoryTheory.Functor (CategoryTheory.Over A)
          (CategoryTheory.Functor (CategoryTheory.Over A) (CategoryTheory.Over A))
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.lintegral_fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {g : β → ENNReal},
  Measurable g → ∫⁻ (c : β), g c ∂κ.fst a = ∫⁻ (bc : β × γ), g bc.1 ∂κ a
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.dvd_lcm : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} {b : β}, b ∈ s → f b ∣ s.lcm f
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (x : ↥X) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap e.inv (e.hom x))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap e.hom x) h) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom h
-- Init.Data.SInt.Lemmas
Int32.ofInt_eq_ofIntLE_div : ∀ {a b : ℤ} (ha₁ : Int32.minValue.toInt ≤ a) (ha₂ : a ≤ Int32.maxValue.toInt) (hb₁ : Int32.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int32.maxValue.toInt), Int32.ofInt (a.tdiv b) = Int32.ofIntLE a ha₁ ha₂ / Int32.ofIntLE b hb₁ hb₂
-- Lean.LabelAttribute
/-- Store the current `LabelExtension`s.  -/
Lean.labelExtensionMapRef : IO.Ref Lean.LabelExtensionMap
-- Lean.Server.Rpc.Basic
/-- Creates an `WithRpcRef` instance with a unique `id`.
As long as the client holds at least one reference to this `WithRpcRef`,
serving it again will yield the same client-side reference.
Thus, when used as React deps,
client-side references can help preserve UI state across RPC requests.
 -/
Lean.Server.WithRpcRef.mk : {α : Type} → α → BaseIO (Lean.Server.WithRpcRef α)
-- Mathlib.NumberTheory.NumberField.EquivReindex
NumberField.canonicalEmbedding_eq_basisMatrix_mulVec : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α : K),
  (NumberField.canonicalEmbedding K) α =
    (NumberField.basisMatrix K).transpose.mulVec fun i =>
      ↑((((NumberField.integralBasis K).reindex (NumberField.equivReindex K).symm).repr α) i)
-- Init.Control.Option
OptionT.instMonadExceptOf : {m : Type u → Type v} → (ε : Type u) → [MonadExceptOf ε m] → MonadExceptOf ε (OptionT m)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
algebraMap_le_of_le_spectrum : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {r : R} {a : A},
  (∀ x ∈ spectrum R a, r ≤ x) → autoParam (p a) algebraMap_le_of_le_spectrum._auto_1 → (algebraMap R A) r ≤ a
-- Mathlib.Algebra.Free
FreeAddSemigroup.hom_ext : ∀ {α : Type u} {β : Type v} [inst : Add β] {f g : FreeAddSemigroup α →ₙ+ β},
  ⇑f ∘ FreeAddSemigroup.of = ⇑g ∘ FreeAddSemigroup.of → f = g
-- Std.Http.Protocol.H1.Parser
/-- Parses the size and extensions of a chunk.
 -/
Std.Http.Protocol.H1.parseChunkSize : Std.Http.Protocol.H1.Config →
  Std.Internal.Parsec.ByteArray.Parser (ℕ × Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue))
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.map_pow : ∀ {R : Type u_4} {S : Type u_5} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S) (a : R) (n : ℕ),
  f (a ^ n) = f a ^ n
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t₁ t₂ : Finset α}, s - (t₁ ∪ t₂) = s - t₁ ∪ (s - t₂)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_iSup : ∀ {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ι → G.Subgraph), (⨆ i, f i).edgeSet = ⋃ i, (f i).edgeSet
-- Plausible.Testable
Plausible.Iff.printableProp : {x y : Prop} → [Plausible.PrintableProp x] → [Plausible.PrintableProp y] → Plausible.PrintableProp (x ↔ y)
-- Mathlib.Order.JordanHolder
CompositionSeries.le_last : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X} (i : Fin (s.length + 1)),
  s.toFun i ≤ RelSeries.last s
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_left_add : ∀ {α : Type u} [inst : Ring α] (x y : α), Ideal.span {x, x + y} = Ideal.span {x, y}
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.IsCofibrant.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X X_1 : C),
  X = X_1 → HomotopicalAlgebra.IsCofibrant X = HomotopicalAlgebra.IsCofibrant X_1
-- Mathlib.Geometry.Manifold.Algebra.SMul
/-- For any `G` in which multiplication is Cⁿ, the action of `G` on itself via left multiplication
is Cⁿ too.  -/
ContMDiffMul.contMDiffSMul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_8}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Mul G] {n : WithTop ℕ∞} [ContMDiffMul I n G],
  ContMDiffSMul I I n G G
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.mem_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} [K.IsStableUnderComposition]
  [K.HasIsos] {X : C} {E F : CategoryTheory.PreZeroHypercover X} (e : E ≅ F),
  E.presieve₀ ∈ K.coverings X → F.presieve₀ ∈ K.coverings X
-- Init.Data.UInt.Lemmas
UInt32.ofInt_add : ∀ (x y : ℤ), UInt32.ofInt (x + y) = UInt32.ofInt x + UInt32.ofInt y
-- Mathlib.Algebra.Lie.Normalizer
LieSubmodule.mem_idealizer : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (N : LieSubmodule R L M) {x : L}, x ∈ N.idealizer ↔ ∀ (m : M), ⁅x, m⁆ ∈ N
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WP.wp_consequence_le : ∀ {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] (x : Prog)
  (post post' : Value → Pred) (epost : EPred),
  Lean.Order.PartialOrder.rel post post' →
    ∀ {pre : Pred},
      Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post epost) →
        Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post' epost)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.update.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ) (a : R),
  p.update n a = { toFinsupp := AddMonoidAlgebra.update n a p.toFinsupp }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α} {h' : a ∈ t}, t.getKey a h' = t.getKeyD a fallback
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.ofLinearEquiv_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f : M ≃ₗ[R] M)
  (x : M), LinearMap.GeneralLinearGroup.ofLinearEquiv f • x = f x
-- Lean.Elab.Do.InferControlInfo
/-- Represents information about what control effects a `do` block has.

The fields split by flavor:

* `breaks`, `continues`, `returnsEarly`, and `reassigns` are **syntactic**: `true`/non-empty iff
  the corresponding construct appears anywhere in the source text of the block, independent of
  whether it is semantically reachable. Downstream elaborators must assume every such syntactic
  effect may occur, because the elaborator visits every doElem (only top-level
  `return`/`break`/`continue` short-circuit via `elabAsSyntacticallyDeadCode`).
* `numRegularExits` is also **syntactic**: the number of times the block wires the enclosing
  continuation into its elaborated expression. `withDuplicableCont` reads it as a join-point
  duplication trigger (`> 1`).
* `noFallthrough = true` asserts that the next doElem in the enclosing sequence is semantically
  irrelevant (control never falls through to it). `noFallthrough = false` makes no such
  assertion. The dead-code warning fires on the next element when this is `true`.

Invariant: `numRegularExits = 0 → noFallthrough`. The converse does not hold.
 -/
Lean.Elab.Do.ControlInfo : Type
-- Mathlib.Algebra.Group.Defs
AddLeftCancelMonoid.toAddMonoid : {M : Type u} → [self : AddLeftCancelMonoid M] → AddMonoid M
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : N →ₗ[R] N) (n : ℕ),
  LinearMap.lTensor M f ^ n = LinearMap.lTensor M (f ^ n)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.memLp_stoppedProcess : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {μ : MeasureTheory.Measure Ω}
  {τ : Ω → WithTop ι} {E : Type u_4} {p : ENNReal} {u : ι → Ω → E} [inst_1 : LinearOrder ι]
  [inst_2 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : MeasureTheory.Filtration ι m}
  [inst_5 : NormedAddCommGroup E] [LocallyFiniteOrderBot ι],
  MeasureTheory.IsStoppingTime ℱ τ →
    (∀ (n : ι), MeasureTheory.MemLp (u n) p μ) → ∀ (n : ι), MeasureTheory.MemLp (MeasureTheory.stoppedProcess u τ n) p μ
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.neg.instSFinite : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Neg G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ],
  MeasureTheory.SFinite μ.neg
-- Init.Data.Range.Polymorphic.UInt
UInt16.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE UInt16
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Complex.volume_closedBall : ∀ (a : ℂ) (r : ℝ), MeasureTheory.volume (Metric.closedBall a r) = ENNReal.ofReal r ^ 2 * ↑NNReal.pi
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_add_eq_mk_right : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk b < ArchimedeanClass.mk a → ArchimedeanClass.mk (a + b) = ArchimedeanClass.mk b
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.ofLinear_symm_toLinearMap : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂)
  (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f ∘ₛₗ g = LinearMap.id} {h₂ : g ∘ₛₗ f = LinearMap.id},
  ↑(LinearEquiv.ofLinear f g h₁ h₂).symm = g
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux1 : {α : Type u} →
  List (Computation α) × Stream'.WSeq (Computation α) → α ⊕ List (Computation α) × Stream'.WSeq (Computation α)
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.curr : ∀ {l r : List Char} {it : String.Legacy.Iterator}, String.Legacy.Iterator.ValidFor l r it → it.curr = r.headD default
-- Lean.Util.Trace
Lean.instInhabitedTraceElem.default : Lean.TraceElem
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.lowerEquivalence_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : C} {B : D} (e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B),
  (CategoryTheory.Subobject.lowerEquivalence e).inverse = CategoryTheory.Subobject.lower e.inverse
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.mem_interior_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} {a : α},
  a ∈ interior s ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
-- Mathlib.Data.List.Cycle
List.nextOr_getLast_of_notMem_dropLast : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} (hl : l ≠ []),
  l.getLast hl ∉ l.dropLast → ∀ (d : α), l.nextOr (l.getLast hl) d = d
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.HasEval.mul_left : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : TopologicalSpace S] [IsLinearTopology S S] (c : S) {x : S},
  PowerSeries.HasEval x → PowerSeries.HasEval (c * x)
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
/-- Convert a `CNF Nat` with a certain maximum variable number into the `DefaultFormula`
format for usage with `bv_decide`'s `LRAT.Internal`.

Notably this:
1. Increments all variables as DIMACS variables start at 1 instead of 0
2. Adds a leading `none` clause. This clause *must* be persistent as the LRAT checker wants to have
  the DIMACS file line by line and the DIMACS file begins with the `p cnf x y` meta instruction.
 -/
Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT : (cnf : Std.Sat.CNF ℕ) → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula (cnf.numLiterals + 1)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_closure_range_iff_nat : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {e : β → α} {a : α},
  a ∈ closure (Set.range e) ↔ ∀ (n : ℕ), ∃ k, dist a (e k) < 1 / (↑n + 1)
-- Init.Data.SInt.Lemmas
Int16.one_mul : ∀ (a : Int16), 1 * a = a
-- Init.Data.SInt.Lemmas
ISize.ofInt_add : ∀ (a b : ℤ), ISize.ofInt (a + b) = ISize.ofInt a + ISize.ofInt b
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `NormedSpace 𝕜 E` instance from a `NormedSpace.Core`. This is meant to be used
on types where the `NormedAddCommGroup E` instance has also been defined using `core`.
See note [reducible non-instances].  -/
NormedSpace.ofCore : {𝕜 : Type u_8} →
  {E : Type u_9} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module 𝕜 E] → NormedSpace.Core 𝕜 E → NormedSpace 𝕜 E
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!_le_max!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → ∀ {k : α}, (cmp t.max! (t.insert k).max!).isLE = true
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_iff_equalizerSieve_mem_imp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂),
  CategoryTheory.Presheaf.IsLocallyInjective J φ ↔
    ∀ ⦃X : Cᵒᵖ⦄ (x y : CategoryTheory.ToType (F₁.obj X)),
      CategoryTheory.Presheaf.equalizerSieve ((CategoryTheory.ConcreteCategory.hom (φ.app X)) x)
            ((CategoryTheory.ConcreteCategory.hom (φ.app X)) y) ∈
          J (Opposite.unop X) →
        CategoryTheory.Presheaf.equalizerSieve x y ∈ J (Opposite.unop X)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.map_comp : ∀ {R : CommRingCat} {M N P : ModuleCat ↑R} (f : M ⟶ N) (g : N ⟶ P),
  AlgebraicGeometry.tilde.map (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map f) (AlgebraicGeometry.tilde.map g)
-- Mathlib.Data.Set.Lattice
Set.biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ : ∀ {α : Type u_1} {ι : Type u_12} {Es : ι → Set α},
  ⋃ i, Es i = Set.univ → (Pairwise fun i j => Disjoint (Es i) (Es j)) → ∀ (I : Set ι), (⋃ i ∈ I, Es i)ᶜ = ⋃ i ∈ Iᶜ, Es i
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- the composition of morphisms  -/
CategoryTheory.SmallCategoryOfSet.comp : {Ω : Type w} →
  (self : CategoryTheory.SmallCategoryOfSet Ω) →
    {X Y Z : ↑self.obj} → ↑(self.hom X Y) → ↑(self.hom Y Z) → ↑(self.hom X Z)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- Note that this is an equality of elements of `ℝ≥0∞`. See also
`MeasureTheory.FiniteMeasure.map_apply` for the corresponding equality as elements of `ℝ≥0`.  -/
MeasureTheory.FiniteMeasure.map_apply' : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν : MeasureTheory.FiniteMeasure Ω) {f : Ω → Ω'},
  AEMeasurable f ↑ν → ∀ {A : Set Ω'}, MeasurableSet A → ↑(ν.map f) A = ↑ν (f ⁻¹' A)
-- Mathlib.LinearAlgebra.Dimension.Basic
rank_range_of_injective : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (f : M →ₗ[R] M₁),
  Function.Injective ⇑f → Module.rank R ↥f.range = Module.rank R M
-- Mathlib.Tactic.Ring.Common
/-- Equality test for expressions. This is not a `BEq` instance because it is heterogeneous.  -/
Mathlib.Tactic.Ring.Common.ExProd.eq : Mathlib.Tactic.Ring.Common.RingCompare Mathlib.Tactic.Ring.Common.btℕ →
  {u : Lean.Level} →
    {α : Q(Type u)} →
      {bt : Q(«$α») → Type} →
        {sα : Q(CommSemiring «$α»)} →
          Mathlib.Tactic.Ring.Common.RingCompare bt →
            {a b : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExProd bt sα a → Mathlib.Tactic.Ring.Common.ExProd bt sα b → Bool
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- Right homotopic edges represent the same morphism in the homotopy category.
 -/
SSet.Truncated.HomotopicR.congr_homotopyCategory₂HomMk : ∀ {A : SSet.Truncated 2} [inst : A.Quasicategory₂]
  {x y : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f g : SSet.Truncated.Edge x y},
  SSet.Truncated.HomotopicR f g → SSet.Truncated.HomotopyCategory₂.homMk f = SSet.Truncated.HomotopyCategory₂.homMk g
-- Mathlib.Topology.Constructions.SumProd
Continuous.comp₄ : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} {ε : Type u_3} {ζ : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W]
  [inst_4 : TopologicalSpace ε] [inst_5 : TopologicalSpace ζ] {g : X × Y × Z × ζ → ε},
  Continuous g →
    ∀ {e : W → X},
      Continuous e →
        ∀ {f : W → Y},
          Continuous f →
            ∀ {k : W → Z}, Continuous k → ∀ {l : W → ζ}, Continuous l → Continuous fun w => g (e w, f w, k w, l w)
-- Mathlib.Combinatorics.Additive.Corner.Defs
IsCorner.snd_fst_mem : ∀ {G : Type u_1} [inst : AddCommMonoid G] {A : Set (G × G)} {x₁ y₁ x₂ y₂ : G}, IsCorner A x₁ y₁ x₂ y₂ → (x₂, y₁) ∈ A
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.gc : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  GaloisConnection (IntermediateField.adjoin F) fun x => ↑x
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.instMkEvalWhiskerLeftBicategoryM : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft Mathlib.Tactic.Bicategory.BicategoryM
-- Mathlib.RingTheory.Etale.QuasiFinite
Ideal.eq_of_comap_eq_comap_of_bijective_residueFieldMap : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : CommRing S]
  [inst_3 : Algebra R R'] [inst_4 : Algebra R S] {p : Ideal R} {q : Ideal R'} [inst_5 : p.IsPrime] [inst_6 : q.IsPrime]
  [inst_7 : q.LiesOver p],
  Function.Bijective ⇑(Ideal.ResidueField.mapₐ p q (Algebra.ofId R R') ⋯) →
    ∀ (P₁ P₂ : Ideal (TensorProduct R R' S)) [P₁.IsPrime] [P₂.IsPrime] [P₁.LiesOver q] [P₂.LiesOver q],
      Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P₁ =
          Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P₂ →
        P₁ = P₂
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.prodCongr_symm : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] [inst_3 : UniformSpace δ] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ),
  (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm
-- Mathlib.Data.Finset.Defs
Finset.mk.congr_simp : ∀ {α : Type u_4} (val val_1 : Multiset α) (e_val : val = val_1) (nodup : val.Nodup),
  { val := val, nodup := nodup } = { val := val_1, nodup := ⋯ }
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
MeasureTheory.measure_le_eq_lt : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [FiniteDimensional ℝ E] [mE : MeasurableSpace E]
  [tE : TopologicalSpace E] [IsTopologicalAddGroup E] [BorelSpace E] [T2Space E] [ContinuousSMul ℝ E]
  (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {g : E → ℝ},
  g 0 = 0 →
    (∀ (x : E), g (-x) = g x) →
      (∀ (x y : E), g (x + y) ≤ g x + g y) →
        (∀ {x : E}, g x = 0 → x = 0) →
          (∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x) → ∀ [Nontrivial E] (r : ℝ), μ {x | g x ≤ r} = μ {x | g x < r}
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_left_injective : ∀ {x : ℝ}, x ≠ 0 → Function.Injective fun y => y ^ x
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- The derivative of the zero section of the tangent bundle maps `⟨x, v⟩` to `⟨⟨x, 0⟩, ⟨v, 0⟩⟩`.

Note that, as currently framed, this is a statement in coordinates, thus reliant on the choice
of the coordinate system we use on the tangent bundle.

However, the result itself is coordinate-dependent only to the extent that the coordinates
determine a splitting of the tangent bundle.  Moreover, there is a canonical splitting at each
point of the zero section (since there is a canonical horizontal space there, the tangent space
to the zero section, in addition to the canonical vertical space which is the kernel of the
derivative of the projection), and this canonical splitting is also the one that comes from the
coordinates on the tangent bundle in our definitions. So this statement is not as crazy as it
may seem.

TODO define splittings of vector bundles; state this result invariantly.  -/
TangentBundle.tangentMap_tangentBundle_pure : ∀ {𝕜 : 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] [Is : IsManifold I 1 M] (p : TangentBundle I M),
  tangentMap I I.tangent (Bundle.zeroSection E (TangentSpace I)) p = ⟨⟨p.proj, 0⟩, (p.snd, 0)⟩
-- Mathlib.Data.Fintype.EquivFin
Function.Embedding.exists_of_card_eq_finset : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] {s : Finset β},
  Fintype.card α = s.card → ∃ f, Finset.map f Finset.univ = s
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.divRight_symm_apply : ∀ {G : Type u_5} [inst : Group G] (a b : G), (Equiv.divRight a).symm b = b * a