mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Cardinal.Divisibility
Cardinal.dvd_of_le_of_aleph0_le : ∀ {a b : Cardinal.{u}}, a ≠ 0 → a ≤ b → Cardinal.aleph0 ≤ b → a ∣ b
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.liftCone_pt : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T}
  (s : D ⟶ (CategoryTheory.Functor.const J).obj X) (c : CategoryTheory.Limits.Cone D) (p : c.pt ⟶ X)
  (hp : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.π.app j) (s.app j) = p),
  (CategoryTheory.Over.liftCone D s c p hp).pt = CategoryTheory.Over.mk p
-- Mathlib.Data.Finset.Basic
Finset.choose_eq_iff : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : Finset α) (hp : ∃! a, a ∈ l ∧ p a) {a : α},
  Finset.choose p l hp = a ↔ a ∈ l ∧ p a
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.entails_true_intro : ∀ {σs : List (Type u)} (P Q : Std.Do.SPred σs), ⊢ₛ P → Q ↔ P ⊢ₛ Q
-- Mathlib.RingTheory.Polynomial.ShiftedLegendre
/-- The coefficient of the shifted Legendre polynomial at `k` is
`(-1) ^ k * (n.choose k) * (n + k).choose n`.  -/
Polynomial.coeff_shiftedLegendre : ∀ (n k : ℕ), (Polynomial.shiftedLegendre n).coeff k = (-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
groupCohomology.cocyclesMk.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {n : ℕ} (f f_1 : (Fin n → G) → ↑A)
  (e_f : f = f_1) (h : (CategoryTheory.ConcreteCategory.hom (inhomogeneousCochains.d A n)) f = 0),
  groupCohomology.cocyclesMk f h = groupCohomology.cocyclesMk f_1 ⋯
-- Mathlib.CategoryTheory.Equivalence
/-- The functor of an equivalence of categories is faithful.  -/
CategoryTheory.Equivalence.faithful_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  (e : C ≌ E), e.functor.Faithful
-- Mathlib.GroupTheory.Index
Subgroup.isFiniteRelIndex_iff_relIndex_ne_zero : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsFiniteRelIndex K ↔ H.relIndex K ≠ 0
-- Mathlib.Util.AtomM.Recurse
/-- The atom evaluator calls `AtomM.onSubexpressions` recursively.  -/
_private.Mathlib.Util.AtomM.Recurse.0.Mathlib.Tactic.AtomM.RecurseM.run.evalAtom : IO.Ref Mathlib.Tactic.AtomM.State →
  Mathlib.Tactic.AtomM.Recurse.Config →
    Bool →
      (Lean.Expr → Mathlib.Tactic.AtomM Lean.Meta.Simp.Result) →
        Mathlib.Tactic.AtomM.Recurse.Context → Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.refl : ∀ {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β), m.Equiv m
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Ico : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (a b : α i),
  Pi.single i '' Set.Ico a b = Set.Ico (Pi.single i a) (Pi.single i b)
-- Mathlib.Algebra.Lie.BaseChange
LieSubmodule.mk.congr_simp : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (toSubmodule toSubmodule_1 : Submodule R M)
  (e_toSubmodule : toSubmodule = toSubmodule_1)
  (lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier),
  { toSubmodule := toSubmodule, lie_mem := lie_mem } = { toSubmodule := toSubmodule_1, lie_mem := ⋯ }
-- Init.Data.String.Lemmas.Basic
String.ofList_cons : ∀ {c : Char} {l : List Char}, String.ofList (c :: l) = String.singleton c ++ String.ofList l
-- Std.Sync.Channel
/-- Send a value through the channel, blocking until the transmission could be completed.
 -/
Std.Channel.Sync.send : {α : Type} → Std.Channel.Sync α → α → BaseIO Unit
-- Mathlib.Analysis.Normed.Group.Defs
/-- the `ℝ≥0∞`-valued norm function.  -/
«term‖_‖ₑ» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Finset.finsuppAntidiagEquiv.eq_1 : ∀ {ι : Type u_1} [inst : DecidableEq ι] (s : Finset ι) (n : ℕ),
  s.finsuppAntidiagEquiv n = (s.finsuppAntidiagEquivSubtype n).trans (Sym.equivNatSum (↥s) n).symm
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- Pushforwards of finite submodules have a smaller finrank.  -/
Submodule.finrank_map_le : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M']
  [inst_3 : Module R M] [StrongRankCondition R] [inst_5 : Module R M'] (f : M →ₗ[R] M') (p : Submodule R M)
  [Module.Finite R ↥p], Module.finrank R ↥(Submodule.map f p) ≤ Module.finrank R ↥p
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.map_id : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  AdicCompletion.map I LinearMap.id = LinearMap.id
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- An affine-independent family of points in a finite-dimensional affine space is finite.  -/
finite_of_fin_dim_affineIndependent : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [FiniteDimensional k V] {p : ι → P}, AffineIndependent k p → Finite ι
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.rootOrdered_iff : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v : α} {p : RBTree.RBNode.Path α},
  RBTree.RBNode.Path.Ordered cmp p →
    (RBTree.RBNode.Path.RootOrdered cmp p v ↔
      (∀ a ∈ p.listL, RBTree.RBNode.cmpLT cmp a v) ∧ ∀ a ∈ p.listR, RBTree.RBNode.cmpLT cmp v a)
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.instIsPushout_1 : ∀ {R : Type u} [inst : CommSemiring R] {σ : Type u_1} {S : Type u_3} [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.IsPushout R (MvPolynomial σ R) S (MvPolynomial σ S)
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- Given `x` and `y` between `0` and `1`, `x` is between two successive powers of `y`.
This is the same as `exists_nat_pow_near`, but for elements between `0` and `1`  -/
exists_nat_pow_near_of_lt_one : ∀ {K : Type u_4} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K}
  [ExistsAddOfLE K], 0 < x → x ≤ 1 → 0 < y → y < 1 → ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n
-- Mathlib.Algebra.Symmetrized
SymAlg.instNontrivial : ∀ {α : Type u_1} [Nontrivial α], Nontrivial αˢʸᵐ
-- Mathlib.RingTheory.FreeCommRing
/-- The canonical ring homomorphism from the free ring generated by `α` to the free commutative ring
generated by `α`.  -/
FreeRing.toFreeCommRing : {α : Type u_1} → FreeRing α →+* FreeCommRing α
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.dist_eq_of_ne : ∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n}, x ≠ y → dist x y = (1 / 2) ^ PiNat.firstDiff x y
-- Std.Data.Internal.List.Associative
Std.Internal.List.find?_eq_none_iff_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α},
  List.find? (fun x => x.fst == k) l = none ↔ Std.Internal.List.containsKey k l = false
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] {inst_1 : DecidableEq α} [inst_2 : DecidableEq α] (σ σ_1 : Equiv.Perm α),
  σ = σ_1 → σ.cycleType = σ_1.cycleType
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_pos_of_ne : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, u ≠ v → 0 < G.edist u v
-- Mathlib.Topology.Homotopy.Path
/-- A reasoning principle for quotients that allows proofs about quotients to assume that all values are
constructed with `Quotient.mk`.
 -/
Path.Homotopic.Quotient.ind : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X} {motive : Path.Homotopic.Quotient x y → Prop},
  (∀ (a : Path x y), motive (Path.Homotopic.Quotient.mk a)) → ∀ (q : Path.Homotopic.Quotient x y), motive q
-- Std.Data.DTreeMap.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the
proof obligation in the statement of `get_insertIfNew`.  -/
Std.DTreeMap.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {v : β k}, a ∈ t.insertIfNew k v → ¬(cmp k a = Ordering.eq ∧ k ∉ t) → a ∈ t
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.isPrimitiveClassified_of_coprime_of_zero_left : ∀ {x y z : ℤ} (h : PythagoreanTriple x y z), x.gcd y = 1 → x = 0 → h.IsPrimitiveClassified
-- Mathlib.Analysis.Convex.Between
wbtw_neg_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V}, Wbtw R (-x) (-y) (-z) ↔ Wbtw R x y z
-- Mathlib.LinearAlgebra.Dual.BaseChange
_private.Mathlib.LinearAlgebra.Dual.BaseChange.0.IsBaseChange.toDualBaseChangeAux.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] {A : Type u_4} [inst_5 : CommSemiring A] [inst_6 : Algebra R A]
  [inst_7 : Module A W] [inst_8 : IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j),
  IsBaseChange.toDualBaseChangeAux✝ ibc =
    { toAddHom := (TensorProduct.lift { toFun := fun a => a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }).toAddHom,
      map_smul' := ⋯ }
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_eq_eval₂Hom : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁) (p : MvPolynomial σ R), (MvPolynomial.aeval f) p = (MvPolynomial.eval₂Hom (algebraMap R S₁) f) p
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.isoMk_inv_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra}
  (h : A.A ≅ B.A)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom)
      CategoryTheory.Monad.Algebra.isoMk._auto_1),
  (CategoryTheory.Monad.Algebra.isoMk h w).inv.f = h.inv
-- Lean.MetavarContext
Lean.MetavarContext.MkBindingM.Context.mk : Lean.Name → Lean.LocalContext → Lean.MetavarContext.MkBindingM.Context
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.map_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (p : CategoryTheory.Presieve.FamilyOfElements P R) (φ : P ⟶ Q) {Y : C} (f : Y ⟶ X)
  (hf : R f), p.map φ f hf = (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) (p f hf)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
/-- If `μ` is an s-finite measure, then for any function `f`
there exists a measurable function `g ≤ f`
that has the same Lebesgue integral over every set.

For the integral over the whole space, the statement is true without extra assumptions,
see `exists_measurable_le_lintegral_eq`.
See also `MeasureTheory.Measure.restrict_toMeasurable_of_sFinite` for a similar result.  -/
MeasureTheory.exists_measurable_le_forall_setLIntegral_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (f : α → ENNReal),
  ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
-- Std.Async.System
/-- A user identifier, represented by a numeric ID in UNIX systems  (e.g. 1001).
 -/
Std.Async.System.UserId : Type
-- Init.Data.String.Basic
String.instLT : LT String
-- Mathlib.Order.Filter.Basic
/-- **Alias** of the forward direction of `Filter.eventuallyEq_set`. -/
Filter.EventuallyEq.mem_iff : ∀ {α : Type u} {s t : Set α} {l : Filter α}, s =ᶠ[l] t → ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_inj : ∀ {R : Type u_1} [inst : Ring R] {r : R} {p q : Polynomial R}, (Polynomial.taylor r) p = (Polynomial.taylor r) q ↔ p = q
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_symm : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x y : AlgebraicGeometry.Scheme.Pullback.Triplet f g}
  (e : x = y),
  (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e).symm =
    AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯
-- Mathlib.Topology.MetricSpace.Equicontinuity
/-- Characterization of equicontinuity for families of functions taking values in a (pseudo) metric
space.  -/
Metric.equicontinuousAt_iff_right : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : TopologicalSpace β]
  {F : ι → β → α} {x₀ : β}, EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhds x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
-- Init.Data.List.MinMaxIdx
List.maxIdxOn?_eq_some_zero_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β}, List.maxIdxOn? f xs = some 0 ↔ ∃ (h : xs ≠ []), ∀ x ∈ xs, f x ≤ f (xs.head h)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is a `Semigroup` under pointwise operations if `α` is.  -/
Set.semigroup : {α : Type u_2} → [Semigroup α] → Semigroup (Set α)
-- Mathlib.GroupTheory.OrderOfElement
zpowers_mabs : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (g : G),
  Subgroup.zpowers |g|ₘ = Subgroup.zpowers g
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.instIsOverHomOfLE : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (h : U ≤ V), AlgebraicGeometry.Scheme.Hom.IsOver (X.homOfLE h) X
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k a : α},
  (m.erase k).get? a = if (k == a) = true then none else m.get? a
-- Init.Data.Int.Gcd
Int.gcd_sub_mul_left_right : ∀ (m n k : ℤ), m.gcd (n - m * k) = m.gcd n
-- Mathlib.Data.Nat.Log
Nat.log_two_bit : ∀ {b : Bool} {n : ℕ}, n ≠ 0 → Nat.log 2 (Nat.bit b n) = Nat.log 2 n + 1
-- Init.Data.SInt.Lemmas
Int64.toISize_ofInt : ∀ {n : ℤ}, (Int64.ofInt n).toISize = ISize.ofInt n
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap f)
      (HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj Y) =
    CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj X) f
-- Init.Data.String.Decode
Char.utf8Size.eq_1 : ∀ (c : Char),
  c.utf8Size =
    if c.val ≤ UInt32.ofNatLT 127 Char.utf8Size._proof_1 then 1
    else
      if c.val ≤ UInt32.ofNatLT 2047 Char.utf8Size._proof_2 then 2
      else if c.val ≤ UInt32.ofNatLT 65535 Char.utf8Size._proof_3 then 3 else 4
-- Init.Data.List.TakeDrop
List.getElem?_take_of_succ : ∀ {α : Type u_1} {l : List α} {i : ℕ}, (List.take (i + 1) l)[i]? = l[i]?
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
AffineMap.restrict.linear_aux : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} {E : AffineSubspace k P₁}
  {F : AffineSubspace k P₂}, AffineSubspace.map φ E ≤ F → E.direction ≤ Submodule.comap φ.linear F.direction
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.isUnit_iff_norm : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.RingOfIntegers K},
  IsUnit x ↔ |↑((RingOfIntegers.norm ℚ) x)| = 1
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.coe_subRight : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G] (a : G),
  ⇑(Homeomorph.subRight a) = fun x => x - a
-- Mathlib.Algebra.Group.Basic
ite_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul β α] (p : Prop) [inst_1 : Decidable p] (a : α) (b c : β),
  (if p then b else c) • a = if p then b • a else c • a
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
HasStrictFDerivAt.pt_implicitFunctionDataOfProdDomain : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂]
  [inst_5 : NormedSpace 𝕜 E₂] [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {f'u : E₁ × E₂ →L[𝕜] F}
  (dfu : HasStrictFDerivAt f f'u u) (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  (dfu.implicitFunctionDataOfProdDomain if₂u).pt = u
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inl
      (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv =
    CategoryTheory.Limits.coprod.inl
-- Mathlib.Topology.Order.Priestley
PriestleySpace.toTotallySeparatedSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : PartialOrder α] [PriestleySpace α], TotallySeparatedSpace α
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.commRingNorm.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (e : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (p : Lean.Grind.CommRing.Poly),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.commRingNorm c e p) = 1 + sizeOf c + sizeOf e + sizeOf p
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.completeBipartiteGraphCongr_symm_apply : ∀ {V₁ : Type u_5} {V₂ : Type u_6} {W₁ : Type u_7} {W₂ : Type u_8} (hV : V₁ ≃ V₂) (hW : W₁ ≃ W₂) (a : V₂ ⊕ W₂),
  (RelIso.symm (SimpleGraph.completeBipartiteGraphCongr hV hW)) a = Sum.map (⇑hV.symm) (⇑hW.symm) a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_counitIso_hom_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T'),
  ((CategoryTheory.StructuredArrow.mapNatIso i).counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
_private.Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject.0.CategoryTheory.SimplicialObject.Splitting.fromNondegComplex.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C],
  s.fromNondegComplex =
    (CategoryTheory.Idempotents.fullyFaithfulToKaroubi (ChainComplex C ℕ)).preimage
      (CategoryTheory.CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.hom
        { f := AlgebraicTopology.DoldKan.PInfty, comm := ⋯ })
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- The compact sets of a topological space and its compact coherentification agree.  -/
CompactCoherentification.isCompact_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {K : Set (CompactCoherentification X)},
  IsCompact K ↔ IsCompact (⇑(CompactCoherentification.mk X) ⁻¹' K)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.seq_add : ∀ {α β : Type u} (f : FreeAbelianGroup (α → β)) (x y : FreeAbelianGroup α), f <*> x + y = (f <*> x) + (f <*> y)
-- Init.Data.BitVec.Lemmas
BitVec.getElem_and : ∀ {w : ℕ} {x y : BitVec w} {i : ℕ} (h : i < w), (x &&& y)[i] = (x[i] && y[i])
-- Mathlib.Logic.Equiv.Basic
/-- `swap a b` is the permutation that swaps `a` and `b` and
leaves other values as is.  -/
Equiv.swap : {α : Sort u_1} → [DecidableEq α] → α → α → Equiv.Perm α
-- Mathlib.RingTheory.Ideal.Colon
Submodule.colon_union : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  {S₁ S₂ : Set M}, N.colon (S₁ ∪ S₂) = N.colon S₁ ⊓ N.colon S₂
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.ext : ∀ {R : Type u_1} [inst : NonAssocRing R] {p q : MulRingSeminorm R}, (∀ (x : R), p x = q x) → p = q
-- Lean.Parser.Basic
Lean.Parser.TokenMap.instInhabited : {α : Type} → Inhabited (Lean.Parser.TokenMap α)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemTag : Type
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [CategoryTheory.EnoughInjectives C] [CategoryTheory.Mono f] (n₀ n₁ : ℤ),
  (∀ i ≤ n₀, QuasiIsoAt f i) →
    ∀ [CategoryTheory.Mono (HomologicalComplex.homologyMap f n₁)],
      autoParam (n₀ + 1 = n₁) CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂._auto_1✝ →
        ∃ F,
          CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.quasiIsoLE✝ n₁ F ∧
            CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isIsoLE✝ n₁ F
-- Init.Data.String.Basic
String.endExclusive_slice : ∀ {s : String} {startInclusive endExclusive : s.Pos} {h : startInclusive ≤ endExclusive},
  (s.slice startInclusive endExclusive h).endExclusive = endExclusive
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- The tensor product of two objects of `AugmentedSimplexCategory`.  -/
AugmentedSimplexCategory.tensorObj : AugmentedSimplexCategory → AugmentedSimplexCategory → AugmentedSimplexCategory
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.edist_measure_def : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (μ ν : MeasureTheory.LevyProkhorov (MeasureTheory.Measure Ω)),
  edist μ ν = MeasureTheory.levyProkhorovEDist μ.toMeasure ν.toMeasure
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- `ContMDiffAt.comp` for a function of two arguments.  -/
ContMDiffAt.comp₂ : ∀ {𝕜 : 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 : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_12}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {n : WithTop ℕ∞} {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M},
  ContMDiffAt (I'.prod J') J n h (f x, g x) →
    ContMDiffAt I I' n f x → ContMDiffAt I J' n g x → ContMDiffAt I J n (fun x => h (f x, g x)) x
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.smul : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] (r : MvPowerSeries τ S) {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a → MvPowerSeries.HasSubst (r • a)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.leftFunc.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Arrow.leftFunc = CategoryTheory.Comma.fst (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)
-- Mathlib.CategoryTheory.Limits.Sifted
CategoryTheory.IsSifted.nonempty : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsSifted C], Nonempty C