mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Hull
convexHull_pair : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [IsOrderedRing 𝕜] (x y : E), (convexHull 𝕜) {x, y} = segment 𝕜 x y
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.leftComm_def : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P],
  TensorProduct.leftComm R M N P =
    (TensorProduct.assoc R M N P).symm ≪≫ₗ TensorProduct.congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
      TensorProduct.assoc R N M P
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.suppBddBelow_supp_PWO : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [LocallyFiniteOrder Γ] (f : Γ → R),
  BddBelow (Function.support f) → (Function.support f).IsPWO
-- Init.Data.String.Bootstrap
/-- Adds a character to the end of a string.

The internal implementation uses dynamic arrays and will perform destructive updates
if the string is not shared.

Examples:
* `"abc".push 'd' = "abcd"`
* `"".push 'a' = "a"`
 -/
String.push : String → Char → String
-- Mathlib.Data.Set.Insert
Set.forall_of_forall_insert : ∀ {α : Type u_1} {P : α → Prop} {a : α} {s : Set α}, (∀ x ∈ insert a s, P x) → ∀ x ∈ s, P x
-- Mathlib.Analysis.Normed.Group.Quotient
/-- An isometric version of `AddSubgroup.quotientEquivOfEq`.  -/
AddSubgroup.quotientIsometryEquivOfEq : {M : Type u_1} → [inst : SeminormedAddCommGroup M] → {S T : AddSubgroup M} → S = T → M ⧸ S ≃ᵢ M ⧸ T
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_coeAddMonoidHom : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddZeroClass α], ⇑Finset.coeAddMonoidHom = SetLike.coe
-- Mathlib.Data.Set.Prod
Set.mk_preimage_prod_right_fn_eq_if : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {s : Set α} {t : Set β} {a : α} [inst : DecidablePred fun x => x ∈ s]
  (g : δ → β), (fun b => (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.unbotD_natCast : ∀ {α : Type u} [inst : NatCast α] (d : α) (n : ℕ), WithBot.unbotD d ↑n = ↑n
-- Mathlib.Algebra.Vertex.VertexOperator
VertexOperator.ext : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A B : VertexOperator R V), (∀ (v : V), A v = B v) → A = B
-- Mathlib.Dynamics.OmegaLimit
/-- A set is eventually carried into any open neighbourhood of its ω-limit:
if `c` is a compact set such that `closure {ϕ t x | t ∈ v, x ∈ s} ⊆ c` for some `v ∈ f`
and `n` is an open neighbourhood of `ω f ϕ s`, then for some `u ∈ f` we have
`closure {ϕ t x | t ∈ u, x ∈ s} ⊆ n`.  -/
eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  [T2Space β] {c : Set β},
  IsCompact c →
    (∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s c) →
      ∀ {n : Set β}, IsOpen n → omegaLimit f ϕ s ⊆ n → ∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ n
-- Lean.Elab.PreDefinition.PartialFixpoint.Main
/-- For pretty error messages:
Takes `F : (fun f => e)`, where `f` is the packed function, and replaces `f` in `e` with the user-visible
constants, which are added to the environment temporarily.
 -/
_private.Lean.Elab.PreDefinition.PartialFixpoint.Main.0.Lean.Elab.unReplaceRecApps : {α : Type} →
  Array Lean.Elab.PreDefinition →
    Lean.Elab.FixedParamPerms → Array Lean.Expr → Lean.Expr → (Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Data.Part
Part.some_union_some : ∀ {α : Type u_1} [inst : Union α] (a b : α), Part.some a ∪ Part.some b = Part.some (a ∪ b)
-- Lean.Elab.DefView
/-- Header elaboration data of a `DefView`.  -/
Lean.Elab.DefViewElabHeaderData : Type
-- Init.Data.String.Basic
String.Slice.extract_eq_copy_slice : ∀ {s : String.Slice} (p₀ p₁ : s.Pos) (h : p₀ ≤ p₁), s.extract p₀ p₁ = (s.slice p₀ p₁ h).copy
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaGrp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.shrinkYonedaGrp.{w, v, u} =
    { obj := fun X => GrpCat.shrinkFunctor.{w, v, v, u} (CategoryTheory.yonedaGrp.obj X),
      map := fun {X Y} f => GrpCat.shrinkFunctorMap (CategoryTheory.yonedaGrp.map f), map_id := ⋯, map_comp := ⋯ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.of_toList_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.toList.Perm t₂.toList → t₁.Equiv t₂
-- Lean.Server.References
/-- A match in `References.definitionsMatching`.  -/
Lean.Server.References.MatchedDefinition : Type → Type
-- Mathlib.Data.Nat.Factorization.Defs
/-- For any `p`, the power of `p` in `n^k` is `k` times the power in `n`  -/
Nat.factorization_pow : ∀ (n k : ℕ), (n ^ k).factorization = k • n.factorization
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.covarianceBilinDual_self_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : BorelSpace E] (L : StrongDual ℝ E),
  0 ≤ ((ProbabilityTheory.covarianceBilinDual μ) L) L
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.one_ne_of : ∀ {α : Type u_1} (a : α), 1 ≠ FreeGroup.of a
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGE?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.getKeyGE? k = Std.DTreeMap.Internal.Impl.getKeyGE?.go k none
-- Mathlib.CategoryTheory.Linear.LinearFunctor
/-- `F.mapLinearMap` is an `R`-linear map whose underlying function is `F.map`.  -/
CategoryTheory.Functor.mapLinearMap : (R : Type u_1) →
  [inst : Semiring R] →
    {C : Type u_2} →
      {D : Type u_3} →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
          [inst_2 : CategoryTheory.Category.{v_2, u_3} D] →
            [inst_3 : CategoryTheory.Preadditive C] →
              [inst_4 : CategoryTheory.Preadditive D] →
                [inst_5 : CategoryTheory.Linear R C] →
                  [inst_6 : CategoryTheory.Linear R D] →
                    (F : CategoryTheory.Functor C D) →
                      [CategoryTheory.Functor.Linear R F] → [F.Additive] → {X Y : C} → (X ⟶ Y) →ₗ[R] F.obj X ⟶ F.obj Y
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The additive Haar measure is an additive Haar measure, i.e., it is invariant and gives finite
mass to compact sets and positive mass to nonempty open sets.  -/
MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G),
  (MeasureTheory.Measure.addHaarMeasure K₀).IsAddHaarMeasure
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.authorityForm.inj : ∀ {authority authority_1 : Std.Http.URI.Authority},
  Std.Http.RequestTarget.authorityForm authority = Std.Http.RequestTarget.authorityForm authority_1 →
    authority = authority_1
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.completeSpace : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
  Topology.IsCoherentWith {s | Bornology.IsVonNBounded 𝕜 s} → CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
-- Mathlib.Tactic.Tauto
/-- Tries to apply de-Morgan-like rules on a hypothesis.  -/
Mathlib.Tactic.Tauto.distribNotOnceAt : Lean.Expr → Lean.MVarId → Lean.MetaM Lean.Meta.AssertAfterResult
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_snd : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens),
  CategoryTheory.CategoryStruct.comp (I.glueDataT U V)
      (CategoryTheory.Limits.pullback.snd (I.glueDataObjι V) (X.homOfLE ⋯)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯))
      (X.homOfLE ⋯)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.Pseudofunctor B C} (x x_1 : F ⟶ G) (Γ : x ⟶ x_1) (η : G ⟶ H) (a : B),
  (CategoryTheory.Bicategory.whiskerRight Γ η).as.app a = CategoryTheory.Bicategory.whiskerRight (Γ.as.app a) (η.app a)
-- Mathlib.RingTheory.Perfection
Perfection.coeff_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p],
  Function.Surjective ⇑(frobenius R p) → ∀ (n : ℕ), Function.Surjective ⇑(Perfection.coeff R p n)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- **Alias** of `SimpleGraph.IsBridge.sup_edge_of_not_reachable_of_isBridge`.

---

Connecting two unreachable vertices by an edge preserves existing bridges,
provided the bridge is already an edge.  -/
SimpleGraph.IsBridge.sup_fromEdgeSet_of_not_reachable_of_isBridge : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {e : Sym2 V},
  ¬G.Reachable u v → G.IsBridge e → e ∈ G.edgeSet → (G ⊔ SimpleGraph.edge u v).IsBridge e
-- Mathlib.RingTheory.DedekindDomain.Dvr
Localization.AtPrime.isDedekindDomain : ∀ (A : Type u_1) [inst : CommRing A] [IsDomain A] [IsDedekindDomain A] (P : Ideal A) [inst_3 : P.IsPrime],
  IsDedekindDomain (Localization.AtPrime P)
-- ProofWidgets.Data.Html
ProofWidgets.Html.element.sizeOf_spec : ∀ (a : String) (a_1 : Array (String × Lean.Json)) (a_2 : Array ProofWidgets.Html),
  sizeOf (ProofWidgets.Html.element a a_1 a_2) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Aesop.Rule
Aesop.UnfoldRule : Type
-- Mathlib.Data.ZMod.QuotientGroup
Subgroup.quotientEquivSigmaZMod_symm_apply : ∀ {G : Type u_3} [inst : Group G] (H : Subgroup G) (g : G)
  (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H))
  (k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))),
  (H.quotientEquivSigmaZMod g).symm ⟨q, k⟩ = g ^ k.cast • Quotient.out q
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuousWithinAt.congr_of_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f g : α → β} {s : Set α} {a : α},
  UpperSemicontinuousWithinAt f s a →
    a ∈ s → (∀ᶠ (x : α) in nhdsWithin a s, f x = g x) → UpperSemicontinuousWithinAt g s a
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.preservesKernels_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasKernels C] [P.IsClosedUnderKernels]
  ⦃X Y : P.FullSubcategory⦄ (f : X ⟶ Y),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) P.ι
-- Mathlib.Algebra.Group.UniqueProds.Basic
Multiplicative.instTwoUniqueProdsOfTwoUniqueSums : ∀ {M : Type u_1} [inst : Add M] [TwoUniqueSums M], TwoUniqueProds (Multiplicative M)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.state : {α : Type} → Std.CloseableChannel.Bounded✝ α → Std.Mutex (Std.CloseableChannel.Bounded.State✝ α)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.mem_toList_insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k : α} {v : β} {y : α × β} [Std.TransCmp cmp]
  {t : RBTree.RBMap α β cmp}, y ∈ (t.insert k v).toList ↔ y ∈ t.toList ∧ t.findEntry? k ≠ some y ∨ y = (k, v)
-- Mathlib.Data.EReal.Basic
EReal.le_coe_toReal : ∀ {x : EReal}, x ≠ ⊤ → x ≤ ↑x.toReal
-- Mathlib.GroupTheory.OrderOfElement
not_isAddTorsionFree_iff_isOfFinAddOrder : ∀ {G : Type u_1} [inst : AddCommGroup G], ¬IsAddTorsionFree G ↔ ∃ a, a ≠ 0 ∧ IsOfFinAddOrder a
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- `MeromorphicNFAt` is invariant under translation.  -/
meromorphicNFAt_comp_sub_const_iff_meromorphicNFAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E}, MeromorphicNFAt (f ∘ fun x => x - c) x ↔ MeromorphicNFAt f (x - c)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_preBeth : ∀ (o : Ordinal.{u_1}), Cardinal.lift.{v, u_1} (Cardinal.preBeth o) = Cardinal.preBeth (Ordinal.lift.{v, u_1} o)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
/-- Bundle an additive subgroup with typeclass assumptions of normality and finite index.  -/
FiniteIndexNormalAddSubgroup.ofAddSubgroup : {G : Type u_1} →
  [inst : AddGroup G] → (H : AddSubgroup G) → [H.Normal] → [H.FiniteIndex] → FiniteIndexNormalAddSubgroup G
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.map_C_comap_of_comap_eq_leadingCoeff : ∀ {R : Type u} [inst : CommRing R] (I : Ideal (Polynomial R)),
  Ideal.comap Polynomial.C I = I.leadingCoeff → Ideal.map Polynomial.C (Ideal.comap Polynomial.C I) = I
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- Use the coherence theorem for monoidal categories to solve equations in a monoidal equation,
where the two sides only differ by replacing strings of monoidal structural morphisms
(that is, associators, unitors, and identities)
with different strings of structural morphisms with the same source and target.

That is, `coherence` can handle goals of the form
`a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'`
where `a = a'`, `b = b'`, and `c = c'` can be proved using `pure_coherence`.

(If you have very large equations on which `coherence` is unexpectedly failing,
you may need to increase the typeclass search depth,
using e.g. `set_option synthInstance.maxSize 500`.)
 -/
Mathlib.Tactic.Coherence.coherence : Lean.ParserDescr
-- Mathlib.RingTheory.Localization.Away.AdjoinRoot
instFiniteTypeAway : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S] (f : S), Algebra.FiniteType R (Localization.Away f)
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine : ∀ {X : AlgebraicGeometry.Scheme} [h : AlgebraicGeometry.IsLocallyArtinian X] [AlgebraicGeometry.IsAffine X],
  IsArtinianRing ↑(X.presheaf.obj (Opposite.op ⊤))
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.instIsStrictlyGECochainComplexOfNatInt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.InjectiveResolution X),
  R.cochainComplex.IsStrictlyGE 0
-- Init.Data.Sum.Lemmas
Sum.LiftRel.mono : ∀ {α : Type u_1} {α_1 : Type u_2} {r₁ r₂ : α → α_1 → Prop} {β : Type u_3} {β_1 : Type u_4} {s₁ s₂ : β → β_1 → Prop}
  {x : α ⊕ β} {y : α_1 ⊕ β_1},
  (∀ (a : α) (b : α_1), r₁ a b → r₂ a b) →
    (∀ (a : β) (b : β_1), s₁ a b → s₂ a b) → Sum.LiftRel r₁ s₁ x y → Sum.LiftRel r₂ s₂ x y
-- Init.Data.Bool
Bool.xor_not : ∀ (x y : Bool), (x ^^ !y) = !(x ^^ y)
-- Mathlib.Data.ENNReal.Real
/-- **Alias** of the reverse direction of `ENNReal.ofReal_eq_zero`. -/
ENNReal.ofReal_of_nonpos : ∀ {p : ℝ}, p ≤ 0 → ENNReal.ofReal p = 0
-- Mathlib.AlgebraicGeometry.Modules.Tilde
TopCat.Sheaf.restrictHomEquivHom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} {ι : Type u_1} {B : ι → TopologicalSpace.Opens ↑X}
  (F : TopCat.Presheaf C X) (F' : TopCat.Sheaf C X) (h : TopologicalSpace.Opens.IsBasis (Set.range B)),
  TopCat.Sheaf.restrictHomEquivHom F F' h = TopCat.Sheaf.restrictHomEquivHom F F' h
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- Bundled global covariant derivative on a vector bundle.
Caution, the argument order is nonstandard: `cov σ x (X x)` corresponds to `∇_X σ x` on paper.
 -/
CovariantDerivative : {𝕜 : 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] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      (F : Type u_5) →
                        [inst_6 : NormedAddCommGroup F] →
                          [NormedSpace 𝕜 F] →
                            (V : M → Type u_6) →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [FiberBundle F V] → Type (max (max u_2 u_4) u_6)
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.isZero_stupidTrunc_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c')
  [inst_3 : e.IsRelIff], CategoryTheory.Limits.IsZero (K.stupidTrunc e) ↔ K.IsStrictlySupportedOutside e
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.GuitartExact.mk : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {w : CategoryTheory.TwoSquare T L R B},
  (∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), CategoryTheory.IsConnected (w.StructuredArrowRightwards g)) →
    w.GuitartExact
-- Mathlib.LinearAlgebra.TensorProduct.Matrix
/-- `TensorProduct.comm` corresponds to a permutation of the identity matrix.  -/
TensorProduct.toMatrix_comm : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_7} {κ : Type u_8} [inst : DecidableEq ι]
  [inst_1 : DecidableEq κ] [inst_2 : Fintype ι] [inst_3 : Fintype κ] [inst_4 : CommRing R] [inst_5 : AddCommGroup M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R M] [inst_8 : Module R N] (bM : Module.Basis ι R M)
  (bN : Module.Basis κ R N),
  (LinearMap.toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM)) ↑(TensorProduct.comm R M N) =
    Matrix.submatrix 1 Prod.swap id
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.maxKey?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxKey? = t₂.maxKey?
-- Lean.Widget.Diff
/-- Diffs the given hypothesis bundle against the given local context.

If `useAfter == true`, `ctx₀` is the context _before_ and `h₁` is the bundle _after_.
If `useAfter == false`, these are swapped.
  -/
_private.Lean.Widget.Diff.0.Lean.Widget.diffHypothesesBundle : Bool → Lean.LocalContext → Lean.Widget.InteractiveHypothesisBundle → Lean.MetaM Lean.Widget.InteractiveHypothesisBundle
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIioIci_symm_apply_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α} (h : y < x), (OrderIso.sumLexIioIci x).symm y = toLex (Sum.inl ⟨y, h⟩)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.vadd_apply : ∀ {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 : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] P2) (p : P1),
  (f +ᵥ g) p = f p +ᵥ g p
-- Lean.Meta.MkIffOfInductiveProp
/-- Calls `cases` on `h` (assumed to be a binary sum) `n` times, and returns
the resulting subgoals and their corresponding new hypotheses.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.nCasesSum : ℕ → Lean.MVarId → Lean.FVarId → Lean.MetaM (List (Lean.FVarId × Lean.MVarId))
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Triangle.touchpoint_singleton_sbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → Sbtw ℝ (Affine.Simplex.touchpoint t {i₁} i₂) (t.points i₃) (t.points i₁)
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_le_norm_mul : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖a‖ - ‖b‖ ≤ ‖a * b‖
-- Lean.Syntax
Lean.Syntax.getCanonicalAntiquot : Lean.Syntax → Lean.Syntax
-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- The antipode is an endomorphism of the underlying object of the Hopf monoid.  -/
CategoryTheory.HopfObj.antipode : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} → {X : C} → [self : CategoryTheory.HopfObj X] → X ⟶ X
-- Mathlib.Tactic.GCongr.Core
/-- Given an application `f a₁ .. aₙ`, return the name of `f`, and the array of arguments `aᵢ`.  -/
Mathlib.Tactic.GCongr.getCongrAppFnArgs : Lean.Expr → Option (Lean.Name × Array Lean.Expr)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.MonoidalClosed.linearHomEquiv_hom : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B C : Rep.{u, u, v} k G)
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C),
  (Rep.Hom.hom ((Rep.MonoidalClosed.linearHomEquiv A B C) f)).toLinearMap =
    (TensorProduct.curry (Rep.Hom.hom f).toLinearMap).flip
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.p_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), CategoryTheory.CategoryStruct.comp h.p h.g' = S.g
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.span_root_image_eq_top_of_forall_orthogonal : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [NeZero 2]
  [P.IsIrreducible] (s : Set ι),
  s.Nonempty →
    (∀ (j : ι), P.root j ∉ Submodule.span R (⇑P.root '' s) → ∀ i ∈ s, P.IsOrthogonal j i) →
      Submodule.span R (⇑P.root '' s) = ⊤
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.isLittleO_log_id_atTop : Real.log =o[Filter.atTop] id
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexFuel.eq_def : ∀ (fuel : ℕ) (m₁ m₂ : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.revlexFuel fuel m₁ m₂ =
    match fuel with
    | 0 => m₁.revlexWF m₂
    | fuel.succ =>
      match m₁, m₂ with
      | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => Ordering.eq
      | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => Ordering.gt
      | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => Ordering.lt
      | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ =>
        bif pw₁.x == pw₂.x then
          (Lean.Grind.CommRing.Mon.revlexFuel fuel m₁ m₂).then (Lean.Grind.CommRing.powerRevlex pw₁.k pw₂.k)
        else
          bif Nat.blt pw₁.x pw₂.x then
            (Lean.Grind.CommRing.Mon.revlexFuel fuel m₁ (Lean.Grind.CommRing.Mon.mult pw₂ m₂)).then Ordering.lt
          else (Lean.Grind.CommRing.Mon.revlexFuel fuel (Lean.Grind.CommRing.Mon.mult pw₁ m₁) m₂).then Ordering.gt
-- Mathlib.Data.Finset.Defs
Finset.coe_mem : ∀ {α : Type u_1} {s : Finset α} (x : ↑↑s), ↑x ∈ s