mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.parallelPairOpIso_inv_app_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y),
  (CategoryTheory.Limits.parallelPairOpIso f g).inv.app CategoryTheory.Limits.WalkingParallelPair.one =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.walkingParallelPairOpEquiv.functor.comp (CategoryTheory.Limits.parallelPair f g).op).obj
        CategoryTheory.Limits.WalkingParallelPair.one)
-- Mathlib.FieldTheory.LinearDisjoint
RingEquiv.subsemiringCongr.congr_simp : ∀ {R : Type u} [inst : NonAssocSemiring R] {s t : Subsemiring R} (h : s = t),
  RingEquiv.subsemiringCongr h = RingEquiv.subsemiringCongr h
-- Mathlib.RingTheory.Coprime.Lemmas
/-- **Alias** of the forward direction of `Nat.isCoprime_iff_coprime`. -/
IsCoprime.natCoprime : ∀ {m n : ℕ}, IsCoprime ↑m ↑n → m.Coprime n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (m.insertMany l).getKeyD k' fallback = k
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Imp.refl : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n), T.Imp φ φ
-- Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
_private.Mathlib.Combinatorics.Additive.ErdosGinzburgZiv.0.totalDegree_f₁_add_totalDegree_f₂ : ∀ {ι : Type u_1} {p : ℕ} [inst : Fact (Nat.Prime p)] {s : Finset ι} {a : ι → ZMod p},
  (f₁✝ s a).totalDegree + (f₂✝ s a).totalDegree < 2 * p - 1
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Helper monad for implementing `abstractGroundMismatches?`  -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM : Type → Type
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
/-- The natural transformation `X ⟶ Y.obj t.right` for `t : Under j₀`
that is induced by `y : X ⟶ Y.obj j₀`.  -/
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : Type w} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          {Y : CategoryTheory.Functor J C} →
            {j₀ : J} →
              (X ⟶ Y.obj j₀) →
                ((CategoryTheory.Functor.const (CategoryTheory.Under j₀)).obj X ⟶
                  (CategoryTheory.Under.forget j₀).comp Y)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  (t t_1 : Std.ExtDTreeMap α β cmp), t = t_1 → t.minKey! = t_1.minKey!
-- Mathlib.Algebra.MvPolynomial.Basic
/-- **Alias** of `MvPolynomial.coeff_X`. -/
MvPolynomial.coeff_X' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (i : σ) (m : σ →₀ ℕ),
  MvPolynomial.coeff m (MvPolynomial.X i) = if (fun₀ | i => 1) = m then 1 else 0
-- Lean.Meta.WHNF
/-- Applies `whnfCore` while unfolding type annotations (`outParam`/`optParam`/etc.).  -/
Lean.Meta.whnfCoreUnfoldingAnnotations : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Calculus.TangentCone.Pi
/-- The product of a family of sets of unique differentiability is a set of unique
differentiability.  -/
UniqueDiffOn.pi : ∀ {𝕜 : Type u_1} [inst : DivisionSemiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (E i)]
  [inst_2 : (i : ι) → Module 𝕜 (E i)] [inst_3 : TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot]
  [inst_5 : (i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousAdd (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)]
  {s : (i : ι) → Set (E i)} {I : Set ι}, (∀ i ∈ I, UniqueDiffOn 𝕜 (s i)) → UniqueDiffOn 𝕜 (I.pi s)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instInvOneClassOfMulOpposite : {M : Type u_1} → [InvOneClass Mᵐᵒᵖ] → InvOneClass Mᵈᵐᵃ
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.hermiteTheorem.natDegree_le_rankOfDiscrBdd : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {N : ℕ},
  |NumberField.discr K| ≤ ↑N →
    ∀ (a : NumberField.RingOfIntegers K),
      ℚ⟮↑a⟯ = ⊤ → (minpoly ℤ ↑a).natDegree ≤ NumberField.hermiteTheorem.rankOfDiscrBdd N
-- Lean.CoreM
Lean.Core.instMonadNameGeneratorCoreM : Lean.MonadNameGenerator Lean.CoreM
-- Mathlib.Algebra.Group.End
MulAut.inv_apply_self : ∀ (M : Type u_2) [inst : Mul M] (e : MulAut M) (m : M), e⁻¹ (e m) = m
-- Mathlib.MeasureTheory.Measure.Real
/-- Pigeonhole principle for measure spaces: if `s` is a `Finset` and
`∑ i ∈ s, μ.real (t i) > μ.real univ`, then one of the intersections `t i ∩ t j` is not empty.  -/
MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal : ∀ {α : Type u_1} {ι : Type u_3} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {s : Finset ι} {t : ι → Set α},
  (∀ i ∈ s, MeasurableSet (t i)) →
    μ.real Set.univ < ∑ i ∈ s, μ.real (t i) → ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.foldM_iter : ∀ {α β γ : Type u} {m : Type u → Type w} {Pred EPred : Type u} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_6 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {init : γ} {f : γ → β → m γ}
  (inv : Std.Internal.Do.Invariant it.toList γ Pred) {epost : EPred},
  (∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList = pref ++ cur :: suff) (b : γ),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f b cur ⦃ fun b' =>
        inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'; epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := it.toList, property := ⋯ } init ⦄ Std.Iter.foldM f init it ⦃ fun b =>
      inv { «prefix» := it.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Init.Data.Order.Factories
/-- Returns a `LawfulOrderMin α` instance given that `max a b` returns either `a` or `b` and that
it is less than or equal to both of them. The `≤` relation needs to be transitive.

The produced instance entails `LawfulOrderInf α` and `MinEqOr α`.
 -/
Std.LawfulOrderMin.of_min_le : ∀ {α : Type u} [inst : Min α] [inst_1 : LE α]
  [i : Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2],
  (∀ (a b : α), a ⊓ b ≤ a) →
    (∀ (a b : α), a ⊓ b ≤ b) →
      autoParam (∀ (a b : α), a ⊓ b = a ∨ a ⊓ b = b) Std.LawfulOrderMin.of_min_le._auto_1 → Std.LawfulOrderMin α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_eq_isSome_get? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.contains a t = (t.get? a).isSome
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_le_iff : ∀ {X : Type u_2} {s : Set X} [inst : PseudoEMetricSpace X] {d : ENNReal},
  Metric.ediam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d
-- Mathlib.Data.Sign.Basic
SignType.pow_odd : ∀ (s : SignType) {n : ℕ}, Odd n → s ^ n = s
-- Lean.Level
Lean.mkLevelParam : Lean.Name → Lean.Level
-- Init.Data.List.Erase
List.eraseP_eq_nil_iff : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.eraseP p xs = [] ↔ xs = [] ∨ ∃ x, p x = true ∧ xs = [x]
-- Aesop.Tree.Data
Aesop.MVarCluster.elim : Aesop.MVarCluster → Aesop.MVarClusterData Aesop.Goal Aesop.Rapp
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensRangeParams.mk : Lean.Lsp.TextDocumentIdentifier → Lean.Lsp.Range → Lean.Lsp.SemanticTokensRangeParams
-- Mathlib.Algebra.Group.Defs
Monoid.toNPow : {M : Type u} → [self : Monoid M] → NPow M
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_add_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (a : R), ↑⌊a⌋ + Int.fract a = a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_le_add_of_nonpos_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b c : α}, a ≤ b + c → c ≤ 0 → a ≤ b
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.isGenPattern? : Lean.Expr → Option (Lean.Meta.Grind.GenPatternInfo × Lean.Expr)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.fst_swapRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)), κ.swapRight.fst = κ.snd
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_transpose : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
  A.adjugate.transpose = A.transpose.adjugate
-- Mathlib.Topology.Continuous
continuous_iff_preimage_interior_subset_interior_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f ↔ ∀ (s : Set Y), f ⁻¹' interior s ⊆ interior (f ⁻¹' s)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- The underlying family of 2-morphisms.  -/
CategoryTheory.Lax.OplaxTrans.Modification.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Lax.OplaxTrans.Modification η θ → (a : B) → η.app a ⟶ θ.app a
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- A Besicovitch tau-package is a family of balls in a metric space with positive bounded radii,
together with enough data to proceed with the Besicovitch greedy algorithm. We register this in
a single structure to make sure that all our constructions in this algorithm only depend on
one variable.  -/
Besicovitch.TauPackage : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Lean.Environment
Lean.OLeanLevel.noConfusionType : Sort v✝ → Lean.OLeanLevel → Lean.OLeanLevel → Sort v✝
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biprod.decomp_hom_to : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {Z : C} (f : Z ⟶ X ⊞ Y),
  ∃ f₁ f₂,
    f =
      CategoryTheory.CategoryStruct.comp f₁ CategoryTheory.Limits.biprod.inl +
        CategoryTheory.CategoryStruct.comp f₂ CategoryTheory.Limits.biprod.inr
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
/-- The embedding of the Gaussian integers into the complex numbers, as a ring homomorphism.  -/
GaussianInt.toComplex : GaussianInt →+* ℂ
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
/-- If `X` is a Jacobson scheme and `k` is a field,
`Spec(k) ⟶ X` is finite iff it is (locally) of finite type.
(The statement is more general to allow the empty scheme as well)  -/
AlgebraicGeometry.isFinite_iff_locallyOfFiniteType_of_jacobsonSpace : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [AlgebraicGeometry.IsReduced X] [JacobsonSpace ↥Y],
  AlgebraicGeometry.IsFinite f ↔ AlgebraicGeometry.LocallyOfFiniteType f
-- Aesop.Tree.Data
Aesop.MVarClusterUnsafe.brecOn.go : {motive_1 : Aesop.GoalUnsafe → Sort u} →
  {motive_2 : Aesop.MVarClusterUnsafe → Sort u} →
    {motive_3 : Aesop.RappUnsafe → Sort u} →
      {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u} →
        {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u} →
          {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u} →
            {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} →
              {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u} →
                {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} →
                  {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} →
                    {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} →
                      {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u} →
                        {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} →
                          (t : Aesop.MVarClusterUnsafe) →
                            ((t : Aesop.GoalUnsafe) → t.below → motive_1 t) →
                              ((t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t) →
                                ((t : Aesop.RappUnsafe) → t.below → motive_3 t) →
                                  ((t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) →
                                      Aesop.GoalUnsafe.below_1 t → motive_4 t) →
                                    ((t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) →
                                        Aesop.GoalUnsafe.below_2 t → motive_5 t) →
                                      ((t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) →
                                          Aesop.GoalUnsafe.below_3 t → motive_6 t) →
                                        ((t : Array (IO.Ref Aesop.RappUnsafe)) →
                                            Aesop.GoalUnsafe.below_4 t → motive_7 t) →
                                          ((t : Option (IO.Ref Aesop.RappUnsafe)) →
                                              Aesop.GoalUnsafe.below_5 t → motive_8 t) →
                                            ((t : Array (IO.Ref Aesop.GoalUnsafe)) →
                                                Aesop.GoalUnsafe.below_6 t → motive_9 t) →
                                              ((t : Array (IO.Ref Aesop.MVarClusterUnsafe)) →
                                                  Aesop.GoalUnsafe.below_7 t → motive_10 t) →
                                                ((t : List (IO.Ref Aesop.RappUnsafe)) →
                                                    Aesop.GoalUnsafe.below_8 t → motive_11 t) →
                                                  ((t : List (IO.Ref Aesop.GoalUnsafe)) →
                                                      Aesop.GoalUnsafe.below_9 t → motive_12 t) →
                                                    ((t : List (IO.Ref Aesop.MVarClusterUnsafe)) →
                                                        Aesop.GoalUnsafe.below_10 t → motive_13 t) →
                                                      motive_2 t ×' t.below
-- Init.Data.BitVec.Bitblast
BitVec.msb_intMin_umod_neg_of_msb_true : ∀ {w : ℕ} {y : BitVec w}, y.msb = true → (BitVec.intMin w % -y).msb = false
-- Mathlib.Probability.Distributions.Uniform
/-- The uniform pmf taking the same uniform value on all of the fintype `α`  -/
PMF.uniformOfFintype : (α : Type u_2) → [Fintype α] → [Nonempty α] → PMF α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The set of points in the mixedSpace that are equal to `0` at a fixed (real) place has
volume zero.  -/
NumberField.mixedEmbedding.volume_eq_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w : { w // w.IsReal }),
  MeasureTheory.volume {x | x.1 w = 0} = 0
-- Mathlib.LinearAlgebra.Finsupp.Pi
FunOnFinite.map_id : ∀ (M : Type u_5) [inst : AddCommMonoid M] {X : Type u_6} [inst_1 : Finite X], FunOnFinite.map id = id
-- Batteries.Data.AssocList
Batteries.AssocList.toList_toAssocList : ∀ {α : Type u_1} {β : Type u_2} (l : Batteries.AssocList α β), l.toList.toAssocList = l
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_sub : ∀ {𝕜 : 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'] {s : Set M} {z : M} {f g : M → E'},
  MDiffAt[s] f z → MDiffAt[s] g z → UniqueMDiffAt[s] z → mfderiv[s] (f - g) z = mfderiv[s] f z - mfderiv[s] g z
-- Mathlib.Data.Vector.Basic
List.Vector.get_tail_succ : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n.succ) (i : Fin n), v.tail.get i = v.get i.succ
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_iff_notMem_span : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V}, LinearIndependent K v ↔ ∀ (i : ι), v i ∉ Submodule.span K (v '' (Set.univ \ {i}))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdSndIsoProd_inv_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X]
  [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.prod.snd f) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
-- Plausible.Testable
/-- How many test instances to generate.
 -/
Plausible.Configuration.numInst : Plausible.Configuration → ℕ
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i : ι),
  HomologicalComplex.homotopyCofiber.inrX φ i =
    if hi : c.Rel i (c.next i) then
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
        (HomologicalComplex.homotopyCofiber.XIsoBiprod φ i (c.next i) hi).inv
    else (HomologicalComplex.homotopyCofiber.XIso φ i hi).inv
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β} {h₁ : a ∈ t.insertIfNew k v},
  Std.DTreeMap.Const.get (t.insertIfNew k v) a h₁ =
    if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Const.get t a ⋯
-- Std.Time.DateTime.PlainDateTime
/-- Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.atTime : Std.Time.PlainDate → Std.Time.PlainTime → Std.Time.PlainDateTime
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Pi.ι_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasProduct f] (b c : β) {Z : C}
  (h : f c ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f c) h) =
    CategoryTheory.CategoryStruct.comp (if h : b = c then CategoryTheory.eqToHom ⋯ else 0) h
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.mk_eq_zero : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x : ArchimedeanClass.FiniteElement K}, ArchimedeanClass.FiniteResidueField.mk x = 0 ↔ 0 < ArchimedeanClass.mk ↑x
-- Init.Prelude
/-- Gets the end position information of the trailing whitespace of a `SourceInfo`, if available.
If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
will also return `none`.
 -/
Lean.SourceInfo.getTrailingTailPos? : Lean.SourceInfo → optParam Bool false → Option String.Pos.Raw
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.π_map : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (groupCohomology.π A n) (groupCohomology.map f φ n) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ n) (groupCohomology.π B n)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.instAdditiveιHeart : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (H : Type u') [inst_6 : CategoryTheory.Category.{v', u'} H]
  [inst_7 : CategoryTheory.Preadditive H] [inst_8 : t.Heart H], t.ιHeart.Additive
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
HasFDerivAt.of_comp_of_isEmbedding : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {g' : E →L[𝕜] F}
  {f' : F →L[𝕜] G} {a : E},
  ContinuousAt g a →
    HasFDerivAt f f' (g a) →
      Topology.IsEmbedding ⇑f' → HasFDerivAt h (f' ∘SL g') a → f ∘ g =ᶠ[nhds a] h → HasFDerivAt g g' a
-- Aesop.Tree.Data
Aesop.MVarCluster.setIsIrrelevant : Bool → Aesop.MVarCluster → Aesop.MVarCluster
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.MulOpposite.instMulOpposite : ∀ {E : Type u_4} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E], CStarRing Eᵐᵒᵖ
-- Init.Data.Vector.DecidableEq
Vector.instReflBEq : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [ReflBEq α], ReflBEq (Vector α n)
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.CompletelyDistribLattice.MinimalAxioms.toCompleteDistribLattice.match_1_3.eq_1 : ∀ {α : Type u_1} (s : Set α)
  (motive :
    (i : ULift.{u_1, 0} Bool) →
      (match i with
        | { down := true } => PUnit.{u_1 + 1}
        | { down := false } => ↑s) →
        Sort u_2)
  (j :
    match { down := true } with
    | { down := true } => PUnit.{u_1 + 1}
    | { down := false } => ↑s)
  (h_1 :
    (j :
        match { down := true } with
        | { down := true } => PUnit.{u_1 + 1}
        | { down := false } => ↑s) →
      motive { down := true } j)
  (h_2 :
    (j :
        match { down := false } with
        | { down := true } => PUnit.{u_1 + 1}
        | { down := false } => ↑s) →
      motive { down := false } j),
  (match { down := true }, j with
    | { down := true }, j => h_1 j
    | { down := false }, j => h_2 j) =
    h_1 j
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_zero : ExpGrowth.expGrowthInf 0 = ⊥
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- `∏' i, f i` is the unconditional product of `f`, if it exists, or 1 otherwise.

More generally, if `L` is a `SummationFilter`, `∏'[L] i, f i` is the product of `f` with respect to
`L` if it exists, and `1` otherwise.

(Note that even if the unconditional product exists, it might not be unique if the topology is not
separated. When the multiplicative support of `f` is finite, we make the most reasonable choice,
to use the product over the multiplicative support. Otherwise, we choose arbitrarily an `a`
satisfying `HasProd f a`. Similar remarks apply to more general summation filters.)  -/
«term∏'[_]_,_» : Lean.ParserDescr
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.State.addEntry : Lean.Meta.Match.Extension.State → Lean.Meta.Match.Extension.Entry → Lean.Meta.Match.Extension.State
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
/-- A family of objects `Y : I → C` "covers the final object"
if for all `X : C`, the sieve `ofObjects Y X` is a covering sieve.  -/
CategoryTheory.GrothendieckTopology.CoversTop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C → {I : Type u_1} → (I → C) → Prop
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instNonemptyElemERestrictSubtype : ∀ {α : Type u_1} {M : Matroid α} [M.Nonempty], (M.restrictSubtype M.E).Nonempty
-- Mathlib.Data.Int.Cast.Lemmas
SemiconjBy.intCast_mul_left : ∀ {α : Type u_3} [inst : Ring α] {a x y : α}, SemiconjBy a x y → ∀ (n : ℤ), SemiconjBy (↑n * a) x y